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-rank-five-singleton-prefix-bound/LOCAL-PINS.json b/research/p104-rank-five-singleton-prefix-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..d55a4fb0c7 --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/LOCAL-PINS.json @@ -0,0 +1,27 @@ +{ + "PROVENANCE.json": "926a007b0485473089e40a0106fce660a488ed5d415da14c56e1817825aae4af", + "SOURCES.json": "5ae4cfc96aa890b1b06aa0de688e03d9713b2772fb0f9c6ae7e23ad7d49c479d", + "TASK.json": "3c57e217fd36174b238477a23ad0afc36d06e0bbab297b90ee2bd865674b64af", + "VERIFY.json": "bcc88b80a165647babb10052aa5828f4fbd97f2cb56b113a0928808141d8711b", + "independent/compare.py": "5a8d60e34383ca824f8c3c46adf2a0f246c2a10541488af834fea5da7777b7fc", + "independent/pure_support.py": "38c796cbe1a73f386177faf88cd53294d4b911f6cde7fd47cd9fcef3b558373f", + "independent/second_prime.py": "21dbd96192e1f60c00ceddba01a7e8d0ddd7d6ad7da4ad3ed22ef2e47cc589c4", + "independent/singleton.py": "1f6bdf85756623d7909422318d0c09519e551a2ee400b91864d1285d5c663cd9", + "inputs/7334-READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/OLD-WITNESS.json": "5be60a09485041744919696121ae27e57a1aa9de437a2c4494d5fc569af4cdb4", + "inputs/PR7370-SHA256.json": "ea5a3157a967c01b94fd57ca26f8ace1bfa2c6e8165271af917846eb14f9c0d9", + "inputs/PR7375-PRIMARY.json": "d00281b59d994fb96e3f60cedc5c6b3b6277a7d050e8ac7bd6b4a24724219669", + "inputs/PR7375-SECOND.json": "96bdb7a70d247a198a6777fe10e30ce51f7b2e90d4a81f9bf7fea0515f9c1ad0", + "inputs/PR7375-SELECTION.json": "910c8881f31721793cb8e8cbf3b3b3789a9986415e0d48dd9c97d146d5b37bcc", + "inputs/PR7375-SHA256.json": "fd334987adac93393bab7578815ec8f9a9cb16ce8dce9b6620613efddde3203d", + "inputs/R115-GEOMETRY.json": "c2a4406cf7130a819189e8ceefb4bb6e09edd392eb56820f9fcadb0e9415ef4e", + "inputs/R115-PRICE.json": "c04adfb199f6dbc25806d6062562c7d707b8fda8ad73f3ed818901248d25ffbf", + "inputs/bank_trace.py": "681fda5cc1d4b1ac07c62601ceb052f167a51fb73d28b23f454f8f50f6a8e27b", + "inputs/paired_rank.py": "d1b7c34e6f8c8a7b810414762015e6e300a8292422af66ff671ae09741141f09", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "lead/pairs.py": "9c843314d2b78736372bea7aa3b5fd506eda99c01850c779120c116c38e1547a", + "preflight/freeze.py": "9491a7212040c0137e85261895b3489a4267af5eeffa8d77ed1eb3991bc78642", + "receipts/SHA256.json": "32d37f0c89894eaac66258499817829c1a3a5b2ff802cac3a890f28018e1ad2d", + "replay.py": "527761e7b77095e7f44ea54eee94ea0434aac95c26e3ace53c63d1dec4f83a00" +} diff --git a/research/p104-rank-five-singleton-prefix-bound/NOTICE b/research/p104-rank-five-singleton-prefix-bound/NOTICE new file mode 100644 index 0000000000..63cf1af20e --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/NOTICE @@ -0,0 +1,3 @@ +Apache-2.0. + +#7334 and #7113 supply the exact current native word and signed caller. #7370 supplies the current rank-five catalogue, and #7375 the explicit residual keys and independent finite-field methods. #7373 supplies the related prefix precedent, #7303 the older singleton premise, #7382 and #7359 the exact trace and paired-support methods, and #7298 the directed tariff. The historical chart-118 witness described in Discussion #7111 supplies a positive algebraic control. OpenAI Codex and subagents materially assisted. diff --git a/research/p104-rank-five-singleton-prefix-bound/PROOF.md b/research/p104-rank-five-singleton-prefix-bound/PROOF.md new file mode 100644 index 0000000000..c1e774f270 --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/PROOF.md @@ -0,0 +1,11 @@ +# Exterior prefix exclusion on the 14 frozen rank-five banks + +The exact #7370 rank-five catalogue enumerates 68 occupied representatives in five endpoint cohorts. #7370, #7373 and #7375 treat 19, 18 and 17 of them respectively. This package tests the 14 previously unselected keys in the exact #7375 receipt. It authenticates the earlier manifest and the two regenerated #7370 price and geometry receipts, then authenticates the #7375 selection and both prefix receipts. The claims here concern the 14 fresh keys. + +For each frozen pre-event cut, let R be the normalized arbitrary-input row map from the beginning of the exact #7334 word to the public bank. The only productive helper with the required two boundary charts is the listed pivot p. A candidate pure prefix requires a nonzero rational linear combination of rows of R supported on input axis p. Project every bank row to the complementary coordinates. If the resulting matrix has full row rank, no such coefficient combination exists, even granting arbitrary rational coefficients. This necessity precedes all suffix, COPY guard, restoration and physical coefficient obligations. + +The primary engine independently reconstructs a backward rational trace for every bank and applies exact exterior elimination. The forward engine scans all 76,466 original events at prime 65537, verifies the live chart bank and ownership and checks its selected exterior minor again on the original projected rows. Every scalar denominator along the full trace is a unit at 65537. Exact reduction therefore sends each rational minor determinant to its computed field residue. A nonzero residue proves a nonzero rational minor on the same axes. All 14 agree with the primary full ranks, including ordered chart gaps 2+3 at 859 and 875, and 3+2 at 987 and 1001. The exact chart stock and literal owner emptiness also agree. There is no cap hit and no unresolved frozen key. + +For a possible future prefix survivor on a singleton cohort, write the pure endpoint images in the two bases as c and d, with endpoint pairing E = c d^T and local pairing L. If either image is zero, no unit pair exists. Otherwise the rational unit equations fail exactly when L is an unequal scalar multiple of E. To see this, let D=L−E. If some row combination x^T D lies outside span(d), choose one with x·c≠0 and choose y with x^T D y=0 and d·y≠0. Scaling then gives both pairings one. If D has row space contained in span(d), write D=a d^T. Then an x orthogonal to a with x·c≠0 exists unless a is a nonzero multiple of c. This gives the criterion. The exact historical chart-118 unit pair, a planted exterior kernel, an unequal proportional pair and a nonproportional pair exercise the gate. This latter gate was unnecessary on the 14 literal inputs. + +The price freezes one unchanged 110,519-paid complete signed invoice and 17 copies of the productive rank change. The 14 cuts can spend at most two distinct pivots. The compatible upper grants all interactions and ancillary work free, so it cannot be quoted as a realized saving. The measured feasible stock is empty. diff --git a/research/p104-rank-five-singleton-prefix-bound/PROVENANCE.json b/research/p104-rank-five-singleton-prefix-bound/PROVENANCE.json new file mode 100644 index 0000000000..959a9075e8 --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/PROVENANCE.json @@ -0,0 +1,98 @@ +{ + "files": { + "independent/pure_support.py": { + "commit": "b1faee3840a2d0186375b412d1813bf757903a99", + "git_blob": "46180f7b496c002f1ee216e03fcdc85cf57a14aa", + "path": "research/p104-rank-four-five-bank-bound/inputs/paired_support.py", + "sha256": "38c796cbe1a73f386177faf88cd53294d4b911f6cde7fd47cd9fcef3b558373f", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/b1faee3840a2d0186375b412d1813bf757903a99/research/p104-rank-four-five-bank-bound/inputs/paired_support.py" + }, + "independent/second_prime.py": { + "commit": "2bf6a806bac491c69182ce366230c1fa7a646fec", + "git_blob": "0be5407fe6beec909aa4862c653a64973bb7b93b", + "path": "research/p104-rank-five-chart233-prefix-bound/inputs/second_prime.py", + "sha256": "21dbd96192e1f60c00ceddba01a7e8d0ddd7d6ad7da4ad3ed22ef2e47cc589c4", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/2bf6a806bac491c69182ce366230c1fa7a646fec/research/p104-rank-five-chart233-prefix-bound/inputs/second_prime.py" + }, + "inputs/7334-READBACK.json": { + "commit": "2bf6a806bac491c69182ce366230c1fa7a646fec", + "git_blob": "625b508eead24b4428253bd257620b7e775800c1", + "path": "research/p104-rank-five-chart233-prefix-bound/inputs/READBACK.json", + "sha256": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/2bf6a806bac491c69182ce366230c1fa7a646fec/research/p104-rank-five-chart233-prefix-bound/inputs/READBACK.json" + }, + "inputs/7334-WORD.json.gz": { + "commit": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "git_blob": "73f43007192eb5a38eb5abb591b871df3e52c7cd", + "path": "research/p104-helper-319-fused-return/WORD.json.gz", + "sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "source": "https://github.com/Clear1nsight/integer-mult-bounds/blob/aaeec8c0acf01e99a5f331ef363a698d9c084ace/research/p104-helper-319-fused-return/WORD.json.gz", + "uncompress": false + }, + "inputs/PR7370-SHA256.json": { + "commit": "a41edc3ae92332a7a1f1ba90e9ea4901d0530185", + "git_blob": "695c7c46ca319b0a6b7ca6154a32021121b22e6a", + "path": "research/p104-rank-five-catalogue-bound/receipts/SHA256.json", + "sha256": "ea5a3157a967c01b94fd57ca26f8ace1bfa2c6e8165271af917846eb14f9c0d9", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/a41edc3ae92332a7a1f1ba90e9ea4901d0530185/research/p104-rank-five-catalogue-bound/receipts/SHA256.json" + }, + "inputs/PR7375-SHA256.json": { + "commit": "2bf6a806bac491c69182ce366230c1fa7a646fec", + "git_blob": "f6da5eb79206fe1e9f67ef97664189df6158e038", + "path": "research/p104-rank-five-chart233-prefix-bound/receipts/SHA256.json", + "sha256": "fd334987adac93393bab7578815ec8f9a9cb16ce8dce9b6620613efddde3203d", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/2bf6a806bac491c69182ce366230c1fa7a646fec/research/p104-rank-five-chart233-prefix-bound/receipts/SHA256.json" + }, + "inputs/bank_trace.py": { + "commit": "408d4268cabb1c15c2b24a262261b1a04ec57a9d", + "git_blob": "996cba9a52498ded0ed72f900c94cc4329fd5fcf", + "path": "research/p104-chart118-pivot635-pairing-bound/engines/r129/chart118.py", + "sha256": "681fda5cc1d4b1ac07c62601ceb052f167a51fb73d28b23f454f8f50f6a8e27b", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/408d4268cabb1c15c2b24a262261b1a04ec57a9d/research/p104-chart118-pivot635-pairing-bound/engines/r129/chart118.py" + }, + "inputs/paired_rank.py": { + "commit": "b1faee3840a2d0186375b412d1813bf757903a99", + "git_blob": "b712cdb1f8a824086e90a81cf22747aa4b63f918", + "path": "research/p104-rank-four-five-bank-bound/inputs/paired_rank.py", + "sha256": "d1b7c34e6f8c8a7b810414762015e6e300a8292422af66ff671ae09741141f09", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/b1faee3840a2d0186375b412d1813bf757903a99/research/p104-rank-four-five-bank-bound/inputs/paired_rank.py" + }, + "inputs/pricing.py": { + "commit": "c522451caf287bb3c16eaece72be4c263315dca4", + "git_blob": "40ec194017bda1d524bba4f07b188c53281419d0", + "path": "research/adjacent-owned-add-exchange-bound/pricing.py", + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/c522451caf287bb3c16eaece72be4c263315dca4/research/adjacent-owned-add-exchange-bound/pricing.py", + "uncompress": false + } + }, + "historical_control": { + "path": "inputs/OLD-WITNESS.json", + "scope": "Historical chart118 pivot635 unit pairing. Full historical candidate is local-only.", + "sha256": "5be60a09485041744919696121ae27e57a1aa9de437a2c4494d5fc569af4cdb4", + "source": "https://github.com/CrocSwap/integer-mult-bounds/discussions/7111" + }, + "regenerated_predecessor_receipts": { + "inputs/PR7375-PRIMARY.json": { + "manifest": "inputs/PR7375-SHA256.json", + "receipt": "PRIMARY.json" + }, + "inputs/PR7375-SECOND.json": { + "manifest": "inputs/PR7375-SHA256.json", + "receipt": "SECOND.json" + }, + "inputs/PR7375-SELECTION.json": { + "manifest": "inputs/PR7375-SHA256.json", + "receipt": "SELECTION.json" + }, + "inputs/R115-GEOMETRY.json": { + "manifest": "inputs/PR7370-SHA256.json", + "receipt": "R115-GEOMETRY.json" + }, + "inputs/R115-PRICE.json": { + "manifest": "inputs/PR7370-SHA256.json", + "receipt": "R115-PRICE.json" + } + }, + "schema_version": 1 +} diff --git a/research/p104-rank-five-singleton-prefix-bound/README.md b/research/p104-rank-five-singleton-prefix-bound/README.md new file mode 100644 index 0000000000..39da6ddfba --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/README.md @@ -0,0 +1,25 @@ +# Fixed-paid rank-five singleton prefix banks + +**NO VERIFIED GAIN.** Exact Δκ = 0 on the independently reproduced conditional κ = 0.00364665195644 from #7334 at `aaeec8c0acf01e99a5f331ef363a698d9c084ace` with signed #7113 at `07a76c5e2738882c0cb322278e56f6cae3c9885d`. + +The two singleton endpoint cohorts 712→127 and 714→127 contain roles 1360 and 1361 respectively. This package closes all 14 owner-empty public bank keys left outside the #7375 support scope, seven per cohort. Exact rational per-bank tracing and an independent whole-word forward traversal agree that every projected exterior prefix matrix has full row rank. No pure prefix direction survives. No suffix test or construction is needed within this scope. [Proof](PROOF.md) + +One productive rank-five split holds all 110,519 paid positions fixed and changes T2 +17, T3 +17 and T5 −17 across the signed 17 copies. The 22,461 productive positions become 22,478. One-edit directed gross upper is 0.207666506667591 raw at the incumbent crossing. The two-pivot compatible relaxation is 0.415333013335181 before ancillary costs, and the fixed-target complete upper stays below −139.3106949909535. The verified saving is zero. + +## Replay + +Use CPython 3.12 with assertions enabled. From a clean checkout: + +```sh +python3.12 -I -B research/p104-rank-five-singleton-prefix-bound/replay.py +``` + +The Git-free replay authenticates the #7370 and #7375 receipts, regenerates the complete directed price and both exact support decisions, and rejects three altered dependencies. Add `--out fresh-directory` to retain four regenerated receipts. [Verification details](VERIFICATION.md) + +## Credit + +#7334 and #7113 supply the current witness and signed caller. #7370 supplies the exact chart catalogue, #7373 and #7375 supply adjacent cohort exclusions, and #7303 supplies the earlier literal singleton scope. #7382 supplies the exact rational trace, #7359 the paired-basis method, and #7298 the directed tariff. The historical chart-118 witness in #7111 supplies the known-good pairing control. OpenAI Codex and subagents materially assisted. + +## Open next questions + +Can a different paid route or new literal cut supply a pure prefix direction? Start by pinning one changed route and pricing the complete signed invoice. All 14 original fixed-paid banks fail before suffix support, so that search must change the available inputs or cut geometry. diff --git a/research/p104-rank-five-singleton-prefix-bound/SOURCES.json b/research/p104-rank-five-singleton-prefix-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-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-rank-five-singleton-prefix-bound/TASK.json b/research/p104-rank-five-singleton-prefix-bound/TASK.json new file mode 100644 index 0000000000..fe12b6cf68 --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Exact #7334 fixed-paid rank-five productive split on the two singleton endpoint cohorts 712\u2192127 and 714\u2192127. All 14 prior untested public banks.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "P104 rank-five residual pairing research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "A fixed-paid productive split requires a pure prefix direction before any pairing or native lowering.", + "budget_minutes": 6, + "evidence": "Fourteen exact rational prefix exclusions independently confirmed by nonzero exterior minors modulo 65537. Full signed predecode directed quote and known-good/mutation controls.", + "open_questions": [ + { + "blocked_by": "Both frozen singleton cohorts have full exterior prefix rank at all 14 cuts.", + "first_step": "Price a single changed paid route and pin its exact affected bank before extending the search.", + "question": "Can another paid route or a different exact cut supply a pure prefix direction?", + "why_it_matters": "A legal productive split can move the binding complex moment." + } + ], + "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": "Continue the 14 exact untested #7370 catalogue keys explicitly preserved by #7375, allowing arbitrary public bank coefficients.", + "scope_status": "changed", + "stop_rule": "14 frozen cases and 25 runner seconds, followed by a bounded rational suffix gate only after a prefix survivor.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-rank-five-singleton-prefix-bound/VERIFICATION.md b/research/p104-rank-five-singleton-prefix-bound/VERIFICATION.md new file mode 100644 index 0000000000..847373ca94 --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/VERIFICATION.md @@ -0,0 +1,5 @@ +# Verification + +The registered replay requires standard-library CPython 3.12. It uses immutable path-keyed inputs and rebuilds a private scratch tree. It checks the exact compressed word SHA-256 and canonical payload SHA-256. The regenerated price authenticates the previous Git source manifests and all derived predecessor receipt hashes. The exact backward rational and independent 65537 forward engines both exhaust their 14 keys under their 25-second science caps. No literal suffix gate, changed native supplier, full candidate compiler or all-size replay ran because the prefix gate excludes every candidate. + +Historical unit pairing, planted kernel, signed nonzero minor, exact direct impulse, unequal proportional pairing, nonproportional pairing, nonunit denominator and owned COPY/adjoint controls are checked. The replay rejects changes to the #7375 second-prime receipt, frozen metadata and compressed native word. `receipts/SHA256.json` binds all four regenerated outputs. `PROVENANCE.json` supplies exact source references and `LOCAL-PINS.json` authenticates the closure. diff --git a/research/p104-rank-five-singleton-prefix-bound/VERIFY.json b/research/p104-rank-five-singleton-prefix-bound/VERIFY.json new file mode 100644 index 0000000000..405729e7c3 --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Regenerate directed price, both exact prefix engines and 14-key agreement. Authenticate exact predecessor manifests and reject three changed dependencies.", + "timeout_seconds": 140 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-rank-five-singleton-prefix-bound/independent/compare.py b/research/p104-rank-five-singleton-prefix-bound/independent/compare.py new file mode 100644 index 0000000000..645208b339 --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/independent/compare.py @@ -0,0 +1,40 @@ +"""Compare the 14 independent nonzero rational-rank certificates to lead.""" +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "lead/RESULT.json": "aa3e2a52214451c4bd99c231a3a30823a8017f53e5e9e2705ed884335c705a7a", + "independent/RESULT.json": "76f6d7b38943b457ad70942cacc530ce531ceec6e4defe6ef425cacb68bd409b", +} + + +def read(path): + raw = (ROOT/path).read_bytes() + if sha256(raw).hexdigest() != PINS[path]: + raise ValueError(f"changed dependency {path}") + return loads(raw) + + +def main(): + lead, independent = map(read,PINS) + assert all(lead[k] == independent[k] for k in ("head","caller","case_cap")) + assert not lead["unvisited"] and not lead["survivors"] and not independent["unresolved"] + a = {tuple(r["key"]):r for r in lead["tested"]} + b = {tuple(r["key"]):r for r in independent["rows"]} + assert a.keys() == b.keys() and len(a) == 14 + for key, left in a.items(): + right = b[key] + assert left["bank"] == right["public"] and not right["owned"] + assert left["pivot"] == right["pivot"] and left["child_ranks"] == right["ordered_child_ranks"] + assert left["disposition"] == "absent pure prefix direction" + assert right["disposition"] == "exact full prefix rank" + assert left["prefix_exterior_rank"] == right["prefix_minor"]["rank"] == len(left["bank"]) + assert right["prefix_minor"]["determinant"] and not right["prefix_minor"]["kernel"] + print(dumps({"pins":PINS,"case_agreements":len(a),"suffix_required":0,"unresolved":0}, + indent=2,sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-five-singleton-prefix-bound/independent/pure_support.py b/research/p104-rank-five-singleton-prefix-bound/independent/pure_support.py new file mode 100644 index 0000000000..46180f7b49 --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/independent/pure_support.py @@ -0,0 +1,356 @@ +"""Exact pure prefix/suffix and unit pairing for the #7334 chart-207 split.""" +from argparse import ArgumentParser +from collections import defaultdict +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic + +HEAD = 'aaeec8c0acf01e99a5f331ef363a698d9c084ace' +WORD = '4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a' +ADMISSION = 'c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13' +PROTECTED = {319,863,1355,1568} +CAP = 128 + + +class Capped(Exception): + pass + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def check_time(deadline): + if monotonic() >= deadline: + raise Capped + + +def pinned(path, digest): + raw = path.read_bytes() + need(sha256(raw).hexdigest() == digest, f'Changed input {path.name}') + return raw + + +def unique(pairs): + doc = dict(pairs) + need(len(doc) == len(pairs), 'Duplicate receipt key') + return doc + + +def read(raw): + return loads(raw,object_pairs_hook=unique) + + +@cache +def rational(value): + return Q(value) + + +def axpy(dst, src, factor): + for j,v in src.items(): + value = dst.get(j,0) + factor*v + if value: + dst[j] = value + else: + dst.pop(j,None) + + +def dot(a,b): + return sum(v*b.get(j,0) for j,v in a.items()) + + +def compose(weights, rows): + vector = {} + for role, coefficient in weights.items(): + axpy(vector,rows[role],coefficient) + return vector + + +def pure_kernel(rows, allowed, deadline): + pivots, pure = {}, [] + for role,row in rows.items(): + check_time(deadline) + exterior = {j:v for j,v in row.items() if j not in allowed} + coeff = {role:Q(1)} + while exterior: + j = min(exterior) + if j not in pivots: + lead = exterior[j] + pivots[j] = ({k:v/lead for k,v in exterior.items()}, + {k:v/lead for k,v in coeff.items()}) + break + other, op = pivots[j] + factor = -exterior[j] + axpy(exterior,other,factor) + axpy(coeff,op,factor) + else: + projection = compose(coeff,rows) + assert projection.keys() <= allowed + pure.append((coeff,projection)) + assert len(pivots)+len(pure) == len(rows) + return sorted(pivots), pure + + +def solve_bilinear(B,D,deadline): + """Find x,y with xBy=1 and xDy=0, or prove no such rational pair.""" + n = len(B) + def trial(x): + bx,dx = compose(x,B),compose(x,D) + if not bx: + return None + if not dx: + j = min(bx) + return x,{j:1/bx[j]} + pivot = min(dx) + for j in sorted(bx.keys() | dx.keys()): + value = bx.get(j,0)*dx[pivot]-bx.get(pivot,0)*dx.get(j,0) + if value: + y = {j:dx[pivot]/value} + if dx.get(j,0): + y[pivot] = -dx[j]/value + assert dot(bx,y) == 1 and dot(dx,y) == 0 + return x,y + return None + for i in range(n): + check_time(deadline) + hit = trial({i:Q(1)}) + if hit: + return hit + # Each wedge coordinate is a homogeneous quadratic in x. Basis vectors + # and pair sums determine all coefficients over Q. + for i in range(n): + check_time(deadline) + for j in range(i+1,n): + hit = trial({i:Q(1),j:Q(1)}) + if hit: + return hit + # All wedges vanish. Only xD=0 but xB!=0 can give a pair. + _, kernel = pure_kernel(dict(enumerate(D)),set(),deadline) + for x,_ in kernel: + hit = trial(x) + if hit: + return hit + return None + + +def paired(prefix,suffix,deadline): + B,D = [],[] + for a,c in prefix: + check_time(deadline) + dot_boundary = {j:v for j,(_,d) in enumerate(suffix) if (v:=dot(c,d))} + dot_difference = {j:v for j,(b,_) in enumerate(suffix) if (v:=dot(a,b)-dot_boundary.get(j,0))} + B.append(dot_boundary); D.append(dot_difference) + hit = solve_bilinear(B,D,deadline) + if hit is None: + return None + x,y = hit + a,c = (compose(x,[pair[i] for pair in prefix]) for i in (0,1)) + b,d = (compose(y,[pair[i] for pair in suffix]) for i in (0,1)) + assert dot(a,b)==dot(c,d)==1 + return dict(a=a,b=b,c=c,d=d) + + +def initial_groups(word): + n = word['public'] + main = set(word['live']) | {r+112 for r in word['live']} + main.update(word['hosted']['X2']); main.update(word['hosted']['Y2']) + cohort = {r for r in range(n) if r not in main and (word['initial'][r],word['final'][r])==(3,127)} + return cohort-PROTECTED,cohort-PROTECTED + + +def prefix_rows(word, cuts, deadline): + n = word['public']; rows = [{r:Q(1)} for r in range(n)]+[None]*word['owned_fields'] + charts = word['initial']+[None]*word['owned_fields'] + banks, seen = {}, 0 + try: + for clock,event in enumerate(word['program']): + if clock%64 == 0 or clock in cuts: + check_time(deadline) + if clock in cuts: + banks[clock] = {r:rows[r].copy() for r in range(n) if charts[r]==207} + if clock >= max(cuts): + break + op,dst,*args = event + if op == 'MOVE': + old,new,owned = args + assert charts[dst] == old and owned==(dst>=n) + charts[dst]=new + elif op == 'INIT': + assert dst>=n and rows[dst] is None + rows[dst],charts[dst]={},args[0] + elif op == 'CLEAR': + assert dst>=n and charts[dst]==args[0] + rows[dst]=charts[dst]=None + elif op == 'SCALE': + assert charts[dst]==args[1] + rows[dst]={j:rational(args[0])*v for j,v in rows[dst].items()} + else: + src,q,chart=args + assert charts[dst]==charts[src]==chart and src!=dst and op in {'ADD','COPY'} + if op=='COPY': + assert dst>=n and not rows[dst], 'Dirty COPY' + axpy(rows[dst],rows[src],rational(q)) + seen=clock+1 + except Capped: + pass + return banks,seen + + +def suffix_rows(word,banks,deadline): + n=word['public']; cols=[{r:Q(1)} for r in range(n)]+[{} for _ in range(word['owned_fields'])] + snapshots,seen={},0 + try: + for clock in range(len(word['program']),min(banks)-1,-1): + if clock%64==0 or clock in banks: + check_time(deadline) + if clock in banks: + snapshots[clock]={r:cols[r].copy() for r in banks[clock]} + if clock==min(banks): + break + op,dst,*args=word['program'][clock-1] + if op in {'ADD','COPY'}: + src,q,_=args + axpy(cols[src],cols[dst],rational(q)) + if op=='COPY': + cols[dst]={} + elif op=='SCALE': + cols[dst]={j:rational(args[0])*v for j,v in cols[dst].items()} + elif op in {'INIT','CLEAR'}: + cols[dst]={} + else: + assert op=='MOVE' + seen+=1 + except Capped: + pass + return snapshots,seen + + +def geometry_keys(geometry): + if 'representative_keys' in geometry: + raw=geometry['representative_keys'] + elif 'keys' in geometry: + raw=geometry['keys'] + else: + raw=[(row['cut'],row['chart'],pivot) for row in geometry['segments'] for pivot in row['pivots']] + result=[tuple(row) if not isinstance(row,dict) else (row['cut'],row['chart'],row['pivot']) for row in raw] + need(len(result)==len(set(result)) and all(len(row)==3 and row[1]==207 and 44588<=row[0]<=44628 for row in result),'Wrong geometry key inventory') + return result + + +def audit(word,geometry,deadline): + all_keys=geometry_keys(geometry) + if not all_keys: + return dict(status='empty_geometry',selected=0,decisions=[],unresolved=[]) + keys=all_keys[:CAP] + cohort,pivots=initial_groups(word) + if 'endpoint_cohort' in geometry: + assert sorted(cohort)==geometry['endpoint_cohort'] + overflow=[tuple(key) for key in geometry.get('unvisited_keys',())] + assert len(overflow)==len(set(overflow)) and not set(overflow).intersection(all_keys) + bank_plan=defaultdict(list) + for cut,chart,pivot in keys: + need(pivot in pivots,'Protected or non-helper pivot') + bank_plan[cut].append(pivot) + banks,forward=prefix_rows(word,bank_plan,deadline) + decisions,opens={}, {} + try: + for cut,bank in banks.items(): + need(set(bank_plan[cut])<=bank.keys(),'Pivot absent from literal chart bank') + exterior,pure=pure_kernel(bank,cohort,deadline) + if any(c for _,c in pure): + opens[cut]=(exterior,pure) + else: + decisions[cut]=dict(status='no_nonzero_pure_prefix',public_bank=list(bank), + prefix_exterior_pivots=exterior,prefix_nullity=len(pure)) + except Capped: + pass + backward=0 + if opens: + snapshots,backward=suffix_rows(word,{c:banks[c] for c in opens},deadline) + try: + for cut,bank in snapshots.items(): + exterior,pure=pure_kernel(bank,cohort,deadline) + pre_rank,pre=opens[cut] + row=dict(public_bank=list(bank),prefix_exterior_pivots=pre_rank, + suffix_exterior_pivots=exterior,prefix_nullity=len(pre),suffix_nullity=len(pure)) + if not any(d for _,d in pure): + decisions[cut]=row|dict(status='no_nonzero_pure_suffix') + continue + witness=paired(pre,pure,deadline) + if witness is None: + decisions[cut]=row|dict(status='no_unit_pairing') + continue + assert compose(witness['a'],banks[cut])==witness['c'] + assert compose(witness['b'],bank)==witness['d'] + decisions[cut]=row|dict(status='exact_support_only',witness={k:{j:str(v) for j,v in value.items()} for k,value in witness.items()}) + except Capped: + pass + rows=[dict(key=key,**decisions[key[0]]) for key in keys if key[0] in decisions] + unresolved=[key for key in all_keys if key[0] not in decisions or key not in keys] + overflow + return dict(status='CAPPED' if unresolved else 'EXHAUSTED',selected=len(keys), + eligible_cohort=sorted(cohort),prefix_events=forward,suffix_events=backward, + decisions=rows,unresolved=unresolved,support_only=[row['key'] for row in rows if row['status']=='exact_support_only']) + + +def controls(): + inf=float('inf') + _,a=pure_kernel({4:{0:Q(1),2:Q(1)},5:{2:Q(1)}},{0},inf) + _,b=pure_kernel({4:{0:Q(1)},5:{3:Q(1)}},{0},inf) + hit=paired(a,b,inf) + assert hit and hit['a'][4] == -hit['a'][5] != 0 + assert dot(hit['a'],hit['b']) == dot(hit['c'],hit['d']) == 1 + _,wrong=pure_kernel({4:{0:Q(1),3:Q(1)},5:{3:Q(1)}},{0},inf) + assert paired(a,wrong,inf) is None + assert solve_bilinear([{0:Q(1)},{1:Q(1)}],[{0:Q(1)},{1:Q(2)}],inf)[0]=={0:Q(1),1:Q(1)} + assert solve_bilinear([{0:Q(1)},{0:Q(2)}],[{0:Q(1)},{0:Q(1)}],inf) is not None + return ['signed_unit_pair','unequal_pairing_rejected','quadratic_cross_term','left_kernel_D'] + + +def main(): + p=ArgumentParser(description=__doc__) + p.add_argument('--controls-only',action='store_true') + for key in ('word','price','geometry','admission'): + p.add_argument('--'+key,type=Path) + p.add_argument('--price-sha'); p.add_argument('--geometry-sha') + a=p.parse_args() + assert __debug__ + checks=controls() + if a.controls_only: + print(dumps(dict(controls=checks),indent=2,sort_keys=True)); return + need(all((a.word,a.price,a.geometry,a.admission,a.price_sha,a.geometry_sha)),'Sealed geometry and price are required') + price=read(pinned(a.price,a.price_sha)); geom=read(pinned(a.geometry,a.geometry_sha)) + admission=read(pinned(a.admission,ADMISSION)) + assert price['head']==admission['head']==HEAD and admission['exit']==0 + assert price['productive_delta']=={'1':17,'8':17,'9':-17} and not price['paid_delta'] + assert admission['inputs']['WORD.json.gz']==WORD + if 'price_sha256' in geom: + assert geom['price_sha256']==a.price_sha + if 'word_sha256' in geom: + assert geom['word_sha256']==WORD + keys=geometry_keys(geom) + if keys: + def watchdog(*_): + raise TimeoutError('hard support watchdog') + signal(SIGALRM,watchdog) + alarm(35) + try: + deadline=monotonic()+32 + result=audit(read(decompress(pinned(a.word,WORD))),geom,deadline) + finally: + alarm(0) + else: + result=dict(status='empty_geometry',selected=0,decisions=[],unresolved=[]) + result.update(head=HEAD,word_sha256=WORD,admission_sha256=ADMISSION,price_sha256=a.price_sha, + geometry_sha256=a.geometry_sha,cap=CAP,seconds_cap=35,controls=checks, + unvisited_credit_upper=price['one_edit_optimistic_credit'][1]) + print(dumps(result,indent=2,sort_keys=True)) + + +if __name__=='__main__': + main() diff --git a/research/p104-rank-five-singleton-prefix-bound/independent/second_prime.py b/research/p104-rank-five-singleton-prefix-bound/independent/second_prime.py new file mode 100644 index 0000000000..0be5407fe6 --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/independent/second_prime.py @@ -0,0 +1,339 @@ +"""Independently verify R97's 310 frozen R96 bank keys modulo 65537.""" + +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from math import isqrt +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic +import sys + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +WORD = "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PINS = { + "inputs/PRICE.json": "a78be64c3e3ae8a0e532237c4dd3541aa9ad3fcbbc3c25d79c8a03fb7e07c525", + "inputs/GEOMETRY.json": "c6f9f018df8b58fcdf4f44356bd59bcac6d411b7845104ff4ad372ed4a95cfbd", + "inputs/REMAINING.json": "3597499663a57702856945e91214a65e1d0f94db8643b93c0234c2bbf9291b1a", + "inputs/7334-WORD.json.gz": WORD, +} +PRIME = 65537 +CASES = 310 +SECONDS = 25 +EVENTS = 76466 + + +def unique(items): + data = dict(items) + if len(items) != len(data): + raise ValueError("duplicate JSON key") + return data + + +def authenticate(root): + raw = {} + for rel, expected in PINS.items(): + data = (root / rel).read_bytes() + if sha256(data).hexdigest() != expected: + raise ValueError(f"changed dependency: {rel}") + raw[rel] = data + return raw + + +@cache +def coefficient(value): + q = Fraction(value) + if not q or q.denominator % PRIME == 0: + raise ValueError("zero scalar or denominator divisible by modulus") + return q.numerator * pow(q.denominator, -1, PRIME) % PRIME, q.denominator + + +def axpy(target, source, scale): + if scale: + for role, old in source.items(): + current = (target.get(role, 0) + scale * old) % PRIME + if current: + target[role] = current + else: + target.pop(role, None) + + +def scaled(vector, scale): + return {i: y for i, x in vector.items() if (y := x * scale % PRIME)} + + +def verify_minor(vectors, columns): + """Independently recompute a minor on the original projected rows.""" + matrix = [[row.get(c, 0) for c in columns] for row in vectors] + determinant = 1 + for c in range(len(matrix)): + pivot = next((r for r in range(c, len(matrix)) if matrix[r][c]), None) + if pivot is None: + return 0 + if pivot != c: + matrix[c], matrix[pivot] = matrix[pivot], matrix[c] + determinant = -determinant + diag = matrix[c][c] + determinant = determinant * diag % PRIME + inverse = pow(diag, -1, PRIME) + for r in range(c + 1, len(matrix)): + factor = matrix[r][c] * inverse % PRIME + if factor: + for k in range(c + 1, len(matrix)): + matrix[r][k] = (matrix[r][k] - factor * matrix[c][k]) % PRIME + matrix[r][c] = 0 + return determinant % PRIME + + +def classify(bank, vectors, cohort): + full_rows = [vectors[r] for r in bank] + exterior = [{i: x for i, x in row.items() if i not in cohort} for row in full_rows] + basis, kernel = [], [] + determinant = 1 + for index, vector in enumerate(exterior): + work = vector.copy() + combination = {index: 1} + for col, known, combo in basis: + factor = -work.get(col, 0) + axpy(work, known, factor) + axpy(combination, combo, factor) + if not work: + image = {} + for i, factor in combination.items(): + axpy(image, full_rows[i], factor) + assert image.keys() <= cohort + kernel.append(dict(cut={bank[i]: x for i, x in combination.items()}, endpoint=image)) + continue + col = max(work) + pivot = work[col] + determinant = determinant * pivot % PRIME + inverse = pow(pivot, -1, PRIME) + basis.append((col, scaled(work, inverse), scaled(combination, inverse))) + rank = len(basis) + assert rank + len(kernel) == len(bank) + columns = [col for col, _, _ in basis] + if kernel: + return dict(rank=rank, kernel=kernel, minor_axes=None, determinant=None) + assert columns and verify_minor(exterior, columns) == determinant != 0 + return dict(rank=rank, kernel=[], minor_axes=columns, determinant=determinant) + + +def apply(event, state, vectors, fresh, n, denominators, backward): + op, r, *args = event + current = state[r] + if op == "MOVE": + old, new, owned = args + assert owned == (r >= n) + assert current == (new if backward else old) + state[r] = old if backward else new + fresh.discard(r) + return + if op in ("INIT", "CLEAR"): + assert r >= n + c, = args + entering = (op == "CLEAR") if backward else (op == "INIT") + if entering: + assert current is None and vectors[r] is None + state[r], vectors[r] = c, {} + if not backward: + fresh.add(r) + else: + assert current == c and vectors[r] is not None + state[r] = vectors[r] = None + fresh.discard(r) + return + assert op in ("SCALE", "ADD", "COPY") and current == args[-1] and vectors[r] is not None + factor, denominator = coefficient(args[-2]) + denominators.add(denominator) + if op == "SCALE": + vectors[r] = scaled(vectors[r], factor) + else: + src = args[0] + assert src != r and state[src] == current and vectors[src] is not None + if backward: + axpy(vectors[src], vectors[r], factor) + if op == "COPY": + assert r >= n + vectors[r] = {} + elif op == "COPY": + assert r >= n and r in fresh and not vectors[r] + vectors[r] = scaled(vectors[src], factor) + else: + axpy(vectors[r], vectors[src], factor) + fresh.discard(r) + + +def controls(): + assert all(PRIME % i for i in range(2, isqrt(PRIME) + 1)) + witness = classify([0, 1], [{3: 2, 8: 1}, {3: 3, 8: 4}], set()) + assert witness["minor_axes"] == [8, 3] and witness["determinant"] == PRIME - 5 + dropped = classify([0, 1], [{0: 1, 8: 1}, {1: 1, 8: 1}], {0, 1}) + assert dropped["kernel"] == [dict(cut={0: PRIME - 1, 1: 1}, endpoint={0: PRIME - 1, 1: 1})] + tape = [("ADD", 1, 0, "-3/2", 4), ("SCALE", 0, "2", 4), ("INIT", 2, 4), + ("COPY", 2, 1, "1", 4), ("ADD", 0, 2, "5", 4), ("CLEAR", 2, 4)] + result = [] + for backward in (False, True): + state, vectors, fresh, denoms = [4, 4, None], [{0: 1}, {1: 1}, None], set(), set() + for event in reversed(tape) if backward else tape: + apply(event, state, vectors, fresh, 2, denoms, backward) + assert state == [4, 4, None] and not fresh and denoms == {1, 2} + result.append(vectors) + assert result[0] == [{0: coefficient("-11/2")[0], 1: 5}, {0: coefficient("-3/2")[0], 1: 1}, None] + assert result[1] == [{0: coefficient("-11/2")[0], 1: coefficient("-3/2")[0]}, {0: 5, 1: 1}, None] + try: + coefficient("1/65537") + except ValueError: + pass + else: + raise AssertionError("nonunit denominator admitted") + return ["prime and signed nonzero minor", "planted pure kernel", "owned COPY forward and adjoint", + "nonunit denominator rejection"] + + +def span(frame): + vectors = {0} + for v in frame: + assert v not in vectors + vectors |= {v ^ w for w in vectors} + return vectors + + +def sweep(word, keys, cohort, deadline, result, progress, backward, previous=None): + tape, n, owned = (word[k] for k in ("program", "public", "owned_fields")) + assert (len(tape), n, owned) == (EVENTS, 1501, 68) + origin, target = ("final", "initial") if backward else ("initial", "final") + state = word[origin] + [None] * owned + vectors = [{r: 1} for r in range(n)] + [None] * owned + fresh, denoms = set(), set() + request = defaultdict(list) + frames = word["frames"] + low, high = span(frames[3]), span(frames[245]) + for cut, chart in keys: + assert 0 <= cut <= EVENTS and len(frames[chart]) == 4 and low < span(frames[chart]) < high + request[cut].append(chart) + boundaries = range(EVENTS, -1, -1) if backward else range(EVENTS + 1) + progress.update(events=0, first_unvisited_cut=boundaries.start, denominator_units=[]) + for cut in boundaries: + progress["first_unvisited_cut"] = cut + if (cut % 128 == 0 or cut in request) and monotonic() >= deadline: + break + for chart in request.get(cut, []): + key = (cut, chart) + public_bank = [r for r in range(n) if state[r] == chart] + owned_bank = [r for r in range(n, n + owned) if state[r] == chart] + pivots = sorted(set(public_bank) & cohort) + assert public_bank and pivots + if cut: + event = tape[cut - 1] + assert chart in (event[2:4] if event[0] == "MOVE" else event[-1:]) + bank = dict(public=public_bank, owned=owned_bank, pivots=pivots) + if previous is not None: + assert bank == previous[key]["bank"] + result[key] = dict(bank=bank, **classify(public_bank, vectors, cohort)) + if cut == (0 if backward else EVENTS): + assert state == word[target] + [None] * owned and not fresh + assert set(result) == set(keys) + progress["first_unvisited_cut"] = None + break + apply(tape[cut - 1 if backward else cut], state, vectors, fresh, n, denoms, backward) + progress["events"] += 1 + progress["denominator_units"] = sorted(denoms) + + +def pairing(prefix, suffix): + def dot(left, right): + return sum(v * right.get(i, 0) for i, v in left.items()) % PRIME + + return [[dict(cut=dot(a["cut"], b["cut"]), endpoint=dot(a["endpoint"], b["endpoint"])) + for b in suffix["kernel"]] for a in prefix["kernel"]] + + +def main(): + parser = ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=ROOT) + parser.add_argument("--controls-only", action="store_true") + args = parser.parse_args() + assert __debug__ and sys.version_info[:2] == (3, 12) + checks = controls() + if args.controls_only: + print(dumps(checks)) + return + + def stop(*_): + raise TimeoutError("hard 25-second cap") + + start = monotonic() + signal(SIGALRM, stop) + alarm(SECONDS) + timeout = None + keys, prior, prefix, suffix = [], [], {}, {} + prefix_progress, suffix_progress = {}, {} + try: + raw = authenticate(args.root) + price, geom, remaining = [loads(raw[f"inputs/{name}.json"], object_pairs_hook=unique) + for name in ("PRICE", "GEOMETRY", "REMAINING")] + assert price["head"] == geom["head"] == remaining["head"] == HEAD and price["caller"] == CALLER + assert price["word_sha256"] == geom["word_sha256"] == WORD + assert geom["price_sha256"] == PINS["inputs/PRICE.json"] + assert remaining["input_sha256"]["lead/GEOMETRY.json"] == PINS["inputs/GEOMETRY.json"] + assert geom["status"] == "EXHAUSTED" and geom["visited_events"] == EVENTS + keys = list(map(tuple, remaining["unvisited_prefix"])) + prior = remaining["dual_drops_requiring_rational"] + assert len(keys) == len(set(keys)) == remaining["next_modular_cases"] == CASES + assert remaining["next_modular_runner_seconds"] == SECONDS + assert keys == list(map(tuple, geom["unvisited_keys"])) + selected = {tuple(row["key"]) for row in geom["selected"]} + assert len(selected) == 16 and not set(keys) & selected and set(map(tuple, prior)) <= selected + assert set(keys) | selected == set(map(tuple, geom["all_representative_keys"])) + assert prior == [[41740, 242], [45266, 242]] + payload = decompress(raw["inputs/7334-WORD.json.gz"]) + assert sha256(payload).hexdigest() == PAYLOAD + word = loads(payload, object_pairs_hook=unique) + cohort = set(price["cohort"]) + assert len(cohort) == 15 and all((word["initial"][r], word["final"][r]) == (3, 245) for r in cohort) + deadline = start + SECONDS - 2 + sweep(word, keys, cohort, deadline, prefix, prefix_progress, False) + candidates = [key for key in keys if key in prefix and prefix[key]["kernel"]] + if candidates: + sweep(word, candidates, cohort, deadline, suffix, suffix_progress, True, prefix) + else: + suffix_progress.update(events=0, first_unvisited_cut=None, denominator_units=[]) + except TimeoutError as error: + timeout = str(error) + finally: + alarm(0) + + results = [] + for key in keys: + left, right = prefix.get(key), suffix.get(key) + pair = None + if left and not left["kernel"]: + status = "prefix_exclusion" + elif right and not right["kernel"]: + status = "suffix_exclusion" + elif right: + status = "dual_drop" + pair = pairing(left, right) + else: + status = "unvisited" + results.append(dict(key=key, status=status, prefix=left, suffix=right, modular_pairings=pair)) + complete = (timeout is None and prefix_progress.get("first_unvisited_cut", 0) is None + and suffix_progress.get("first_unvisited_cut", 0) is None) + print(dumps(dict(head=HEAD, caller=CALLER, pins=PINS, modulus=PRIME, controls=checks, + cap_cases=CASES, cap_seconds=SECONDS, prefix_progress=prefix_progress, suffix_progress=suffix_progress, + timeout=timeout, complete=complete, results=results, + counts=Counter(row["status"] for row in results), previously_frozen_exact_keys=prior), + indent=2, sort_keys=True)) + if not complete: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-five-singleton-prefix-bound/independent/singleton.py b/research/p104-rank-five-singleton-prefix-bound/independent/singleton.py new file mode 100644 index 0000000000..8ce2c5b50f --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/independent/singleton.py @@ -0,0 +1,262 @@ +"""Whole-word forward exact-prime audit of both frozen rank-five cohorts.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +FROZEN = "preflight/FROZEN.json" +WORD = "inputs/7334-WORD.json.gz" +OLD = "inputs/OLD-WITNESS.json" +MODULAR = "independent/second_prime.py" +PURE = "independent/pure_support.py" +PINS = { + FROZEN: "3861fa02acfafd35f3c437397f8aecd282a21687d81e426e25e2289f21d54a4a", + WORD: "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + OLD: "5be60a09485041744919696121ae27e57a1aa9de437a2c4494d5fc569af4cdb4", + MODULAR: "21dbd96192e1f60c00ceddba01a7e8d0ddd7d6ad7da4ad3ed22ef2e47cc589c4", + PURE: "38c796cbe1a73f386177faf88cd53294d4b911f6cde7fd47cd9fcef3b558373f", +} +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +GROUPS = {(712, 127): 1360, (714, 127): 1361} +EVENTS, CAP, SECONDS, PRIME = 76466, 14, 25, 65537 + + +def unique(rows): + value = dict(rows) + if len(value) != len(rows): + raise ValueError("duplicate metadata key") + return value + + +def read(root, name): + raw = (root/name).read_bytes() + if sha256(raw).hexdigest() != PINS[name]: + raise ValueError(f"changed dependency {name}") + return raw + + +def stop(*_): + raise TimeoutError("hard 25-second cap") + + +def deadline_check(deadline): + if monotonic() >= deadline: + raise TimeoutError("cooperative cap") + + +def cohort_cases(price): + assert price["head"] == HEAD and price["caller"] == CALLER + assert price["word_sha256"] == PINS[WORD] and price["case_count"] == CAP + assert price["caps"]["initial_seconds"] == SECONDS + assert price["max_distinct_compatible_edits"] == 2 and not price["paid_delta"] + assert Q(price["complete_one_probe"][0]) > 0 > Q(price["complete_two_target"][1]) + assert {tuple(r["endpoints"]):r["pivot"] for r in price["cohorts"]} == GROUPS + cases = {tuple(row["key"]):row for row in price["cases"]} + assert len(cases) == CAP + assert Counter(k[2:] for k in cases) == {g:7 for g in GROUPS} + for k, row in cases.items(): + assert row["pivots"] == [GROUPS[k[2:]]] and row["owned"] == [] + assert row["productive_parent_rank"] == 5 and row["productive_child_ranks_sorted"] == [2,3] + return cases + + +def forward(word, cases, mod, deadline, out, progress, denoms): + n, owners, tape = (word[k] for k in ("public", "owned_fields", "program")) + assert (n, owners, len(tape)) == (1501, 68, EVENTS) + frames = word["frames"] + + @cache + def span(chart): + return mod["span"](frames[chart]) + + requests = defaultdict(list) + for k, row in cases.items(): + t, mid, low, high = k + pivot, = row["pivots"] + assert (word["initial"][pivot], word["final"][pivot]) == (low, high) + assert span(low) < span(mid) < span(high) + ordered = [len(frames[mid])-len(frames[low]), len(frames[high])-len(frames[mid])] + assert sorted(ordered) == [2,3] + requests[t].append((k, ordered)) + state = word["initial"] + [None]*owners + rows = [{r:1} for r in range(n)] + [None]*owners + fresh = set() + for t in range(EVENTS+1): + if t % 128 == 0: + deadline_check(deadline) + for k, ordered in requests.get(t, ()): + _, mid, *_ = k + frozen = cases[k] + bank = [r for r in range(n) if state[r] == mid] + owned = [r for r in range(n,n+owners) if state[r] == mid] + assert bank == frozen["public"] and owned == frozen["owned"] == [] + pivot, = frozen["pivots"] + assert pivot in bank + cert = mod["classify"](bank, rows, {pivot}) + exterior = [{r:v for r,v in rows[b].items() if r != pivot} for b in bank] + if not cert["kernel"]: + assert cert["rank"] == len(bank) + assert mod["verify_minor"](exterior, cert["minor_axes"]) == cert["determinant"] != 0 + out[k] = dict(key=k, public=bank, owned=owned, pivot=pivot, + ordered_child_ranks=ordered, exterior_rows=exterior, prefix_minor=cert, + disposition="modular prefix drop" if cert["kernel"] else "exact full prefix rank") + if t == EVENTS: + assert state == word["final"] + [None]*owners and not fresh + break + op, _, *args = tape[t] + if op == "MOVE": + old, new, owner = args + assert span(old) < span(new) or owner and span(new) < span(old) + mod["apply"](tape[t], state, rows, fresh, n, denoms, False) + progress["events"] = t+1 + + +@cache +def scalar(raw): + return Q(raw) + + +def put(vector, role, value): + if value: + vector[role] = value + else: + vector.pop(role, None) + + +def impulse(tape, cut, role, before, deadline): + """Exact one-axis row before cut or column after cut.""" + v = {role:Q(1)} + times = range(cut-1,-1,-1) if before else range(cut,len(tape)) + for t in times: + if t % 128 == 0: + deadline_check(deadline) + op, dest, *a = tape[t] + if op == "MOVE": + continue + if op in ("INIT", "CLEAR"): + v.pop(dest, None) + continue + if op == "SCALE": + if dest in v: + put(v,dest,v[dest]*scalar(a[0])) + continue + assert op in ("ADD","COPY") + source, q, _ = a + if before: + current = v.get(dest,0) + if op == "COPY": + v.pop(dest,None) + if current: + put(v,source,v.get(source,0)+scalar(q)*current) + else: + current = scalar(q)*v.get(source,0) + if op == "ADD": + current += v.get(dest,0) + put(v,dest,current) + return v + + +def pair_kind(local, endpoint): + entries = [(x,y) for lr,er in zip(local,endpoint,strict=True) for x,y in zip(lr,er,strict=True)] + nonzero = next(((x,y) for x,y in entries if y), None) + if nonzero is None: + return "zero endpoint pairing", None + u,v = nonzero + mu = u/v + if all(x == mu*y for x,y in entries): + return ("relaxed rational pairing" if mu == 1 else "unequal proportional pairing"), mu + return "relaxed rational pairing", None + + +def exact_on_drop(word, row, pure, deadline): + t = row["key"][0] + p, bank = row["pivot"], row["public"] + tape = word["program"] + fp = {r:impulse(tape,t,r,True,deadline) for r in bank} + _, f = pure["pure_kernel"](fp,{p},deadline) + row["exact_prefix_dimension"] = len(f) + if not any(c for _,c in f): + row["disposition"] = "no nonzero exact prefix" + return + n = word["public"] + sp = {r:{i:v for i,v in impulse(tape,t,r,False,deadline).items() if i= deadline: + stop() + if t in requests: + residents = tuple(r for r, frame in enumerate(state) if frame == CHART) + assert residents == requests[t] and PIVOT in residents and max(residents) < n + seen[t] = (epoch, residents) + if t == hi: + break + op, d, *args = event + before = state[d] + if op == "MOVE": + assert args[0] == before and args[2] == (d >= n) + after = args[1] + elif op == "INIT": + assert before is None and d >= n + after = args[0] + elif op == "CLEAR": + assert before == args[0] and d >= n + after = None + else: + after = before + assert op in ("ADD", "COPY", "SCALE") and after == args[-1] + if op in ("ADD", "COPY"): + assert state[args[0]] == before and args[0] != d + if t >= lo and CHART in (before, after): + invertible = d < n and (op == "SCALE" or (op == "ADD" and args[0] < n)) and bool(scalar(args[-2])) + if not invertible: + epoch += 1 + contacts.append({"clock": t, "event": event, "within_epoch": invertible}) + state[d] = after + assert set(seen) == set(requests) + grouped = defaultdict(list) + for t, key in seen.items(): + grouped[key].append(t) + return list(grouped.items()), contacts + + +def trace(word, cut, bank, deadline, reverse): + tape = word["program"] + n, owned = word["public"], word["owned_fields"] + values = [{} for _ in range(n+owned)] + for role in bank: + values[role] = {role: Q(1)} + clocks = range(cut-1, -1, -1) if reverse else range(cut, len(tape)) + for t in clocks: + if t % 256 == 0 and monotonic() >= deadline: + stop() + op, d, *args = tape[t] + if op in ("CLEAR", "INIT"): + values[d] = {} + elif op == "SCALE" and values[d]: + q = scalar(args[0]) + values[d] = {j:q*v for j,v in values[d].items() if q*v} + elif op in ("ADD", "COPY"): + source, factor = args[:2] + q = scalar(factor) + if reverse: + axpy(values[source], values[d], q) + if op == "COPY": + values[d] = {} + elif op == "COPY": + values[d] = {j:q*v for j,v in values[source].items() if q*v} + else: + axpy(values[d], values[source], q) + responses = {r:{} for r in bank} + for coordinate, data in enumerate(values[:n]): + for role, value in data.items(): + responses[role][coordinate] = value + return responses + + +def kernel(columns, allowed): + basis, pure = {}, [] + for role, full in columns.items(): + row = {j:v for j,v in full.items() if j not in allowed} + combo = {role:Q(1)} + for pivot, (old, old_combo) in sorted(basis.items()): + q = -row.get(pivot, 0) + axpy(row, old, q) + axpy(combo, old_combo, q) + if row: + pivot = min(row) + q = row[pivot] + basis[pivot] = ({j:v/q for j,v in row.items()}, {j:v/q for j,v in combo.items()}) + else: + image = {} + for j, q in combo.items(): + axpy(image, columns[j], q) + assert set(image) <= allowed + pure.append((combo, image)) + assert len(basis) + len(pure) == len(columns) + return len(basis), pure + + +def printed(vector): + return {j:str(v) for j,v in sorted(vector.items())} + + +def controls(old): + vectors = {k:{int(j):Q(v) for j,v in old[k].items()} for k in "abcd"} + assert (old["pivot"], old["frame"], old["cut_before"]) == (635, 118, 37473) + assert dot(vectors["a"], vectors["b"]) == dot(vectors["c"], vectors["d"]) == 1 + rank, pure = kernel({4:{0:Q(2),5:Q(1)}, 6:{5:Q(1)}}, {0}) + assert rank == 1 and pure == [({6:Q(1),4:Q(-1)}, {0:Q(-2)})] + assert dot(vectors["c"], {j:2*v for j,v in vectors["d"].items()}) == 2 + return ["historical exact unit pair", "planted exact exterior kernel", "wrong endpoint pairing"] + + +def main(): + assert __debug__ + signal(SIGALRM, hard_stop) + alarm(35) + deadline = monotonic()+32 + price, prior, old, _source, packed = map(checked, PINS) + price, prior, old = [loads(raw, object_pairs_hook=unique) for raw in (price, prior, old)] + assert price["head"] == prior["head"] == HEAD and price["caller"] == CALLER + assert Q(price["complete_probe"][0]) > 0 + tests = controls(old) + rows = [r for r in prior["results"] if r["key"][1] == CHART and PIVOT in r["pivots"]] + requests = {r["key"][0]:tuple(r["public"]) for r in rows} + keys = [r["key"] for r in price["selected"]] + price["unvisited"] + assert len(requests) == len(rows) == len(keys) == CASE_CAP + assert set(requests) == {k[0] for k in keys} and all(k[1] == CHART for k in keys) + assert all(not r["owned"] and r["disposition"] == "rank drop" for r in rows) + raw = decompress(packed) + assert sha256(raw).hexdigest() == PAYLOAD + word = loads(raw, object_pairs_hook=unique) + assert (word["public"], word["owned_fields"], len(word["program"])) == (1501,68,76466) + cohort = set(price["endpoint_cohort"]) + assert len(cohort) == 615 and PIVOT in cohort and 631 not in cohort + assert all((word["initial"][r],word["final"][r]) == (3,127) for r in cohort) + assert [len(word["frames"][r]) for r in (3,118,127)] == [0,5,9] + classes, contacts = cohorts(word, requests, deadline) + results = [] + for (_epoch, bank), aliases in classes: + cut = aliases[0] + f = trace(word,cut,bank,deadline,True) + s = trace(word,cut,bank,deadline,False) + fp, pure_f = kernel(f,cohort) + sp, pure_s = kernel(s,cohort) + local = [[str(dot(a,b)) for b,_ in pure_s] for a,_ in pure_f] + endpoint = [[str(dot(c,d)) for _,d in pure_s] for _,c in pure_f] + zero = all(v=="0" for matrix in (local,endpoint) for row in matrix for v in row) + results.append(dict(representative=[cut,CHART], keys=[[t,CHART] for t in aliases], bank=bank, + prefix_rank=fp, suffix_rank=sp, + pure_prefix=[dict(a=printed(a),c=printed(c)) for a,c in pure_f], + pure_suffix=[dict(b=printed(b),d=printed(d)) for b,d in pure_s], + local=local, endpoint=endpoint, status="zero pairing" if zero else "requires exact pairing test")) + excluded = sum(len(row["keys"]) for row in results if row["status"] == "zero pairing") + alarm(0) + print(dumps(dict(head=HEAD,caller=CALLER,pins=PINS,controls=tests,cap_cases=CASE_CAP,cap_seconds=35, + representative_count=len(results),case_count=len(requests),contacts=contacts,results=results, + excluded=excluded,unresolved=CASE_CAP-excluded, + scope="Relaxed exact rational normalized prefix and suffix pairing, original fixed paid paths."), + indent=2,sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-five-singleton-prefix-bound/inputs/paired_rank.py b/research/p104-rank-five-singleton-prefix-bound/inputs/paired_rank.py new file mode 100644 index 0000000000..b712cdb1f8 --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/inputs/paired_rank.py @@ -0,0 +1,187 @@ +"""Rational paired exclusion using wedge identities and a stacked rank check.""" +from collections import Counter +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +import sys +from time import monotonic + +GEOMETRY="4c349e06b22bfebb431fab1c9ae04f0e798f398acc6fdd99591b49b1c95ef6ca" +WORD="4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" + + +@cache +def coefficient(s): + return Q(s) + + +def checked(path,digest): + data=path.read_bytes() + if sha256(data).hexdigest()!=digest: + raise ValueError(f"changed pin: {path.name}") + return data + + +def plus(row,other,q): + for i,x in other.items(): + v=row.get(i,0)+q*x + if v: + row[i]=v + else: + row.pop(i,None) + + +def null_pure(bank,rows,allowed): + """Eliminate exterior inputs, carrying coefficient vectors on the bank.""" + pivots={} + pure=[] + for r in bank: + row={i:x for i,x in rows[r].items() if i not in allowed} + u={r:Q(1)} + while row: + lead=max(row) + if lead not in pivots: + pivots[lead]=row,u + break + p,a=pivots[lead] + ratio=-row[lead]/p[lead] + plus(row,p,ratio) + plus(u,a,ratio) + else: + full={} + for i,x in u.items(): + plus(full,rows[i],x) + assert set(full)<=allowed + pure.append((u,full)) + assert len(pivots)+len(pure)==len(bank) + return pure + + +def rank(matrix): + basis={} + for source in matrix: + row=source.copy() + while row: + lead=max(row) + if lead not in basis: + basis[lead]=row + break + plus(row,basis[lead],-row[lead]/basis[lead][lead]) + return len(basis) + + +def pairing(B,D): + # No (x,y) with xBy=1 and xDy=0 iff each xB is proportional to xD + # and ker(x -> xD) lies inside ker(x -> xB). + rows=len(B) + cols=len(B[0]) if B else 0 + def wedge(b,d): + return any(b[i]*d[j]!=b[j]*d[i] for i in range(cols) for j in range(i)) + has_wedge=any(wedge(b,d) for b,d in zip(B,D,strict=True)) + if not has_wedge: + for i in range(rows): + for j in range(i): + if wedge([x+y for x,y in zip(B[i],B[j],strict=True)], + [x+y for x,y in zip(D[i],D[j],strict=True)]): + has_wedge=True + break + if has_wedge: + break + dr=rank([{i:x for i,x in enumerate(r) if x} for r in D]) + sr=rank([{i:x for i,x in enumerate(d+b) if x} for d,b in zip(D,B,strict=True)]) + return has_wedge,dr,sr + + +def side(word,banks,allowed,deadline,reverse): + n=word["public"] + tape=word["program"] + vectors=[{i:Q(1)} for i in range(n)]+[{} for _ in range(word["owned_fields"])] + rows={} + cuts=range(len(tape),min(banks)-1,-1) if reverse else range(0,max(banks)+1) + for t in cuts: + if t%128==0 and monotonic()>=deadline: + break + if t in banks: + rows[t]=null_pure(banks[t],vectors,allowed) + if t==0 and reverse: + break + op,d,*args=tape[t-1 if reverse else t] + if op=="MOVE": + continue + if op in ("INIT","CLEAR"): + vectors[d]={} + else: + q=coefficient(args[-2]) + source=d if op=="SCALE" else args[0] + assert op=="SCALE" or source!=d + if op=="SCALE": + vectors[d]={i:q*x for i,x in vectors[d].items()} + elif reverse: + plus(vectors[source],vectors[d],q) + if op=="COPY": + vectors[d]={} + elif op=="COPY": + vectors[d]={i:q*x for i,x in vectors[source].items()} + else: + assert op=="ADD" + plus(vectors[d],vectors[source],q) + return rows + + +def run(word,geom,keys): + deadline=monotonic()+32 + groups=Counter(k[0] for k in keys) + banks={row["cut"]:row["public_bank"] for row in geom["new"]["rows"] if row["cut"] in groups} + allowed=set(geom["endpoint_cohort"]) + forward=side(word,banks,allowed,deadline,False) + reverse=side(word,banks,allowed,deadline,True) + ans=[] + def dot(a,b): + return sum(x*b.get(i,0) for i,x in a.items()) + for t,n in sorted(groups.items()): + if t not in forward or t not in reverse or monotonic()>=deadline: + continue + F,R=forward[t],reverse[t] + w=dr=sr=None + if not any(c for a,c in F): + status="no nonzero pure prefix" + elif not any(d for b,d in R): + status="no nonzero pure suffix" + else: + B=[[dot(a,b) for b,d in R] for a,c in F] + C=[[dot(c,d) for b,d in R] for a,c in F] + D=[[x-y for x,y in zip(b,c,strict=True)] for b,c in zip(B,C,strict=True)] + w,dr,sr=pairing(B,D) + status="paired support unresolved" if w or dr!=sr else "no unit pairing" + ans.append(dict(cut=t,cases=n,status=status,prefix_dimension=len(F),suffix_dimension=len(R), + nonzero_wedge=w,exterior_rank=dr,stacked_rank=sr)) + missing=set(groups)-{r["cut"] for r in ans} + counts=Counter() + for row in ans: + counts[row["status"]]+=row["cases"] + return dict(cases=len(keys),rows=ans,counts=dict(counts), + unvisited=[key for key in keys if key[0] in missing]) + + +def main(): + root=Path(sys.argv[1]) + which=sys.argv[2] + assert which in ("first","remaining") + geom=json.loads(checked(root/"lead/OCCUPANCY.json",GEOMETRY)) + word=json.loads(decompress(checked(root/"inputs/7334-WORD.json.gz",WORD))) + assert pairing([[Q(1),Q(0)]],[[Q(0),Q(1)]])[0] + assert pairing([[Q(1)]],[[Q(2)]])==(False,1,1) + assert pairing([[Q(1)]],[[Q(0)]])==(False,0,1) + keys=geom["representative_keys" if which=="first" else "unvisited_keys"] + assert len(keys)==(128 if which=="first" else 18) + data=run(word,geom,keys) + print(json.dumps(data|dict(selection=which,word_sha256=WORD,geometry_sha256=GEOMETRY, + controls=["nonzero wedge","proportional equal rank","nonzero pairing on difference kernel"]), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-rank-five-singleton-prefix-bound/inputs/pricing.py b/research/p104-rank-five-singleton-prefix-bound/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/inputs/pricing.py @@ -0,0 +1,82 @@ +"""Directed interval arithmetic and the retained signed BIT invoice.""" +from collections import Counter +from fractions import Fraction +from functools import cache + +TARGET = "10018846261809/2500000000000000" +SCALE = 10**49 + + +def rounded(x, upper): + scaled = SCALE*x + if upper: + return Fraction(-((-scaled.numerator) // scaled.denominator), SCALE) + return Fraction(scaled.numerator // scaled.denominator, SCALE) + + +@cache +def log_bounds(x): + z = (x-1)/(x+1) + terms = 60 + exact_partial = 2*sum(z**(2*i+1)/(2*i+1) for i in range(terms)) + tail = 2*z**(2*terms+1)/((2*terms+1)*(1-z*z)) + return rounded(exact_partial, False), rounded(exact_partial+tail, True) + + +@cache +def power_bounds(rank, k): + binary = 2**(rank.bit_length()-1) + shift = binary.bit_length()-1 + l2, u2 = log_bounds(Fraction(2)) + lo, hi = log_bounds(Fraction(rank, binary)) + lo, hi = k*(lo+shift*l2), k*(hi+shift*u2) + assert 0 <= lo <= hi < 1 + + def exponential(z, terms): + total = term = Fraction(1) + for i in range(1, terms+1): + term *= -z/i + total += term + return total + + return rounded(rank*exponential(hi, 35), False), rounded(rank*exponential(lo, 34), True) + + +def cost(hist, k): + lower = upper = Fraction(0) + for r, n in hist.items(): + a, b = (n*x for x in power_bounds(r, k)) + lower += min(a, b) + upper += max(a, b) + return lower, upper + + +def profile(invoice, native, word, ranks): + copies = invoice["native_calls"] + assert copies == len(invoice["native_instances"]) == 36 + assert {tuple((r["stage"], r["copy"])) for r in invoice["native_instances"]} == { + (stage, which) for stage in range(1, 19) for which in (0, 1) + } + assert all(r["ports"] == 111 for r in invoice["native_instances"]) + assert native == Counter({int(r): n for r, n in invoice["native_paid"].items()}) + assert sum(native.values()) == 2871 + caller_paid = {1: 444, **{r: 444 for r in range(7, 57, 7)}} + assert invoice["event_counts"]["QUERY"]*111 == caller_paid[1] + assert invoice["event_counts"]["IDLE_ONE"]*111 == 8*444 + full_paid = Counter({r: copies*n for r, n in native.items()}) + full_paid.update(caller_paid) + + helpers = Counter(ranks[word["final"][j]]-ranks[word["start"][j]] + for j in range(222, word["public"])) + assert helpers == Counter({int(r): n for r, n in invoice["native_helpers"].items()}) + caller_targets = {**{r: 444 for r in range(8, 65, 7)}, 127: 222} + full_targets = Counter({r: copies*n for r, n in helpers.items()}) + full_targets.update(caller_targets) + assert full_paid == Counter({int(r): n for r, n in invoice["paid"].items()}) + assert full_targets == Counter({int(r): n for r, n in invoice["targets"].items()}) + assert sum(full_paid.values()) == invoice["paid_jobs"] + assert sum(full_targets.values()) == invoice["productive_fields"] + signed = full_targets.copy() + signed.subtract(full_paid) + assert sum(r*n for r, n in signed.items()) == invoice["rank_surplus"] + return signed, copies diff --git a/research/p104-rank-five-singleton-prefix-bound/lead/pairs.py b/research/p104-rank-five-singleton-prefix-bound/lead/pairs.py new file mode 100644 index 0000000000..ff4d5190c4 --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/lead/pairs.py @@ -0,0 +1,152 @@ +"""Check exact paired support on the two singleton rank-five cohorts.""" +from fractions import Fraction as Q +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "preflight/FROZEN.json": "3861fa02acfafd35f3c437397f8aecd282a21687d81e426e25e2289f21d54a4a", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/OLD-WITNESS.json": "5be60a09485041744919696121ae27e57a1aa9de437a2c4494d5fc569af4cdb4", + "inputs/bank_trace.py": "681fda5cc1d4b1ac07c62601ceb052f167a51fb73d28b23f454f8f50f6a8e27b", + "inputs/paired_rank.py": "d1b7c34e6f8c8a7b810414762015e6e300a8292422af66ff671ae09741141f09", +} +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + + +def unique(items): + out = dict(items) + if len(out) != len(items): + raise ValueError("duplicate JSON key") + return out + + +def checked(path): + raw = (ROOT / path).read_bytes() + if sha256(raw).hexdigest() != PINS[path]: + raise ValueError(f"changed dependency {path}") + return raw + + +def span(frame): + values = {0} + for a in frame: + assert a not in values + values.update(v ^ a for v in tuple(values)) + return values + + +def topology(word, cases): + n = word["public"] + frames = word["frames"] + state = word["initial"][:] + [None] * word["owned_fields"] + by_cut = {row["key"][0]: row for row in cases} + assert len(by_cut) == len(cases) + ranks, copies = {}, [] + for t, (op, r, *a) in enumerate(word["program"]): + if t in by_cut: + row = by_cut[t] + _, mid, lo, hi = row["key"] + pivot, = row["pivots"] + assert [j for j in range(n) if (word["initial"][j],word["final"][j]) == (lo,hi)] == [pivot] + assert [j for j,c in enumerate(state) if c == mid] == row["public"] and not row["owned"] + assert max(row["public"]) < n and pivot in row["public"] + assert span(frames[lo]) < span(frames[mid]) < span(frames[hi]) + a0,a1,a2 = map(lambda c:len(frames[c]), (lo,mid,hi)) + ranks[t] = [a1-a0,a2-a1] + assert sorted(ranks[t]) == row["productive_child_ranks_sorted"] + before = state[r] + if op == "MOVE": + assert a[0] == before and a[2] == (r >= n) + state[r] = a[1] + elif op == "INIT": + assert before is None and r >= n + state[r] = a[0] + elif op == "CLEAR": + assert before == a[0] and r >= n + state[r] = None + else: + assert op in {"ADD","COPY","SCALE"} and before == a[-1] + if op != "SCALE": + assert r != a[0] and state[a[0]] == before + if op == "COPY": + copies.append(t) + assert state == word["final"] + [None] * word["owned_fields"] + assert set(ranks) == set(by_cut) and all(t < min(by_cut) for t in copies) + return ranks, copies + + +def pair(left, right, pivot, dot, engine): + local = [[dot(a,b) for b,_ in right] for a,_ in left] + end = [[c.get(pivot,0)*d.get(pivot,0) for _,d in right] for _,c in left] + first = next(((i,j) for i,row in enumerate(end) for j,v in enumerate(row) if v), None) + if first is None: + return local,end,"absent pure suffix direction",None + i,j = first + q = local[i][j] / end[i][j] + proportional = all(v == q*x for a,b in zip(local,end,strict=True) for v,x in zip(a,b,strict=True)) + possible = not proportional or q == 1 + defect = [[a-b for a,b in zip(x,y,strict=True)] for x,y in zip(local,end,strict=True)] + wedge, dr, sr = engine(local,defect) + assert possible == (wedge or dr != sr) + return local,end,"unit pairing survivor" if possible else "no unit pairing",str(q) if proportional else None + + +def main(): + assert __debug__ + data = {path:checked(path) for path in PINS} + frozen = loads(data["preflight/FROZEN.json"],object_pairs_hook=unique) + old = loads(data["inputs/OLD-WITNESS.json"],object_pairs_hook=unique) + assert not frozen["literal_decode"] and frozen["case_count"] == len(frozen["cases"]) == 14 + assert Q(frozen["complete_one_probe"][0])>0 and Q(frozen["complete_two_target"][1])<0 + helper = run_path(str(ROOT/"inputs/bank_trace.py")) + engine = run_path(str(ROOT/"inputs/paired_rank.py"))["pairing"] + dot = helper["dot"] + controls = helper["controls"](old) + toy = [({1:Q(1)},{0:Q(1)})] + assert pair(toy,toy,0,dot,engine)[2] == "unit pairing survivor" + assert pair(toy,[({2:Q(1)},{0:Q(1)})],0,dot,engine)[2] == "no unit pairing" + raw = decompress(data["inputs/7334-WORD.json.gz"]) + assert sha256(raw).hexdigest()==PAYLOAD + word = loads(raw,object_pairs_hook=unique) + assert len(word["program"])==76466 + deadline = monotonic()+23 + ranks,copies = topology(word,frozen["cases"]) + rows = [] + for case in frozen["cases"]: + if monotonic()>=deadline: + break + cut,chart,*_ = case["key"] + pivot, = case["pivots"] + bank = case["public"] + try: + fp,left = helper["kernel"](helper["trace"](word,cut,bank,deadline,True),{pivot}) + sp,right,local,end,q = None,[],[],[],None + decision = "absent pure prefix direction" + if any(c for _,c in left): + sp,right = helper["kernel"](helper["trace"](word,cut,bank,deadline,False),{pivot}) + local,end,decision,q = pair(left,right,pivot,dot,engine) + except TimeoutError: + break + def matrix(m): + return [[str(v) for v in r] for r in m] + def basis(value): + return [[helper["printed"](a),helper["printed"](c)] for a,c in value] + rows.append(dict(key=case["key"],pivot=pivot,bank=bank,child_ranks=ranks[cut], + prefix_exterior_rank=fp,suffix_exterior_rank=sp,pure_prefix=basis(left),pure_suffix=basis(right), + local=matrix(local),endpoint=matrix(end),proportional_ratio=q,disposition=decision)) + pending = [x["key"] for x in frozen["cases"][len(rows):]] + print(dumps(dict(head=frozen["head"],caller=frozen["caller"],pins=PINS,controls=controls, + old_copy_clocks=copies,case_cap=14,runner_seconds_cap=25,tested=rows,unvisited=pending, + survivors=[x["key"] for x in rows if x["disposition"]=="unit pairing survivor"]), + indent=2,sort_keys=True)) + if pending: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-five-singleton-prefix-bound/preflight/freeze.py b/research/p104-rank-five-singleton-prefix-bound/preflight/freeze.py new file mode 100644 index 0000000000..e8bbcdd807 --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/preflight/freeze.py @@ -0,0 +1,132 @@ +"""Price and bind only the two singleton residual endpoint groups, no word decode.""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +PINS = { + "inputs/PR7370-SHA256.json": "ea5a3157a967c01b94fd57ca26f8ace1bfa2c6e8165271af917846eb14f9c0d9", + "inputs/R115-PRICE.json": "c04adfb199f6dbc25806d6062562c7d707b8fda8ad73f3ed818901248d25ffbf", + "inputs/R115-GEOMETRY.json": "c2a4406cf7130a819189e8ceefb4bb6e09edd392eb56820f9fcadb0e9415ef4e", + "inputs/PR7375-SHA256.json": "fd334987adac93393bab7578815ec8f9a9cb16ce8dce9b6620613efddde3203d", + "inputs/PR7375-SELECTION.json": "910c8881f31721793cb8e8cbf3b3b3789a9986415e0d48dd9c97d146d5b37bcc", + "inputs/PR7375-PRIMARY.json": "d00281b59d994fb96e3f60cedc5c6b3b6277a7d050e8ac7bd6b4a24724219669", + "inputs/PR7375-SECOND.json": "96bdb7a70d247a198a6777fe10e30ce51f7b2e90d4a81f9bf7fea0515f9c1ad0", + "inputs/7334-READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "inputs/CHART118-CONTROL.json": "5be60a09485041744919696121ae27e57a1aa9de437a2c4494d5fc569af4cdb4", +} +GROUPS = {(712, 127): 1360, (714, 127): 1361} +EXPECTED = { + (712, 127): [(39267, 859), (39268, 859), (41551, 859), (41552, 859), + (41827, 987), (41828, 987), (41829, 987)], + (714, 127): [(41599, 875), (41600, 875), (41606, 875), (41607, 875), + (42113, 1001), (42114, 1001), (42115, 1001)], +} + + +def unique(items): + result = dict(items) + if len(result) != len(items): + raise ValueError("duplicate receipt key") + return result + + +def authenticated(path): + raw = (ROOT / path).read_bytes() + if sha256(raw).hexdigest() != PINS[path]: + raise ValueError(f"changed dependency {path}") + return loads(raw, object_pairs_hook=unique) if path.endswith(".json") else raw + + +def text(values): + return list(map(str, values)) + + +def main(): + assert __debug__ + docs = {path: authenticated(path) for path in PINS} + def get(name): + return docs[f"inputs/{name}.json"] + a, b = get("PR7370-SHA256"), get("PR7375-SHA256") + for name in ("R115-PRICE.json", "R115-GEOMETRY.json"): + assert a[name] == PINS[f"inputs/{name}"] + for name in ("SELECTION.json", "PRIMARY.json", "SECOND.json"): + assert b[name] == PINS[f"inputs/PR7375-{name}"] + price, geom, old = get("R115-PRICE"), get("R115-GEOMETRY"), get("7334-READBACK") + selection, primary, second = (get(f"PR7375-{s}") for s in ("SELECTION", "PRIMARY", "SECOND")) + assert all(item["head"] == HEAD for item in (price,geom,old,selection,primary,second)) + assert price["caller"] == selection["caller"] == old["caller_head"] == CALLER + assert geom["status"] == "EXHAUSTED" and not geom["timeout"] and geom["visited_events"] == 76466 + assert geom["selected_group"] == [3,241] and len(geom["candidate_rows"]) == 68 + assert selection["selected_group"] == [3,233] and len(selection["selected"]) == 17 + assert primary["counts"] == {"prefix exclusion": 17} + assert len(second["rows"]) == 17 + groups = {tuple(row["endpoints"]): row for row in geom["groups"]} + cases = [] + for endpoints, pivot in GROUPS.items(): + group = groups[endpoints] + assert group["roles"] == [pivot] and group["banks"] == 7 + rows = [r for r in geom["candidate_rows"] if tuple(r["key"][2:]) == endpoints] + assert [tuple(r["key"][:2]) for r in rows] == EXPECTED[endpoints] + for row in rows: + assert row["pivots"] == [pivot] and not row["owned"] + assert row["key"][1] in group["labels"] and pivot in row["public"] + assert len(row["public"]) in (2,3) + cases.append(row | {"productive_parent_rank":5,"productive_child_ranks_sorted":[2,3]}) + assert sorted(row["key"] for row in cases) == sorted(selection["unselected"]) + assert len(cases) == len({tuple(r["key"]) for r in cases}) == 14 + + earlier = get("CHART118-CONTROL") + vectors = {k:{r:Q(v) for r,v in earlier[k].items()} for k in "abcd"} + def dot(u, v): + return sum(value*v.get(r,0) for r,value in u.items()) + assert dot(vectors["a"],vectors["b"]) == dot(vectors["c"],vectors["d"]) == 1 + assert old["copies"] == 17 and old["empty_root_credits"] == 0 + paid = Counter({int(r):n for r,n in old["paid"].items()}) + targets = Counter({int(r):n for r,n in old["targets"].items()}) + net = targets.copy() + net.subtract(paid) + assert (sum(paid.values()),sum(targets.values()),sum(r*n for r,n in net.items())) == (110519,22461,1424) + delta = Counter({2:17,3:17,5:-17}) + assert price["productive_delta"] == {str(r):n for r,n in delta.items()} and price["paid_delta"] == {} + lo, hi = map(Q,old["new_raw_interval"]) + probe = Q(price["probe"]) + assert probe == hi+Q(1,10**9) + target, bit = Q(price["moonshot"]),Q(old["bit_premise"]) + cost = run_path(str(ROOT/"inputs/pricing.py"))["cost"] + one, two, extra = net.copy(), net.copy(), net.copy() + one.update(delta) + two.update({r:2*n for r,n in delta.items()}) + extra.update(delta) + extra[1] -= 1 + gross = cost(delta,hi) + assert text(gross) == price["at_incumbent"]["gross_one"] + assert cost(one,probe)[0] > 0 and cost(two,target)[1] < 0 and cost(extra,lo)[1] < 0 + print(dumps({ + "head":HEAD,"caller":CALLER,"pins":PINS,"word_sha256":price["word_sha256"], + "sources":{"#7370":"a41edc3ae92332a7a1f1ba90e9ea4901d0530185", + "#7375":"2bf6a806bac491c69182ce366230c1fa7a646fec"}, + "cases":cases,"cohorts":[{"endpoints":list(e),"pivot":p} for e,p in GROUPS.items()], + "case_count":14,"max_distinct_compatible_edits":2,"paid_delta":{}, + "productive_delta_per_edit":delta,"complete_paid":110519, + "complete_productive_old":22461,"complete_productive_one":22478,"complete_productive_two":22495, + "rank_surplus":1424,"empty_root_credits":0, + "old_crossing":text((lo,hi)),"higher_probe":str(probe),"fixed_target":str(target),"retained_BIT":str(bit), + "one_gross_at_old_upper":text(gross),"whole_gross_upper_at_old_upper":str(2*gross[1]), + "complete_one_probe":text(cost(one,probe)),"complete_two_probe":text(cost(two,probe)), + "complete_one_target":text(cost(one,target)),"complete_two_target":text(cost(two,target)), + "one_with_one_additional_rank_one_at_old_lower":text(cost(extra,lo)), + "control":"Historical chart118 pivot635: local and endpoint exact pairing both one", + "caps":{"initial_cases":14,"initial_seconds":25,"exact_followup_cases":4,"exact_followup_seconds":35}, + "literal_decode":False, + },indent=2,sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-five-singleton-prefix-bound/receipts/SHA256.json b/research/p104-rank-five-singleton-prefix-bound/receipts/SHA256.json new file mode 100644 index 0000000000..b1b1236710 --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/receipts/SHA256.json @@ -0,0 +1,6 @@ +{ + "AGREEMENT.json": "b3cd113640a35adcbb857e2f2d0da00a78d66282dc451b1c6390d093987221ff", + "FORWARD.json": "76f6d7b38943b457ad70942cacc530ce531ceec6e4defe6ef425cacb68bd409b", + "FROZEN.json": "3861fa02acfafd35f3c437397f8aecd282a21687d81e426e25e2289f21d54a4a", + "RATIONAL.json": "aa3e2a52214451c4bd99c231a3a30823a8017f53e5e9e2705ed884335c705a7a" +} diff --git a/research/p104-rank-five-singleton-prefix-bound/replay.py b/research/p104-rank-five-singleton-prefix-bound/replay.py new file mode 100644 index 0000000000..15e7a11fdd --- /dev/null +++ b/research/p104-rank-five-singleton-prefix-bound/replay.py @@ -0,0 +1,134 @@ +"""Git-free replay of the two exact residual rank-five endpoint cohorts.""" +from argparse import ArgumentParser +from hashlib import sha1, sha256 +from json import loads +from pathlib import Path, PurePosixPath +from runpy import run_path +from shutil import copyfile +from subprocess import run +import sys +from tempfile import TemporaryDirectory + +ROOT = Path(__file__).resolve().parent +STAGES = ( + ("preflight/freeze.py", "preflight/FROZEN.json", "FROZEN.json"), + ("lead/pairs.py", "lead/RESULT.json", "RATIONAL.json"), + ("independent/singleton.py", "independent/RESULT.json", "FORWARD.json"), + ("independent/compare.py", "independent/AGREEMENT.json", "AGREEMENT.json"), +) + + +def unique(rows): + result = dict(rows) + if len(result) != len(rows): + raise ValueError("duplicate package key") + return result + + +def read_json(path): + return loads(path.read_bytes(), object_pairs_hook=unique) + + +def digest(raw): + return sha256(raw).hexdigest() + + +def relative(name): + path = PurePosixPath(name) + if path.is_absolute() or path.as_posix() != name or ".." in path.parts: + raise ValueError(f"invalid relative path {name}") + return path + + +def authenticate(): + pins = read_json(ROOT / "LOCAL-PINS.json") + for name, expected in pins.items(): + data = (ROOT / relative(name)).read_bytes() + if digest(data) != expected: + raise ValueError(f"changed package dependency {name}") + prov = read_json(ROOT / "PROVENANCE.json") + for name, source in prov["files"].items(): + data = (ROOT / relative(name)).read_bytes() + assert digest(data) == pins[name] == source["sha256"] + if "git_blob" in source: + assert sha1(f"blob {len(data)}\0".encode()+data).hexdigest() == source["git_blob"] + for name, source in prov["regenerated_predecessor_receipts"].items(): + manifest = read_json(ROOT / relative(source["manifest"])) + assert manifest[source["receipt"]] == pins[name] + control = prov["historical_control"] + assert pins[control["path"]] == control["sha256"] + return pins + + +def command(root, script): + return run([sys.executable, "-I", "-B", str(root/script)], cwd=root, + capture_output=True, timeout=35) + + +def reject(root, path, script): + target = root/path + original = target.read_bytes() + try: + target.write_bytes(original+b"\n") + proc = command(root,script) + assert proc.returncode == 1 and not proc.stdout + assert b"changed dependency" in proc.stderr and target.name.encode() in proc.stderr + finally: + target.write_bytes(original) + + +def replay(root): + pins = authenticate() + expected = read_json(ROOT/"receipts/SHA256.json") + assert set(expected) == {name for _,_,name in STAGES} + for name in pins: + if not name.startswith(("inputs/","preflight/","lead/","independent/")): + continue + target = root/relative(name) + target.parent.mkdir(parents=True, exist_ok=True) + copyfile(ROOT/name,target) + for name in run_path(str(root/"preflight/freeze.py"))["PINS"]: + local = root/"preflight"/relative(name) + local.parent.mkdir(parents=True, exist_ok=True) + source = "inputs/OLD-WITNESS.json" if name == "inputs/CHART118-CONTROL.json" else name + copyfile(root/source,local) + outputs = {} + for script, path, name in STAGES: + result = command(root,script) + if result.returncode: + sys.stderr.write(result.stderr.decode(errors="replace")) + result.check_returncode() + assert not result.stderr and digest(result.stdout) == expected[name], ("changed receipt",name) + (root/path).write_bytes(result.stdout) + outputs[name] = result.stdout + frozen = read_json(root/"preflight/FROZEN.json") + agreement = read_json(root/"independent/AGREEMENT.json") + assert frozen["case_count"] == agreement["case_agreements"] == 14 + assert agreement["suffix_required"] == agreement["unresolved"] == 0 + for target, script in [ + ("preflight/inputs/PR7375-SECOND.json","preflight/freeze.py"), + ("preflight/FROZEN.json","independent/singleton.py"), + ("inputs/7334-WORD.json.gz","lead/pairs.py"), + ]: + reject(root,target,script) + return outputs + + +def main(): + parser = ArgumentParser() + parser.add_argument("--out",type=Path,help="write the four regenerated receipts to a fresh directory") + args = parser.parse_args() + assert __debug__ and sys.version_info[:2] == (3,12) + with TemporaryDirectory(prefix="rank-five-pairing-") as directory: + outputs = replay(Path(directory)) + if args.out: + args.out.mkdir(parents=True,exist_ok=True) + if any(args.out.iterdir()): + raise ValueError("receipt output directory must be empty") + for name, raw in outputs.items(): + (args.out/name).write_bytes(raw) + print("PASS_RANK_FIVE_SINGLETON_RESIDUAL 14 exact prefixes excluded; 0 unresolved; 3 mutation controls") + + +if __name__ == "__main__": + main()