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-eight-fixed-paid-bank-bound/LOCAL-PINS.json b/research/p104-rank-eight-fixed-paid-bank-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..100bd9cd63 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/LOCAL-PINS.json @@ -0,0 +1,41 @@ +{ + "NOTICE": "a103976d6f63f7798580cce5481d60705e0753f97b1d064fe57717d5b4f6441a", + "PROOF.md": "888a80e6f8dc0c2a875cde9940d5a1868d79749007929eebf223da5d09855dcc", + "PROVENANCE.json": "0a5f5f67afa6c5e5c9344d75be12a7ae5b2acc689be231bb34ddf21889c80940", + "README.md": "bfa676bb1d4d67270a1291b0c4a786fa3729a700a354b67c516831af468c5053", + "SOURCES.json": "5ae4cfc96aa890b1b06aa0de688e03d9713b2772fb0f9c6ae7e23ad7d49c479d", + "TASK.json": "8198b4a9f5618a1d2fda2e40e40d67fd197dde3e5700a7caaf4245936b1ec756", + "VERIFICATION.md": "cad30fe3215974566d34a96051b46a4e8644e803488b31c3aee7135a4bbfe8cd", + "VERIFY.json": "2d16f628bbde19c72e3a869d10a2d918021023d49d7a0e7e57b9ddc489b9c9ad", + "engines/r96/continue_modular.py": "02a1694b25e64815462d8c98ca0ea670ea67544ae5bcf4e6d728cd3d53635dd3", + "engines/r96/exact_four.py": "aa0155d61b9861a49d228fcc241dcf073f2ed0f2ae1e3ae898524c9b58ddcb0f", + "engines/r96/freeze_remaining.py": "8754dfcca9e089b0a6eb2935428bf95d65483f14b4fcf96cccb876e51abd751b", + "engines/r96/geometry.py": "3d7e6935053b910022072dadd6085fc6b68534b792085d5a8ddcd2bdc32b75e7", + "engines/r96/prefix.py": "3bfc69f588d1d9edfb7c172980570545d52463ae4942fb78490e6f5d167716c3", + "engines/r96/select.py": "f356d31d330bd9b17e5ed8a4186432cce2025a79d42afb267d91416c52502fa8", + "engines/r96/suffix.py": "eb0216f7c4188abb7dcfa30829e24e34c03cc58671c49b8810981a52f86cdffa", + "engines/r97/freeze.py": "a56c0ee8b830838a67b3a11f77f614e5d78f2181750adaa830b1719337895812", + "engines/r97/modular_compare.py": "70097a64b158489eac7a9fd0a82bb482a9eba8e57f2280dbb45c3d1fa9a8f607", + "engines/r97/second_prime.py": "21dbd96192e1f60c00ceddba01a7e8d0ddd7d6ad7da4ad3ed22ef2e47cc589c4", + "engines/rational/exact_six.py": "5bffcbbbdc5b0622e29fbc778540cc240b41e7d252e3e5c68d708d48808fcb5a", + "engines/rational/r96_compare.py": "2c30156846f73b383786fb9966f06b4b8b06aaaabb8a0cc9ab6c30439b82b281", + "engines/rational/r96_independent.py": "0bbf9d1ea0957de30dbe9f7afa4a6fb86236b2910127f1af2722cab6b597ab26", + "engines/rational/r96_pairing_obstruction.py": "aa321146f36814ba7b45904387577aa4de06e18df952866a191d60d41cd77865", + "engines/rational/r97_independent.py": "7762b236d62fe7dd9a3ab89b81ede93f4101ae9254ea72d1226409a75632fcc6", + "engines/rational/rolling_exterior.py": "ffc6dfa01554974f2b913b65c39230d3a7f7b6c06da1c940617b7938afe2b9c7", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/exterior_minor.py": "b25fef5432d8ea9cff9eecc422cf07ccf7473568084de3e8d3d1b5224793504d", + "inputs/paired_rank.py": "d1b7c34e6f8c8a7b810414762015e6e300a8292422af66ff671ae09741141f09", + "inputs/paired_support.py": "38c796cbe1a73f386177faf88cd53294d4b911f6cde7fd47cd9fcef3b558373f", + "inputs/reverse_engine.py": "751d5d0c4c665c8768ff69bcf939700d3be2f989c59f09af3a4aa14d3c1ebbc4", + "price/inputs/7314-HELPERS.json.gz": "e817ac36ffd85b5b8ad7320daf57bedfa5692b4a0f2990570008afe4888bca6d", + "price/inputs/7334-CHANGED.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "price/inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "price/inputs/PR7319-SHA256.json": "ca3ed296a19bdd7b2b37608e93d1763d97c7620ac9faef732a01bae4f485114c", + "price/inputs/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "price/inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "price/quote.py": "7767925228e4c3bec74071eac7fe2cf47695a6f4ffbd5f6dd934457f39af32a6", + "receipts/SHA256.json": "91aa157df8168be25cfda9acdeea45e097e17d4047e7b37c935061e5a2a44f47", + "receipts/UNRESOLVED.json": "90bad1091b3008cedcbf02d3ad91de1879faee5784ae2771ea54cdab199434dc", + "replay.py": "fa44267689a4d07f9a72db2427aa08c30687ed9f6cb8265593fd5ba2f59ffd32" +} diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/NOTICE b/research/p104-rank-eight-fixed-paid-bank-bound/NOTICE new file mode 100644 index 0000000000..789e1f8cb9 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/NOTICE @@ -0,0 +1,7 @@ +Apache-2.0. + +#7334 and #7113 supply the pinned word and signed caller. #7298 and #7338 supply +directed pricing and admitted accounting. #7314 and #7319 supply the inherited +census. #5599, #7121, #7244, #7274, #7339, #7353 and #7359 are relevant +construction and support precedents. OpenAI Codex and subagents materially +assisted proof, implementation, independent replay and packaging. diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/PROOF.md b/research/p104-rank-eight-fixed-paid-bank-bound/PROOF.md new file mode 100644 index 0000000000..62a95de824 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/PROOF.md @@ -0,0 +1,35 @@ +# Exact scope and necessary conditions + +Let C be the 15-element cohort of unchanged public helpers with endpoints chart 3 and chart 245 and original productive rank eight. The cohort comes from the exact inherited #7314 census after omitting the changed #7334 roles and protected roles. Both endpoint charts, every paid event, the signed #7113 caller and every other target stay fixed. The proposed edit splits one productive target into two rank-four targets using a single basis coordinate in a public bank on an existing chart V with strict GF(2) inclusion `chart 3 < V < chart 245` and absolute rank four. At least one original public bank role belongs to C. + +The chronological walk tests the initial bank where applicable and records a representative after every incident event that leaves a productive pivot present. ADD and COPY are cocharted. MOVE is incident to both its old and new charts. INIT and CLEAR are incident to the associated chart. An event away from a given chart keeps that bank's occupancy and normalized scalar prefix and suffix maps fixed. The result counts the 326 frozen incident-event representatives, without treating signed physical materialization at distinct clocks as equivalent. + +At a pre-event cut, let P be the normalized prefix map from all public inputs to the public bank, and S the suffix map from that bank to all public outputs. The retained single-coordinate factorization chooses a cut row a and a column b of the inverse basis. Their product must satisfy `a·b = 1`. Their endpoint images `c = aP` and `d = Sb` must be nonzero, have no support outside C, and pair to one under the endpoint basis and inverse basis. Thus the necessary equations are + +```text +supp(aP) ⊆ C, supp(Sb) ⊆ C +c = aP, d = Sb +a·b = c·d = 1. +``` + +The replay exposes all public coordinates, even those outside C. Live owned roles are tracked and follow the unchanged literal word. They are never variables of a public bank coefficient vector. + +## Exterior minors + +Deleting coordinates in C from a prefix row gives the exterior map whose coefficient kernel contains every candidate a. The same applies to b using the suffix columns. Each input scalar denominator is a unit at the relevant prime. Rational MOVE normalization, scaled additions and the owned field lifecycle commute with reduction. A nonzero minor of order equal to the public bank size proves full exterior rank over the rationals. That side has zero coefficient kernel, so the bank cannot have a unit pair. A modular rank drop contributes no rational exclusion. + +The first 16 representatives yield nine prefix and one suffix exterior exclusions. The complementary 310 yield 279 more prefix exclusions. The two continuation engines reconstruct all 310 banks with different trace directions and check their rank and disposition independently modulo 65521 and 65537. + +## Exact pairing + +The exact continuations construct both exterior kernels and their productive images over the rationals. The primary and independent rational engines use different replay directions and reduction routines. On seven chart-242 cuts both coefficient kernels are lines with nonzero productive images. The independent receipt gives signed generators and exact bilinear forms. Their cut and endpoint pairings are zero, and rescaling the lines preserves zero. On cut 45675 at chart 1091 the prefix coefficient kernel is a line whose productive image is the zero vector. A nonzero productive prefix therefore cannot be formed from that public bank. The two original owned fields are recorded and held fixed. + +Of the 326 frozen representatives, the modular exclusions and eight rational exclusions are disjoint. The remaining 29 are modular dual drops without a rational decision. + +## Directed price and comparability + +Across the 17 caller copies, one fixed-paid split would change the productive histogram by T4 +34 and T8 −17. The paid histogram and other target counts remain fixed. The exact #7334 complete invoice has 110,519 paid positions, 22,461 productive positions and signed rank surplus 1,424. The hypothetical split preserves that rank surplus. + +The signed crossing of #7334 lies in the strict interval `(0.00364665195644044790699554028334161, 0.00364665195644044790699554028334162)`. At the certified upper endpoint the one-edit directed gross upper is about 0.3415972937126856 raw. The exact price replay gives a positive complete margin at the frozen incumbent-plus-`10^-9` probe for the hypothetical zero-overhead edit. A raw paid rank-one position costs one and consumes that one-edit margin. The optimistic whole-cohort upper grants 15 compatible edits and all ancillary work free, giving 5.123959405690284 raw at the incumbent. The complete margin upper at the fixed moonshot κ = 0.0040075385047236 is below −134.1394 raw. No priced edit has been physically constructed. + +The comparator retains `native_all_columns`, `owned_erasure`, `compiler`, `precision_tape` and `analytic_recovery`. This package reuses the admitted comparator receipt. It does not replace its full native or outer replay. The selected certificate is unchanged. diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/PROVENANCE.json b/research/p104-rank-eight-fixed-paid-bank-bound/PROVENANCE.json new file mode 100644 index 0000000000..99d08ce63a --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/PROVENANCE.json @@ -0,0 +1,61 @@ +{ + "derived_inputs": { + "price/inputs/7314-HELPERS.json.gz": { + "compression": "gzip", + "keys": [ + "REVERSE.json" + ], + "receipt": "price/inputs/PR7319-SHA256.json" + }, + "price/inputs/7334-CHANGED.json": { + "keys": [ + "receipt", + "peer-prep/IDENTITIES.json" + ], + "receipt": "price/inputs/ADMITTED.json" + } + }, + "files": { + "inputs/7334-WORD.json.gz": { + "commit": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "git_blob": "73f43007192eb5a38eb5abb591b871df3e52c7cd", + "path": "research/p104-helper-319-fused-return/WORD.json.gz", + "sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "source": "https://github.com/Clear1nsight/integer-mult-bounds/blob/aaeec8c0acf01e99a5f331ef363a698d9c084ace/research/p104-helper-319-fused-return/WORD.json.gz", + "uncompress": false + }, + "price/inputs/ADMITTED.json": { + "commit": "349996445176e934ffb3c76813adcd230ca8f783", + "git_blob": "464c89e45c4eca230c099e8bac784a90200a5069", + "path": "research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "sha256": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/349996445176e934ffb3c76813adcd230ca8f783/research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "uncompress": false + }, + "price/inputs/PR7319-SHA256.json": { + "commit": "b2d3bc4dd584f8d3aacd244505b12286db4d4875", + "git_blob": "3a28905e8d69888617b56578761c16d39fcdf7a6", + "path": "research/p104-helper-entrance-first-contact-bound/receipts/SHA256.json", + "sha256": "ca3ed296a19bdd7b2b37608e93d1763d97c7620ac9faef732a01bae4f485114c", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/b2d3bc4dd584f8d3aacd244505b12286db4d4875/research/p104-helper-entrance-first-contact-bound/receipts/SHA256.json", + "uncompress": false + }, + "price/inputs/READBACK.json": { + "commit": "349996445176e934ffb3c76813adcd230ca8f783", + "git_blob": "625b508eead24b4428253bd257620b7e775800c1", + "path": "research/p104-compensated-fusion-readout-bound/price/READBACK.json", + "sha256": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/349996445176e934ffb3c76813adcd230ca8f783/research/p104-compensated-fusion-readout-bound/price/READBACK.json", + "uncompress": false + }, + "price/inputs/pricing.py": { + "commit": "c522451caf287bb3c16eaece72be4c263315dca4", + "git_blob": "40ec194017bda1d524bba4f07b188c53281419d0", + "path": "research/adjacent-owned-add-exchange-bound/pricing.py", + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/c522451caf287bb3c16eaece72be4c263315dca4/research/adjacent-owned-add-exchange-bound/pricing.py", + "uncompress": false + } + }, + "schema_version": 1 +} diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/README.md b/research/p104-rank-eight-fixed-paid-bank-bound/README.md new file mode 100644 index 0000000000..390a8b75e5 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/README.md @@ -0,0 +1,36 @@ +# Fixed-paid rank-eight chart-245 bank bound + +**NO VERIFIED GAIN.** This package excludes 297 of 326 frozen public cochart bank representatives for one productive rank-eight 4+4 split. It preserves the 29 unresolved bank keys for exact continuation. The comparator is conditional κ = 0.00364665195644 from exact [#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334), head `aaeec8c0acf01e99a5f331ef363a698d9c084ace`. Δκ = 0 and the relative gain is exactly 0%. + +The literal native word and [#7113 signed caller](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) stay fixed. The productive target is one of the 15 unprotected rank-eight helpers with endpoints chart 3→245. The cut uses an existing rank-four cochart bank on chart 242, 772 or 1091. The bank may use exterior public axes. The productive prefix and suffix images must stay in the fixed 15-role cohort. Original owned fields keep their operations and remain outside the public basis. + +| Screen | Tested | Excluded | Result | +| --- | ---: | ---: | --- | +| Initial modular prefix and suffix | 16 | 10 | Nine full exterior prefix ranks, one full exterior suffix rank | +| First exact pairing continuation | 4 | 4 | Both pure lines exist and their generator pairing vanishes at cut and endpoint | +| Remaining modular representatives | 310 | 279 | Full exterior prefix ranks verified independently modulo 65521 and 65537 | +| Second exact pairing continuation | 4 | 4 | Three zero pairings and one zero productive prefix image | + +The second rational continuation tests two inherited drops and two new drops, all distinct from the initial rational cases. The eight exact dispositions agree between independent engines. The one zero-image case has a nonzero exterior-kernel line at chart 1091 with two unchanged owned occupants. The seven other exact cases are on chart 242. See the [exact argument and paid invoice](PROOF.md) and [verification receipts](VERIFICATION.md). + +## Reproduce + +Use CPython 3.12 with assertions enabled and the standard library. From the package directory in a clean checkout or Git-free export: + +```sh +python3.12 -I -B replay.py +``` + +To inspect the exact sparse domain matrices, pairing forms and minors, run `python3.12 -I -B replay.py --output replayed`. This materializes the [17 path-keyed receipts](receipts/SHA256.json). All inputs travel with the package. [Source provenance](PROVENANCE.json) + +## Open next questions + +Start with the [29 exact keys](receipts/UNRESOLVED.json). Freeze at most four, favoring distinct chart and bank shapes, and reconstruct both rational exterior kernels and the signed pairing. A nonzero rational unit pair still requires a legal signed basis change, the arbitrary-input forward and adjoint identities, restoration, the complete paid and ordinary invoice, precision and tape, and a full independent replay. One new paid rank-one position would erase the favorable one-edit directed price. + +The result covers the frozen single-pivot, fixed public bank contract. Other chart labels, changes to paid paths, a basis using owned fields, wider cohorts and interacting edits are open as different scopes. + +## Credit + +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) supplies the literal paid word and comparable complete witness. [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) supplies the signed caller. [#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) and [#7338](https://github.com/CrocSwap/integer-mult-bounds/pull/7338) supply the directed pricing and independently admitted invoice. [#7314](https://github.com/CrocSwap/integer-mult-bounds/pull/7314) and [#7319](https://github.com/CrocSwap/integer-mult-bounds/pull/7319) supply the inherited helper census and exact cohort source. + +[#5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599) supplies the paired cochart split. [#7121](https://github.com/CrocSwap/integer-mult-bounds/pull/7121) supplies a rank-eight split in a different cohort. [#7244](https://github.com/CrocSwap/integer-mult-bounds/pull/7244) and [#7274](https://github.com/CrocSwap/integer-mult-bounds/pull/7274) use chart 245 with older paid-path changes. [#7339](https://github.com/CrocSwap/integer-mult-bounds/pull/7339), [#7353](https://github.com/CrocSwap/integer-mult-bounds/pull/7353) and [#7359](https://github.com/CrocSwap/integer-mult-bounds/pull/7359) supply earlier exact support tests for rank-nine helpers. OpenAI Codex and subagents materially assisted the proof, implementation, independent replay and packaging. diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/SOURCES.json b/research/p104-rank-eight-fixed-paid-bank-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-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-eight-fixed-paid-bank-bound/TASK.json b/research/p104-rank-eight-fixed-paid-bank-bound/TASK.json new file mode 100644 index 0000000000..005cbe1ac4 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Exact #7334 fixed-paid 4+4 split on the 15 public chart-3 to chart-245 rank-eight helpers and 326 frozen incident-event bank representatives.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "P104 rank-eight split research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "A fixed-paid 4+4 productive split improves the directed complex invoice only with legal signed cochart unit pairing and retained route, ownership, precision and tape.", + "budget_minutes": 25, + "evidence": "326 representatives across three strict rank-four intermediate charts. Exact evidence excludes 297 and leaves 29 unresolved. Two modular engines agree for every continuation key; two rational engines agree for both four-key selections.", + "open_questions": [ + { + "blocked_by": "A modular rank drop gives no rational result. Even a rational pair would require signed materialization, full cost accounting and complete independent replay.", + "first_step": "Pin at most four keys from receipts/UNRESOLVED.json, then compute both exact exterior kernels, images and pairing forms from the literal word.", + "question": "Does any of the remaining 29 exact bank keys admit a nonzero rational unit pair on its fixed public bank?", + "why_it_matters": "A legal single 4+4 split has positive directed price with the paid itinerary fixed." + } + ], + "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": "Uses the separate rank-eight chart-3 to chart-245 cohort with two bounded exact selections, distinct from earlier rank-nine and changed paid path scopes.", + "scope_status": "changed", + "stop_rule": "Sweep at most 76,466 literal events, screen the first frozen 16 and then the complementary 310, and replay only the two exact four-key selections with a 35-second cap per round.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/VERIFICATION.md b/research/p104-rank-eight-fixed-paid-bank-bound/VERIFICATION.md new file mode 100644 index 0000000000..8c6f984165 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/VERIFICATION.md @@ -0,0 +1,9 @@ +# Verification + +The direct replay passed on CPython 3.12 with assertions, using only the standard library. It rebuilds the exact preprice and literal geometry, regenerates 17 path-keyed receipts byte-for-byte, compares both modular and both rational engines, and checks that the exclusion and unresolved sets partition the 326 frozen keys. The [receipt manifest](receipts/SHA256.json) and [remaining keys](receipts/UNRESOLVED.json) are compact. Pass `--output` to retain every regenerated result, including the exact signed sparse matrices, kernel generators and pairing forms. + +Round 96 screened its first 16 representatives and four rational drops. Round 97's 310-case primary and independent modular stages each exhausted their scope under 25 seconds, taking 1.56 and 1.86 seconds. The four exact keys in the Round 97 primary took 4.97 seconds. The independent two batches took 0.14 and 0.13 seconds and shared the four-key cap. No exact-selected key remains unresolved. The other 29 dual drops have no rational disposition. + +The wrapper runs a signed owned COPY/CLEAR control, a determinant sign control, a planted rank-drop control, a nonunit denominator control and positive and negative exact pairing controls. It rejects altered selection, remaining-key and word bytes. Each negative control requires exit code 1 and no result receipt. + +The comparator's four independent local stages are recorded in [the exact admission](https://github.com/CrocSwap/integer-mult-bounds/blob/349996445176e934ffb3c76813adcd230ca8f783/research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json). Its [exact-head hosted replay](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/43114736518) passed. The contribution itself uses the registered focused replay. No changed signed supplier or complete outer replay was run because the exact support stage produced no admissible candidate. diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/VERIFY.json b/research/p104-rank-eight-fixed-paid-bank-bound/VERIFY.json new file mode 100644 index 0000000000..dae3635dc2 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Regenerate exact price, 326-bank geometry, 17 pinned receipts, modular and rational agreements, and unresolved keys. Check rejection of corrupted selection, remaining list and native word.", + "timeout_seconds": 180 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/continue_modular.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/continue_modular.py new file mode 100644 index 0000000000..b2a4d18ca8 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/continue_modular.py @@ -0,0 +1,62 @@ +"""Check only the 310 banks outside the first R96 modular cap.""" +from collections import Counter +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path +import sys +from time import monotonic + +PINS = { + "price/PRICE.json": "a78be64c3e3ae8a0e532237c4dd3541aa9ad3fcbbc3c25d79c8a03fb7e07c525", + "lead/REMAINING.json": "3597499663a57702856945e91214a65e1d0f94db8643b93c0234c2bbf9291b1a", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/exterior_minor.py": "b25fef5432d8ea9cff9eecc422cf07ccf7473568084de3e8d3d1b5224793504d", + "inputs/reverse_engine.py": "751d5d0c4c665c8768ff69bcf939700d3be2f989c59f09af3a4aa14d3c1ebbc4", +} + + +def main(): + assert __debug__ and sys.version_info[:2] == (3,12) + deadline = monotonic() + 22 + root = Path(sys.argv[1]) + inputs = {} + for name, expected in PINS.items(): + data = (root/name).read_bytes() + if sha256(data).hexdigest() != expected: + raise ValueError(f"changed dependency: {name}") + inputs[name] = data + engine = run_path(str(root/"inputs/exterior_minor.py")) + reverse = run_path(str(root/"inputs/reverse_engine.py")) + unique = engine["unique"] + price = json.loads(inputs["price/PRICE.json"],object_pairs_hook=unique) + previous = json.loads(inputs["lead/REMAINING.json"],object_pairs_hook=unique) + assert price["head"] == previous["head"] == engine["HEAD"] + keys = [tuple(k) for k in previous["unvisited_prefix"]] + assert len(keys) == len(set(keys)) == previous["next_modular_cases"] == 310 + assert not set(keys) & set(map(tuple,previous["dual_drops_requiring_rational"])) + word = json.loads(decompress(inputs["inputs/7334-WORD.json.gz"]),object_pairs_hook=unique) + cohort = set(price["cohort"]) + controls = reverse["controls"](engine) + prefix, visited_prefix = engine["sweep"](word,keys,cohort,deadline) + remaining = [prefix[key] for key in keys if key in prefix and prefix[key]["disposition"] == "rank drop"] + suffix, visited_suffix = reverse["sweep"](word,remaining,cohort,engine,deadline) + rows = [] + for key in keys: + p, s = prefix.get(key), suffix.get(key) + if p and p["disposition"] == "excluded": + status = "prefix_exclusion" + elif s: + status = "suffix_exclusion" if s["disposition"] == "excluded" else "dual_drop" + else: + status = "capped" + rows.append({"key":list(key),"prefix":p,"suffix":s,"status":status}) + print(json.dumps({"head":price["head"],"pins":PINS,"controls":controls,"case_cap":310, + "runner_seconds":25,"visited_prefix_events":visited_prefix,"visited_suffix_events":visited_suffix, + "counts":Counter(r["status"] for r in rows),"rows":rows, + "existing_exact_pending":previous["dual_drops_requiring_rational"]},indent=2,sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/exact_four.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/exact_four.py new file mode 100644 index 0000000000..0ddc369a26 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/exact_four.py @@ -0,0 +1,75 @@ +"""Rational two-sided pairing for the frozen six-bank continuation.""" +from collections import Counter +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path +import sys +from time import monotonic + +PINS = { + "lead/SELECTION.json": "b95765ffa0bd426b3dae781aaafc1c21e3b25bcebc71b71a3871824f9009fd5f", + "price/PRICE.json": "a78be64c3e3ae8a0e532237c4dd3541aa9ad3fcbbc3c25d79c8a03fb7e07c525", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/paired_rank.py": "d1b7c34e6f8c8a7b810414762015e6e300a8292422af66ff671ae09741141f09", + "inputs/paired_support.py": "38c796cbe1a73f386177faf88cd53294d4b911f6cde7fd47cd9fcef3b558373f", +} + + +def main(): + deadline = monotonic() + 32 + root = Path(sys.argv[1]) + raw = {} + for path, pin in PINS.items(): + value = (root/path).read_bytes() + if sha256(value).hexdigest() != pin: + raise ValueError(f"changed dependency: {path}") + raw[path] = value + select = json.loads(raw["lead/SELECTION.json"]) + price = json.loads(raw["price/PRICE.json"]) + word = json.loads(decompress(raw["inputs/7334-WORD.json.gz"])) + rank, solve = [run_path(str(root/"inputs"/x)) for x in ("paired_rank.py", "paired_support.py")] + cohort = set(price["cohort"]) + assert len(cohort) == 15 and all(word["initial"][r] == 3 and word["final"][r] == 245 for r in cohort) + controls = solve["controls"]() + banks = {r["key"][0]: r["public"] for r in select["selected"]} + assert len(banks) == 4 + prefix = rank["side"](word, banks, cohort, deadline, False) + open_banks = {t: banks[t] for t, rows in prefix.items() if any(c for _, c in rows)} + suffix = rank["side"](word, open_banks, cohort, deadline, True) if open_banks else {} + results, pending = [], [] + for row in select["selected"]: + t = row["key"][0] + if t not in prefix or (t in open_banks and t not in suffix): + pending.append(row["key"]) + continue + f = prefix[t] + record = {**row, "pure_prefix_dimension": len(f), + "nonzero_prefix_images": sum(bool(c) for _, c in f)} + if t not in open_banks: + results.append(record | dict(status="no nonzero pure prefix")) + continue + s = suffix[t] + record.update(pure_suffix_dimension=len(s), nonzero_suffix_images=sum(bool(d) for _, d in s)) + if not any(d for _, d in s): + results.append(record | dict(status="no nonzero pure suffix")) + continue + try: + pair = solve["paired"](f, s, deadline) + except solve["Capped"]: + pending.append(row["key"]) + continue + if pair is None: + results.append(record | dict(status="no unit pairing")) + continue + assert solve["dot"](pair["a"],pair["b"]) == solve["dot"](pair["c"],pair["d"]) == 1 + results.append(record | dict(status="exact paired support", + witness={k: {j: str(x) for j,x in v.items()} for k,v in pair.items()})) + print(json.dumps(dict(head=price["head"],pins=PINS,controls=controls,exact_cap=4,seconds_cap=32, + results=results,counts=Counter(r["status"] for r in results),selected_unresolved=pending, + unselected=select["unselected"]), indent=2,sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/freeze_remaining.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/freeze_remaining.py new file mode 100644 index 0000000000..190fd36df1 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/freeze_remaining.py @@ -0,0 +1,34 @@ +"""Identify unvisited rank-eight banks and the two unresolved dual drops.""" +from hashlib import sha256 +import json +from pathlib import Path +import sys + +PINS = { + "lead/GEOMETRY.json": "c6f9f018df8b58fcdf4f44356bd59bcac6d411b7845104ff4ad372ed4a95cfbd", + "lead/RESULT.json": "45b6c8992dcff04b7252dfec809fc64812b86f094531ed3964ff967408057ed2", + "lead/SUFFIX.json": "77d78eb692bf6d3f0433730b48dbf8a0178c3288eeca961f94b2aaa6683eb59a", + "lead/EXACT.json": "362a879401158678c8a30ea0dbd4f919a9a0e907db2d2247ce96ac8724f68b14", +} + +root = Path(sys.argv[1]) +receipts = {} +for name, digest in PINS.items(): + raw = (root/name).read_bytes() + if sha256(raw).hexdigest() != digest: + raise ValueError(f"changed receipt: {name}") + receipts[Path(name).stem] = json.loads(raw) +g, p, s, e = (receipts[k] for k in ("GEOMETRY","RESULT","SUFFIX","EXACT")) +assert g["eligible_bank_count"] == 326 and g["status"] == "EXHAUSTED" +assert p["counts"] == {"excluded":9,"rank drop":7} and not p["unvisited"] +assert s["counts"] == {"excluded":1,"rank drop":6} and not s["unvisited"] +assert e["counts"] == {"no unit pairing":4} and not e["selected_unresolved"] +exact = {tuple(r["key"]) for r in e["results"]} +unresolved = [r["key"] for r in s["rows"] if r["disposition"] == "rank drop" and tuple(r["key"]) not in exact] +unvisited = g["unvisited_keys"] +assert len(unvisited) == 310 and len(unresolved) == 2 +assert e["unselected"] == unresolved + unvisited +print(json.dumps({"head":g["head"],"input_sha256":PINS,"excluded":14, + "unresolved":312,"unvisited_prefix":unvisited,"dual_drops_requiring_rational":unresolved, + "next_modular_cases":310,"next_modular_runner_seconds":25, + "next_exact_cases":4,"next_exact_runner_seconds":35},indent=2,sort_keys=True)) diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/geometry.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/geometry.py new file mode 100644 index 0000000000..3050905547 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/geometry.py @@ -0,0 +1,112 @@ +"""Exact full-word occupied rank-four cochart bank census.""" +from collections import defaultdict +from gzip import decompress +from hashlib import sha256 +from pathlib import Path +from time import monotonic +import json +import sys + +PRICE="a78be64c3e3ae8a0e532237c4dd3541aa9ad3fcbbc3c25d79c8a03fb7e07c525" +WORD="4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" + + +def checked(path,pin): + b=path.read_bytes() + if sha256(b).hexdigest()!=pin: + raise ValueError(f"changed dependency: {path.name}") + return b + + +def span(frame): + result={0} + for v in frame: + assert v not in result + result|={w^v for w in result} + return result + + +def main(): + root=Path(sys.argv[1]) + price=json.loads(checked(root/"price/PRICE.json",PRICE)) + word=json.loads(decompress(checked(root/"inputs/7334-WORD.json.gz",WORD))) + assert price["word_sha256"]==WORD and price["support_cap"]==16 + n=word["public"] + cohort=set(price["cohort"]) + assert len(cohort)==15 and all(word["initial"][r]==3 and word["final"][r]==245 for r in cohort) + spaces=list(map(span,word["frames"])) + intermediate={i for i,w in enumerate(spaces) if len(w)==16 and spaces[3]=n),pivots=sorted(pivots))) + for c in sorted(bank): + save(0,c) + until=monotonic()+18 + visited=0 + for t,e in enumerate(word["program"]): + if t%128==0 and monotonic()>=until: + break + op,r,*args=e + old=chart[r] + if op=="MOVE": + assert old==args[0] and args[2]==(r>=n) + new=args[1] + elif op=="INIT": + assert old is None and r>=n + new=args[0] + elif op=="CLEAR": + assert old==args[0] and r>=n + new=None + else: + assert old==args[-1] and op in ("ADD","COPY","SCALE") + if op in ("ADD","COPY"): + assert chart[args[0]]==old + new=old + if old in intermediate: + bank[old].remove(r) + if new in intermediate: + bank[new].add(r) + chart[r]=new + for c in sorted({v for v in (old,new) if v in intermediate}): + save(t+1,c) + visited=t+1 + complete=visited==len(word["program"]) + if complete: + assert chart==word["final"]+[None]*word["owned_fields"] + def score(r): + return (bool(r["owned"]),len(r["pivots"])<2,len(r["public"])-len(r["pivots"]), + len(r["public"]),r["key"]) + selected=[] + bank_shapes=set() + selected_clocks=set() + if complete: + for row in sorted(rows,key=score): + shape=row["key"][1],tuple(row["public"]),tuple(row["owned"]) + if shape in bank_shapes or row['key'][0] in selected_clocks: + continue + bank_shapes.add(shape) + selected_clocks.add(row['key'][0]) + selected.append(row) + if len(selected)==16: + break + assert len({tuple(row["key"]) for row in rows})==len(rows) + picked={tuple(r["key"]) for r in selected} + print(json.dumps(dict(head=price["head"],word_sha256=WORD,price_sha256=PRICE,visited_events=visited, + status="EXHAUSTED" if complete else "CAPPED",ranks=[4],bank_cap=16, + eligible_bank_count=len(rows),eligible_chart_count=len({r["key"][1] for r in rows}), + selected=selected,unvisited_keys=[r["key"] for r in rows if tuple(r["key"]) not in picked], + all_representative_keys=[r["key"] for r in rows],scope="Representatives after each chart incident event; grouping for selection only."), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/prefix.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/prefix.py new file mode 100644 index 0000000000..ecd90a7378 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/prefix.py @@ -0,0 +1,49 @@ +"""Test the frozen sixteen rank-eight-cohort banks by exact exterior minors.""" +from collections import Counter +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path +import sys +from time import monotonic + +PINS = { + "price/PRICE.json": "a78be64c3e3ae8a0e532237c4dd3541aa9ad3fcbbc3c25d79c8a03fb7e07c525", + "lead/GEOMETRY.json": "c6f9f018df8b58fcdf4f44356bd59bcac6d411b7845104ff4ad372ed4a95cfbd", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/exterior_minor.py": "b25fef5432d8ea9cff9eecc422cf07ccf7473568084de3e8d3d1b5224793504d", +} + + +def main(): + assert __debug__ + deadline = monotonic() + 22 + root = Path(sys.argv[1]) + raw = {} + for name, digest in PINS.items(): + raw[name] = (root/name).read_bytes() + if sha256(raw[name]).hexdigest() != digest: + raise ValueError(f"changed dependency: {name}") + engine = run_path(str(root/"inputs/exterior_minor.py")) + unique = engine["unique"] + price = json.loads(raw["price/PRICE.json"], object_pairs_hook=unique) + geometry = json.loads(raw["lead/GEOMETRY.json"], object_pairs_hook=unique) + word = json.loads(decompress(raw["inputs/7334-WORD.json.gz"]), object_pairs_hook=unique) + assert geometry["head"] == price["head"] == engine["HEAD"] + assert geometry["status"] == "EXHAUSTED" and geometry["eligible_bank_count"] == 326 + assert len(geometry["selected"]) == 16 and len(price["cohort"]) == 15 + selected = {tuple(row["key"]): row for row in geometry["selected"]} + controls = engine["controls"]() + result, events = engine["sweep"](word, list(selected), set(price["cohort"]), deadline) + assert all(all(row[k] == selected[key][k] for k in ("key","public","owned","pivots")) + for key,row in result.items()) + rows = [result[k] for k in selected if k in result] + print(json.dumps({"head":price["head"],"pins":PINS,"event_count":events,"case_cap":16,"runner_seconds":25, + "controls":controls,"rows":rows,"counts":Counter(row["disposition"] for row in rows), + "unvisited":[list(k) for k in selected if k not in result], + "unselected":geometry["unvisited_keys"]},indent=2,sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/select.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/select.py new file mode 100644 index 0000000000..4e8102db18 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/select.py @@ -0,0 +1,14 @@ +"""Freeze the first four suffix drops in the original rank-eight bank order.""" +from hashlib import sha256 +import json +from pathlib import Path +import sys + +root = Path(sys.argv[1]) +raw = (root/"lead/SUFFIX.json").read_bytes() +assert sha256(raw).hexdigest()=="77d78eb692bf6d3f0433730b48dbf8a0178c3288eeca961f94b2aaa6683eb59a" +s = json.loads(raw) +assert not s["unvisited"] and s["counts"]=={"excluded":1,"rank drop":6} +drops=[r for r in s["rows"] if r["disposition"]=="rank drop"] +print(json.dumps({"selected":drops[:4],"unselected":[r["key"] for r in drops[4:]]+s["unselected"], + "case_cap":4,"seconds_cap":35},indent=2,sort_keys=True)) diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/suffix.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/suffix.py new file mode 100644 index 0000000000..8b02139632 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r96/suffix.py @@ -0,0 +1,68 @@ +"""Check the seven frozen prefix drops in the rank-eight cohort.""" +from collections import Counter +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path +import sys +from time import monotonic + +PINS = { + "lead/RESULT.json": "45b6c8992dcff04b7252dfec809fc64812b86f094531ed3964ff967408057ed2", + "price/PRICE.json": "a78be64c3e3ae8a0e532237c4dd3541aa9ad3fcbbc3c25d79c8a03fb7e07c525", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/exterior_minor.py": "b25fef5432d8ea9cff9eecc422cf07ccf7473568084de3e8d3d1b5224793504d", + "inputs/reverse_engine.py": "751d5d0c4c665c8768ff69bcf939700d3be2f989c59f09af3a4aa14d3c1ebbc4", +} + + +def main(): + assert __debug__ + deadline = monotonic() + 20 + root = Path(sys.argv[1]) + raw = {} + for name, digest in PINS.items(): + raw[name] = (root/name).read_bytes() + if sha256(raw[name]).hexdigest() != digest: + raise ValueError(f"changed dependency: {name}") + engine = run_path(str(root/"inputs/exterior_minor.py")) + reverse = run_path(str(root/"inputs/reverse_engine.py")) + unique, scalar, plus, prime, minor = (engine[k] for k in ("unique","scalar","plus","P","exterior_minor")) + price = json.loads(raw["price/PRICE.json"],object_pairs_hook=unique) + prefix = json.loads(raw["lead/RESULT.json"],object_pairs_hook=unique) + word = json.loads(decompress(raw["inputs/7334-WORD.json.gz"]),object_pairs_hook=unique) + assert prefix["head"] == price["head"] == engine["HEAD"] + assert prefix["counts"] == {"excluded":9,"rank drop":7} and not prefix["unvisited"] + requests = {row["key"][0]: row for row in prefix["rows"] if row["disposition"] == "rank drop"} + assert len(requests)==7 + controls = reverse["controls"](engine) + public = word["public"] + active = word["final"] + [None] * word["owned_fields"] + columns = [{i:1} for i in range(public)] + [None]*word["owned_fields"] + cohort = set(price["cohort"]) + results = {} + tape = word["program"] + for cut in range(len(tape),-1,-1): + if (cut % 128 == 0 or cut in requests) and monotonic() >= deadline: + break + if cut in requests: + row = requests[cut] + c = row["key"][1] + bank = [i for i in range(public) if active[i] == c] + owners = [i for i in range(public,len(active)) if active[i] == c] + assert bank == row["public"] and owners == row["owned"] + result = minor(bank,columns,cohort) + results[cut] = {k: row[k] for k in ("key","public","owned","pivots")} | result + if cut: + reverse["reverse_event"](tape[cut-1],active,columns,public,scalar,plus,prime) + if cut == 0: + assert active == word["initial"]+[None]*word["owned_fields"] + rows = [results[t] for t in requests if t in results] + print(json.dumps({"head":price["head"],"pins":PINS,"controls":controls,"rows":rows, + "counts":Counter(r["disposition"] for r in rows),"unvisited":[requests[t]["key"] for t in requests if t not in results], + "unselected":prefix["unselected"]},indent=2,sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/engines/r97/freeze.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r97/freeze.py new file mode 100644 index 0000000000..30f34da614 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r97/freeze.py @@ -0,0 +1,29 @@ +from hashlib import sha256 +from pathlib import Path +import json +root=Path('.') +lead=root/'lead' +one=json.loads((lead/'CONTINUATION.json').read_bytes()) +two=json.loads((root/'modular/RESULT.json').read_bytes()) +old=json.loads((root/'input/lead/SUFFIX.json').read_bytes()) +assert [(r['key'],r['status']) for r in one['rows']]==[(r['key'],r['status']) for r in two['results']] +for a,b in zip(one['rows'],two['results'],strict=True): + for part in ('prefix','suffix'): + if a[part] is not None: + assert all(a[part][f]==b[part]['bank'][f] for f in ('public','owned','pivots')) +known=[(41740,242),(45266,242)] +new=[(40243,242),(45675,1091)] +by_key={tuple(r['key']): r for r in old['rows']} +by_key.update({tuple(r['key']): r['prefix'] for r in one['rows'] if r['status']=='dual_drop'}) +selected=[{k:by_key[key][k] for k in ('key','public','owned','pivots')} for key in known+new] +all_open=set(known+[tuple(r['key']) for r in one['rows'] if r['status']=='dual_drop']) +out={'selected':selected,'unselected':sorted(all_open-set(known+new)), + 'basis':'Inherited first two. Added smallest/earliest chart-242 bank and first of distinct chart-1091 owned-coexistence banks, after two independent primes agreed.', + 'inputs':{name:sha256((root/name).read_bytes()).hexdigest() for name in ('lead/CONTINUATION.json','modular/RESULT.json','input/lead/SUFFIX.json')}} +data=(json.dumps(out,indent=2,sort_keys=True)+'\n').encode() +(lead/'SELECTION.json').write_bytes(data) +source=(root/'input/lead/exact_four.py').read_text() +source=source.replace('"lead/SELECTION.json": "b95765ffa0bd426b3dae781aaafc1c21e3b25bcebc71b71a3871824f9009fd5f"',f'"../lead/SELECTION.json": "{sha256(data).hexdigest()}"') +source=source.replace('raw["lead/SELECTION.json"]','raw["../lead/SELECTION.json"]') +(lead/'exact_four.py').write_text(source) +print(sha256(data).hexdigest()) diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/engines/r97/modular_compare.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r97/modular_compare.py new file mode 100644 index 0000000000..8963dabfd0 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r97/modular_compare.py @@ -0,0 +1,56 @@ +"""Reconcile all R97 frozen bank labels, modular ranks and dispositions.""" +from collections import Counter +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +import sys + +PINS = { + "modular/RESULT.json": "6710e8711907a0c8412660696cf821e69fdc42bebf7fc24689fc3385fe7aabf3", + "lead/CONTINUATION.json": "1f1b1db497436811c3d18219a2277fff6fedc8ad19b7e3c4a486fdfc53c7907a", +} + + +def unique(items): + value = dict(items) + if len(value) != len(items): + raise ValueError("duplicate JSON key") + return value + + +def main(root): + documents = {} + for path, digest in PINS.items(): + raw = (root / path).read_bytes() + if sha256(raw).hexdigest() != digest: + raise ValueError(f"changed receipt: {path}") + documents[path] = loads(raw, object_pairs_hook=unique) + independent, lead = (documents[k] for k in PINS) + assert independent["head"] == lead["head"] + assert independent["complete"] and independent["modulus"] == 65537 + assert independent["previously_frozen_exact_keys"] == lead["existing_exact_pending"] + assert independent["cap_cases"] == lead["case_cap"] == 310 + assert independent["cap_seconds"] == lead["runner_seconds"] == 25 + assert independent["prefix_progress"]["events"] == lead["visited_prefix_events"] == 76466 + assert independent["suffix_progress"]["events"] == lead["visited_suffix_events"] == 76466 + out = [] + for a,b in zip(independent["results"], lead["rows"], strict=True): + assert a["key"] == b["key"] and a["status"] == b["status"] + bank = a["prefix"]["bank"] + assert all(v == b["prefix"][k] for k,v in bank.items()) + assert a["prefix"]["rank"] == b["prefix"]["exterior_rank"] + assert bool(a["suffix"]) == bool(b["suffix"]) + if a["suffix"]: + assert a["suffix"]["rank"] == b["suffix"]["suffix_rank_mod_65521"] + assert all(v == b["suffix"][k] for k,v in bank.items()) + out.append({"key":a["key"], "bank":bank, "status":a["status"], + "prefix_rank":a["prefix"]["rank"], + "suffix_rank":a["suffix"]["rank"] if a["suffix"] else None}) + assert len(out) == len({tuple(r["key"]) for r in out}) == 310 + print(dumps(dict(head=lead["head"], input_sha256=PINS, moduli=[65521,65537], + counts=Counter(r["status"] for r in out), rows=out, matched=310), indent=2, sort_keys=True)) + + +if __name__ == "__main__": + assert __debug__ + main(Path(sys.argv[1])) diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/engines/r97/second_prime.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r97/second_prime.py new file mode 100644 index 0000000000..0be5407fe6 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/r97/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-eight-fixed-paid-bank-bound/engines/rational/exact_six.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/exact_six.py new file mode 100644 index 0000000000..d3807ea5d6 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/exact_six.py @@ -0,0 +1,355 @@ +"""Exact six-bank rational check by dual-direction replay and transposed pairing.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +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 + +_mod = run_path(str(Path(__file__).resolve().with_name('rolling_exterior.py'))) +HEAD, PROTECTED, checked, unique = (_mod[k] for k in ('HEAD','PROTECTED','checked','unique')) + +SELECTION = "a4877749084f276d00917c137fda2b2593894daca1e10629a4a27de7914b4574" +MODULAR = "fa35b69613ad4af03eada14f251827464dba0d002f67da085817422ec3351649" +PRIMARY = "a3505dd0cfd3ee9e242f804e12e3c4705ea6548080d537f597cec355f358e92c" + + +def read_extra(path, pin): + raw = path.read_bytes() + assert sha256(raw).hexdigest() == pin, f"Changed input {path.name}" + return loads(raw, object_pairs_hook=unique) + + +@cache +def scalar(value): + return Q(value) + + +def add(dst,src,k): + for j,v in src.items(): + x = dst.get(j,0)+k*v + if x: + dst[j]=x + else: + dst.pop(j,None) + + +def scale(row,k): + return {j:k*v for j,v in row.items() if k*v} + + +def compose(weights, rows): + out={} + for j,value in weights.items(): + add(out,rows[j],value) + return out + + +def dot(a,b): + return sum((v*b.get(j,0) for j,v in a.items()),Q(0)) + + +def stop_at(deadline): + if monotonic() >= deadline: + raise TimeoutError("exact rational continuation cap") + + +def trace(word, selected, deadline): + n=word["public"] + tape=word["program"] + size=n+word["owned_fields"] + requests=defaultdict(list) + offsets=[] + count=0 + for row in selected: + t,_=row["key"] + offsets.append((count,count+len(row["public"]))) + for r in row["public"]: + requests[t].append((r,count)) + count+=1 + + # Prefix rows via backward covectors injected at each pre-event cut. + carry=[{} for _ in range(size)] + for t in range(max(requests),-1,-1): + if t%128==0: + stop_at(deadline) + op,d,*args=tape[t] + if op in ("INIT","CLEAR"): + carry[d]={} + elif op=="SCALE" and carry[d]: + carry[d]=scale(carry[d],scalar(args[0])) + elif op in ("ADD","COPY"): + add(carry[args[0]],carry[d],scalar(args[-2])) + if op=="COPY": + carry[d]={} + for r,j in requests.get(t,()): + add(carry[r],{j:Q(1)},1) + assert not any(carry[n:]) + prefix=[{} for _ in range(count)] + for coordinate,vec in enumerate(carry[:n]): + for j,v in vec.items(): + prefix[j][coordinate]=v + + # Suffix columns via forward impulses injected at each pre-event cut. + carry=[{} for _ in range(size)] + charts=list(word["initial"])+[None]*(size-n) + for t, event in enumerate(tape): + if t%128==0: + stop_at(deadline) + for r,j in requests.get(t,()): + # Any other cotangents in carry refer to earlier, independent cuts. + add(carry[r],{j:Q(1)},1) + op,d,*args=event + if op=="MOVE": + a,b,owned=args + assert charts[d]==a and owned==(d>=n) + charts[d]=b + elif op=="INIT": + assert d>=n and charts[d] is None + carry[d]={} + charts[d]=args[0] + elif op=="CLEAR": + assert d>=n and charts[d]==args[0] + carry[d]={} + charts[d]=None + elif op=="SCALE": + assert charts[d]==args[-1] + if carry[d]: + carry[d]=scale(carry[d],scalar(args[0])) + else: + src= args[0] + assert op in ("ADD","COPY") and charts[d]==charts[src]==args[-1] and d!=src + if op=="COPY": + assert d>=n and not carry[d] + carry[d]={} + add(carry[d],carry[src],scalar(args[-2])) + assert charts==list(word["final"])+[None]*(size-n) and not any(carry[n:]) + suffix=[{} for _ in range(count)] + for coordinate,vec in enumerate(carry[:n]): + for j,v in vec.items(): + suffix[j][coordinate]=v + return [(prefix[a:b],suffix[a:b]) for a,b in offsets] + + +def kernel(equations,width): + """Exact column-variable nullspace by descending-coordinate row reduction.""" + pivots={} + for equation in equations: + row=equation.copy() + while row: + j=max(row) + if j in pivots: + add(row,pivots[j],-row[j]) + else: + pivots[j]=scale(row,1/row[j]) + break + basis=[] + for free in sorted(set(range(width))-pivots.keys()): + vec={free:Q(1)} + for j,row in sorted(pivots.items()): + v=-dot(row,vec) + if v: + vec[j]=v + assert all(dot(row,vec)==0 for row in pivots.values()) + basis.append(vec) + return len(pivots),basis + + +def pure(rows,cohort): + equations=defaultdict(dict) + for j,row in enumerate(rows): + for i,v in row.items(): + if i not in cohort: + equations[i][j]=v + rank,coefficients=kernel(equations.values(),len(rows)) + result=[] + for weights in coefficients: + image=compose(weights,rows) + assert image.keys()<=cohort + result.append((weights,image)) + return rank,result + + +def pair(prefix,suffix,deadline): + """Use transposed bilinear maps and their explicit wedge coefficients.""" + B,D=[],[] + for b,d in suffix: + bv,dv={},{} + for i,(a,c) in enumerate(prefix): + if value:=dot(c,d): + bv[i]=value + if value:=dot(a,b)-bv.get(i,0): + dv[i]=value + B.append(bv) + D.append(dv) + + def columns(y): + return compose(y,B),compose(y,D) + + def solve(y): + u,v=columns(y) + if not u: + return None + if not v: + i=min(u) + return {i:1/u[i]},y + j=min(v) + for i in sorted(u.keys()|v.keys()): + den=u.get(i,0)*v[j]-u.get(j,0)*v.get(i,0) + if den: + return {i:v[j]/den,j:-v.get(i,0)/den},y + return None + + def wedge(u,v): + coords=sorted(u.keys()|v.keys()) + return {(i,j):x for k,i in enumerate(coords) for j in coords[k+1:] + if (x:=u.get(i,0)*v.get(j,0)-u.get(j,0)*v.get(i,0))} + + hit=None + for j,(u,v) in enumerate(zip(B,D,strict=True)): + stop_at(deadline) + if wedge(u,v): + hit=solve({j:Q(1)}) + assert hit + break + if hit is None: + for j,u in enumerate(B): + stop_at(deadline) + for k in range(j+1,len(B)): + mixed=wedge(u,D[k]) + add(mixed,wedge(B[k],D[j]),1) + if mixed: + hit=solve({j:Q(1),k:Q(1)}) + assert hit + break + if hit is not None: + break + if hit is None: + equations=[{j:D[j][i] for j in range(len(D)) if i in D[j]} for i in range(len(prefix))] + _,right_null=kernel(equations,len(D)) + for y in right_null: + stop_at(deadline) + hit=solve(y) + if hit is not None: + break + if hit is None: + return None + x,y=hit + a,c=(compose(x,[p[i] for p in prefix]) for i in (0,1)) + b,d=(compose(y,[p[i] for p in suffix]) for i in (0,1)) + assert dot(a,b)==dot(c,d)==1 + return {k:{j:v for j,v in row.items() if v} for k,row in zip("abcd",(a,b,c,d))} + + +def smooth(v): + v=abs(v) + assert v + for p in (2,3,5): + while v%p==0: + v//=p + return v==1 + + +def physical_screen(witness,pivots): + # This is only a coefficient and reciprocal preflight. + def pivots_for(row, allowed): + return [j for j,v in sorted(row.items()) if j in allowed and smooth(v.numerator) and smooth(v.denominator)] + return { + "cut_unit_pivots":pivots_for(witness["a"],set(pivots)), + "boundary_unit_pivots":pivots_for(witness["c"],set(witness["c"])), + "all_denominators_in_Z_1_over_30":all(smooth(v.denominator) for row in witness.values() for v in row.values()), + "physical_route_price_tape_unverified":True, + } + + +def checks(): + inf=float("inf") + pref=[({0:Q(1)},{10:Q(2)})] + suf=[({0:Q(1)},{10:Q(1,2)})] + assert pair(pref,suf,inf) + assert pair(pref,[({0:Q(1)},{10:Q(1)})],inf) is None + # Both single suffix basis directions fail, but their mixed wedge works. + pref=[({0:Q(1)},{10:Q(1)}),({1:Q(1)},{11:Q(1)})] + suf=[({0:Q(2)},{10:Q(1)}),({1:Q(3)},{11:Q(1)})] + assert pair(pref,suf,inf) + assert kernel([{1:Q(1),0:Q(2)},{1:Q(2),0:Q(4)}],2)[1] == [{0:Q(1),1:Q(-2)}] + return ["signed_unit","unequal_pairing_rejected","mixed_wedge","dependent_kernel"] + + +def main(): + parser=ArgumentParser(description=__doc__) + for name in ("word","price","selection","modular"): + parser.add_argument("--"+name,type=Path) + parser.add_argument("--controls-only",action="store_true") + a=parser.parse_args() + if not __debug__: + raise RuntimeError("Run with assertions") + if a.controls_only: + print(dumps(checks())) + return + if not all((a.word,a.price,a.selection,a.modular)): + parser.error("All four pinned input paths required") + selected, results=[],[] + diagnostics=[] + timeout=None + + def stop(*_): + raise TimeoutError("hard exact 35-second cap") + + signal(SIGALRM,stop) + alarm(35) + deadline=monotonic()+33 + try: + diagnostics=checks() + price=checked(a.price,"price") + selection=read_extra(a.selection,SELECTION) + mod=read_extra(a.modular,MODULAR) + assert selection["modular_sha256"]==PRIMARY and selection["exact_cap"]==6 and selection["exact_seconds_cap"]==35 + selected=selection["selected"] + assert len(selected)==len({tuple(x["key"]) for x in selected})==6 + modular={tuple(row["key"]):row for row in mod["tested"]} + for row in selected: + other=modular[tuple(row["key"])] + assert all(row[k]==other[k] for k in ("key","public","owned","pivots")) + assert row["exterior_rank"]==other["modular_rank"] and other["status"]=="modular_rank_drop" + assert not row["owned"] and len(row["pivots"])>=2 + word=checked(a.word,"word") + n=word["public"] + main_roles=set(word["live"])|{r+112 for r in word["live"]}|set(word["hosted"]["X2"])|set(word["hosted"]["Y2"]) + cohort={r for r,(a,z) in enumerate(zip(word["initial"],word["final"],strict=True)) + if (a,z)==(3,127) and r not in main_roles|PROTECTED} + assert len(cohort)==615 and cohort==set(price["endpoint_cohort"]) + all_rows=trace(word,selected,deadline) + for bank,(P,S) in zip(selected,all_rows,strict=True): + stop_at(deadline) + pr,prefix=pure(P,cohort) + sr,suffix=pure(S,cohort) + assert pr>=bank["exterior_rank"] + answer=pair(prefix,suffix,deadline) + entry=dict(key=bank["key"],bank=bank["public"],prefix_exterior_rank=pr,suffix_exterior_rank=sr, + prefix_nullity=len(prefix),suffix_nullity=len(suffix),modular_rank=bank["exterior_rank"], + status="exact_unit_pair" if answer else "no_exact_unit_pair") + if answer: + for name in ("a","b"): + answer[name]={bank["public"][j]:v for j,v in answer[name].items()} + entry["materialization_preflight"]=physical_screen(answer,bank["pivots"]) + entry["witness"]={name:{j:str(v) for j,v in w.items()} for name,w in answer.items()} + results.append(entry) + except TimeoutError as exc: + timeout=str(exc) + finally: + alarm(0) + print(dumps(dict(head=HEAD,selection_sha256=SELECTION,independent_modular_sha256=MODULAR, + case_cap=6,runner_cap_seconds=35,controls=diagnostics,results=results, + unresolved=[r["key"] for r in selected[len(results):]],modular_drops_outside_exact_scope=2128, + status_counts=dict(Counter(row["status"] for row in results)),timeout=timeout),indent=2,sort_keys=True)) + if timeout: + raise SystemExit(2) + + +if __name__=="__main__": + main() diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/r96_compare.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/r96_compare.py new file mode 100644 index 0000000000..cbc29dfea5 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/r96_compare.py @@ -0,0 +1,55 @@ +"""Authenticate and compare the primary and independent R96 exact dispositions.""" +from argparse import ArgumentParser +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path + +PINS = { + "primary": "362a879401158678c8a30ea0dbd4f919a9a0e907db2d2247ce96ac8724f68b14", + "independent": "69c694a17e562a6e6534406e252428ca081f8e2ac6673ec01cf21e77cb468b58", +} + + +def unique(pairs): + result = dict(pairs) + if len(result) != len(pairs): + raise ValueError("Duplicate JSON key") + return result + + +def main(): + assert __debug__ + parser = ArgumentParser(description=__doc__) + for name in PINS: + parser.add_argument("--" + name, type=Path, required=True) + args = parser.parse_args() + data = {} + for name, expected in PINS.items(): + raw = getattr(args, name).read_bytes() + if sha256(raw).hexdigest() != expected: + raise ValueError(f"Changed receipt {name}") + data[name] = loads(raw, object_pairs_hook=unique) + primary, independent = data["primary"], data["independent"] + assert primary["head"] == independent["head"] + assert primary["selected_unresolved"] == independent["selected_unvisited"] == [] + assert len(primary["results"]) == len(independent["results"]) == 4 + rows = [] + for p, i in zip(primary["results"], independent["results"], strict=True): + assert all(p[field] == i[field] for field in ("key", "owned", "public", "pivots")) + assert p["status"] == "no unit pairing" and i["status"] == "no_exact_unit_pair" + assert p["pure_prefix_dimension"] == i["prefix_nullity"] == 1 + assert p["pure_suffix_dimension"] == i["suffix_nullity"] == 1 + assert p["nonzero_prefix_images"] == i["nonzero_prefix_basis_images"] == 1 + assert p["nonzero_suffix_images"] == i["nonzero_suffix_basis_images"] == 1 + rows.append(dict(key=p["key"], prefix_rank=i["prefix_rank"], suffix_rank=i["suffix_rank"], + prefix_nonzero_dimension=1, suffix_nonzero_dimension=1, + exact_unit_pair=False)) + assert len(primary["unselected"]) == independent["modular_dual_drops_outside_exact_scope"] + ( + independent["unvisited_modular_representatives"]) == 312 + print(dumps(dict(head=primary["head"], receipt_sha256=PINS, agree=True, + results=rows, outside_exact_scope=primary["unselected"]), + indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/r96_independent.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/r96_independent.py new file mode 100644 index 0000000000..51d2306200 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/r96_independent.py @@ -0,0 +1,158 @@ +"""Check four frozen R96 banks using independent exact dual-direction replay.""" +from argparse import ArgumentParser +from collections import Counter +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().parent +PINS = { + "inputs/GEOMETRY.json": "c6f9f018df8b58fcdf4f44356bd59bcac6d411b7845104ff4ad372ed4a95cfbd", + "inputs/SELECTION.json": "b95765ffa0bd426b3dae781aaafc1c21e3b25bcebc71b71a3871824f9009fd5f", + "inputs/SUFFIX.json": "77d78eb692bf6d3f0433730b48dbf8a0178c3288eeca961f94b2aaa6683eb59a", + "inputs/PRICE.json": "a78be64c3e3ae8a0e532237c4dd3541aa9ad3fcbbc3c25d79c8a03fb7e07c525", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "reused/exact_six.py": "5bffcbbbdc5b0622e29fbc778540cc240b41e7d252e3e5c68d708d48808fcb5a", + "reused/rolling_exterior.py": "ffc6dfa01554974f2b913b65c39230d3a7f7b6c06da1c940617b7938afe2b9c7", +} +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +KEYS = [[45269, 242], [45276, 242], [45434, 242], [40242, 242]] +CAP = 4 +SECONDS = 35 +FIELDS = ("key", "owned", "pivots", "public") + + +def pinned(path, rel): + data = path.read_bytes() + if sha256(data).hexdigest() != PINS[rel]: + raise ValueError(f"Changed input {rel}") + return data + + +def selected_banks(selection, geometry, suffix, price): + assert selection["case_cap"] == price["exact_cap"] == CAP + assert selection["seconds_cap"] == price["exact_runner_seconds"] == SECONDS + assert geometry["head"] == suffix["head"] == price["head"] == HEAD + assert geometry["price_sha256"] == PINS["inputs/PRICE.json"] + assert geometry["word_sha256"] == price["word_sha256"] == PINS["inputs/7334-WORD.json.gz"] + assert geometry["eligible_bank_count"] == 326 and geometry["eligible_chart_count"] == 3 + assert not suffix["unvisited"] + geo = {tuple(row["key"]): row for row in geometry["selected"]} + mod = {tuple(row["key"]): row for row in suffix["rows"] if row["disposition"] == "rank drop"} + assert len(geo) == 16 and len(mod) == 6 + selected = selection["selected"] + assert [row["key"] for row in selected] == KEYS + assert len(selection["unselected"]) == len({tuple(k) for k in selection["unselected"]}) == 312 + assert set(mod) - {tuple(k) for k in KEYS} == {(41740, 242), (45266, 242)} + assert {tuple(k) for k in selection["unselected"]} == ( + {tuple(k) for k in geometry["unvisited_keys"]} | {(41740, 242), (45266, 242)}) + for row in selected: + key = tuple(row["key"]) + assert row["disposition"] == "rank drop" and not row["owned"] and row["pivots"] + assert all(row[k] == geo[key][k] == mod[key][k] for k in FIELDS) + return selected, mod + + +def validate_cuts(word, rows, cohort): + requests = {r["key"][0]: r for r in rows} + n = word["public"] + chart = word["initial"] + [None] * word["owned_fields"] + assert len(word["program"]) == 76466 and len(requests) == CAP + for t, (op, role, *args) in enumerate(word["program"]): + if t in requests: + row = requests.pop(t) + label = row["key"][1] + live = [i for i, loc in enumerate(chart) if loc == label] + assert row["public"] == [i for i in live if i < n] + assert row["owned"] == [i for i in live if i >= n] == [] + assert row["pivots"] == sorted(cohort.intersection(live)) + if op == "MOVE": + chart[role] = args[1] + elif op == "INIT": + chart[role] = args[0] + elif op == "CLEAR": + chart[role] = None + assert not requests and chart == word["final"] + [None] * word["owned_fields"] + + +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__ + for rel in ("reused/exact_six.py", "reused/rolling_exterior.py"): + pinned(ROOT / rel, rel) + engine = run_path(str(ROOT / "reused/exact_six.py")) + checks = engine["checks"]() + if args.controls_only: + print(dumps(checks)) + return + + def stop(*_): + raise TimeoutError("Hard 35-second exact cap") + + selected, results = [], [] + timeout = None + signal(SIGALRM, stop) + alarm(SECONDS) + deadline = monotonic() + SECONDS - 2 + try: + def read(name): + rel = f"inputs/{name}.json" + return loads(pinned(args.root / rel, rel), object_pairs_hook=engine["unique"]) + + selection, geometry, suffix, price = (read(x) for x in ("SELECTION", "GEOMETRY", "SUFFIX", "PRICE")) + selected, mod = selected_banks(selection, geometry, suffix, price) + word = engine["checked"](args.root / "inputs/7334-WORD.json.gz", "word") + cohort = set(price["cohort"]) + assert len(cohort) == len(price["cohort"]) == 15 + assert all((word["initial"][r], word["final"][r]) == (3, 245) for r in cohort) + validate_cuts(word, selected, cohort) + exact = engine["trace"](word, selected, deadline) + for row, (p, s) in zip(selected, exact, strict=True): + engine["stop_at"](deadline) + pre_rank, pre = engine["pure"](p, cohort) + suf_rank, suf = engine["pure"](s, cohort) + mod_rank = mod[tuple(row["key"])]["exterior_rank"] + assert pre_rank >= row["exterior_rank"] and suf_rank >= mod_rank + a_count = sum(bool(v) for _, v in pre) + b_count = sum(bool(v) for _, v in suf) + pair = engine["pair"](pre, suf, deadline) + status = ("exact_unit_pair" if pair else "no_nonzero_pure_prefix" if not a_count else + "no_nonzero_pure_suffix" if not b_count else "no_exact_unit_pair") + record = {k: row[k] for k in FIELDS} + record.update(prefix_rank=pre_rank, suffix_rank=suf_rank, + prefix_nullity=len(pre), suffix_nullity=len(suf), + nonzero_prefix_basis_images=a_count, nonzero_suffix_basis_images=b_count, + prefix_modular_rank=row["exterior_rank"], suffix_modular_rank=mod_rank, + status=status) + if pair: + assert engine["compose"](pair["a"], p) == pair["c"] + assert engine["compose"](pair["b"], s) == pair["d"] + assert pair["c"].keys() <= cohort and pair["d"].keys() <= cohort + assert engine["dot"](pair["a"], pair["b"]) == engine["dot"](pair["c"], pair["d"]) == 1 + for name in ("a", "b"): + pair[name] = {row["public"][j]: v for j, v in pair[name].items()} + record["physical_coefficient_preflight"] = engine["physical_screen"](pair, row["pivots"]) + record["witness"] = {name: {j: str(v) for j, v in vec.items()} for name, vec in pair.items()} + results.append(record) + except TimeoutError as error: + timeout = str(error) + finally: + alarm(0) + print(dumps(dict(head=HEAD, input_sha256=PINS, exact_case_cap=CAP, runner_seconds_cap=SECONDS, + controls=checks, timeout=timeout, results=results, + selected_unvisited=[row["key"] for row in selected[len(results):]] if selected else KEYS, + counts=dict(Counter(r["status"] for r in results)), + modular_dual_drops_outside_exact_scope=2, unvisited_modular_representatives=310), + indent=2, sort_keys=True)) + if timeout: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/r96_pairing_obstruction.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/r96_pairing_obstruction.py new file mode 100644 index 0000000000..96714118a2 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/r96_pairing_obstruction.py @@ -0,0 +1,55 @@ +"""Record the exact two scalar pairings on each of four independently traced lines.""" +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().parent +SOURCE_SHA = "0bbf9d1ea0957de30dbe9f7afa4a6fb86236b2910127f1af2722cab6b597ab26" + + +def main(): + assert __debug__ + source = ROOT / "exact_four.py" + assert sha256(source.read_bytes()).hexdigest() == SOURCE_SHA + adapter = run_path(str(source)) + for rel in ("reused/exact_six.py", "reused/rolling_exterior.py"): + adapter["pinned"](ROOT / rel, rel) + exact = run_path(str(ROOT / "reused/exact_six.py")) + + def read(name): + rel = f"inputs/{name}.json" + return loads(adapter["pinned"](ROOT / rel, rel), object_pairs_hook=exact["unique"]) + + def stop(*_): + raise TimeoutError("Hard 35-second verification cap") + + signal(SIGALRM, stop) + alarm(35) + deadline = monotonic() + 33 + try: + rows, _ = adapter["selected_banks"](*(read(x) for x in ("SELECTION", "GEOMETRY", "SUFFIX", "PRICE"))) + word = exact["checked"](ROOT / "inputs/7334-WORD.json.gz", "word") + cohort = set(read("PRICE")["cohort"]) + result = [] + for row, (p, s) in zip(rows, exact["trace"](word, rows, deadline), strict=True): + _, pre = exact["pure"](p, cohort) + _, suf = exact["pure"](s, cohort) + assert len(pre) == len(suf) == 1 + (a, c), (b, d) = pre[0], suf[0] + cut, endpoint = exact["dot"](a, b), exact["dot"](c, d) + assert c and d and (cut == 0 or cut != endpoint) + a = {row["public"][i]: v for i, v in a.items()} + b = {row["public"][i]: v for i, v in b.items()} + result.append(dict(key=row["key"], cut_pairing=str(cut), endpoint_pairing=str(endpoint), + generators={name: {i: str(v) for i, v in values.items()} + for name, values in zip("abcd", (a,b,c,d), strict=True)})) + finally: + alarm(0) + print(dumps(dict(adapter_sha256=SOURCE_SHA, results=result), indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/r97_independent.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/r97_independent.py new file mode 100644 index 0000000000..0b499179ad --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/r97_independent.py @@ -0,0 +1,210 @@ +"""Independently replay the frozen R97 cohort cuts using exact dual-direction traces.""" +from argparse import ArgumentParser +from collections import Counter +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().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +KEYS = ((41740, 242), (45266, 242)) +FOLLOWUP_KEYS = ((40243, 242), (45675, 1091)) +FOLLOWUP_SHA = "53f3a3b08bd6e97514e7077e7c0b55c9d272b0527f3a1b0e415f0924514fddf1" +SECONDS = 35 +CASE_CAP = 4 +PINS = { + "inputs/REMAINING.json": "3597499663a57702856945e91214a65e1d0f94db8643b93c0234c2bbf9291b1a", + "inputs/PREFIX.json": "45b6c8992dcff04b7252dfec809fc64812b86f094531ed3964ff967408057ed2", + "inputs/SUFFIX.json": "77d78eb692bf6d3f0433730b48dbf8a0178c3288eeca961f94b2aaa6683eb59a", + "inputs/PRICE.json": "a78be64c3e3ae8a0e532237c4dd3541aa9ad3fcbbc3c25d79c8a03fb7e07c525", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "reused/exact_six.py": "5bffcbbbdc5b0622e29fbc778540cc240b41e7d252e3e5c68d708d48808fcb5a", + "reused/rolling_exterior.py": "ffc6dfa01554974f2b913b65c39230d3a7f7b6c06da1c940617b7938afe2b9c7", +} +BANK = ("key", "public", "owned", "pivots") + + +def checked(path, expected): + raw = path.read_bytes() + if sha256(raw).hexdigest() != expected: + raise ValueError(f"Changed input {path.name}") + return raw + + +def index(rows): + out = {tuple(r["key"]): r for r in rows} + assert len(out) == len(rows) + return out + + +def inherited_keys(remaining, prefix, suffix): + assert remaining["head"] == prefix["head"] == suffix["head"] == HEAD + assert remaining["input_sha256"]["lead/RESULT.json"] == PINS["inputs/PREFIX.json"] + assert remaining["input_sha256"]["lead/SUFFIX.json"] == PINS["inputs/SUFFIX.json"] + assert [tuple(k) for k in remaining["dual_drops_requiring_rational"]] == list(KEYS) + assert remaining["next_exact_cases"] == CASE_CAP and remaining["next_exact_runner_seconds"] == SECONDS + assert len(remaining["unvisited_prefix"]) == 310 and remaining["unresolved"] == 312 + p, s = index(prefix["rows"]), index(suffix["rows"]) + out = [] + for key in KEYS: + a, b = p[key], s[key] + assert all(a[k] == b[k] for k in BANK) + assert a["disposition"] == b["disposition"] == "rank drop" and not a["owned"] + out.append({k: a[k] for k in BANK} | dict( + prefix_modular_rank=a["exterior_rank"], suffix_modular_rank=b["exterior_rank"])) + return out + + +def cut_check(word, rows, cohort): + def span(basis): + seen = {0} + for v in basis: + assert v not in seen + seen |= {u ^ v for u in seen} + return seen + + frames = word["frames"] + lo, hi = span(frames[3]), span(frames[245]) + requested = {} + for row in rows: + t, label = row["key"] + assert len(frames[label]) == 4 and lo < span(frames[label]) < hi + requested.setdefault(t, []).append(row) + n = word["public"] + chart = word["initial"] + [None] * word["owned_fields"] + for t, (op, dst, *args) in enumerate(word["program"]): + for row in requested.pop(t, ()): + _, target = row["key"] + live = [r for r, label in enumerate(chart) if label == target] + assert row["public"] == [r for r in live if r < n] + assert row["owned"] == [r for r in live if r >= n] + assert row["pivots"] == sorted(cohort.intersection(live)) and row["pivots"] + if op == "MOVE": + chart[dst] = args[1] + elif op == "INIT": + chart[dst] = args[0] + elif op == "CLEAR": + chart[dst] = None + assert not requested and chart == word["final"] + [None] * word["owned_fields"] + + +def rational_row(vec): + return {str(k): str(v) for k, v in sorted(vec.items())} + + +def evaluate(exact, row, prefix, suffix, cohort, deadline): + a_rank, a_basis = exact["pure"](prefix, cohort) + b_rank, b_basis = exact["pure"](suffix, cohort) + assert a_rank >= row.get("prefix_modular_rank", 0) + assert b_rank >= row.get("suffix_modular_rank", 0) + a_images = sum(bool(c) for _, c in a_basis) + b_images = sum(bool(d) for _, d in b_basis) + pair = exact["pair"](a_basis, b_basis, deadline) + status = ("exact_unit_pair" if pair else "no_nonzero_pure_prefix" if not a_images else + "no_nonzero_pure_suffix" if not b_images else "no_exact_unit_pair") + a_form = [[str(exact["dot"](a, b)) for b, _ in b_basis] for a, _ in a_basis] + c_form = [[str(exact["dot"](c, d)) for _, d in b_basis] for _, c in a_basis] + if len(a_basis) == len(b_basis) == 1: + assert bool(pair) == (a_form[0][0] != "0" and a_form == c_form) + pub = row["public"] + + def at_cut(weights): + return rational_row({pub[j]: value for j, value in weights.items()}) + + entry = row | dict(status=status, prefix_rank=a_rank, suffix_rank=b_rank, + prefix_nullity=len(a_basis), suffix_nullity=len(b_basis), + nonzero_prefix_basis_images=a_images, nonzero_suffix_basis_images=b_images, + prefix_rows=[rational_row(vec) for vec in prefix], + suffix_columns=[rational_row(vec) for vec in suffix], + prefix_pure_basis=[dict(a=at_cut(a), c=rational_row(c)) for a, c in a_basis], + suffix_pure_basis=[dict(b=at_cut(b), d=rational_row(d)) for b, d in b_basis], + cut_pairing_matrix=a_form, endpoint_pairing_matrix=c_form) + if pair: + assert exact["compose"](pair["a"], prefix) == pair["c"] + assert exact["compose"](pair["b"], suffix) == pair["d"] + assert pair["c"].keys() <= cohort and pair["d"].keys() <= cohort + assert exact["dot"](pair["a"], pair["b"]) == exact["dot"](pair["c"], pair["d"]) == 1 + pair["a"] = {pub[j]: v for j, v in pair["a"].items()} + pair["b"] = {pub[j]: v for j, v in pair["b"].items()} + entry["physical_coefficient_preflight"] = exact["physical_screen"](pair, row["pivots"]) + entry["witness"] = {k: rational_row(v) for k, v in pair.items()} + return entry + + +def main(): + assert __debug__ + parser = ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=ROOT) + parser.add_argument("--followup", type=Path) + parser.add_argument("--followup-sha") + parser.add_argument("--only-followup", action="store_true") + parser.add_argument("--controls-only", action="store_true") + args = parser.parse_args() + if bool(args.followup) != bool(args.followup_sha) or args.only_followup and not args.followup: + parser.error("Use a pinned follow-up file and its exact SHA together") + for rel in ("reused/exact_six.py", "reused/rolling_exterior.py"): + checked(ROOT / rel, PINS[rel]) + exact = run_path(str(ROOT / "reused/exact_six.py")) + checks = exact["checks"]() + if args.controls_only: + print(dumps(checks)) + return + + def read(name): + rel = f"inputs/{name}.json" + return loads(checked(args.root / rel, PINS[rel]), object_pairs_hook=exact["unique"]) + + def stop(*_): + raise TimeoutError("Hard 35-second exact cap") + + selected, results, fail = [], [], None + input_pins = dict(PINS) + signal(SIGALRM, stop) + phase_seconds = SECONDS - int(args.only_followup) + alarm(phase_seconds) + deadline = monotonic() + phase_seconds - 2 + try: + remaining, prefix, suffix, price = (read(k) for k in ("REMAINING", "PREFIX", "SUFFIX", "PRICE")) + assert price["head"] == HEAD and price["word_sha256"] == PINS["inputs/7334-WORD.json.gz"] + inherited = inherited_keys(remaining, prefix, suffix) + selected = [] if args.only_followup else inherited + if args.followup: + assert args.followup_sha == FOLLOWUP_SHA + raw = checked(args.followup, FOLLOWUP_SHA) + followup = loads(raw, object_pairs_hook=exact["unique"]) + assert followup["inputs"]["input/lead/SUFFIX.json"] == PINS["inputs/SUFFIX.json"] + assert len(followup["selected"]) == CASE_CAP and len(followup["unselected"]) == 29 + first, added = followup["selected"][:len(KEYS)], followup["selected"][len(KEYS):] + for saved, previous in zip(first, inherited, strict=True): + assert all(saved[k] == previous[k] for k in BANK) + assert tuple(tuple(r["key"]) for r in added) == FOLLOWUP_KEYS + assert index(added).keys() <= {tuple(k) for k in remaining["unvisited_prefix"]} + selected = selected + added + input_pins["inputs/R97-SELECTION.json"] = FOLLOWUP_SHA + assert 0 < len(selected) <= CASE_CAP + word = exact["checked"](args.root / "inputs/7334-WORD.json.gz", "word") + cohort = set(price["cohort"]) + assert len(cohort) == 15 and len(word["program"]) == 76466 + assert all((word["initial"][r], word["final"][r]) == (3, 245) for r in cohort) + cut_check(word, selected, cohort) + for row, (p, s) in zip(selected, exact["trace"](word, selected, deadline), strict=True): + exact["stop_at"](deadline) + results.append(evaluate(exact, row, p, s, cohort, deadline)) + except TimeoutError as err: + fail = str(err) + finally: + alarm(0) + print(dumps(dict(head=HEAD, input_sha256=input_pins, case_cap=CASE_CAP, + runner_seconds_cap=SECONDS, controls=checks, results=results, + selected_unvisited=[row["key"] for row in selected[len(results):]], + counts=dict(Counter(row["status"] for row in results)), timeout=fail), + indent=2, sort_keys=True)) + if fail: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/rolling_exterior.py b/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/rolling_exterior.py new file mode 100644 index 0000000000..621640c40a --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/engines/rational/rolling_exterior.py @@ -0,0 +1,286 @@ +"""Independent full exterior rank for the 4,183 frozen R86 bank keys.""" +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 + +PRIME = 65537 +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +PINS = { + "price": "b4bf8e00a8289f03b1da731fb3ab563a771d88d875e0da73acf70954df2f2c56", + "geometry": "238135413a5646cb39b34dd65dad73b3032f28352f114da9d67b854ffff39250", + "prior": "60ccc6007510c1125a5dee8612f0a3474c2d7e5c21f931745a58a8d4e2077d7b", + "word": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", +} +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PROTECTED = {319, 863, 1355, 1568} + + +def unique(pairs): + values = dict(pairs) + if len(values) != len(pairs): + raise ValueError("Duplicate JSON key") + return values + + +def checked(path, name): + raw = path.read_bytes() + if sha256(raw).hexdigest() != PINS[name]: + raise ValueError(f"Changed input {name}") + if name == "word": + raw = decompress(raw) + assert sha256(raw).hexdigest() == PAYLOAD + return loads(raw, object_pairs_hook=unique) + + +@cache +def coefficient(value): + q = Fraction(value) + if not q or not q.denominator % PRIME: + raise ValueError("Zero native scalar or nonunit denominator") + return q.numerator * pow(q.denominator, -1, PRIME) % PRIME, q.denominator + + +def axpy(dst, src, scalar): + for column, value in src.items(): + current = (dst.get(column, 0) + scalar * value) % PRIME + if current: + dst[column] = current + else: + dst.pop(column, None) + + +def rank_witness(rows): + """Use greatest available columns, preserving the order of accepted rows.""" + basis = [] + determinant = 1 + for row in rows: + reduced = row.copy() + for pivot, inverse, earlier in basis: + if (value := reduced.get(pivot, 0)): + axpy(reduced, earlier, -value*inverse) + if reduced: + pivot = max(reduced) + diagonal = reduced[pivot] + determinant = determinant * diagonal % PRIME + basis.append((pivot, pow(diagonal, -1, PRIME), reduced)) + rank = len(basis) + if rank != len(rows): + return {"status":"modular_rank_drop","modular_rank":rank} + # In pivot insertion order, the selected original columns become upper + # triangular under the same determinant-preserving row additions. + assert determinant + columns = [p for p,_,_ in basis] + return {"status":"no_nonzero_pure_prefix","modular_rank":rank, + "minor_columns":columns,"minor_determinant_mod_prime":determinant} + + +def controls(): + assert all(PRIME % divisor for divisor in range(2, isqrt(PRIME)+1)) + # The first selected column is 8, so the minor order swaps the natural axes. + proof = rank_witness([{3:2,8:1},{3:3,8:4}]) + assert proof["minor_columns"] == [8,3] and proof["minor_determinant_mod_prime"] == PRIME-5 + assert rank_witness([{3:2,8:1},{3:6,8:3}]) == {"status":"modular_rank_drop","modular_rank":1} + assert rank_witness([{},{}])["modular_rank"] == 0 + row = {1:1, 2:3} + axpy(row,{2:1,9:2},coefficient("-3")[0]) + assert row == {1:1,9:PRIME-6} + try: + coefficient("1/65537") + except ValueError: + pass + else: + raise AssertionError("Nonunit denominator was accepted") + return ["nontrivial_signed_minor","planted_rank_drop","zero_rows","signed_cancellation","nonunit_denominator_rejected"] + + +def admission(price, geometry, prior): + assert price["head"] == geometry["head"] == prior["head"] == HEAD + assert geometry["word_sha256"] == price["word_sha256"] == prior["pins"]["word"] == PINS["word"] + assert geometry["price_sha256"] == prior["pins"]["price"] == PINS["price"] + assert prior["pins"]["geometry"] == PINS["geometry"] and prior["prime"] == 65521 + assert geometry["status"] == "EXHAUSTED" and geometry["visited_events"] == 76466 + assert geometry["ranks"] == [4,5] and geometry["bank_cap"] == 24 + chosen = {tuple(x["key"]):x for x in geometry["selected"]} + keys = [tuple(k) for k in geometry["unvisited_keys"]] + entire = {tuple(k) for k in geometry["all_representative_keys"]} + assert len(chosen) == 24 and len(keys) == len(set(keys)) == 4183 + assert len(entire) == 4207 and not chosen.keys() & set(keys) and entire == chosen.keys() | set(keys) + previous = {tuple(r["key"]):r for r in prior["results"]} + assert previous.keys() == chosen.keys() and not prior["selected_unresolved"] + for k, row in chosen.items(): + record = previous[k] + assert all(record[field] == row[field] for field in ("key","public","owned","pivots")) + assert record["status"] == "no nonzero pure prefix" and record["minor"]["determinant_mod_prime"] + return keys, chosen + + +def exterior_rows(word, cohort, keys, chosen, deadline, results, previous, progress): + n = word["public"] + owners = word["owned_fields"] + initial, final = word["initial"], word["final"] + assert (n, owners, len(word["program"])) == (1501,68,76466) + mains = set(word["live"]) | {r+112 for r in word["live"]} + mains.update(word["hosted"]["X2"],word["hosted"]["Y2"]) + expected = {r for r,(a,z) in enumerate(zip(initial,final,strict=True)) + if (a,z)==(3,127) and r not in mains | PROTECTED} + assert expected == cohort and len(cohort) == 615 + frames = word["frames"] + + @cache + def space(chart): + values = {0} + for v in frames[chart]: + assert v not in values + values.update(v ^ x for x in tuple(values)) + return values + + banks = defaultdict(set) + states = list(initial) + [None]*owners + revision = [0]*len(states) + for r,c in enumerate(initial): + banks[c].add(r) + rows = [({r:1} if r not in cohort else {}) for r in range(n)] + [None]*owners + requests = defaultdict(list) + for t,c in [*keys,*chosen]: + assert len(frames[c]) in (4,5) and space(3) < space(c) < space(127) + requests[t].append(c) + + fresh = set() + cache_by_rows = {} + denoms = set() + moves = Counter() + tape = word["program"] + for t in range(len(tape)+1): + if t % 128 == 0 and monotonic() >= deadline: + raise TimeoutError("normalized exterior replay") + progress["first_unvisited_event"] = t + for c in requests.get(t,()): + if monotonic() >= deadline: + raise TimeoutError("frozen bank rank") + key = (t,c) + public = sorted(r for r in banks[c] if r=n) + eligible = sorted(set(public)&cohort) + assert public and eligible + if t: + op = tape[t-1] + incident = op[2:4] if op[0]=="MOVE" else op[-1:] + assert c in incident + signature = tuple((r,revision[r]) for r in public) + if signature not in cache_by_rows: + cache_by_rows[signature] = rank_witness([rows[r] for r in public]) + rank = cache_by_rows[signature] + record = dict(key=list(key),chart_rank=len(frames[c]),public=public,owned=owned,pivots=eligible,**rank) + if key in chosen: + assert all(record[k] == chosen[key][k] for k in ("key","public","owned","pivots")) + previous[key] = record + else: + results[key] = record + if t == len(tape): + break + op,d,*args = tape[t] + assert 0 <= d < len(states) + old = states[d] + if op=="MOVE": + a,b,owned = args + assert old == a and owned == (d>=n) + assert space(a)=n and old is None and rows[d] is None + states[d]=args[0] + banks[args[0]].add(d) + rows[d]={} + fresh.add(d) + elif op=="CLEAR": + assert d>=n and old==args[0] and rows[d] is not None + banks[old].remove(d) + states[d]=rows[d]=None + fresh.discard(d) + else: + assert old==args[-1] and rows[d] is not None and op in ("SCALE","ADD","COPY") + scale,denominator=coefficient(args[-2]) + denoms.add(denominator) + if op=="SCALE": + rows[d]={i:v*scale%PRIME for i,v in rows[d].items() if v*scale%PRIME} + else: + s=args[0] + assert d!=s and states[s]==old and rows[s] is not None + if op=="COPY": + assert d>=n and d in fresh and not rows[d] + axpy(rows[d],rows[s],scale) + fresh.discard(d) + revision[d]+=1 + + assert states == list(final)+[None]*owners and not fresh + assert dict(moves)=={1:4000,2:853,3:829,4:223,5:345,6:14,7:10,8:5} + progress.update(first_unvisited_event=None, literal_events_replayed=len(tape), + distinct_exterior_row_sets=len(cache_by_rows), denominator_units=sorted(denoms), + native_paid_histogram=dict(moves)) + + +def main(): + parser=ArgumentParser(description=__doc__) + for k in PINS: + parser.add_argument("--"+k,type=Path) + parser.add_argument("--controls-only",action="store_true") + args=parser.parse_args() + if not __debug__: + raise RuntimeError("Run with assertions") + if args.controls_only: + print(dumps(controls())) + return + if not all(getattr(args,k) for k in PINS): + parser.error("All four explicit inputs are required") + + def stop(*_): + raise TimeoutError("hard 35-second cap") + + keys, chosen, results, previous = [], {}, {}, {} + progress = {} + checks = [] + timed_out = None + signal(SIGALRM,stop) + alarm(35) + deadline=monotonic()+33 + try: + checks = controls() + price = checked(args.price,"price") + geometry = checked(args.geometry,"geometry") + prior = checked(args.prior,"prior") + keys,chosen = admission(price,geometry,prior) + word = checked(args.word,"word") + exterior_rows(word,set(price["endpoint_cohort"]),keys,chosen,deadline,results,previous,progress) + except TimeoutError as exc: + timed_out = str(exc) + finally: + alarm(0) + tested = [results[k] for k in keys if k in results] + tested_prior = [previous[k] for k in chosen if k in previous] + unvisited = [list(k) for k in keys if k not in results] + control_unvisited = [list(k) for k in chosen if k not in previous] + drops = [r["key"] for r in tested if r["status"]=="modular_rank_drop"] + control_drops = [r["key"] for r in tested_prior if r["status"]=="modular_rank_drop"] + print(dumps(dict(head=HEAD,pins=PINS,prime=PRIME,case_cap=4183,runner_cap_seconds=35, + controls=checks,prior_24=tested_prior,prior_unvisited=control_unvisited,prior_rank_drops=control_drops, + tested=tested,unvisited=unvisited,rank_drops=drops,disposition_counts=dict(Counter(r["status"] for r in tested)), + actual_full_rank_only=True,timeout=timed_out,**progress),indent=2,sort_keys=True)) + if timed_out or control_drops or control_unvisited: + raise SystemExit(2) + + +if __name__=="__main__": + main() diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/inputs/7334-WORD.json.gz b/research/p104-rank-eight-fixed-paid-bank-bound/inputs/7334-WORD.json.gz new file mode 100644 index 0000000000..73f4300719 Binary files /dev/null and b/research/p104-rank-eight-fixed-paid-bank-bound/inputs/7334-WORD.json.gz differ diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/inputs/exterior_minor.py b/research/p104-rank-eight-fixed-paid-bank-bound/inputs/exterior_minor.py new file mode 100644 index 0000000000..4e173778c3 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/inputs/exterior_minor.py @@ -0,0 +1,179 @@ +"""Exact modular exterior minors for the frozen rank-four/five banks.""" +from collections import Counter, defaultdict +from fractions import Fraction +from functools import cache +from gzip import decompress +from hashlib import sha256 +import json +from math import isqrt +from pathlib import Path +import sys +from time import monotonic + +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +P = 65521 +PINS = { + "inputs/GEOMETRY.json": "238135413a5646cb39b34dd65dad73b3032f28352f114da9d67b854ffff39250", + "inputs/PRICE.json": "b4bf8e00a8289f03b1da731fb3ab563a771d88d875e0da73acf70954df2f2c56", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", +} + + +def unique(items): + d = dict(items) + if len(d) != len(items): + raise ValueError("duplicate JSON key") + return d + + +def checked(root, name): + raw = (root / name).read_bytes() + if sha256(raw).hexdigest() != PINS[name]: + raise ValueError(f"changed dependency: {name}") + return json.loads(decompress(raw) if name.endswith(".gz") else raw, + object_pairs_hook=unique) + + +@cache +def scalar(x): + q = Fraction(x) + if q.denominator % P == 0: + raise ValueError("nonunit native denominator") + return q.numerator * pow(q.denominator, -1, P) % P + + +def plus(row, other, c): + if c: + for k, x in other.items(): + y = (row.get(k, 0) + c * x) % P + if y: + row[k] = y + else: + row.pop(k, None) + + +def exterior_minor(bank, rows, allowed): + """Use the discovered pivot order as the column order of the minor.""" + basis = [] + determinant = 1 + for role in bank: + row = {i: x for i, x in rows[role].items() if i not in allowed} + for k, vector in basis: + plus(row, vector, -row.get(k, 0)) + if row: + k = min(row) + pivot = row[k] + determinant = determinant * pivot % P + scale = pow(pivot, -1, P) + basis.append((k, {i: x * scale % P for i, x in row.items()})) + rank = len(basis) + full = rank == len(bank) + return dict(exterior_rank=rank, columns=[k for k, _ in basis], + determinant=determinant if full else None, + disposition="excluded" if full else "rank drop") + + +def controls(): + bank = [0, 1] + rows = [{0: 2, 1: 3}, {0: 5, 1: 7}] + x = exterior_minor(bank, rows, set()) + assert x["determinant"] == P - 1 and x["columns"] == [0, 1] + rows = [{0: 1, 2: 1}, {1: 1, 2: 1}] + assert exterior_minor(bank, rows, {0, 1})["disposition"] == "rank drop" + try: + scalar(f"1/{P}") + except ValueError: + pass + else: + raise AssertionError("nonunit denominator admitted") + return ["determinant sign", "planted nonzero pure prefix", "nonunit denominator rejection"] + + +def sweep(word, keys, allowed, deadline): + n = word["public"] + active = word["initial"] + [None] * word["owned_fields"] + rows = [{i: 1} for i in range(n)] + [None] * word["owned_fields"] + requests = defaultdict(list) + for t, c in keys: + requests[t].append(c) + requested = set(keys) + out = {} + finished = 0 + for t, e in enumerate(word["program"]): + if (t % 128 == 0 or t in requests) and monotonic() >= deadline: + break + for c in requests.get(t, ()): + public = [i for i in range(n) if active[i] == c] + owned = [i for i in range(n, len(active)) if active[i] == c] + pivots = sorted(set(public) & allowed) + assert pivots and len(word["frames"][c]) in (4, 5) + if t: + prior = word["program"][t - 1] + charts = prior[2:4] if prior[0] == "MOVE" else prior[-1:] + assert c in charts + out[t, c] = dict(key=[t, c], public=public, owned=owned, pivots=pivots, + **exterior_minor(public, rows, allowed)) + op, r, *a = e + if op == "MOVE": + assert active[r] == a[0] and a[2] == (r >= n) + active[r] = a[1] + elif op == "INIT": + assert active[r] is None and r >= n and rows[r] is None + active[r], rows[r] = a[0], {} + elif op == "CLEAR": + assert active[r] == a[0] and r >= n and rows[r] is not None + active[r] = rows[r] = None + elif op == "SCALE": + assert active[r] == a[1] + c = scalar(a[0]) + rows[r] = {i: c * x % P for i, x in rows[r].items()} if c else {} + else: + s, c, f = a + assert active[r] == active[s] == f and r != s and op in ("ADD", "COPY") + if op == "COPY": + assert r >= n and not rows[r] + plus(rows[r], rows[s], scalar(c)) + finished = t + 1 + if finished == len(word["program"]): + assert active == word["final"] + [None] * word["owned_fields"] + assert requested == out.keys() + return out, finished + + +def main(): + deadline = monotonic() + 32 + root = Path(sys.argv[1]) + geom = checked(root, "inputs/GEOMETRY.json") + price = checked(root, "inputs/PRICE.json") + word = checked(root, "inputs/7334-WORD.json.gz") + assert geom["head"] == price["head"] == HEAD + assert geom["price_sha256"] == PINS["inputs/PRICE.json"] + assert all(P % i for i in range(2, isqrt(P) + 1)) + allowed = set(price["endpoint_cohort"]) + assert len(allowed) == 615 + chosen = {tuple(r["key"]): r for r in geom["selected"]} + keys = [tuple(k) for k in geom["unvisited_keys"]] + assert len(chosen) == 24 and len(set(keys)) == len(keys) == 4183 + assert set(keys) | chosen.keys() == {tuple(k) for k in geom["all_representative_keys"]} + checks = controls() + out, finished = sweep(word, list(chosen) + keys, allowed, deadline) + control_records = [] + for k, earlier in chosen.items(): + if k in out: + r = out[k] + assert r["disposition"] == "excluded" + assert all(r[f] == earlier[f] for f in ("public", "owned", "pivots")) + control_records.append(r) + tested = [out[k] for k in keys if k in out] + missing = [k for k in keys if k not in out] + print(json.dumps(dict(head=HEAD, pins=PINS, prime=P, phase="normalized rational cocharts", + limit_cases=4183, limit_seconds=32, events_processed=finished, + status="CAPPED" if missing or len(control_records) != 24 else "EXHAUSTED", + controls=checks, prior_controls=control_records, results=tested, + counts=Counter(r["disposition"] for r in tested), unvisited=missing, + rank_drops=[r["key"] for r in tested if r["disposition"] == "rank drop"]), + separators=(",", ":"), sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/inputs/paired_rank.py b/research/p104-rank-eight-fixed-paid-bank-bound/inputs/paired_rank.py new file mode 100644 index 0000000000..b712cdb1f8 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-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-eight-fixed-paid-bank-bound/inputs/paired_support.py b/research/p104-rank-eight-fixed-paid-bank-bound/inputs/paired_support.py new file mode 100644 index 0000000000..46180f7b49 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/inputs/paired_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-eight-fixed-paid-bank-bound/inputs/reverse_engine.py b/research/p104-rank-eight-fixed-paid-bank-bound/inputs/reverse_engine.py new file mode 100644 index 0000000000..ebfc82f83f --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/inputs/reverse_engine.py @@ -0,0 +1,148 @@ +"""Check the 2,128 frozen public banks by exact modular suffix minors.""" +from collections import Counter, defaultdict +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path +import sys +from time import monotonic + +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +PINS = { + "price/KEYS.json": "a131ec5bf96baac89f0f6623cf7d9dff06601b36ea720474311ee7ecb394f6e2", + "inputs/PRICE.json": "b4bf8e00a8289f03b1da731fb3ab563a771d88d875e0da73acf70954df2f2c56", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/exterior_minor.py": "b25fef5432d8ea9cff9eecc422cf07ccf7473568084de3e8d3d1b5224793504d", +} + + +def authenticated(root): + raw = {} + for path, expected in PINS.items(): + raw[path] = (root / path).read_bytes() + if sha256(raw[path]).hexdigest() != expected: + raise ValueError(f"changed dependency: {path}") + return raw + + +def reverse_event(event, active, columns, public, scalar, plus, prime): + op, dst, *args = event + if op == "MOVE": + old, new, owned = args + assert active[dst] == new and owned == (dst >= public) + active[dst] = old + elif op == "CLEAR": + assert dst >= public and active[dst] is None and columns[dst] is None + active[dst], columns[dst] = args[0], {} + elif op == "INIT": + assert dst >= public and active[dst] == args[0] + active[dst] = columns[dst] = None + elif op == "SCALE": + coefficient, chart = args + assert active[dst] == chart + factor = scalar(coefficient) + columns[dst] = {k: factor * v % prime for k, v in columns[dst].items() + if factor * v % prime} + else: + src, coefficient, chart = args + assert op in ("ADD", "COPY") and dst != src + assert active[dst] == active[src] == chart + # The source contributes to both post-event fields. A guarded COPY + # replaces the destination, whose required pre-event value is zero. + plus(columns[src], columns[dst], scalar(coefficient)) + if op == "COPY": + assert dst >= public + columns[dst] = {} + + +def controls(engine): + scalar, plus, prime = (engine[name] for name in ("scalar", "plus", "P")) + active = [4, 4, None] + cols = [{0: 1}, {1: 1}, None] + 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), + ] + for event in reversed(tape): + reverse_event(event, active, cols, 2, scalar, plus, prime) + assert cols == [{0: scalar("-11/2"), 1: scalar("-3/2")}, {0: 5, 1: 1}, None] + assert active == [4, 4, None] + minor = engine["exterior_minor"] + assert minor([0, 1], cols, set())["disposition"] == "excluded" + assert minor([0, 1], cols, {0})["disposition"] == "rank drop" + return ["signed two-output impulse with owned COPY and CLEAR", + "full exterior rank", "planted pure suffix", *engine["controls"]()] + + +def sweep(word, records, cohort, engine, deadline): + public = word["public"] + active = word["final"] + [None] * word["owned_fields"] + columns = [{i: 1} for i in range(public)] + [None] * word["owned_fields"] + requests = defaultdict(list) + for record in records: + requests[record["key"][0]].append(record) + scalar, plus, prime, minor = (engine[name] for name in ("scalar", "plus", "P", "exterior_minor")) + seen, visited = {}, 0 + for cut in range(len(word["program"]), -1, -1): + if (cut % 128 == 0 or cut in requests) and monotonic() >= deadline: + break + for record in requests.get(cut, ()): + chart = record["key"][1] + public_bank = [r for r in range(public) if active[r] == chart] + owned_bank = [r for r in range(public, len(active)) if active[r] == chart] + assert public_bank == record["public"] and owned_bank == record["owned"] + assert sorted(set(public_bank) & cohort) == record["pivots"] + result = minor(public_bank, columns, cohort) + seen[tuple(record["key"])] = { + "key": record["key"], "public": public_bank, "owned": owned_bank, + "pivots": record["pivots"], "prefix_rank_mod_65521": record["exterior_rank"], + "suffix_rank_mod_65521": result["exterior_rank"], "output_minor_rows": result["columns"], + "determinant_mod_65521": result["determinant"], "disposition": result["disposition"], + } + if not cut: + assert active == word["initial"] + [None] * word["owned_fields"] + break + reverse_event(word["program"][cut - 1], active, columns, public, scalar, plus, prime) + visited += 1 + return seen, visited + + +def main(): + assert __debug__ + deadline = monotonic() + 32 + root = Path(sys.argv[1]) + raw = authenticated(root) + engine = run_path(str(root / "inputs/exterior_minor.py")) + unique = engine["unique"] + frozen = json.loads(raw["price/KEYS.json"], object_pairs_hook=unique) + price = json.loads(raw["inputs/PRICE.json"], object_pairs_hook=unique) + word = json.loads(decompress(raw["inputs/7334-WORD.json.gz"]), object_pairs_hook=unique) + assert frozen["head"] == price["head"] == HEAD + assert frozen["source_sha256"]["inputs/7334-WORD.json.gz"] == PINS["inputs/7334-WORD.json.gz"] + assert frozen["source_sha256"]["inputs/PRICE.json"] == PINS["inputs/PRICE.json"] + records = frozen["keys"] + keys = [tuple(row["key"]) for row in records] + assert len(keys) == len(set(keys)) == frozen["reverse_case_cap"] == 2128 + cohort = set(price["endpoint_cohort"]) + assert len(cohort) == 615 + checks = controls(engine) + found, visited = sweep(word, records, cohort, engine, deadline) + results = [found[k] for k in keys if k in found] + pending = [list(k) for k in keys if k not in found] + print(json.dumps({ + "head": HEAD, "pins": PINS, "scope": "normalized suffix on the frozen public bank only", + "prime": engine["P"], "cases_cap": 2128, "seconds_cap": 32, "events_processed": visited, + "status": "CAPPED" if pending or visited != len(word["program"]) else "EXHAUSTED", + "controls": checks, "counts": Counter(row["disposition"] for row in results), + "results": results, "unvisited": pending, + "rank_drops": [row["key"] for row in results if row["disposition"] == "rank drop"], + }, separators=(",", ":"), sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/7314-HELPERS.json.gz b/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/7314-HELPERS.json.gz new file mode 100644 index 0000000000..04698c9459 Binary files /dev/null and b/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/7314-HELPERS.json.gz differ diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/7334-CHANGED.json b/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/7334-CHANGED.json new file mode 100644 index 0000000000..b1644106d9 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/7334-CHANGED.json @@ -0,0 +1,72 @@ +{ + "body_clocks": [ + 40222, + 40840, + 42609, + 43022, + 43023, + 43024, + 43025, + 43026, + 43028, + 43030, + 43403, + 43491, + 43535, + 43696, + 43698, + 43887, + 45365, + 45396 + ], + "copy_and_chart_local_ownership_checked": true, + "dirty_readout": { + "319": 1 + }, + "exact_basis_columns": 14, + "forward_direction": { + "1081": -1, + "1467": 1 + }, + "literal_candidate_clocks": [ + 44588, + 44627 + ], + "paid_delta_per_word": { + "1": -1, + "5": -1, + "6": 1 + }, + "ranks": [ + 3, + 8, + 9 + ], + "roles": [ + 198, + 205, + 319, + 532, + 652, + 654, + 962, + 969, + 1081, + 1250, + 1303, + 1305, + 1453, + 1467 + ], + "scope": "Local normalized rational block, literal chart availability and nesting. Absolute Gaussian phase and whole caller separate.", + "status": "PASS_INDEPENDENT_319_BLOCK", + "window": [ + 44616, + 45718 + ], + "word_sha256": [ + "0358b9f6e0340fb3e5aa46c747c558b32a5280cbf9cd92c3b9de627dd18a9a4f", + "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + ], + "wrong_sign_and_omitted_readout_rejected": true +} diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/ADMITTED.json b/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/ADMITTED.json new file mode 100644 index 0000000000..464c89e45c --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/ADMITTED.json @@ -0,0 +1,58 @@ +{ + "assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "base": "e54523517d0f03e58352e647c403a5af3e525a57", + "caller": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "caller_sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "crossing": [ + "0.00364665195644044790699554028334161", + "0.00364665195644044790699554028334162" + ], + "end": "2026-11-11T23:04:43Z", + "exit": 0, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "hosted_at_admission": "plan and historical success; candidate replay in progress", + "inputs": { + "EARLY-RESULT.json": "ad1ca9b2e2febbf80d9bf8b6ceef14ff90fcc29ef9358310e551628eb1706649", + "INPUTS.json": "abedac59097a1c35c27d91cbdb07207bc562a64743bc406d13c94a8bc970592d", + "NATIVE-RESULT.json": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812", + "PROPOSED-CLAIM.json": "6e31241944c123d2bd4aa8bc94d833b44b3d889bd6d9aafc579108f416b45f03", + "RESULT.json": "7f2d587c59f063b01f1e8b320084a7f0943f2f05d65e3e0f5e80448c6c8e8194", + "SOURCES.json": "ac7b4473035af648d6073e78b6c39675e706e8194b346bb55ed62a0adc81d593", + "VERIFY.json": "ede7dd2dd3733b9a73f72af9dd7edfe819b49b859c5c76e227ec82cb9c220513", + "WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" + }, + "kappa": "0.00364665195644", + "ours": "0", + "peer_gain": "0.000000430519994", + "prior_kappa": "0.003646221436446", + "receipt": { + "peer-prep/IDENTITIES.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "peer-prep/STATIC.json": "500cc563b7dac8b1de1faf1dee9b820e73152dfddc15a650cd1191edd39e8c79", + "peer-price/RANK-STOCK.json": "4a7841699dd17688f6aada5c902a2a91e94558b2b1b4460c46b0e55aa95b3f9f", + "peer-price/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "peer/COMMAND.txt": "714bfab024155d8216f3ef99f3ee7627ddc35ab341c486ac6bd53c476b757130", + "peer/COMMIT.stdout": "597470d8132a3812deb3624a859546c0c13d52b094fd6fc61e7416941130bd70", + "peer/END-UTC.txt": "9c46923c616c14da5b8ed503e1652021d7bd409a10ec91a78a03263013fba08a", + "peer/METADATA.stdout": "5873404cb4424dca918a00d503569f3c29a3190fd029a007e1afb2006399f647", + "peer/RUN.exit": "9a271f2a916b0b6ee6cecb2426f0b3206ef074578be55d9bc94f6f3fe3ab86aa", + "peer/RUN.stderr": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "peer/RUN.stdout": "d589626c7581fbb9928bc615364cfee49deb62dfc0a39a903417ca62be89cf8c", + "peer/START-UTC.txt": "5b78fd6d42a2b42206891318c08e6014de57d7ca46b0201cd11a166f452210f7" + }, + "source_history": "exact anchored base and recursive package provenance, sparse shallow stock wrapper not executed", + "stages": { + "caller": "PASS_HELPER_319_FUSED_CALLER 91166298911/25000000000000", + "early": "PASS_HELPER_319_EXACT_NATIVE_AND_SIGNED_PRICE 0.00364665195644", + "frontier": "PASS_HELPER_319_FUSED_FRONTIER_PROPOSAL 91166298911/25000000000000", + "native": "PASS_HELPER_319_FUSED_NATIVE 3646017316711/1000000000000000" + }, + "start": "2026-11-11T22:54:48Z", + "status": "independently_reproduced_comparable", + "tree": "fa98712a459b20c10240450097c87de433f8a750" +} diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/PR7319-SHA256.json b/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/PR7319-SHA256.json new file mode 100644 index 0000000000..3a28905e8d --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/PR7319-SHA256.json @@ -0,0 +1,6 @@ +{ + "COMPARE.json": "58d851ca486ec84ea0d1f063eb427ed0204b1b1e49219376d0ab20f6692e043e", + "CONTACT.json": "6d6cb681db29501aec002bd620514b4c48db03424243bf71686ba023dd8d6507", + "PRICE.json": "8d70669e720faabc932366dafbc1bd1fdaef6f088c4eb02b0ea3707ba309ab53", + "REVERSE.json": "bf353b3e05d0bf5fe3e49c15673c4cb9203251329bd594009303541cf7fecc09" +} diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/READBACK.json b/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/READBACK.json new file mode 100644 index 0000000000..625b508eea --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/READBACK.json @@ -0,0 +1,188 @@ +{ + "assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "bit_admitted": "12039/3125000", + "bit_claim_headroom": "3000951089/25000000000000", + "bit_premise": "376669/100000000", + "caller_head": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "claim": "91166298911/25000000000000", + "context_c": 2430, + "context_headroom": 1666, + "copies": 17, + "directed_bounds": { + "new_at_claim": [ + "347195197206460540909548691538238227127/2000000000000000000000000000000000000000000000000", + "1735975986032302704547743457691191192207/10000000000000000000000000000000000000000000000000" + ], + "new_at_old_crossing_upper": [ + "333717954993733063339209580360321337006028706669/2000000000000000000000000000000000000000000000000", + "1668589774968665316696047901801606685030143589709/10000000000000000000000000000000000000000000000000" + ], + "new_at_raw_lower": [ + "8890529086421014119/10000000000000000000000000000000000000000000000000", + "8890529086421080299/10000000000000000000000000000000000000000000000000" + ], + "new_at_raw_upper": [ + "-29866980917152322049/10000000000000000000000000000000000000000000000000", + "-29866980917152266101/10000000000000000000000000000000000000000000000000" + ], + "new_at_tested": [ + "1464673416007288863003441470091977383033/10000000000000000000000000000000000000000000000000", + "1464673416007288863003441470091977438357/10000000000000000000000000000000000000000000000000" + ], + "old_at_claim": [ + "-1668785950738799647054310634446839861363893886031/10000000000000000000000000000000000000000000000000", + "-66751438029551985882172425377873594454555753177/400000000000000000000000000000000000000000000000" + ], + "old_at_old_crossing_upper": [ + "-357270001119021587349/10000000000000000000000000000000000000000000000000", + "-357270001119021530951/10000000000000000000000000000000000000000000000000" + ] + }, + "empty_root_credits": 0, + "exact_gain": "215259997/500000000000000", + "exact_relative_percent": "21525999700/1823110718223", + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "incumbent": "1823110718223/500000000000000", + "main_boundaries": 104, + "native_grid": [ + 1125, + 25 + ], + "native_ingredient_claim": "3646017316711/1000000000000000", + "new_raw_interval": [ + "364665195644044790699554028334161/100000000000000000000000000000000000", + "182332597822022395349777014167081/50000000000000000000000000000000000" + ], + "old_raw_upper": "36462214364462343366888845568981/10000000000000000000000000000000000", + "ordinary": 782715464, + "ordinary_delta": 52088, + "ordinary_headroom": 217284536, + "outer_functional": 4, + "outer_strict": 54, + "outer_strict_slack": "299635334804355997/10000000000000000000000000000000000", + "owned_lifetimes": 73, + "owned_peak": 50, + "paid": { + "1": 68384, + "2": 14501, + "3": 14093, + "4": 3791, + "5": 5865, + "6": 238, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "paid_delta": { + "1": -17, + "5": -17, + "6": 17 + }, + "paid_positions": 110519, + "parent": "9d0119eb12fbd9fa534b48cd37b68e7099757b91", + "path_pins": { + "dependencies/7298/pricing.py": { + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182" + }, + "dependencies/7314/NATIVE-RESULT.json": { + "sha256": "336f463da5afe5b60bfd3b9f0ce8aeea5a5feb1f854613bf4218ba0b28b3371b" + }, + "dependencies/7314/PROPOSED-CLAIM.json": { + "sha256": "41a08c4b7d0b2de4af22bc778948a143027eb3065fff47b0400b6ded1cc52778" + }, + "dependencies/7314/RESULT.json": { + "sha256": "432191ca572c9221935787ebe392699e3a1ef4512b0bf4fbc704657321cc87ca" + }, + "dependencies/round65/price.json": { + "sha256": "25205ad2cf4230bd2b2b704eec9f96ec4a5486fd575b5599861b28ffdd15b00b" + }, + "receipts/EARLY-RESULT.json": { + "git_blob": "675d6cf2374f3384019dfd53b2bdffd845005f13", + "sha256": "ad1ca9b2e2febbf80d9bf8b6ceef14ff90fcc29ef9358310e551628eb1706649" + }, + "receipts/INPUTS.json": { + "git_blob": "95c53f4594287a72d9b586f10ee136d0a1686984", + "sha256": "abedac59097a1c35c27d91cbdb07207bc562a64743bc406d13c94a8bc970592d" + }, + "receipts/NATIVE-RESULT.json": { + "git_blob": "eb101307d4d0399efed96d88cf6d4c01ec9c7369", + "sha256": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812" + }, + "receipts/PROOF.md": { + "git_blob": "7644e5571d583183ee93b686612b5ec4555f6911", + "sha256": "560de573bfd4563c16ca3c7308fa729b4188fabe802d8830f343c3873f75b59d" + }, + "receipts/PROPOSED-CLAIM.json": { + "git_blob": "6b491894580741e3e2c11a453722a0302db7b5d6", + "sha256": "6e31241944c123d2bd4aa8bc94d833b44b3d889bd6d9aafc579108f416b45f03" + }, + "receipts/README.md": { + "git_blob": "b3a055f4e0d334ce2e7df3310caaa0849eb3eba1", + "sha256": "b4db0eb83ab6a2f7151bed2da955a487f4816ec9d1976eccc21e54c2725490b0" + }, + "receipts/REFERENCE.json": { + "git_blob": "8859e243cc39546bcb1e257d95c19a658c455dc7", + "sha256": "3e66e054b803551f18b8670da0b2990a7d0eeb689dfc45b56dbcba295551da70" + }, + "receipts/REPLAY.txt": { + "git_blob": "0b8d8048c18740060f4b7f6d380a5f3a0f30ee53", + "sha256": "230984f4b8206ae4d0c0f18fbba86ff43a1a9623f8ed337cf1285360f9a67c0c" + }, + "receipts/RESULT.json": { + "git_blob": "3034a490f5b0656ae71495c99493c4ab1ac1f5c6", + "sha256": "7f2d587c59f063b01f1e8b320084a7f0943f2f05d65e3e0f5e80448c6c8e8194" + }, + "receipts/SOURCES.json": { + "git_blob": "6b97e903a6df8de437068a0e2907823885928053", + "sha256": "ac7b4473035af648d6073e78b6c39675e706e8194b346bb55ed62a0adc81d593" + }, + "receipts/VERIFY.json": { + "git_blob": "cc98ee2a5c5a79e670094a6f55c7cacda8fd330c", + "sha256": "ede7dd2dd3733b9a73f72af9dd7edfe819b49b859c5c76e227ec82cb9c220513" + }, + "receipts/construct.py": { + "git_blob": "89e923bd738dfc404ca76b7ae36f13844ac4bfbb", + "sha256": "ecb39578063d7f09153a85370a3b9bb7cbf8b36ff9891033a1cce7a2fe7f7fda" + } + }, + "physical_maps": 3037, + "productive_fields": 22461, + "rank_surplus": 1424, + "raw_strict_separation": "43051999421357030665572644351/100000000000000000000000000000000000", + "scope": "Exact receipt and directed-price readback. No native or caller execution in this audit.", + "source_archive_sha256": "0589953b3886d96eacf3bda3d38d8d574bb739fba1056af7f32f56047b6061e2", + "targets": { + "1": 306, + "2": 357, + "3": 799, + "4": 3825, + "5": 1360, + "6": 731, + "7": 323, + "8": 544, + "9": 10888, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208, + "137": 208 + }, + "tested": "364665195644007/100000000000000000" +} diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/pricing.py b/research/p104-rank-eight-fixed-paid-bank-bound/price/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/price/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-eight-fixed-paid-bank-bound/price/quote.py b/research/p104-rank-eight-fixed-paid-bank-bound/price/quote.py new file mode 100644 index 0000000000..88d4fbf161 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/price/quote.py @@ -0,0 +1,70 @@ +"""Preprice fixed-paid rank-eight splits for the 3-to-245 helper cohort.""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path + +ROOT = Path(__file__).resolve().parent +PINS = { + "inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "inputs/7314-HELPERS.json": "bf353b3e05d0bf5fe3e49c15673c4cb9203251329bd594009303541cf7fecc09", + "inputs/7334-CHANGED.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", +} + + +def unique(pairs): + out = dict(pairs) + if len(out) != len(pairs): + raise ValueError("duplicate input key") + return out + + +def main(): + assert __debug__ + data = {} + for name, pin in PINS.items(): + raw = (ROOT / name).read_bytes() + if sha256(raw).hexdigest() != pin: + raise ValueError(f"changed dependency {name}") + if name.endswith(".json"): + data[Path(name).stem] = json.loads(raw, object_pairs_hook=unique) + a, b, h, x = (data[k] for k in ("ADMITTED", "READBACK", "7314-HELPERS", "7334-CHANGED")) + assert a["head"] == b["head"] == "aaeec8c0acf01e99a5f331ef363a698d9c084ace" + assert a["exit"] == 0 and a["caller"] == b["caller_head"] and b["copies"] == 17 + assert len(h["rows"]) == 1101 and h["complete"] and len(x["roles"]) == 14 + protected = set(x["roles"]) | {863, 1355, 1531, 1567, 1568} + cohort = sorted(r["role"] for r in h["rows"] if r["role"] not in protected + and (r["initial"], r["final"], r["old_productive_rank"]) == (3, 245, 8)) + assert len(cohort) == len(set(cohort)) == 15 + paid, target = [Counter({int(k): v for k, v in b[name].items()}) for name in ("paid", "targets")] + old = target.copy() + old.subtract(paid) + assert (sum(paid.values()),sum(target.values()),sum(k*v for k,v in old.items())) == (110519,22461,1424) + assert target[8] >= 17*len(cohort) and not b["empty_root_credits"] + change = {4:34,8:-17} + new = old.copy() + new.update(change) + cost = run_path(str(ROOT/"inputs/pricing.py"))["cost"] + crossing = Q(a["crossing"][1]) + probe = crossing + Q(1,10**9) + moonshot = Q("0.0040075385047236") + assert cost(old,probe)[1] < 0 < cost(new,probe)[0] + def price(k): + delta = cost(change,k) + incumbent = cost(old,k) + return {"old_margin":list(map(str,incumbent)), "gross_one":list(map(str,delta)), + "whole_15_upper":str(15*delta[1]),"complete_15_upper":str(incumbent[1]+15*delta[1])} + print(json.dumps({"head":a["head"],"caller":a["caller"],"pins":PINS,"cohort":cohort, + "word_sha256":a["inputs"]["WORD.json.gz"],"productive_delta":change,"paid_delta":{}, + "incumbent":str(crossing),"probe":str(probe),"moonshot":str(moonshot), + "at_incumbent":price(crossing),"at_target":price(moonshot), + "event_cap":76466,"geometry_runner_seconds":20,"support_cap":16,"support_runner_seconds":25, + "exact_cap":4,"exact_runner_seconds":35,"build_cap":1},indent=2,sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/receipts/SHA256.json b/research/p104-rank-eight-fixed-paid-bank-bound/receipts/SHA256.json new file mode 100644 index 0000000000..1db37e45ef --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/receipts/SHA256.json @@ -0,0 +1,19 @@ +{ + "independent/FOLLOWUP.json": "53906dcd9ee8b8c7b6a3389c2d1e5ff8157a3191a07bb0e3064b0d1f32bc16f5", + "independent/RESULT.json": "95d34e468683aa64e19d3e4d62745b9fc1d4305b00d25054b34bb5a668639b4b", + "input/independent/AGREEMENT.json": "c718a2444821abd8bbb46a8660a4a1f05922a1446c81353d6ed5df86b02e36e3", + "input/independent/PAIRINGS.json": "2b729494affa110063e329b4f50418ec2ad7d2f821425741bbba43dfb049c879", + "input/independent/RESULT.json": "69c694a17e562a6e6534406e252428ca081f8e2ac6673ec01cf21e77cb468b58", + "input/lead/EXACT.json": "362a879401158678c8a30ea0dbd4f919a9a0e907db2d2247ce96ac8724f68b14", + "input/lead/GEOMETRY.json": "c6f9f018df8b58fcdf4f44356bd59bcac6d411b7845104ff4ad372ed4a95cfbd", + "input/lead/REMAINING.json": "3597499663a57702856945e91214a65e1d0f94db8643b93c0234c2bbf9291b1a", + "input/lead/RESULT.json": "45b6c8992dcff04b7252dfec809fc64812b86f094531ed3964ff967408057ed2", + "input/lead/SELECTION.json": "b95765ffa0bd426b3dae781aaafc1c21e3b25bcebc71b71a3871824f9009fd5f", + "input/lead/SUFFIX.json": "77d78eb692bf6d3f0433730b48dbf8a0178c3288eeca961f94b2aaa6683eb59a", + "input/price/PRICE.json": "a78be64c3e3ae8a0e532237c4dd3541aa9ad3fcbbc3c25d79c8a03fb7e07c525", + "lead/CONTINUATION.json": "1f1b1db497436811c3d18219a2277fff6fedc8ad19b7e3c4a486fdfc53c7907a", + "lead/EXACT.json": "d2d034cb496ddbafdfcdcfe5a4fcb1e0a08c8349d2310c397e5fcb61b670f1d4", + "lead/SELECTION.json": "53f3a3b08bd6e97514e7077e7c0b55c9d272b0527f3a1b0e415f0924514fddf1", + "modular/AGREEMENT.json": "8b7fa3c3f7812c116e652cb7eefd571eeffb495e2c750309b553c457b1dfadc2", + "modular/RESULT.json": "6710e8711907a0c8412660696cf821e69fdc42bebf7fc24689fc3385fe7aabf3" +} diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/receipts/UNRESOLVED.json b/research/p104-rank-eight-fixed-paid-bank-bound/receipts/UNRESOLVED.json new file mode 100644 index 0000000000..7dbe8d9e30 --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/receipts/UNRESOLVED.json @@ -0,0 +1,118 @@ +[ + [ + 40244, + 242 + ], + [ + 40245, + 242 + ], + [ + 40246, + 242 + ], + [ + 40247, + 242 + ], + [ + 40248, + 242 + ], + [ + 41741, + 242 + ], + [ + 45267, + 242 + ], + [ + 45268, + 242 + ], + [ + 45270, + 242 + ], + [ + 45273, + 242 + ], + [ + 45277, + 242 + ], + [ + 45435, + 242 + ], + [ + 45467, + 242 + ], + [ + 45468, + 242 + ], + [ + 45469, + 242 + ], + [ + 45470, + 242 + ], + [ + 45471, + 242 + ], + [ + 45472, + 242 + ], + [ + 45676, + 1091 + ], + [ + 45677, + 1091 + ], + [ + 45678, + 1091 + ], + [ + 45679, + 1091 + ], + [ + 45680, + 1091 + ], + [ + 45681, + 1091 + ], + [ + 45682, + 1091 + ], + [ + 45683, + 1091 + ], + [ + 45684, + 1091 + ], + [ + 45685, + 1091 + ], + [ + 45686, + 1091 + ] +] diff --git a/research/p104-rank-eight-fixed-paid-bank-bound/replay.py b/research/p104-rank-eight-fixed-paid-bank-bound/replay.py new file mode 100644 index 0000000000..aa2033245f --- /dev/null +++ b/research/p104-rank-eight-fixed-paid-bank-bound/replay.py @@ -0,0 +1,250 @@ +"""Regenerate the two bounded rank-eight cochart screens and verify every receipt.""" +from argparse import ArgumentParser +from fractions import Fraction +from gzip import decompress +from hashlib import sha1, sha256 +from json import loads +from pathlib import Path, PurePosixPath +from shutil import copyfile, copytree +from subprocess import run +import sys +from tempfile import TemporaryDirectory + +HERE = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +WORD = "7334-WORD.json.gz" + + +def unique(pairs): + obj = dict(pairs) + if len(obj) != len(pairs): + raise ValueError("duplicate JSON key") + return obj + + +def decode(raw): + return loads(raw, object_pairs_hook=unique) + + +def digest(raw): + return sha256(raw).hexdigest() + + +def relpath(name): + path = PurePosixPath(name) + if path.is_absolute() or path.as_posix() != name or ".." in path.parts: + raise ValueError("invalid package path: " + name) + return path + + +def authenticate(): + pins = decode((HERE / "LOCAL-PINS.json").read_bytes()) + for name, expected in pins.items(): + if digest((HERE / relpath(name)).read_bytes()) != expected: + raise ValueError("changed dependency: " + name) + provenance = decode((HERE / "PROVENANCE.json").read_bytes()) + for name, source in provenance["files"].items(): + raw = (HERE / relpath(name)).read_bytes() + assert pins[name] == source["sha256"] == digest(raw) + assert sha1(f"blob {len(raw)}\0".encode() + raw).hexdigest() == source["git_blob"] + for name, source in provenance["derived_inputs"].items(): + receipt = decode((HERE / relpath(source["receipt"])).read_bytes()) + for key in source["keys"]: + receipt = receipt[key] + if source.get("compression") == "gzip": + raw = decompress((HERE / relpath(name)).read_bytes()) + assert digest(raw) == receipt + else: + assert pins[name] == receipt + + +def command(script, *args, timeout=35, cwd=None, check=True): + return run([sys.executable, "-I", "-B", str(script), *map(str, args)], + capture_output=True, check=check, timeout=timeout, cwd=cwd) + + +def install(source, destination): + destination.parent.mkdir(parents=True, exist_ok=True) + copyfile(source, destination) + + +def rational_engine(destination, version): + suite = HERE / "engines/rational" + install(suite / f"{version}_independent.py", destination) + for name in ("exact_six.py", "rolling_exterior.py"): + install(suite / name, destination.parent / "reused" / name) + + +def rational_agreement(primary, independent, expected_counts): + rows = [row for result in independent for row in result["results"]] + assert len(rows) == len(primary["results"]) == 4 and not primary["selected_unresolved"] + assert all(not receipt["timeout"] and not receipt["selected_unvisited"] for receipt in independent) + assert primary["counts"] == expected_counts + for p, q in zip(primary["results"], rows, strict=True): + assert all(p[k] == q[k] for k in ("key", "public", "owned", "pivots")) + assert p["pure_prefix_dimension"] == q["prefix_nullity"] == 1 + assert p["nonzero_prefix_images"] == q["nonzero_prefix_basis_images"] + if p["status"] == "no unit pairing": + assert q["status"] == "no_exact_unit_pair" + assert p["pure_suffix_dimension"] == q["suffix_nullity"] == 1 + assert p["nonzero_suffix_images"] == q["nonzero_suffix_basis_images"] == 1 + assert q["cut_pairing_matrix"] == q["endpoint_pairing_matrix"] == [["0"]] + else: + assert p["status"] == "no nonzero pure prefix" + assert q["key"] == [45675, 1091] and q["owned"] == [1564, 1565] + assert q["status"] == "no_nonzero_pure_prefix" + assert q["nonzero_prefix_basis_images"] == 0 + assert q["prefix_pure_basis"][0]["a"] and not q["prefix_pure_basis"][0]["c"] + return [row["key"] for row in rows] + + +def replay(scratch, output): + authenticate() + expected = decode((HERE / "receipts/SHA256.json").read_bytes()) + generated = set() + + def record(name, raw): + if digest(raw) != expected[name]: + raise ValueError(f"changed receipt: {name}: {digest(raw)}") + assert name not in generated + generated.add(name) + destination = scratch / relpath(name) + destination.parent.mkdir(parents=True, exist_ok=True) + destination.write_bytes(raw) + return decode(raw) + + def stage(name, script, *args, timeout=35): + return record(name, command(script, *args, timeout=timeout).stdout) + + old = scratch / "input" + copytree(HERE / "inputs", old / "inputs") + old_engines = HERE / "engines/r96" + new_engines = HERE / "engines/r97" + rational = HERE / "engines/rational" + copytree(HERE / "price", old / "price") + compressed_census = old / "price/inputs/7314-HELPERS.json.gz" + compressed_census.with_suffix("").write_bytes(decompress(compressed_census.read_bytes())) + price = stage("input/price/PRICE.json", old / "price/quote.py", timeout=10) + assert price["head"] == HEAD and len(price["cohort"]) == 15 + assert price["productive_delta"] == {"4": 34, "8": -17} and not price["paid_delta"] + assert 0 < Fraction(price["at_incumbent"]["gross_one"][0]) < Fraction(price["at_incumbent"]["gross_one"][1]) < 1 + assert Fraction(price["at_target"]["complete_15_upper"]) < Fraction("-134.1394") + + geometry = stage("input/lead/GEOMETRY.json", old_engines / "geometry.py", old, timeout=20) + assert geometry["status"] == "EXHAUSTED" and geometry["visited_events"] == 76466 + assert geometry["eligible_bank_count"] == 326 and geometry["eligible_chart_count"] == 3 + assert {key[1] for key in geometry["all_representative_keys"]} == {242, 772, 1091} + prefix = stage("input/lead/RESULT.json", old_engines / "prefix.py", old, timeout=25) + assert prefix["counts"] == {"excluded": 9, "rank drop": 7} and not prefix["unvisited"] + suffix = stage("input/lead/SUFFIX.json", old_engines / "suffix.py", old, timeout=20) + assert suffix["counts"] == {"excluded": 1, "rank drop": 6} and not suffix["unvisited"] + stage("input/lead/SELECTION.json", old_engines / "select.py", old, timeout=10) + initial_exact = stage("input/lead/EXACT.json", old_engines / "exact_four.py", old) + assert initial_exact["counts"] == {"no unit pairing": 4} and not initial_exact["selected_unresolved"] + remaining = stage("input/lead/REMAINING.json", old_engines / "freeze_remaining.py", old, timeout=10) + assert remaining["unresolved"] == 312 and remaining["excluded"] == 14 + + first_rational = old / "independent" + first_sources = {"PRICE.json": old / "price/PRICE.json", WORD: old / "inputs" / WORD} + for name, label in (("GEOMETRY", "GEOMETRY"), ("SELECTION", "SELECTION"), + ("SUFFIX", "SUFFIX"), ("PRIMARY", "EXACT")): + first_sources[f"{name}.json"] = old / "lead" / f"{label}.json" + for name, path in first_sources.items(): + install(path, first_rational / "inputs" / name) + rational_engine(first_rational / "exact_four.py", "r96") + stage("input/independent/RESULT.json", first_rational / "exact_four.py") + agreed = stage("input/independent/AGREEMENT.json", rational / "r96_compare.py", + "--primary", first_rational / "inputs/PRIMARY.json", + "--independent", first_rational / "RESULT.json", timeout=10) + assert agreed["agree"] + obstruction = first_rational / "pairing_obstruction.py" + install(rational / "r96_pairing_obstruction.py", obstruction) + initial_forms = stage("input/independent/PAIRINGS.json", obstruction) + assert len(initial_forms["results"]) == 4 + assert all(row["cut_pairing"] == row["endpoint_pairing"] == "0" for row in initial_forms["results"]) + + continued = stage("lead/CONTINUATION.json", old_engines / "continue_modular.py", old, timeout=25) + assert continued["counts"] == {"prefix_exclusion": 279, "dual_drop": 31} + second_prime = new_engines / "second_prime.py" + modular = scratch / "modular" + for name in ("PRICE.json", WORD, "GEOMETRY.json", "REMAINING.json"): + source = first_sources[name] if name in first_sources else old / "lead" / name + install(source, modular / "inputs" / name) + other = stage("modular/RESULT.json", second_prime, "--root", modular, timeout=25) + assert other["complete"] and other["counts"] == continued["counts"] + modular_agreement = stage("modular/AGREEMENT.json", new_engines / "modular_compare.py", scratch, timeout=10) + assert modular_agreement["matched"] == 310 and modular_agreement["moduli"] == [65521, 65537] + + install(old_engines / "exact_four.py", old / "lead/exact_four.py") + frozen = command(new_engines / "freeze.py", timeout=10, cwd=scratch) + assert frozen.stdout.decode().strip() == expected["lead/SELECTION.json"] + selection_file = scratch / "lead/SELECTION.json" + selection = record("lead/SELECTION.json", selection_file.read_bytes()) + primary = stage("lead/EXACT.json", scratch / "lead/exact_four.py", old) + + second_rational = scratch / "independent" + rational_engine(second_rational / "exact_pairing.py", "r97") + for name, source in (("PRICE.json", first_sources["PRICE.json"]), (WORD, first_sources[WORD]), + ("REMAINING.json", old / "lead/REMAINING.json"), + ("PREFIX.json", old / "lead/RESULT.json"), ("SUFFIX.json", old / "lead/SUFFIX.json")): + install(source, second_rational / "inputs" / name) + independent_source = second_rational / "exact_pairing.py" + inherited = stage("independent/RESULT.json", independent_source) + follow_args = ("--only-followup", "--followup", selection_file, + "--followup-sha", expected["lead/SELECTION.json"]) + followup = stage("independent/FOLLOWUP.json", independent_source, *follow_args, timeout=34) + exact_keys = rational_agreement(primary, (inherited, followup), + {"no unit pairing": 3, "no nonzero pure prefix": 1}) + assert exact_keys == [row["key"] for row in selection["selected"]] + unresolved = decode((HERE / "receipts/UNRESOLVED.json").read_bytes()) + assert unresolved == selection["unselected"] == primary["unselected"] + assert len(unresolved) == len(set(map(tuple, unresolved))) == 29 + + def keys(rows, status, field="disposition"): + return {tuple(row["key"]) for row in rows if row[field] == status} + + excluded_sets = ( + keys(prefix["rows"], "excluded"), + keys(suffix["rows"], "excluded"), + keys(initial_exact["results"], "no unit pairing", "status"), + keys(continued["rows"], "prefix_exclusion", "status"), + set(map(tuple, exact_keys)), + ) + exclusions = set.union(*excluded_sets) + assert len(exclusions) == sum(map(len, excluded_sets)) == 297 + assert not exclusions.intersection(map(tuple, unresolved)) + assert exclusions | set(map(tuple, unresolved)) == set(map(tuple, geometry["all_representative_keys"])) + + damaged_selection = scratch / "bad-selection.json" + damaged_selection.write_bytes(selection_file.read_bytes() + b"\n") + negative = command(independent_source, "--only-followup", "--followup", damaged_selection, + "--followup-sha", expected["lead/SELECTION.json"], timeout=10, check=False) + assert negative.returncode == 1 and b"Changed input bad-selection.json" in negative.stderr and not negative.stdout + for name in ("REMAINING.json", WORD): + target = modular / "inputs" / name + original = target.read_bytes() + target.write_bytes(original + b"\n") + try: + bad = command(second_prime, "--root", modular, timeout=10, check=False) + assert bad.returncode == 1 and b"changed dependency:" in bad.stderr and not bad.stdout + finally: + target.write_bytes(original) + + assert generated == set(expected) + if output: + for name in sorted(generated): + install(scratch / relpath(name), output / relpath(name)) + print("PASS_P104_RANK_EIGHT_FIXED_PAID banks=326 excluded=297 unresolved=29 receipts=17") + + +def main(): + assert __debug__ and sys.version_info[:2] == (3, 12) + parser = ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="Optional root for regenerated JSON receipts") + args = parser.parse_args() + with TemporaryDirectory(prefix="rank-eight-replay-") as temporary: + replay(Path(temporary), args.output) + + +if __name__ == "__main__": + main()