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-four-five-bank-bound/LOCAL-PINS.json b/research/p104-rank-four-five-bank-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..167ce8e30f --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/LOCAL-PINS.json @@ -0,0 +1,35 @@ +{ + "PROVENANCE.json": "0f63087a246b3562940e662ab8e28a221f80479abb9895bd0f783dac46dfe2f2", + "engines/compare.py": "a0e07c9925a44a8de9890eef1d4496c009978ee0403c740c915c2da8a0c42d81", + "engines/exact_independent.py": "5bffcbbbdc5b0622e29fbc778540cc240b41e7d252e3e5c68d708d48808fcb5a", + "engines/exact_primary.py": "2aa2f0ca7cca7c97fa4224393f631739f56f74cc90e33fb7f0843531e966fd96", + "engines/geometry.py": "8b6830e1d61d177bcdc0ab78f96a618a832bbe6037fdeae901dd832ca6d0e779", + "engines/modular_primary.py": "b25fef5432d8ea9cff9eecc422cf07ccf7473568084de3e8d3d1b5224793504d", + "engines/prior_minors.py": "60bedb237f3a3f6aaa053d8ede7508367732e681c20627dfd23afe4f4e82050d", + "engines/prior_rational.py": "c691eb92c525cd1ba3204603e0e80dd7de230aa8b9cbf8707638de9043648cbc", + "engines/r89/compare_exact.py": "2099c870b3f99d373ecc44084d05de948b187d02fd8f2964dde8621da52a849a", + "engines/r89/compare_modular.py": "42bd8ad9e8057e9e7b58728a98d363a5dc5e1c4fa9d9b76eca670c0f4eeeaa2a", + "engines/r89/exact_independent.py": "c62ef2ea79b034a08154b60742e67e96954ac676e3f34c5e8e6b36cb44d0344d", + "engines/r89/exact_primary.py": "1c2024487dae9ea677c8fd4d3d69c1161ac12a50bfa870de98a87f303cf57d8d", + "engines/r89/freeze.py": "3c3ad93f5d29b350ad40c15598b117cd82c48b7a21eb112b01189cab60ddaf4e", + "engines/r89/rank_pairs.py": "4d177a546cc534b8068968d4e76eb6907e1b03eb7ab6dd91d11d68084ed5908d", + "engines/r89/reverse_suffix.py": "da0927eb5ef1b6a8e062c91d7cc7ec60ad350e9a00b77bfff5ca589c1574ba5e", + "engines/r89/select.py": "8b74c8b9fd386b88faa2983e3ebb1eb4d4c4651473eb10e3c0d48c5f496efccc", + "engines/r89/suffix_sweep.py": "751d5d0c4c665c8768ff69bcf939700d3be2f989c59f09af3a4aa14d3c1ebbc4", + "engines/rolling_exterior.py": "ffc6dfa01554974f2b913b65c39230d3a7f7b6c06da1c940617b7938afe2b9c7", + "engines/select_six.py": "e710a43a397f678eec2d83c656b75c11cb5f1884375b97a322d697c83e7cdb6a", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/paired_rank.py": "d1b7c34e6f8c8a7b810414762015e6e300a8292422af66ff671ae09741141f09", + "inputs/paired_support.py": "38c796cbe1a73f386177faf88cd53294d4b911f6cde7fd47cd9fcef3b558373f", + "price/inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "price/inputs/PR7338-SHA256.json": "25425e3a6fc025666f50faea07e9d41fa1924a44c121c5503b122f082bed2542", + "price/inputs/PR7339-SHA256.json": "1286dc448a254babfd6f4768ee450e3cce6ca077bef0e6802afc304724304fd1", + "price/inputs/R72-OCCUPANCY.json.gz": "fb27dc6b07fd16f421d63d77b0bba89ecd4cb3cffc8346a3fde249a61a430656", + "price/inputs/RANK-STOCK.json": "4a7841699dd17688f6aada5c902a2a91e94558b2b1b4460c46b0e55aa95b3f9f", + "price/inputs/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "price/inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "price/quote.py": "d4727ea853435b0415d59373f7e3516ce5ab9d31effea8a9f61e6b70583ae9fc", + "receipts/SHA256.json": "7298b16c914823fa58ca71d4abc65694e1c34dc005fbed24f4ea2bf96d664753", + "receipts/UNRESOLVED.json": "90f148044f491e1c804299216d4665f6cc770e87315b1b7ec14cdf60e02150e2", + "replay.py": "b26087fe7a66c23a2062876602f2d6a7be7e316d7f769024af8e21e364041093" +} diff --git a/research/p104-rank-four-five-bank-bound/NOTICE b/research/p104-rank-four-five-bank-bound/NOTICE new file mode 100644 index 0000000000..88693b9fd7 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/NOTICE @@ -0,0 +1,6 @@ +Apache-2.0. + +#7334 supplies the native word, #7113 the signed caller, and #7298 and +#7338 the directed tariff and admitted rank stock. #5599, #7110, #7130, +#7339 and #7353 supply the split and exact support precedents. OpenAI +Codex and subagents materially assisted. diff --git a/research/p104-rank-four-five-bank-bound/PROOF.md b/research/p104-rank-four-five-bank-bound/PROOF.md new file mode 100644 index 0000000000..ad4d572a5a --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/PROOF.md @@ -0,0 +1,115 @@ +# Exterior rank and exact pairing for a fixed-paid 4+5 split + +A cut t is the state immediately before native event t. For each strict +intermediate chart with dimension four or five, the census records the +initial cut and the cut after each event incident to that chart if a +public endpoint-cohort role is present. An event disjoint from the chart +cannot change the public bank, a current public bank role's normalized +prefix row, or its normalized suffix impulse column. A fixed-paid split +whose local basis uses only that bank has the same support equations +through such an interval. The receipt keys consist of the cut and chart. +Multiple eligible pivots in one bank share its exterior rank equations. + +Let P be the normalized literal prefix to the bank and S the normalized +literal suffix from it. A split needs a local functional a and direction +b with `c = aP` and `d = Sb` supported on the retained endpoint cohort. +It also needs `ab = cd = 1`. For a public bank of size m, restrict the m +prefix rows to the exterior boundary coordinates. A nonzero m×m minor +proves the left kernel is zero. All literal scalar denominators are +units in the verifier's finite field. A modular nonzero minor therefore +certifies a rational nonzero minor. Modular rank drops may reflect +reduction, so they only select cases for exact work. + +The first engine propagates sparse normalized rows through the literal +word and eliminates bank exterior rows using prime 65521. The second +propagates exterior-only rows, uses a different elimination pivot order +with prime 65537, and authenticates all 98 literal denominator values. +Both recover the exact public, owned and eligible role sets. Both replay +the original 24 selected banks as controls and agree on every exact bank +key and exterior rank. The independent engine also checks the signed +MOVE stock and fresh owned COPY behavior. The original selected 24 have +a separate rational replay and a transposed modular minor replay. + +The six exact continuations use two independent chronological methods. +One propagates prefix rows forward and suffix columns backward. The +other propagates prefix covectors backward and suffix impulses forward. +Rational elimination gives bases for the pure prefix and suffix +spaces. Four keys have zero pure suffix dimension. For the other two, +let B represent the bilinear form cd on the pure bases and D represent +ab−cd. A pairing exists precisely when some x,y satisfy xBy≠0 and +xDy=0. For fixed x, this is equivalent to xB lying outside the span of +xD. The two engines check the wedge coefficients exactly. If all wedge +coefficients vanish, a solution requires a vector in the kernel of D +with nonzero B image. The independent check uses the transposed pairing +test and exact kernel. Both exclude the two remaining keys. + +The structural census exhausted 4,207 representatives. The first +scientific gate capped at 24 banks and excluded all of them. The next +modular gate exhausted 4,183 new keys within a 35-second budget. It +excluded 2,049 and recorded 2,134 rank drops. The separately frozen +rational continuation hit its six-key cap within 35 seconds and excluded +all six. This prefix continuation leaves 2,128 unresolved keys for the suffix sweep below. + +## Complete price + +The complete signed comparator has 110,519 paid positions, 22,461 +productive positions, signed rank surplus 1,424, and zero empty-root +credit. Repeating one fixed-paid split in 17 copies changes productive +counts by T4+17, T5+17 and T9−17 and leaves paid counts fixed. The exact +optimistic one-edit gross upper at the comparator crossing upper is + +```text +1903560515893109741953230020081417399578277511361/5000000000000000000000000000000000000000000000000 +``` + +The gross credit is approximately 0.380712103179 raw. The unchanged +paid itinerary is part of the test. One extra raw rank-one paid +position makes the complete directed margin negative. The pre-support +price grants ancillary work for free and at most one split per distinct +cohort owner. Its 615-owner relaxation gives about 234.137943454853 raw +at the comparator. This is a price bound with unproved compatibility. +The verified exclusions produce no supplier or saving, and the unresolved +scope remains open. + +## Reverse suffix continuation + +For each of the 2,128 remaining frozen banks, restrict the normalized +suffix matrix to public output coordinates outside the endpoint cohort. +A bank perturbation is pure only when it is in the kernel of this +exterior map. Both reverse engines propagate suffix influence from the +literal final boundary, where every exterior public output has its +coordinate indicator. In an ADD, the destination's suffix vector +contributes to the source with the literal coefficient. Fresh COPY +also drops the destination variable. SCALE rescales and INIT/CLEAR +erase the corresponding dependency. The exact signed MOVE changes the +chart and preserves the normalized scalar action. + +The primary engine uses prime 65521 and row pivots. The independent +engine reconstructs live banks backwards and eliminates columns over +prime 65537. At full rank, the reported row and column order gives a +nonzero square minor of the original bank exterior matrix. The reverse +replay checks all 98 scalar denominator values are units modulo the +prime. Both fields give 663 rational exclusions and agree on the ranks +and banks of all 2,128 keys. The six earlier exact banks give four +full exterior suffix ranks and two drops as controls. + +The 1,465 suffix drops enter a finite-field pairing prioritization +under a separate 30-second cap. It returns zero modular pairs. A +rational kernel or pairing can degenerate modulo the prime, so this +stage supplies no rational exclusion. The frozen fallback takes six +deterministic keys in distinct charts and cuts. Both exact methods +verify nonzero pure prefix and suffix images at all six and exclude +the unit pairing. Their prefix/suffix nullities are (1,2) at +(cut 36807, chart 288) and (1,1) at the other five keys. No materialized +basis, native candidate or changed caller replay was required. + +Across the two continuations, the accounting is 24 prior controls, +2,049 new prefix exclusions, six first exact exclusions, 663 suffix +exclusions and six second exact exclusions. The remaining 1,459 +keys are included explicitly. The updated 109-pivot stock caps the +optimistic complete complex credit at the incumbent crossing by +41.49761924646979 raw. At fixed κ 0.0040075385047236 the complete complex +margin upper is −94.19289336391955 raw even with free ancillary work. +The retained BIT premise is also below that target. These stock bounds +grant one split per eligible literal pivot and unverified compatibility +among those edits. The selected result and κ stay unchanged. diff --git a/research/p104-rank-four-five-bank-bound/PROVENANCE.json b/research/p104-rank-four-five-bank-bound/PROVENANCE.json new file mode 100644 index 0000000000..b2e13e381e --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/PROVENANCE.json @@ -0,0 +1,64 @@ +{ + "derived_inputs": { + "price/inputs/R72-OCCUPANCY.json.gz": { + "compression": "gzip", + "published_receipt": "price/inputs/PR7339-SHA256.json", + "receipt_key": "OCCUPANCY.json" + }, + "price/inputs/RANK-STOCK.json": { + "published_receipt": "price/inputs/PR7338-SHA256.json", + "receipt_key": "RANK-STOCK.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/PR7338-SHA256.json": { + "commit": "349996445176e934ffb3c76813adcd230ca8f783", + "git_blob": "8a4d2a0cf37422891787610ba0ae95b869e29751", + "path": "research/p104-compensated-fusion-readout-bound/receipts/SHA256.json", + "sha256": "25425e3a6fc025666f50faea07e9d41fa1924a44c121c5503b122f082bed2542", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/349996445176e934ffb3c76813adcd230ca8f783/research/p104-compensated-fusion-readout-bound/receipts/SHA256.json", + "uncompress": false + }, + "price/inputs/PR7339-SHA256.json": { + "commit": "4b958b057e133e92a5c3a07f1fb489c626dc2525", + "git_blob": "585b9a98d2839b010c8d687effab0ecbbcfb7363", + "path": "research/p104-retimed-chart207-split-bound/receipts/SHA256.json", + "sha256": "1286dc448a254babfd6f4768ee450e3cce6ca077bef0e6802afc304724304fd1", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/4b958b057e133e92a5c3a07f1fb489c626dc2525/research/p104-retimed-chart207-split-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-four-five-bank-bound/README.md b/research/p104-rank-four-five-bank-bound/README.md new file mode 100644 index 0000000000..127859e2c7 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/README.md @@ -0,0 +1,36 @@ +# Fixed-paid rank-four/five public banks for P104 + +**NO VERIFIED GAIN. Conditional κ change 0%.** On exact [#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334), a rank-nine productive split into four and five would keep the paid itinerary and signed #7113 caller fixed. The structural census exhausts 76,466 literal events and freezes 4,207 public-bank representatives on 90 strict intermediate charts. + +| Support stage | Exact scope | Certified exclusions | +| --- | ---: | ---: | +| Initial prefix controls | 24 | 24 | +| Dual-prime exterior prefix | 4,183 | 2,049 | +| First exact prefix/suffix pairing | 6 of 2,134 modular drops | 6 | +| Dual-prime exterior suffix | 2,128 remaining | 663 | +| Second exact prefix/suffix pairing | 6 of 1,465 modular drops | 6 | + +The two modular engines agree on every bank, rank and disposition in each sweep. The first six exact checks find four missing pure suffixes and two failed unit pairings. The second six find six failed unit pairings. A separate finite-field pairing pass ranks the 1,465 suffix rank drops for selection. Its zero modular pairs contribute no rational exclusions. + +There are **2,724 new exclusions**, plus the 24 prior controls. The other [1,459 exact bank keys](receipts/UNRESOLVED.json), covering 109 distinct eligible pivots, remain unresolved. The full public cochart bank may supply the cut basis. Boundary images must stay in the fixed 615-member chart-3→127 cohort. Any owned roles in a bank retain their original operations. [Proof and exact cost](PROOF.md) + +## Exact inputs and replay + +The comparator is [#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) at `aaeec8c0acf01e99a5f331ef363a698d9c084ace`, independently reproduced conditional κ `0.00364665195644`. Its peer gain over #7314 is `0.000000430519994`. It inherits the exact [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) caller at `07a76c5e2738882c0cb322278e56f6cae3c9885d` and the native all-column, owned erasure, compiler, precision/tape and analytic recovery premises. [Provenance](PROVENANCE.json) and [path-keyed hashes](LOCAL-PINS.json) authenticate the inputs. + +Use CPython 3.12 with assertions from a clean checkout. + +```sh +python3.12 -I -B research/p104-rank-four-five-bank-bound/replay.py +python3.12 -B scripts/research_package.py --package research/p104-rank-four-five-bank-bound +``` + +The standard-library replay rebuilds the complete directed price before decoding the native word, then regenerates the geometry, prior controls, prefix and suffix sweeps, and both bounded exact continuations. The suffix key manifest is derived from the regenerated prefix receipts. The package bundles one exact compressed native word and reuses the pinned engines where their bytes agree. No network, previous temporary state or external dependency root is needed. Add `--out fresh-directory` to the direct command to retain all 19 regenerated receipts and their bank-level minors, ranks and scopes. [Verification receipts](VERIFICATION.md) + +## Open next questions + +The 1,459 remaining keys still require a rational decision. For a bounded continuation, pin at most six of them and verify the exact exterior kernels and the bilinear pairing for their current banks. A nonzero pair would still require a legal signed basis change, full-factor arbitrary-input forward and adjoint action, ownership and restoration, complete tape and precision checks, and a positive charged bill before a complete caller replay. The one-edit optimistic credit cannot absorb an additional paid rank-one position. Changed paid paths, wider endpoint cohorts, owned basis edits and interacting changes that alter the exterior constraints remain separate scopes. + +## Credit + +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) supplies the retimed native word and complete comparator. [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) supplies the signed caller, [#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) the exact tariff, and [#7338](https://github.com/CrocSwap/integer-mult-bounds/pull/7338) the independent admission and rank stock. [#5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599) supplies the cochart split identity. [#7110](https://github.com/CrocSwap/integer-mult-bounds/pull/7110) and [#7130](https://github.com/CrocSwap/integer-mult-bounds/pull/7130) supply earlier 4+5 and 5+4 constructions. [#7339](https://github.com/CrocSwap/integer-mult-bounds/pull/7339) supplies the exact endpoint cohort and two-sided gate on chart 207. [#7353](https://github.com/CrocSwap/integer-mult-bounds/pull/7353) provides the independent exterior minor test on a different split rank. OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging. diff --git a/research/p104-rank-four-five-bank-bound/SOURCES.json b/research/p104-rank-four-five-bank-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-rank-four-five-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-four-five-bank-bound/TASK.json b/research/p104-rank-four-five-bank-bound/TASK.json new file mode 100644 index 0000000000..c279717dda --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Exact #7334 whole-word rank-four/five productive split under fixed paid itinerary and retained public cochart basis; dual-prime prefix and suffix sweeps plus two frozen six-key rational pairings.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "P104 productive split research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "A rank-nine 4+5 productive split improves the signed complete directed invoice if an exact legal unit pairing can preserve the paid itinerary.", + "budget_minutes": 6, + "evidence": "4,207 exact bank representatives. 24 prior exclusions plus 2,724 new exclusions and 1,459 unresolved modular drops. Both primes agree on each tested bank and rank; both rational engines exclude each frozen exact continuation.", + "open_questions": [ + { + "blocked_by": "Modular rank drops and pairing prioritization do not certify rational witnesses or exclusions.", + "first_step": "Freeze at most six remaining keys and independently reconstruct both rational exterior kernels and their bilinear pairing.", + "question": "Does any of the remaining 1,459 bank keys have a legal exact two-sided unit pairing?", + "why_it_matters": "A fixed-paid 4+5 split can improve the binding complex recurrence if the actual basis and route preserve a positive complete price." + } + ], + "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": "Continues the capped 24-bank scope through every frozen exterior prefix and suffix key. Exact rational pairing stays capped at two separate six-key selections.", + "scope_status": "changed", + "stop_rule": "Exhaust the exact frozen modular prefix and suffix sets within their respective 35-second caps. Test only the two independently frozen six-key rational selections within their separate 35-second caps.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-rank-four-five-bank-bound/VERIFICATION.md b/research/p104-rank-four-five-bank-bound/VERIFICATION.md new file mode 100644 index 0000000000..b3dc58f183 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/VERIFICATION.md @@ -0,0 +1,13 @@ +# Verification receipts + +The package verifies the exact #7334 and #7113 dependency chain and regenerates 19 path-keyed receipts. The original R86 exact controls, both R87 prefix sweeps, both R89 suffix sweeps, modular pairing ranking and both independent rational exact continuations are included. The final unresolved manifest contains 1,459 ordered exact bank keys. No changed supplier was built or subjected to the complete outer gate. + +The R87 primary and independent modular replays took 1.35 and 0.49 seconds. The independent exact six took 0.20 seconds. The R89 primary and independent reverse suffix replays took 0.91 and 0.42 seconds. The R89 primary and independent exact six took 5.55 and 0.24 seconds. Relocated independent replays regenerated the R89 modular and exact receipts byte-for-byte in 0.52 and 0.30 seconds. + +The prefix and suffix stages independently verify full-rank minors with unit denominators. Controls include signed owned COPY and CLEAR, an exact determinant sign, a planted rank drop, a rejected nonunit denominator and synthetic unit and unequal pairings. The wrapper rejects corrupted geometry, modular, suffix key, compressed word and exact-selection bytes. It replays the finite-field pairing pass for ranking only. Exact rational checks supply all reported unit-pair exclusions. + +The complete comparator's four independent local stages and its [exact-head hosted run](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/43114736518) passed. Final committed transport, official committed export and hosted checks for the combined contribution are publication steps. + +The direct combined replay passed in 25.97 seconds and emitted all 19 expected receipts. No previous temporary state was used. + +The staged Git-free tar replay passed in 22.33 seconds and matched all 19 direct receipts byte-for-byte. The archive contains one native word and no Git metadata. Committed export and hosted checks remain for publication. diff --git a/research/p104-rank-four-five-bank-bound/VERIFY.json b/research/p104-rank-four-five-bank-bound/VERIFY.json new file mode 100644 index 0000000000..fdbaa166b8 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Rebuild exact price, geometry, controls, dual-prime prefix and suffix sweeps, bounded pairing prioritization and both six-key rational continuations; verify 19 receipts, final unresolved keys and input mutation controls.", + "timeout_seconds": 300 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-rank-four-five-bank-bound/engines/compare.py b/research/p104-rank-four-five-bank-bound/engines/compare.py new file mode 100644 index 0000000000..30ff1514fe --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/compare.py @@ -0,0 +1,56 @@ +"""Reconcile both primes and both exact six-bank receipts.""" +from argparse import ArgumentParser +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path + +PINS = { + "lead_modular": "a3505dd0cfd3ee9e242f804e12e3c4705ea6548080d537f597cec355f358e92c", + "independent_modular": "fa35b69613ad4af03eada14f251827464dba0d002f67da085817422ec3351649", + "lead_exact": "6c89dc61732e9f3dd0bd6bf7b3653c0aae555543959919b6955c3d49e8caf3c6", + "independent_exact": "f68c7033ed1840704c5b66edb9dc6ad223628c80879b1862796de6735a41b961", +} + + +def main(): + p=ArgumentParser(description=__doc__) + for name in PINS: + p.add_argument(name,type=Path) + args=p.parse_args() + assert __debug__ + docs=[] + for name, pin in PINS.items(): + raw=getattr(args,name).read_bytes() + assert sha256(raw).hexdigest()==pin, f"Changed receipt {name}" + docs.append(loads(raw)) + lead,independent,lead_exact,independent_exact=docs + assert len({r["head"] for r in docs})==1 and lead["prime"]!=independent["prime"] + for old,new,expected in ( + (lead["results"],independent["tested"],4183), + (lead["prior_controls"],independent["prior_24"],24), + ): + by_key={tuple(r["key"]):r for r in new} + assert len(old)==len(by_key)==expected + for row in old: + other=by_key[tuple(row["key"])] + assert all(row[k]==other[k] for k in ("key","public","owned","pivots")) + assert row["exterior_rank"]==other["modular_rank"] + assert (row["disposition"]=="excluded") == (other["status"]=="no_nonzero_pure_prefix") + assert lead["rank_drops"]==independent["rank_drops"] and len(lead["rank_drops"])==2134 + assert not lead["unvisited"] and not independent["unvisited"] + exact={} + for row,other in zip(lead_exact["results"],independent_exact["results"],strict=True): + assert row["key"]==other["key"] and row["public"]==other["bank"] + assert row["pure_prefix_dimension"]==other["prefix_nullity"] + assert row["pure_suffix_dimension"]==other["suffix_nullity"] + assert row["status"] == ("no nonzero pure suffix" if not other["suffix_nullity"] else "no unit pairing") + assert other["status"]=="no_exact_unit_pair" + exact[tuple(row["key"])]=[other["prefix_nullity"],other["suffix_nullity"]] + assert len(exact)==6 and not lead_exact["selected_unresolved"] and not independent_exact["unresolved"] + print(dumps(dict(head=lead["head"],input_sha256=PINS,modular_exact_bank_agreements=4207, + new_full_rank_exclusions=2049,modular_rank_drops=2134,exact_scope_exclusions=6, + remaining_unresolved=2128,exact_nullities=[[list(k),d] for k,d in exact.items()]),indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-rank-four-five-bank-bound/engines/exact_independent.py b/research/p104-rank-four-five-bank-bound/engines/exact_independent.py new file mode 100644 index 0000000000..d3807ea5d6 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/exact_independent.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-four-five-bank-bound/engines/exact_primary.py b/research/p104-rank-four-five-bank-bound/engines/exact_primary.py new file mode 100644 index 0000000000..096760bfaa --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/exact_primary.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": "a4877749084f276d00917c137fda2b2593894daca1e10629a4a27de7914b4574", + "inputs/PRICE.json": "b4bf8e00a8289f03b1da731fb3ab563a771d88d875e0da73acf70954df2f2c56", + "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["inputs/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, _ = solve["initial_groups"](word) + assert set(price["endpoint_cohort"]) == cohort + controls = solve["controls"]() + banks = {r["key"][0]: r["public"] for r in select["selected"]} + assert len(banks) == 6 and all(not r["owned"] for r in select["selected"]) + 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=6,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-four-five-bank-bound/engines/geometry.py b/research/p104-rank-four-five-bank-bound/engines/geometry.py new file mode 100644 index 0000000000..136937484c --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/geometry.py @@ -0,0 +1,112 @@ +"""Exact full-word occupied rank-four/five 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="b4bf8e00a8289f03b1da731fb3ab563a771d88d875e0da73acf70954df2f2c56" +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["selected_bank_cap"]==24 + n=word["public"] + cohort=set(price["endpoint_cohort"]) + assert len(cohort)==615 and all(word["initial"][r]==3 and word["final"][r]==127 for r in cohort) + spaces=list(map(span,word["frames"])) + intermediate={i for i,w in enumerate(spaces) if len(w) in (16,32) 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)==24: + 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,5],bank_cap=24, + 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-four-five-bank-bound/engines/modular_primary.py b/research/p104-rank-four-five-bank-bound/engines/modular_primary.py new file mode 100644 index 0000000000..4e173778c3 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/modular_primary.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-four-five-bank-bound/engines/prior_minors.py b/research/p104-rank-four-five-bank-bound/engines/prior_minors.py new file mode 100644 index 0000000000..f460b75282 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/prior_minors.py @@ -0,0 +1,275 @@ +"""Verify the 24 frozen rank-four/five banks by backward modular covectors.""" +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 + +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +PINS = { + "price": "b4bf8e00a8289f03b1da731fb3ab563a771d88d875e0da73acf70954df2f2c56", + "geometry": "238135413a5646cb39b34dd65dad73b3032f28352f114da9d67b854ffff39250", + "primary": "4000abaf88ad7ecb1f76a59b9eb5bafc64d0c3db75e6af159826a4431ca8f884", + "word": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", +} +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PRIME = 65521 +PROTECTED = {319, 863, 1355, 1568} + + +def unique(pairs): + value = dict(pairs) + assert len(value) == len(pairs), "Duplicate JSON key" + return value + + +def checked(path, name): + raw = path.read_bytes() + if sha256(raw).hexdigest() != PINS[name]: + raise ValueError(f"Changed dependency {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) + assert q and q.denominator % PRIME, "Nonunit native denominator" + return q.numerator * pow(q.denominator, -1, PRIME) % PRIME, q.denominator + + +def chart_audit(word, chosen, cohort, deadline): + n = word["public"] + frames = word["frames"] + states = list(word["initial"]) + [None] * word["owned_fields"] + fresh = set() + moves = Counter() + denoms = set() + requests = defaultdict(list) + + @cache + def span(chart): + space = {0} + for v in frames[chart]: + assert v not in space + space.update(v ^ w for w in tuple(space)) + return space + + at_cut = defaultdict(list) + for k, row in enumerate(chosen): + t, chart = row["key"] + assert len(frames[chart]) in (4, 5) and span(3) < span(chart) < span(127) + at_cut[t].append((k, row)) + tape = word["program"] + for t in range(len(tape) + 1): + if t % 128 == 0 and monotonic() >= deadline: + raise TimeoutError("literal selected-bank occupancy") + for k, row in at_cut.get(t, ()): + chart = row["key"][1] + public = [r for r in range(n) if states[r] == chart] + owned = [r for r in range(n, len(states)) if states[r] == chart] + assert public == row["public"] == row["pivots"] and len(public) == 2 + assert owned == row["owned"] == [] and all(r in cohort for r in public) + if t: + prev = tape[t-1] + touched = prev[2:4] if prev[0] == "MOVE" else prev[-1:] + assert chart in touched + for i, r in enumerate(public): + requests[t].append((r, 2*k+i)) + if t == len(tape): + break + op, d, *args = tape[t] + assert 0 <= d < len(states) + if op == "INIT": + assert d >= n and states[d] is None + states[d] = args[0] + fresh.add(d) + elif op == "CLEAR": + assert d >= n and states[d] == args[0] + states[d] = None + fresh.discard(d) + elif op == "MOVE": + a,b,owned = args + assert states[d] == a and owned == (d >= n) + assert span(a) < span(b) or owned and span(b) < span(a) + moves[abs(len(frames[a])-len(frames[b]))] += 1 + states[d] = b + fresh.discard(d) + else: + assert states[d] == args[-1] and op in ("ADD","COPY","SCALE") + _, denominator = coefficient(args[-2]) + denoms.add(denominator) + if op != "SCALE": + s = args[0] + assert s != d and states[s] == args[-1] + if op == "COPY": + assert d >= n and d in fresh + fresh.discard(d) + assert states == word["final"] + [None] * word["owned_fields"] and not fresh + assert sum(map(len, requests.values())) == 2*len(chosen) + return requests, dict(moves), sorted(denoms) + + +def axpy(dst, src, scale): + for j, value in src.items(): + updated = (dst.get(j, 0) + scale * value) % PRIME + if updated: + dst[j] = updated + else: + dst.pop(j, None) + + +def reverse_rows(word, requests, count, deadline): + n = word["public"] + active = [{} for _ in range(n + word["owned_fields"])] + for t in range(max(requests), -1, -1): + if t % 128 == 0 and monotonic() >= deadline: + raise TimeoutError("reverse modular prefix") + if t < len(word["program"]): + op,d,*args = word["program"][t] + if op in ("INIT","CLEAR"): + active[d] = {} + elif op == "SCALE" and active[d]: + scale,_ = coefficient(args[0]) + active[d] = {j: value*scale%PRIME for j,value in active[d].items() if value*scale%PRIME} + elif op in ("ADD","COPY"): + if active[d]: + scale,_ = coefficient(args[-2]) + axpy(active[args[0]], active[d], scale) + if op == "COPY": + active[d] = {} + for r,k in requests.get(t, ()): + axpy(active[r], {k:1}, 1) + assert not any(active[n:]) + rows = [{} for _ in range(count)] + for coordinate, weights in enumerate(active[:n]): + for k,value in weights.items(): + rows[k][coordinate] = value + return rows + + +def exterior_minor(rows, cohort): + assert len(rows) == 2 + a,b = rows + coords = sorted((a.keys() | b.keys()) - cohort) + if not coords: + return None + j = coords[0] + for k in coords[1:]: + matrix = [[a.get(j,0),a.get(k,0)], [b.get(j,0),b.get(k,0)]] + det = (matrix[0][0]*matrix[1][1]-matrix[0][1]*matrix[1][0]) % PRIME + if det: + return {"outside_input_coordinates":[j,k],"modular_matrix":matrix,"determinant_mod_prime":det} + return None + + +def controls(): + toy = {"public":3, "owned_fields":1, + "program":[["INIT",3,0],["COPY",3,1,"-3/2",0],["ADD",0,3,"1",0], + ["SCALE",1,"2/5",0],["CLEAR",3,0]]} + rows = reverse_rows(toy, {5:[(0,0),(1,1)]}, 2, float("inf")) + assert rows == [{0:1,1:coefficient("-3/2")[0]}, {1:coefficient("2/5")[0]}] + witness = exterior_minor(rows,{2}) + assert witness["outside_input_coordinates"] == [0,1] + assert witness["determinant_mod_prime"] == coefficient("2/5")[0] + assert exterior_minor(rows,{0,2}) is None + assert exterior_minor([{0:1,1:2},{0:3,1:6}],set()) is None + try: + coefficient("1/65521") + except AssertionError: + pass + else: + raise AssertionError("Nonunit scalar was accepted") + return ["signed_owned_COPY_and_backward_ADD_SCALE_CLEAR","full_exterior_minor", + "pure_prefix_survivor_and_dependent_exterior","nonunit_denominator_rejected"] + + +def main(): + parser = ArgumentParser(description=__doc__) + for name in PINS: + parser.add_argument("--"+name, type=Path) + parser.add_argument("--controls-only", action="store_true") + args = parser.parse_args() + assert __debug__ + if args.controls_only: + print(dumps(controls())) + return + assert all(getattr(args,name) for name in PINS) + start = monotonic() + deadline = start+23 + tests, chosen, results, denoms = [], [], [], [] + geometry = {} + compared = False + interruption = None + + def stop(*_): + raise TimeoutError("hard 25-second runner cap") + signal(SIGALRM, stop) + alarm(25) + try: + assert all(PRIME%d for d in range(2,isqrt(PRIME)+1)) + tests = controls() + price = checked(args.price,"price") + geometry = checked(args.geometry,"geometry") + assert price["head"] == geometry["head"] == HEAD and geometry["status"] == "EXHAUSTED" + assert geometry["price_sha256"] == PINS["price"] and geometry["word_sha256"] == price["word_sha256"] == PINS["word"] + chosen = geometry["selected"] + all_keys = {tuple(k) for k in geometry["all_representative_keys"]} + chosen_keys = {tuple(row["key"]) for row in chosen} + unvisited = {tuple(k) for k in geometry["unvisited_keys"]} + assert len(chosen_keys) == len(chosen) == 24 and len(unvisited) == 4183 + assert len(all_keys) == 4207 and all_keys == chosen_keys | unvisited and not chosen_keys & unvisited + word = checked(args.word,"word") + assert (word["public"],word["owned_fields"],len(word["program"])) == (1501,68,76466) + main_roles = set(word["live"]) | {r+112 for r in word["live"]} | set(word["hosted"]["X2"]) | set(word["hosted"]["Y2"]) + cohort = {r for r, ends in enumerate(zip(word["initial"],word["final"],strict=True)) + if ends == (3,127) and r not in main_roles | PROTECTED} + assert len(cohort) == 615 and cohort == set(price["endpoint_cohort"]) + requests,hist,denoms = chart_audit(word,chosen,cohort,deadline) + assert hist == {1:4000,2:853,3:829,4:223,5:345,6:14,7:10,8:5} + rows = reverse_rows(word,requests,48,deadline) + for k, bank in enumerate(chosen): + if monotonic() >= deadline: + raise TimeoutError("selected exterior minor check") + row_pair = rows[2*k:2*k+2] + proof = exterior_minor(row_pair,cohort) + results.append(bank | {"chart_rank":len(word["frames"][bank["key"][1]]), + "row_nnz_mod_prime":[len(row) for row in row_pair], + "status":"no nonzero pure prefix" if proof else "unresolved_modular_rank", "minor":proof}) + primary = checked(args.primary,"primary") + assert primary["head"] == HEAD and primary["geometry_sha256"] == PINS["geometry"] + assert primary["price_sha256"] == PINS["price"] and primary["word_sha256"] == PINS["word"] + by_key = {tuple(row["key"]):row for row in primary["results"]} + assert len(by_key) == 24 and set(by_key) == chosen_keys + for row in results: + expected = by_key[tuple(row["key"])] + assert all(row[k] == expected[k] for k in ("key","public","owned","pivots")) + assert expected["prefix_kernel"] == 0 and expected["status"] == "no nonzero pure prefix" + compared = True + except TimeoutError as exc: + interruption = str(exc) + finally: + alarm(0) + + unverified = [r["key"] for r in chosen[len(results):]] + counts = dict(Counter(r["status"] for r in results)) + unresolved = unverified+[r["key"] for r in results if r["minor"] is None] + print(dumps(dict(head=HEAD, pins=PINS, prime=PRIME, selected_cap=24, runner_cap_seconds=25, + geometry_banks=geometry.get("eligible_bank_count"), outside_selected_unvisited=len(geometry.get("unvisited_keys",[])), + selected_unresolved=unresolved, status_counts=counts, denominator_units=denoms, + independently_checked_public_banks_and_lifetimes=compared, controls=tests, results=results, + primary_comparison_passed=compared, timeout=interruption),sort_keys=True,indent=2)) + if interruption: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-four-five-bank-bound/engines/prior_rational.py b/research/p104-rank-four-five-bank-bound/engines/prior_rational.py new file mode 100644 index 0000000000..68d8029bcb --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/prior_rational.py @@ -0,0 +1,83 @@ +"""Exact two-sided unit pairing on the structurally selected banks.""" +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 + +from_path=Path(sys.argv[1]) +PRICE="b4bf8e00a8289f03b1da731fb3ab563a771d88d875e0da73acf70954df2f2c56" +WORD="4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PINS={"inputs/paired_rank.py":"d1b7c34e6f8c8a7b810414762015e6e300a8292422af66ff671ae09741141f09", + "inputs/paired_support.py":"38c796cbe1a73f386177faf88cd53294d4b911f6cde7fd47cd9fcef3b558373f"} + + +def checked(rel,want): + data=(from_path/rel).read_bytes() + if sha256(data).hexdigest()!=want: + raise ValueError(f"changed dependency: {rel}") + return data + + +def main(): + price=json.loads(checked("price/PRICE.json",PRICE)) + geom=json.loads(checked("lead/GEOMETRY.json",sys.argv[2])) + assert geom["status"]=="EXHAUSTED" and geom["price_sha256"]==PRICE + word=json.loads(decompress(checked("inputs/7334-WORD.json.gz",WORD))) + engines=[] + for rel,pin in PINS.items(): + checked(rel,pin) + engines.append(run_path(str(from_path/rel))) + rank,solve=engines + checks=solve["controls"]() + cohort,_=solve["initial_groups"](word) + assert set(price["endpoint_cohort"])==cohort + select={row["key"][0]:row for row in geom["selected"]} + assert len(select)==len(geom["selected"])<=24 + banks={k:row["public"] for k,row in select.items()} + deadline=monotonic()+22 + forward=rank["side"](word,banks,cohort,deadline,False) if banks else {} + open_banks={} + results={} + for t,rows in forward.items(): + p=len(rows) + if any(c for _,c in rows): + open_banks[t]=p + else: + results[t]=dict(status="no nonzero pure prefix",prefix_kernel=p) + if open_banks: + deadline=monotonic()+32 + continuation=[row["key"][0] for row in geom["selected"] if row["key"][0] in open_banks][:6] + back=rank["side"](word,{t:banks[t] for t in continuation},cohort,deadline,True) + for t,rows in back.items(): + if monotonic()>=deadline: + break + row=dict(prefix_kernel=open_banks[t],suffix_kernel=len(rows)) + if not any(c for _,c in rows): + results[t]=row|dict(status="no nonzero pure suffix") + continue + try: + w=solve["paired"](forward[t],rows,deadline) + except solve["Capped"]: + break + if w is None: + results[t]=row|dict(status="no unit pairing") + continue + results[t]=row|dict(status="exact rational support only", + witness={k:{i:str(x) for i,x in v.items()} for k,v in w.items()}) + output=[select[t]|result for t,result in sorted(results.items())] + pending=[select[t]["key"] for t in select if t not in results] + hits=[r["key"] for r in output if r["status"]=="exact rational support only"] + print(json.dumps(dict(head=price["head"],price_sha256=PRICE,geometry_sha256=sys.argv[2],word_sha256=WORD, + controls=checks,cap=24,paired_cap=6,prefix_seconds=22,paired_seconds=32, + prefix_survivors=[select[t]["key"] for t in open_banks],results=output, + counts=Counter(x["status"] for x in output),rational_survivors=hits,selected_unresolved=pending, + unvisited_structural_keys=geom["unvisited_keys"], + status="CAPPED" if geom["unvisited_keys"] or pending else "EXHAUSTED"),indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-rank-four-five-bank-bound/engines/r89/compare_exact.py b/research/p104-rank-four-five-bank-bound/engines/r89/compare_exact.py new file mode 100644 index 0000000000..f2f2a9dc73 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/r89/compare_exact.py @@ -0,0 +1,51 @@ +"""Reconcile the two exact R89 selected-bank proofs.""" +from argparse import ArgumentParser +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path + +PINS={ + "selection":"27a14af96296f0f2d162c77aa38e4051f3aaf8a8156dd654b414dd1196a6d597", + "lead":"d2369e9657a8bb99cd07813f354a44e9fb02a74245a2ff188723d295d93ce609", + "independent":"6821bf1f2df591d076528757fd02ce32e35743557ac33ee8b6a6810f4c81b4a3", + "suffix":"560a22da8219d5ca3d5ec9cb8fa25bdd32f068ca28242cdd4383351dbed82f67", +} + + +def main(): + p=ArgumentParser(description=__doc__) + for name in PINS: + p.add_argument(name,type=Path) + a=p.parse_args() + docs=[] + for name,pin in PINS.items(): + raw=getattr(a,name).read_bytes() + assert sha256(raw).hexdigest()==pin, f"Changed input {name}" + docs.append(loads(raw)) + selection,lead,ind,suffix=docs + assert lead["head"]==ind["head"]==suffix["head"] + expected=[tuple(r["key"]) for r in selection["selected"]] + old={tuple(r["key"]):r for r in lead["results"]} + new={tuple(r["key"]):r for r in ind["results"]} + assert len(expected)==6 and set(expected)==old.keys()==new.keys() + assert not lead["selected_unresolved"] and not ind["unresolved"] + assert lead["counts"]=={"no unit pairing":6} and ind["counts"]=={"no_exact_unit_pair":6} + nullities=[] + for key in expected: + a,b=old[key],new[key] + assert all(a[k]==b[k] for k in ("key","public","owned","pivots")) + assert a["pure_prefix_dimension"]==b["prefix_nullity"] + assert a["pure_suffix_dimension"]==b["suffix_nullity"] + assert bool(a["nonzero_prefix_images"])==bool(b["nonzero_prefix_basis_images"]) + assert bool(a["nonzero_suffix_images"])==bool(b["nonzero_suffix_basis_images"]) + nullities.append([list(key),[b["prefix_nullity"],b["suffix_nullity"]]]) + remaining=[r for r in suffix["tested"] if r["status"]=="modular_suffix_rank_drop" and tuple(r["key"]) not in new] + assert len(remaining)==1459 + print(dumps(dict(head=lead["head"],pins=PINS,exact_agreements=6,exact_unit_pairs=0, + remaining_modular_drops=1459,remaining_literal_pivots=sorted({p for r in remaining for p in r["pivots"]}), + exact_nullities=nullities),indent=2,sort_keys=True)) + + +if __name__=="__main__": + assert __debug__ + main() diff --git a/research/p104-rank-four-five-bank-bound/engines/r89/compare_modular.py b/research/p104-rank-four-five-bank-bound/engines/r89/compare_modular.py new file mode 100644 index 0000000000..167c3b948c --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/r89/compare_modular.py @@ -0,0 +1,48 @@ +"""Reconcile both R89 suffix fields on the exact frozen keys.""" +from argparse import ArgumentParser +from fractions import Fraction +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path + +PINS = { + "keys":"a131ec5bf96baac89f0f6623cf7d9dff06601b36ea720474311ee7ecb394f6e2", + "lead":"340d1beb37477198e4690a56153d1a225c8ad70e00cf470c07a5bc080c0255ad", + "independent":"560a22da8219d5ca3d5ec9cb8fa25bdd32f068ca28242cdd4383351dbed82f67", +} + + +def main(): + p=ArgumentParser(description=__doc__) + for name in PINS: + p.add_argument(name,type=Path) + a=p.parse_args() + docs=[] + for name,pin in PINS.items(): + raw=getattr(a,name).read_bytes() + assert sha256(raw).hexdigest()==pin, f"Changed input {name}" + docs.append(loads(raw)) + frozen,lead,ind=docs + assert frozen["head"]==lead["head"]==ind["head"] and lead["prime"]==65521 and ind["prime"]==65537 + assert not lead["unvisited"] and not ind["unvisited"] and not ind["control_discrepancies"] + assert len(ind["prior_exact_controls"])==6 and not ind["control_unvisited"] + for left,right,key in zip(lead["results"],ind["tested"],frozen["keys"],strict=True): + assert all(left[k]==right[k]==key[k] for k in ("key","public","owned","pivots")) + assert left["suffix_rank_mod_65521"]==right["suffix_exterior_rank"] + assert (left["disposition"]=="excluded")==(right["status"]=="no_nonzero_pure_suffix") + assert lead["rank_drops"]==ind["suffix_rank_drops"] and len(ind["tested"])==2128 + remaining=[r for r in ind["tested"] if r["status"]=="modular_suffix_rank_drop"] + pivots=sorted({p for r in remaining for p in r["pivots"]}) + assert len(remaining)==1465 and len(pivots)==109 + print(dumps(dict(head=lead["head"],pins=PINS,agreed_keys=2128,full_suffix_exclusions=663, + suffix_rank_drops=1465,unresolved_before_exact_followup=1465, + remaining_pivots=pivots,remaining_charts=len({r["key"][1] for r in remaining}), + old_crossing_optimistic_gross_upper=str(len(pivots)*Fraction(frozen["at_incumbent"]["one_edit_credit"][1])), + moonshot_optimistic_complete_upper=str(Fraction(frozen["at_moonshot"]["old_margin"][1])+ + len(pivots)*Fraction(frozen["at_moonshot"]["one_edit_credit"][1]))), + sort_keys=True,indent=2)) + + +if __name__=="__main__": + assert __debug__ + main() diff --git a/research/p104-rank-four-five-bank-bound/engines/r89/exact_independent.py b/research/p104-rank-four-five-bank-bound/engines/r89/exact_independent.py new file mode 100644 index 0000000000..5b49e8276d --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/r89/exact_independent.py @@ -0,0 +1,143 @@ +"""Verify only the explicitly frozen R89 exact suffix-drop selection.""" +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={ + "keys":"a131ec5bf96baac89f0f6623cf7d9dff06601b36ea720474311ee7ecb394f6e2", + "price":"b4bf8e00a8289f03b1da731fb3ab563a771d88d875e0da73acf70954df2f2c56", + "word":"4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "suffix":"560a22da8219d5ca3d5ec9cb8fa25bdd32f068ca28242cdd4383351dbed82f67", + "reused/exact_six.py":"5bffcbbbdc5b0622e29fbc778540cc240b41e7d252e3e5c68d708d48808fcb5a", + "reused/rolling_exterior.py":"ffc6dfa01554974f2b913b65c39230d3a7f7b6c06da1c940617b7938afe2b9c7", +} +HEAD="aaeec8c0acf01e99a5f331ef363a698d9c084ace" + + +def pinned(path,pin): + raw=path.read_bytes() + if sha256(raw).hexdigest()!=pin: + raise ValueError(f"Changed input {path.name}") + return raw + + +def read(path,pin,unique): + return loads(pinned(path,pin),object_pairs_hook=unique) + + +def normalize_selection(rows): + return [tuple(r["key"] if isinstance(r,dict) else r) for r in rows] + + +def selected_banks(frozen,suffix,selection): + assert frozen["head"]==suffix["head"]==HEAD and suffix["prime"]==65537 + assert suffix["pins"]["keys"]==PINS["keys"] and suffix["pins"]["word"]==PINS["word"] + assert not suffix["unvisited"] and not suffix["control_discrepancies"] + banks={tuple(r["key"]):r for r in frozen["keys"]} + modular={tuple(r["key"]):r for r in suffix["tested"] if r["status"]=="modular_suffix_rank_drop"} + assert len(banks)==2128 and len(modular)==1465 + rows=selection["selected"] + keys=normalize_selection(rows) + assert 0=bank["exterior_rank"] and suf_rank>=bank["suffix_modular_rank"] + answer=engine["pair"](prefix,suffix_basis,deadline) + if answer: + assert engine["compose"](answer["a"],P)==answer["c"] + assert engine["compose"](answer["b"],S)==answer["d"] + assert answer["c"].keys()<=cohort and answer["d"].keys()<=cohort + assert engine["dot"](answer["a"],answer["b"])==engine["dot"](answer["c"],answer["d"])==1 + counts=(sum(bool(x) for _,x in prefix),sum(bool(x) for _,x in suffix_basis)) + status="exact_unit_pair" if answer else ( + "no_nonzero_pure_prefix" if not counts[0] else "no_nonzero_pure_suffix" if not counts[1] else "no_exact_unit_pair") + entry=dict(key=bank["key"],public=bank["public"],owned=bank["owned"],pivots=bank["pivots"], + prefix_rank=pre_rank,suffix_rank=suf_rank,prefix_nullity=len(prefix),suffix_nullity=len(suffix_basis), + nonzero_prefix_basis_images=counts[0],nonzero_suffix_basis_images=counts[1], + prefix_rank_mod_65521=bank["exterior_rank"],suffix_rank_mod_65537=bank["suffix_modular_rank"], + status=status) + if answer: + for name in ("a","b"): + answer[name]={bank["public"][j]:v for j,v in answer[name].items()} + entry["physical_coefficient_preflight"]=engine["physical_screen"](answer,bank["pivots"]) + entry["witness"]={k:{j:str(v) for j,v in row.items()} for k,row in answer.items()} + results.append(entry) + except TimeoutError as exc: + timeout=str(exc) + finally: + alarm(0) + print(dumps(dict(head=HEAD,input_sha256=PINS|{"selection":args.selection_sha}, + case_cap=6,runner_cap_seconds=35,controls=checks,results=results, + modular_drops_outside_exact_scope=1465-len(selected), + unresolved=[r["key"] for r in selected[len(results):]],timeout=timeout, + counts=dict(Counter(r["status"] for r in results))),indent=2,sort_keys=True)) + if timeout: + raise SystemExit(2) + + +if __name__=="__main__": + main() diff --git a/research/p104-rank-four-five-bank-bound/engines/r89/exact_primary.py b/research/p104-rank-four-five-bank-bound/engines/r89/exact_primary.py new file mode 100644 index 0000000000..cb1fedb219 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/r89/exact_primary.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": "27a14af96296f0f2d162c77aa38e4051f3aaf8a8156dd654b414dd1196a6d597", + "inputs/PRICE.json": "b4bf8e00a8289f03b1da731fb3ab563a771d88d875e0da73acf70954df2f2c56", + "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["inputs/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, _ = solve["initial_groups"](word) + assert set(price["endpoint_cohort"]) == cohort + controls = solve["controls"]() + banks = {r["key"][0]: r["public"] for r in select["selected"]} + assert len(banks) == 6 and all(not r["owned"] for r in select["selected"]) + 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=6,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-four-five-bank-bound/engines/r89/freeze.py b/research/p104-rank-four-five-bank-bound/engines/r89/freeze.py new file mode 100644 index 0000000000..c7616cc120 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/r89/freeze.py @@ -0,0 +1,101 @@ +"""Freeze the R87 unresolved public-bank keys without decoding the native word.""" +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +import json +from pathlib import Path +import sys + +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +PINS = { + "inputs/PRICE.json": "b4bf8e00a8289f03b1da731fb3ab563a771d88d875e0da73acf70954df2f2c56", + "inputs/GEOMETRY.json": "238135413a5646cb39b34dd65dad73b3032f28352f114da9d67b854ffff39250", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "lead/RESULT.json": "a3505dd0cfd3ee9e242f804e12e3c4705ea6548080d537f597cec355f358e92c", + "lead/SELECTION.json": "a4877749084f276d00917c137fda2b2593894daca1e10629a4a27de7914b4574", + "lead/EXACT.json": "6c89dc61732e9f3dd0bd6bf7b3653c0aae555543959919b6955c3d49e8caf3c6", +} + + +def unique(pairs): + result = dict(pairs) + if len(result) != len(pairs): + raise ValueError("duplicate JSON key") + return result + + +def checked(root, path): + raw = (root / path).read_bytes() + if sha256(raw).hexdigest() != PINS[path]: + raise ValueError(f"changed dependency: {path}") + if path.endswith(".gz"): + return None + return json.loads(raw, object_pairs_hook=unique) + + +def price_at_cap(one_split, count): + base_lo, base_hi = map(Fraction, one_split["old_complete_margin"]) + credit_lo, credit_hi = map(Fraction, one_split["gross_credit"]) + return {"gross_ceiling": str(count * credit_hi), + "complete_margin_upper": str(base_hi + count * credit_hi), + "one_edit_credit": list(map(str, (credit_lo, credit_hi))), + "old_margin": list(map(str, (base_lo, base_hi)))} + + +def main(): + root = Path(sys.argv[1]) + prior = {path: checked(root, path) for path in PINS} + price, geom = prior["inputs/PRICE.json"], prior["inputs/GEOMETRY.json"] + primary = prior["lead/RESULT.json"] + selection, exact = prior["lead/SELECTION.json"], prior["lead/EXACT.json"] + assert all(r["head"] == HEAD for r in (price, geom, primary, exact)) + assert geom["price_sha256"] == PINS["inputs/PRICE.json"] + assert price["word_sha256"] == PINS["inputs/7334-WORD.json.gz"] + assert primary["pins"]["inputs/GEOMETRY.json"] == PINS["inputs/GEOMETRY.json"] + assert selection["modular_sha256"] == PINS["lead/RESULT.json"] + assert exact["pins"]["lead/SELECTION.json"] == PINS["lead/SELECTION.json"] + assert primary["status"] == "EXHAUSTED" and not primary["unvisited"] + assert len(primary["results"]) == 4183 + assert [r["key"] for r in primary["results"]] == geom["unvisited_keys"] + drops = [r for r in primary["results"] if r["disposition"] == "rank drop"] + assert len(drops) == 2134 and [r["key"] for r in drops] == primary["rank_drops"] + assert exact["counts"] == {"no nonzero pure suffix": 4, "no unit pairing": 2} + assert not exact["selected_unresolved"] + earlier = {tuple(r["key"]) for r in exact["results"]} + assert len(earlier) == 6 and earlier == {tuple(r["key"]) for r in selection["selected"]} + remaining = [r for r in drops if tuple(r["key"]) not in earlier] + assert len(remaining) == len({tuple(r["key"]) for r in remaining}) == 2128 + assert [r["key"] for r in remaining] == selection["unselected"] == exact["unselected"] + allowed = set(price["endpoint_cohort"]) + assert len(allowed) == 615 + for r in remaining: + assert r["pivots"] and set(r["pivots"]) == set(r["public"]) & allowed + pivots = sorted({r for case in remaining for r in case["pivots"]}) + count = min(price["cohort_cap"], len(pivots)) + receipt = { + "head": HEAD, + "source_sha256": PINS, + "scope": "public cochart basis with unchanged paid itinerary; same chart-3 to chart-127 endpoint cohort", + "cases": len(remaining), + "charts": len({r["key"][1] for r in remaining}), + "cuts": len({r["key"][0] for r in remaining}), + "bank_size_histogram": dict(sorted(Counter(len(r["public"]) for r in remaining).items())), + "presence_of_unmodified_owned_rows": sum(bool(r["owned"]) for r in remaining), + "possible_literal_pivots": pivots, + "one_split_per_literal_pivot_cap": count, + "at_incumbent": price_at_cap(price["one_split"], count), + "at_moonshot": price_at_cap(price["one_split_at_moonshot"], count), + "moonshot_target": price["moonshot"], + "moonshot_minimum_edits_necessary": price["moonshot_minimum_edits_necessary"], + "reverse_case_cap": 2128, + "reverse_runner_seconds_cap": 35, + "exact_case_cap": 6, + "exact_runner_seconds_cap": 35, + "keys": remaining, + "controls": exact["results"], + } + print(json.dumps(receipt, separators=(",", ":"), sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-four-five-bank-bound/engines/r89/rank_pairs.py b/research/p104-rank-four-five-bank-bound/engines/r89/rank_pairs.py new file mode 100644 index 0000000000..6d1b375d6d --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/r89/rank_pairs.py @@ -0,0 +1,157 @@ +"""Rank, without excluding, the banks that dropped on both sides.""" +from collections import 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 + +SUFFIX_RESULT = "340d1beb37477198e4690a56153d1a225c8ad70e00cf470c07a5bc080c0255ad" +SUFFIX_ENGINE = "751d5d0c4c665c8768ff69bcf939700d3be2f989c59f09af3a4aa14d3c1ebbc4" + + +def checked(path, want): + raw = path.read_bytes() + if sha256(raw).hexdigest() != want: + raise ValueError(f"changed dependency: {path.name}") + return raw + + +def exterior_kernel(roles, vectors, cohort, prime, plus): + basis, kernel = [], [] + for role in roles: + row, weights = vectors[role].copy(), {role: 1} + for pivot, old_row, old_weights in basis: + amount = -row.get(pivot, 0) + plus(row, old_row, amount) + plus(weights, old_weights, amount) + exterior = row.keys() - cohort + if not exterior: + kernel.append((weights, row)) + continue + pivot = min(exterior) + inverse = pow(row[pivot], -1, prime) + basis.append((pivot, {k: v * inverse % prime for k, v in row.items()}, + {k: v * inverse % prime for k, v in weights.items()})) + return kernel + + +def dot(a, b, prime): + return sum(v * b.get(k, 0) for k, v in a.items()) % prime + + +def independent(b, d, prime): + pivot = next((i for i, value in enumerate(d) if value), None) + if pivot is None: + return any(b) + return any((value * d[pivot] - other * b[pivot]) % prime + for value, other in zip(b, d, strict=True)) + + +def pair_class(prefix, suffix, prime, plus): + b_rows = [[dot(c, d, prime) for _, d in suffix] for _, c in prefix] + d_rows = [[(dot(a, b, prime) - value) % prime + for (b, _), value in zip(suffix, row, strict=True)] + for (a, _), row in zip(prefix, b_rows, strict=True)] + direct = [sum(map(len, (a, b, c, d))) for i, (a, c) in enumerate(prefix) + for j, (b, d) in enumerate(suffix) if b_rows[i][j] and not d_rows[i][j]] + if direct: + return 0, min(direct) + # A nonzero wedge is witnessed by a basis vector or a sum of two. + for i, (br, dr) in enumerate(zip(b_rows, d_rows, strict=True)): + if independent(br, dr, prime): + return 1, 0 + for j in range(i): + bs = [(x + y) % prime for x, y in zip(br, b_rows[j], strict=True)] + ds = [(x + y) % prime for x, y in zip(dr, d_rows[j], strict=True)] + if independent(bs, ds, prime): + return 1, 0 + width = len(suffix) + joint = {i: {j: v for j, v in enumerate(d_rows[i] + b_rows[i]) if v} + for i in range(len(prefix))} + # In the proportional case, only xD=0 and xB nonzero can work. + kernel = exterior_kernel(list(joint), joint, set(range(width, 2 * width)), prime, plus) + return (1, 0) if any(image for _, image in kernel) else (2, 0) + + +def forward_event(event, rows, scalar, plus, prime): + op, dst, *args = event + if op == "INIT": + rows[dst] = {} + elif op == "CLEAR": + rows[dst] = None + elif op == "SCALE": + factor = scalar(args[0]) + rows[dst] = {k: factor * v % prime for k, v in rows[dst].items() if factor * v % prime} + elif op in ("COPY", "ADD"): + if op == "COPY": + assert not rows[dst] + plus(rows[dst], rows[args[0]], scalar(args[1])) + else: + assert op == "MOVE" + + +def main(): + assert __debug__ + deadline = monotonic() + 30 + root = Path(sys.argv[1]) + checked(root / "lead/suffix_sweep.py", SUFFIX_ENGINE) + reverse = run_path(str(root / "lead/suffix_sweep.py")) + raw = reverse["authenticated"](root) + engine = run_path(str(root / "inputs/exterior_minor.py")) + unique, scalar, plus, prime = (engine[k] for k in ("unique", "scalar", "plus", "P")) + word = json.loads(decompress(raw["inputs/7334-WORD.json.gz"]), object_pairs_hook=unique) + price = json.loads(raw["inputs/PRICE.json"], object_pairs_hook=unique) + suffix_receipt = json.loads(checked(root / "lead/RESULT.json", SUFFIX_RESULT), object_pairs_hook=unique) + assert suffix_receipt["status"] == "EXHAUSTED" and not suffix_receipt["unvisited"] + assert suffix_receipt["head"] == price["head"] == reverse["HEAD"] + banks = [row for row in suffix_receipt["results"] if row["disposition"] == "rank drop"] + assert len(banks) == 1465 + assert pair_class([({0: 1}, {3: 1})], [({0: 1}, {3: 1})], prime, plus) == (0, 4) + assert pair_class([({0: 1}, {3: 1})], [({0: 2}, {3: 1})], prime, plus) == (2, 0) + cohort = set(price["endpoint_cohort"]) + public = word["public"] + tape = word["program"] + requests = defaultdict(list) + for row in banks: + requests[row["key"][0]].append(row) + rows = [{i: 1} for i in range(public)] + [None] * word["owned_fields"] + prefixes, results = {}, {} + for cut in range(len(tape) + 1): + if (cut % 128 == 0 or cut in requests) and monotonic() >= deadline: + break + for row in requests.get(cut, ()): + key = tuple(row["key"]) + prefix = exterior_kernel(row["public"], rows, cohort, prime, plus) + assert len(prefix) == len(row["public"]) - row["prefix_rank_mod_65521"] + prefixes[key] = prefix + if cut < len(tape): + forward_event(tape[cut], rows, scalar, plus, prime) + active = word["final"] + [None] * word["owned_fields"] + columns = [{i: 1} for i in range(public)] + [None] * word["owned_fields"] + for cut in range(len(tape), -1, -1): + if (cut % 128 == 0 or cut in requests) and monotonic() >= deadline: + break + for row in requests.get(cut, ()): + key = tuple(row["key"]) + if key not in prefixes: + continue + suffix = exterior_kernel(row["public"], columns, cohort, prime, plus) + assert len(suffix) == len(row["public"]) - row["suffix_rank_mod_65521"] + kind, terms = pair_class(prefixes[key], suffix, prime, plus) + results[key] = {**row, "pair_class": kind, "direct_terms": terms} + if cut: + reverse["reverse_event"](tape[cut - 1], active, columns, public, scalar, plus, prime) + records = [results[tuple(row["key"])] for row in banks if tuple(row["key"]) in results] + print(json.dumps({"head": price["head"], "prime": prime, "cases_cap": 1465, "seconds_cap": 30, + "controls": ["planted unit pair", "wrong local pairing"], + "cases": len(records), "modular_pairs": sum(r["pair_class"] < 2 for r in records), + "unvisited": [row["key"] for row in banks if tuple(row["key"]) not in results], + "results": records, "input_sha256": {"suffix_result": SUFFIX_RESULT, "suffix_engine": SUFFIX_ENGINE}}, + separators=(",", ":"), sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-four-five-bank-bound/engines/r89/reverse_suffix.py b/research/p104-rank-four-five-bank-bound/engines/r89/reverse_suffix.py new file mode 100644 index 0000000000..9589a02cc4 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/r89/reverse_suffix.py @@ -0,0 +1,312 @@ +"""Independent reverse suffix rank on the 2,128 frozen R89 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 + +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +PRIME = 65537 +PINS = { + "keys": "a131ec5bf96baac89f0f6623cf7d9dff06601b36ea720474311ee7ecb394f6e2", + "price": "b4bf8e00a8289f03b1da731fb3ab563a771d88d875e0da73acf70954df2f2c56", + "word": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", +} +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PROTECTED = {319,863,1355,1568} + + +def unique(pairs): + result = dict(pairs) + if len(result) != len(pairs): + raise ValueError("Duplicate JSON key") + return result + + +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 scalar(value): + q = Fraction(value) + if q.denominator % PRIME == 0: + raise ValueError("Nonunit native denominator") + assert q + return q.numerator * pow(q.denominator, -1, PRIME) % PRIME, q.denominator + + +def add(target, other, coefficient): + if not coefficient: + return + for i,v in other.items(): + x = (target.get(i,0)+coefficient*v) % PRIME + if x: + target[i]=x + else: + target.pop(i,None) + + +def scale(row, coefficient): + return {i:x for i,v in row.items() if (x:=v*coefficient%PRIME)} + + +def column_rank(bank, suffix): + """Eliminate columns over live role coordinates and retain the original minor.""" + n = len(bank) + columns = defaultdict(dict) + for row, role in enumerate(bank): + for output, coefficient in suffix[role].items(): + columns[output][row]=coefficient + echelon = [] + used = [] + determinant = 1 + for output in sorted(columns,reverse=True): + column=columns[output].copy() + for pivot,inverse,earlier in echelon: + add(column,earlier,-column.get(pivot,0)*inverse) + if not column: + continue + pivot=max(column) + diagonal=column[pivot] + echelon.append((pivot,pow(diagonal,-1,PRIME),column)) + used.append(output) + determinant=determinant*diagonal%PRIME + if len(echelon)==n: + break + rank=len(echelon) + rows=[bank[p] for p,_,_ in echelon] + if rank=n + columns[d]={} + return (d,),None + if op=="MOVE": + return (),None + coefficient,denom=scalar(args[-2]) + if op=="SCALE": + columns[d]=scale(columns[d],coefficient) + return (d,),denom + assert op in ("ADD","COPY") and args[0]!=d + s=args[0] + add(columns[s],columns[d],coefficient) + if op=="COPY": + assert d>=n + columns[d]={} + return (s,d),denom + return (s,),denom + + +def controls(): + assert all(PRIME%d for d in range(2,isqrt(PRIME)+1)) + full=column_rank([5,7],{5:{2:2,8:3},7:{2:5,8:7}}) + assert full["minor_exterior_output_columns"]==[8,2] and full["minor_role_rows"]==[7,5] + assert full["minor_determinant_mod_prime"]==PRIME-1 + deficient=column_rank([5,7],{5:{2:2,8:3},7:{2:4,8:6}}) + assert deficient["suffix_exterior_rank"]==1 and deficient["status"]=="modular_suffix_rank_drop" + tape=[["INIT",3,0],["COPY",3,1,"-3/2",0],["ADD",0,3,"1",0], + ["SCALE",1,"2/5",0],["CLEAR",3,0]] + columns=[{0:1},{1:1},{2:1},{}] + for event in reversed(tape): + reverse_event(event,columns,3) + assert columns==[{0:1},{0:scalar("-3/2")[0],1:scalar("2/5")[0]},{2:1},{}] + try: + scalar("1/65537") + except ValueError: + pass + else: + raise AssertionError("Nonunit denominator was admitted") + return ["column_order_determinant","planted_suffix_rank_drop","signed_COPY_ADD_SCALE_CLEAR_adjoint", + "nonunit_denominator_rejected"] + + +def admission(keys, price): + assert keys["head"]==price["head"]==HEAD + assert keys["source_sha256"]["inputs/PRICE.json"]==PINS["price"] + assert keys["source_sha256"]["inputs/7334-WORD.json.gz"]==price["word_sha256"]==PINS["word"] + assert keys["reverse_case_cap"]==keys["cases"]==2128 and keys["reverse_runner_seconds_cap"]==35 + new={tuple(r["key"]):r for r in keys["keys"]} + known={tuple(r["key"]):r for r in keys["controls"]} + assert len(new)==len(keys["keys"])==2128 and len(known)==len(keys["controls"])==6 + assert not new.keys() & known.keys() + assert all(r["disposition"]=="rank drop" for r in new.values()) + assert len({t for t,c in new})==2128 and len({c for t,c in new})==27 + assert {p for r in new.values() for p in r["pivots"]}==set(keys["possible_literal_pivots"]) + assert len(keys["possible_literal_pivots"])==keys["one_split_per_literal_pivot_cap"]==129 + return new,known + + +def sweep(word, cohort, keys, prior, deadline, out, old_out, progress): + n,owned = word["public"],word["owned_fields"] + tape=word["program"] + assert (n,owned,len(tape))==(1501,68,76466) + mains=set(word["live"])|{r+112 for r in word["live"]} + mains.update(word["hosted"]["X2"],word["hosted"]["Y2"]) + assert cohort=={i for i,az in enumerate(zip(word["initial"],word["final"],strict=True)) + if az==(3,127) and i not in mains|PROTECTED} + assert len(cohort)==615 + frames=word["frames"] + + @cache + def space(chart): + span={0} + for v in frames[chart]: + assert v not in span + span.update(v^x for x in tuple(span)) + return span + + requests=defaultdict(list) + for t,c in [*keys,*prior]: + assert len(frames[c]) in (4,5) and space(3)=deadline: + raise TimeoutError("bounded suffix replay") + for c in requests.get(t,()): + k=t,c + pinned=keys[k] if k in keys else prior[k] + roles=sorted(banks[c]) + public=[r for r in roles if r=n] + pivots=sorted(set(public)&cohort) + assert public==pinned["public"] and owner==pinned["owned"] and pivots==pinned["pivots"] + assert pivots + if t: + event=tape[t-1] + incident=event[2:4] if event[0]=="MOVE" else event[-1:] + assert c in incident + signature=tuple((r,revision[r]) for r in public) + if signature not in rank_cache: + rank_cache[signature]=column_rank(public,suffix) + result=dict(key=list(k),chart_rank=len(frames[c]),public=public,owned=owner,pivots=pivots, + **rank_cache[signature]) + if k in prior: + expected=len(public)-pinned["pure_suffix_dimension"] + result["prior_exact_suffix_rank"]=expected + old_out[k]=result + else: + out[k]=result + if not t: + break + event=tape[t-1] + op,d,*args=event + if op=="MOVE": + a,b,is_owned=args + assert states[d]==b and is_owned==(d>=n) + assert space(a)=n and states[d]==chart + states[d]=None + banks[chart].remove(d) + elif op=="CLEAR": + chart=args[0] + assert d>=n and states[d] is None and not suffix[d] + states[d]=chart + banks[chart].add(d) + else: + chart=args[-1] + assert states[d]==chart and op in ("ADD","COPY","SCALE") + if op!="SCALE": + assert states[args[0]]==chart + changed,denominator=reverse_event(event,suffix,n) + for r in changed: + revision[r]+=1 + if denominator is not None: + denoms.add(denominator) + assert states==list(word["initial"])+[None]*owned and not any(suffix[n:]) + assert dict(histogram)=={1:4000,2:853,3:829,4:223,5:345,6:14,7:10,8:5} + progress.update(first_unvisited_reverse_event=None,events_replayed=len(tape), + denominator_units=sorted(denoms),native_paid_histogram=dict(histogram), + distinct_suffix_exterior_row_sets=len(rank_cache)) + + +def main(): + parser=ArgumentParser(description=__doc__) + for n in PINS: + parser.add_argument("--"+n,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,n) for n in PINS): + parser.error("Require all three pinned input paths") + + def stop(*_): + raise TimeoutError("hard 35-second cap") + + checks=[] + keys,prior,results,prior_results,progress={},{},{},{},{} + interruption=None + signal(SIGALRM,stop) + alarm(35) + deadline=monotonic()+33 + try: + checks=controls() + document=checked(args.keys,"keys") + price=checked(args.price,"price") + keys,prior=admission(document,price) + word=checked(args.word,"word") + sweep(word,set(price["endpoint_cohort"]),keys,prior,deadline,results,prior_results,progress) + except TimeoutError as error: + interruption=str(error) + finally: + alarm(0) + rows=[results[k] for k in keys if k in results] + olds=[prior_results[k] for k in prior if k in prior_results] + unvisited=[list(k) for k in keys if k not in results] + control_unvisited=[list(k) for k in prior if k not in prior_results] + control_discrepancies=[r["key"] for r in olds if r["suffix_exterior_rank"]!=r["prior_exact_suffix_rank"]] + drops=[r["key"] for r in rows if r["status"]=="modular_suffix_rank_drop"] + print(dumps(dict(head=HEAD,pins=PINS,prime=PRIME,case_cap=2128,runner_cap_seconds=35, + controls=checks,prior_exact_controls=olds,control_unvisited=control_unvisited, + control_discrepancies=control_discrepancies,tested=rows,unvisited=unvisited,suffix_rank_drops=drops, + status_counts=dict(Counter(r["status"] for r in rows)),timeout=interruption,**progress), + indent=2,sort_keys=True)) + if interruption or control_unvisited or control_discrepancies: + raise SystemExit(2) + + +if __name__=="__main__": + main() diff --git a/research/p104-rank-four-five-bank-bound/engines/r89/select.py b/research/p104-rank-four-five-bank-bound/engines/r89/select.py new file mode 100644 index 0000000000..6a0e3e485f --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/r89/select.py @@ -0,0 +1,31 @@ +"""Freeze six deterministic rational checks from the bounded modular ranking.""" +from hashlib import sha256 +import json +from pathlib import Path +import sys + +PIN = "4b8f2963ae0ef7bd357c3129e8287f79c5c1fccca6375c41e35fa01c476cb2ae" + +root = Path(sys.argv[1]) +raw = (root / "lead/PAIR.json").read_bytes() +if sha256(raw).hexdigest() != PIN: + raise ValueError("changed pair-priority receipt") +receipt = json.loads(raw) +assert receipt["cases"] == 1465 and not receipt["unvisited"] +records = receipt["results"] +selected, clocks, charts = [], set(), set() +for row in sorted(records, key=lambda r: (r["pair_class"] == 2, bool(r["owned"]), + r["pair_class"], r["direct_terms"], len(r["public"]) - len(r["pivots"]), r["key"])): + cut, chart = row["key"] + if cut in clocks or chart in charts: + continue + selected.append(row) + clocks.add(cut) + charts.add(chart) + if len(selected) == 6: + break +assert len(selected) == 6 and not any(r["owned"] for r in selected) +used = {tuple(r["key"]) for r in selected} +print(json.dumps({"pair_sha256": PIN, "case_cap": 6, "seconds_cap": 35, + "selected": selected, "unselected": [r["key"] for r in records if tuple(r["key"]) not in used]}, + indent=2, sort_keys=True)) diff --git a/research/p104-rank-four-five-bank-bound/engines/r89/suffix_sweep.py b/research/p104-rank-four-five-bank-bound/engines/r89/suffix_sweep.py new file mode 100644 index 0000000000..ebfc82f83f --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/r89/suffix_sweep.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-four-five-bank-bound/engines/rolling_exterior.py b/research/p104-rank-four-five-bank-bound/engines/rolling_exterior.py new file mode 100644 index 0000000000..621640c40a --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/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-four-five-bank-bound/engines/select_six.py b/research/p104-rank-four-five-bank-bound/engines/select_six.py new file mode 100644 index 0000000000..8c8f08f721 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/engines/select_six.py @@ -0,0 +1,40 @@ +"""Freeze six exact continuations from the modular rank drops.""" +from hashlib import sha256 +from pathlib import Path +import json +import sys + +PIN = "a3505dd0cfd3ee9e242f804e12e3c4705ea6548080d537f597cec355f358e92c" +root = Path(sys.argv[1]) +raw = (root/"lead/RESULT.json").read_bytes() +if sha256(raw).hexdigest() != PIN: + raise ValueError("changed modular support receipt") +d = json.loads(raw) +assert d["status"] == "EXHAUSTED" and d["counts"]["rank drop"] == 2134 +rank_drops = [r for r in d["results"] if r["disposition"] == "rank drop"] + + +def priority(r): + return (bool(r["owned"]), len(r["pivots"]) < 2, + len(r["public"]) - len(r["pivots"]), + r["exterior_rank"] - len(r["public"]), + -len(r["pivots"]), -r["key"][0], r["key"][1]) + + +selected, charts, clocks = [], set(), set() +for row in sorted(rank_drops, key=priority): + t, c = row["key"] + if c in charts or t in clocks: + continue + selected.append(row) + charts.add(c) + clocks.add(t) + if len(selected) == 6: + break +assert len(selected) == 6 +used = {tuple(r["key"]) for r in selected} +print(json.dumps(dict(modular_sha256=PIN, exact_cap=6, exact_seconds_cap=35, + ordered_score="no owned, >=2 pivots, fewest external roles, greatest nullity, most pivots, later cut, chart", + diversification="one cut per chart and one chart per cut", + selected=selected, unselected=[r["key"] for r in rank_drops if tuple(r["key"]) not in used]), + indent=2, sort_keys=True)) diff --git a/research/p104-rank-four-five-bank-bound/inputs/7334-WORD.json.gz b/research/p104-rank-four-five-bank-bound/inputs/7334-WORD.json.gz new file mode 100644 index 0000000000..73f4300719 Binary files /dev/null and b/research/p104-rank-four-five-bank-bound/inputs/7334-WORD.json.gz differ diff --git a/research/p104-rank-four-five-bank-bound/inputs/paired_rank.py b/research/p104-rank-four-five-bank-bound/inputs/paired_rank.py new file mode 100644 index 0000000000..b712cdb1f8 --- /dev/null +++ b/research/p104-rank-four-five-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-four-five-bank-bound/inputs/paired_support.py b/research/p104-rank-four-five-bank-bound/inputs/paired_support.py new file mode 100644 index 0000000000..46180f7b49 --- /dev/null +++ b/research/p104-rank-four-five-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-four-five-bank-bound/price/inputs/ADMITTED.json b/research/p104-rank-four-five-bank-bound/price/inputs/ADMITTED.json new file mode 100644 index 0000000000..464c89e45c --- /dev/null +++ b/research/p104-rank-four-five-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-four-five-bank-bound/price/inputs/PR7338-SHA256.json b/research/p104-rank-four-five-bank-bound/price/inputs/PR7338-SHA256.json new file mode 100644 index 0000000000..8a4d2a0cf3 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/price/inputs/PR7338-SHA256.json @@ -0,0 +1,19 @@ +{ + "BANK-INDEPENDENT.json": "16563e927ec1c1ec783f92862fe4b8027e8daab35ba80b1607e10c26c3bc28ee", + "BANK.json": "ac659b807f526dfb79f9bb173c3861bc743f112a7f40bc42a8b5dc57f48a058d", + "GEOMETRY-68.json": "ce9604444161b3532d02eb788cb3a24fbbdaf4c1354d596ac08a2c9edeb72c76", + "GEOMETRY-69.json": "a2dd10737f5bfbd3818e6766df3890e445fd46f661af9521f5d724b7c56c1d45", + "GEOMETRY-CONTROL.json": "df4175b6cee565ba0792a3207dee5ebd1c31868a441a276de68bf75536a089d6", + "RANK-STOCK.json": "4a7841699dd17688f6aada5c902a2a91e94558b2b1b4460c46b0e55aa95b3f9f", + "READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "RELAXED-COMPARE.json": "23b9a5c0e5507db1bdc2cd39fc7422216bf68b0dd0dbc1e78d315ae25dfe4926", + "RELAXED-INDEPENDENT.json": "dc227ae7aca5f470f148db76a32304ed21c6d4143af3a1d0e7cfd6947856edfb", + "RELAXED.json": "34738b6d9031b3170a58f0cb590d81c01ea2c1038810008483d1c24dc7574150", + "RETIME-KNOWN.json": "08402221016a0a7ed0b2716b3ab1c8de4afcf54158c381ca441320b71b8abac4", + "RETIME-SYNTHETIC.json": "fe9e20a455b87fc43843b221ac061652d2fd2af2c11de2e7b3c9323cc0e883fe", + "STRICT-68.json": "471d5c8f1cb87e1c054b6ea376f4f083f9bac76eabc5823811484f0ed30357b3", + "STRICT-69.json": "bd4c2284ec073e8c3e565350e868595d09098f7ab8347eef440343964f6dbac5", + "STRICT-COMPARE-69.json": "f6538af89286b5e3805f6ed4494e2df095ce62d114c814ae7cdfe820a655a08c", + "STRICT-INDEPENDENT-68.json": "3d9ec5a87d71bc1f669ea8d02591b3fa2d4db282bfc47d3af72335cd57e42587", + "STRICT-INDEPENDENT-69.json": "1eddd0476a4caff1ef6423458f88471f1ce07adcd119171714c9261f8d9d7387" +} diff --git a/research/p104-rank-four-five-bank-bound/price/inputs/PR7339-SHA256.json b/research/p104-rank-four-five-bank-bound/price/inputs/PR7339-SHA256.json new file mode 100644 index 0000000000..585b9a98d2 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/price/inputs/PR7339-SHA256.json @@ -0,0 +1,12 @@ +{ + "FIRST-RANK.json": "5529a4338efed76989d113100eed30a46bc15c572ab55a58020e8eab423f9143", + "FIRST-SUPPORT.json": "d90ce338aab69c0c074f72e2e91e2eaa04fd347ea6cded83237d0996af327f98", + "GEOMETRY-COMPARE.json": "0217f80d0aafdc9fa8f281bf725ff68ba2952b68b19e6ab5b3fee802000ed97c", + "OCCUPANCY.json": "4c349e06b22bfebb431fab1c9ae04f0e798f398acc6fdd99591b49b1c95ef6ca", + "PRICE.json": "b3c36d5a1d199a1e74f979d660fac295c55659a9d4edb70eaef541095670323b", + "RECONCILED.json": "3a4b86b169fcac7ef447dda2a819ea07fe7957f6fc859b035246d6ac55128444", + "REMAINING-RANK.json": "9b06f7b2e17e6d46fa811e05ab7e0fcc45ff5ecd98cacecb8617b662142a6ddc", + "REMAINING-SUPPORT.json": "8ef9be1998d67edf665fc9be07b96e00157f17e86f22f87038ec3b84aa3334ba", + "REVERSE.json": "587739d21541e7ffe01af9cb7e51abaa757ee69b580befe8bb768a81b614aa08", + "SELECTION.json": "d68ce20cabfd2262aec3925d6b055dcc9ffa08d125e694401760c1ffab5d899a" +} diff --git a/research/p104-rank-four-five-bank-bound/price/inputs/R72-OCCUPANCY.json.gz b/research/p104-rank-four-five-bank-bound/price/inputs/R72-OCCUPANCY.json.gz new file mode 100644 index 0000000000..91d032cb6f Binary files /dev/null and b/research/p104-rank-four-five-bank-bound/price/inputs/R72-OCCUPANCY.json.gz differ diff --git a/research/p104-rank-four-five-bank-bound/price/inputs/RANK-STOCK.json b/research/p104-rank-four-five-bank-bound/price/inputs/RANK-STOCK.json new file mode 100644 index 0000000000..7043a8a985 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/price/inputs/RANK-STOCK.json @@ -0,0 +1,538 @@ +{ + "admission": "scientific admission pending at preflight; price is conditional on exact #7334 passing", + "complete_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 + }, + "crossing_upper": "182332597822022395349777014167081/50000000000000000000000000000000000", + "disjoint_move_pair_count_upper": 3116, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "input_sha256": { + "READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "dependencies/7298/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "dependencies/round41/RESULT.json": "1b993aa8c66ffce5d2d9f13cafae320c62230722d599d251fa61afc6534b1bc7", + "receipts/NATIVE-RESULT.json": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812", + "receipts/construct.py": "ecb39578063d7f09153a85370a3b9bb7cbf8b36ff9891033a1cce7a2fe7f7fda" + }, + "old_complete_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 + }, + "old_margin": [ + "-29866980917152322049/10000000000000000000000000000000000000000000000000", + "-29866980917152266101/10000000000000000000000000000000000000000000000000" + ], + "one_edit_optimistic_upper": "1903560515893109741953230020081417399578277511361/5000000000000000000000000000000000000000000000000", + "one_per_public_helper_optimistic_upper": "2095820127998313825890506252109640556935683540008461/5000000000000000000000000000000000000000000000000", + "owned_paid_histogram": { + "1": 20, + "2": 9, + "3": 2, + "4": 13, + "5": 2, + "6": 1 + }, + "public_helper_count": 1101, + "public_paid_histogram": { + "1": 3980, + "2": 844, + "3": 827, + "4": 210, + "5": 343, + "6": 13, + "7": 10, + "8": 5 + }, + "public_paid_moves": 6232, + "rank_prices": { + "1+1": { + "complete_margin": [ + "858321385403521186417773068772405712363430437203/10000000000000000000000000000000000000000000000000", + "53645086587720074151110816798275357022714405823/625000000000000000000000000000000000000000000000" + ], + "credit": [ + "214580346350880296604443267200568173320145689813/2500000000000000000000000000000000000000000000000", + "858321385403521186417773068802272693280582759269/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-9141678614596478813582226931227594287636569562797/10000000000000000000000000000000000000000000000000", + "-571354913412279925848889183201724642977285594177/625000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -34, + "2": 17 + }, + "ranks": [ + 1, + 1 + ] + }, + "1+2": { + "complete_margin": [ + "1180782193580878473879905453225185303784278217059/10000000000000000000000000000000000000000000000000", + "1180782193580878473879905453225185303784278273007/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1180782193580878473879905453255052284701430539091/10000000000000000000000000000000000000000000000000", + "9446257548647027791039243626040418277611444313/80000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-8819217806419121526120094546774814696215721782941/10000000000000000000000000000000000000000000000000", + "-8819217806419121526120094546774814696215721726993/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "2": -17, + "3": 17 + }, + "ranks": [ + 1, + 2 + ] + }, + "1+3": { + "complete_margin": [ + "1389848341449443791535950684381027395734536124509/10000000000000000000000000000000000000000000000000", + "1389848341449443791535950684381027395734536180423/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "347462085362360947883987671102723594162922111631/2500000000000000000000000000000000000000000000000", + "694924170724721895767975342205447188325844223279/5000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-8610151658550556208464049315618972604265463875491/10000000000000000000000000000000000000000000000000", + "-8610151658550556208464049315618972604265463819577/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "3": -17, + "4": 17 + }, + "ranks": [ + 1, + 3 + ] + }, + "1+4": { + "complete_margin": [ + "193142263828747485141280111129765972731137687109/1250000000000000000000000000000000000000000000000", + "772569055314989940565120444519063890924550776427/5000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1545138110629979881130240889067994762766253818921/10000000000000000000000000000000000000000000000000", + "309027622125995976226048177813598952553250763791/2000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-1056857736171252514858719888870234027268862312891/1250000000000000000000000000000000000000000000000", + "-4227430944685010059434879555480936109075449223573/5000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "4": -17, + "5": 17 + }, + "ranks": [ + 1, + 4 + ] + }, + "1+5": { + "complete_margin": [ + "834392976237489866662283238867233696199702541757/5000000000000000000000000000000000000000000000000", + "417196488118744933331141619433616848099851284857/2500000000000000000000000000000000000000000000000" + ], + "credit": [ + "1668785952474979733324566477764334373316557405529/10000000000000000000000000000000000000000000000000", + "1668785952474979733324566477764334373316557405563/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-4165607023762510133337716761132766303800297458243/5000000000000000000000000000000000000000000000000", + "-2082803511881255066668858380566383151900148715143/2500000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "5": -17, + "6": 17 + }, + "ranks": [ + 1, + 5 + ] + }, + "1+6": { + "complete_margin": [ + "1771542005129348740048881099908835681263784441249/10000000000000000000000000000000000000000000000000", + "1771542005129348740048881099908835681263784497197/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1771542005129348740048881099938702662180936763281/10000000000000000000000000000000000000000000000000", + "354308401025869748009776219987740532436187352663/2000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-8228457994870651259951118900091164318736215558751/10000000000000000000000000000000000000000000000000", + "-8228457994870651259951118900091164318736215502803/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "6": -17, + "7": 17 + }, + "ranks": [ + 1, + 6 + ] + }, + "1+7": { + "complete_margin": [ + "1859458789326391366180127207106590253932358169757/10000000000000000000000000000000000000000000000000", + "1859458789326391366180127207106590253932358225739/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "929729394663195683090063603568228617424755245903/5000000000000000000000000000000000000000000000000", + "5810808716644973019312897522301428858904720287/31250000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-8140541210673608633819872792893409746067641830243/10000000000000000000000000000000000000000000000000", + "-8140541210673608633819872792893409746067641774261/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "7": -17, + "8": 17 + }, + "ranks": [ + 1, + 7 + ] + }, + "1+8": { + "complete_margin": [ + "1936286205289343096186514461761692902526099784907/10000000000000000000000000000000000000000000000000", + "1936286205289343096186514461761692902526099840821/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "968143102644671548093257230895779941721626053461/5000000000000000000000000000000000000000000000000", + "484071551322335774046628615447889970860813026739/2500000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-8063713794710656903813485538238307097473900215093/10000000000000000000000000000000000000000000000000", + "-8063713794710656903813485538238307097473900159179/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "8": -17, + "9": 17 + }, + "ranks": [ + 1, + 8 + ] + }, + "2+2": { + "complete_margin": [ + "342461829925360215799616613766761397431076780873/2000000000000000000000000000000000000000000000000", + "856154574813400539499041534416903493577691980131/5000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1712309149626801078998083068863673968072536226363/10000000000000000000000000000000000000000000000000", + "856154574813400539499041534431836984036268113207/5000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-1657538170074639784200383386233238602568923219127/2000000000000000000000000000000000000000000000000", + "-4143845425186599460500958465583096506422308019869/5000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -34, + "4": 17 + }, + "ranks": [ + 2, + 2 + ] + }, + "2+3": { + "complete_margin": [ + "1038332533337951243124209252323374732610103592089/5000000000000000000000000000000000000000000000000", + "2076665066675902486248418504646749465220207240109/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "2076665066675902486248418504676616446137359506193/10000000000000000000000000000000000000000000000000", + "519166266668975621562104626169154111534339876561/2500000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-3961667466662048756875790747676625267389896407911/5000000000000000000000000000000000000000000000000", + "-7923334933324097513751581495353250534779792759891/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -17, + "3": -17, + "5": 17 + }, + "ranks": [ + 2, + 3 + ] + }, + "2+4": { + "complete_margin": [ + "2355602677701438428037034298000189461885076143183/10000000000000000000000000000000000000000000000000", + "1177801338850719214018517149000094730942538099557/5000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1177801338850719214018517149015028221401114232599/5000000000000000000000000000000000000000000000000", + "2355602677701438428037034298030056442802228465249/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-7644397322298561571962965701999810538114923856817/10000000000000000000000000000000000000000000000000", + "-3822198661149280785981482850999905269057461900443/5000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -17, + "4": -17, + "6": 17 + }, + "ranks": [ + 2, + 4 + ] + }, + "2+5": { + "complete_margin": [ + "64550164305020182173891862721772434032493977189/250000000000000000000000000000000000000000000000", + "2582006572200807286955674508870897361299759143457/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1291003286100403643477837254450382171108455704779/5000000000000000000000000000000000000000000000000", + "2582006572200807286955674508900764342216911409609/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-185449835694979817826108137278227565967506022811/250000000000000000000000000000000000000000000000", + "-7417993427799192713044325491129102638700240856543/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -17, + "5": -17, + "7": 17 + }, + "ranks": [ + 2, + 5 + ] + }, + "2+6": { + "complete_margin": [ + "2772679409052218919811235238243020222832712173803/10000000000000000000000000000000000000000000000000", + "346584926131527364976404404780377527854089028721/1250000000000000000000000000000000000000000000000" + ], + "credit": [ + "554535881810443783962247047654577440749972899167/2000000000000000000000000000000000000000000000000", + "1386339704526109459905617619136443601874932247943/5000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-7227320590947781080188764761756979777167287826197/10000000000000000000000000000000000000000000000000", + "-903415073868472635023595595219622472145910971279/1250000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -17, + "6": -17, + "8": 17 + }, + "ranks": [ + 2, + 6 + ] + }, + "2+7": { + "complete_margin": [ + "2937423609212213275948868600095877444095027517461/10000000000000000000000000000000000000000000000000", + "183588975575763329746804287505992340255939223337/625000000000000000000000000000000000000000000000" + ], + "credit": [ + "734355902303053318987217150031436106253044959869/2500000000000000000000000000000000000000000000000", + "2937423609212213275948868600125744425012179839527/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-7062576390787786724051131399904122555904972482539/10000000000000000000000000000000000000000000000000", + "-441411024424236670253195712494007659744060776663/625000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -17, + "7": -17, + "9": 17 + }, + "ranks": [ + 2, + 7 + ] + }, + "3+3": { + "complete_margin": [ + "2564668825570003745693079529156031553835334050633/10000000000000000000000000000000000000000000000000", + "256466882557000374569307952915603155383533410653/1000000000000000000000000000000000000000000000000" + ], + "credit": [ + "2564668825570003745693079529185898534752486372631/10000000000000000000000000000000000000000000000000", + "1282334412785001872846539764592949267376243186341/5000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-7435331174429996254306920470843968446164665949367/10000000000000000000000000000000000000000000000000", + "-743533117442999625430692047084396844616466589347/1000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "3": -34, + "6": 17 + }, + "ranks": [ + 3, + 3 + ] + }, + "3+4": { + "complete_margin": [ + "2946362489249908694206009944683839839364582367373/10000000000000000000000000000000000000000000000000", + "368295311156238586775751243085479979920572802913/1250000000000000000000000000000000000000000000000" + ], + "credit": [ + "736590622312477173551502486178426705070433672347/2500000000000000000000000000000000000000000000000", + "2946362489249908694206009944713706820281734689439/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-7053637510750091305793990055316160160635417632627/10000000000000000000000000000000000000000000000000", + "-881704688843761413224248756914520020079427197087/1250000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "3": -17, + "4": -17, + "7": 17 + }, + "ranks": [ + 3, + 4 + ] + }, + "3+5": { + "complete_margin": [ + "1630341583973160089627948131376151155723919520129/5000000000000000000000000000000000000000000000000", + "3260683167946320179255896262752302311447839096189/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "3260683167946320179255896262782169292364991362273/10000000000000000000000000000000000000000000000000", + "815170791986580044813974065695542323091247840581/2500000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-3369658416026839910372051868623848844276080479871/5000000000000000000000000000000000000000000000000", + "-6739316832053679820744103737247697688552160903811/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "3": -17, + "5": -17, + "8": 17 + }, + "ranks": [ + 3, + 5 + ] + }, + "3+6": { + "complete_margin": [ + "3528183420760683542117844246779527821574533741651/10000000000000000000000000000000000000000000000000", + "1764091710380341771058922123389763910787266898791/5000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1764091710380341771058922123404697401245843031833/5000000000000000000000000000000000000000000000000", + "3528183420760683542117844246809394802491686063717/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-6471816579239316457882155753220472178425466258349/10000000000000000000000000000000000000000000000000", + "-3235908289619658228941077876610236089212733101209/5000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "3": -17, + "6": -17, + "9": 17 + }, + "ranks": [ + 3, + 6 + ] + }, + "4+4": { + "complete_margin": [ + "3415972937126856268850186467409402697562404412621/10000000000000000000000000000000000000000000000000", + "170798646856342813442509323370470134878120223431/500000000000000000000000000000000000000000000000" + ], + "credit": [ + "341597293712685626885018646743926967847955673467/1000000000000000000000000000000000000000000000000", + "3415972937126856268850186467439269678479556734721/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-6584027062873143731149813532590597302437595587379/10000000000000000000000000000000000000000000000000", + "-329201353143657186557490676629529865121879776569/500000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "4": -34, + "8": 17 + }, + "ranks": [ + 4, + 4 + ] + }, + "4+5": { + "complete_margin": [ + "237945064486638717744153752508310488639962668791/625000000000000000000000000000000000000000000000", + "3807121031786219483906460040132967818239402756587/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "3807121031786219483906460040162834799156555022671/10000000000000000000000000000000000000000000000000", + "1903560515893109741953230020081417399578277511361/5000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-387054935513361282255846247491689511360037331209/625000000000000000000000000000000000000000000000", + "-6192878968213780516093539959867032181760597243413/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "4": -17, + "5": -17, + "9": 17 + }, + "ranks": [ + 4, + 5 + ] + } + }, + "scope": "Predecode price only. Pair arithmetic grants all ordinary and physical costs free; each original paid MOVE contributes at most once.", + "whole_move_capacity_optimistic_upper": "477927259198812997685714233883646598515886014070727/625000000000000000000000000000000000000000000000", + "word_git_blob": "73f43007192eb5a38eb5abb591b871df3e52c7cd" +} diff --git a/research/p104-rank-four-five-bank-bound/price/inputs/READBACK.json b/research/p104-rank-four-five-bank-bound/price/inputs/READBACK.json new file mode 100644 index 0000000000..625b508eea --- /dev/null +++ b/research/p104-rank-four-five-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-four-five-bank-bound/price/inputs/pricing.py b/research/p104-rank-four-five-bank-bound/price/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-rank-four-five-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-four-five-bank-bound/price/quote.py b/research/p104-rank-four-five-bank-bound/price/quote.py new file mode 100644 index 0000000000..81ec3a144b --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/price/quote.py @@ -0,0 +1,99 @@ +"""Price a fixed-paid 4+5 split before decoding the exact #7334 word.""" +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +WORD = "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PINS = { + "inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/RANK-STOCK.json": "4a7841699dd17688f6aada5c902a2a91e94558b2b1b4460c46b0e55aa95b3f9f", + "inputs/R72-OCCUPANCY.json": "4c349e06b22bfebb431fab1c9ae04f0e798f398acc6fdd99591b49b1c95ef6ca", + "inputs/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", +} +MOONSHOT = Fraction("0.0040075385047236") + + +def unique(pairs): + result = dict(pairs) + if len(result) != len(pairs): + raise ValueError("Duplicate JSON key") + return result + + +def main(): + documents = {} + for rel, pin in PINS.items(): + raw = (ROOT / rel).read_bytes() + if sha256(raw).hexdigest() != pin: + raise ValueError(f"Changed input {rel}") + if rel.endswith(".json"): + documents[Path(rel).name] = loads(raw, object_pairs_hook=unique) + admitted, stock, occupancy, readback = (documents[name] for name in ( + "ADMITTED.json", "RANK-STOCK.json", "R72-OCCUPANCY.json", "READBACK.json")) + assert admitted["head"] == stock["head"] == occupancy["head"] == readback["head"] == HEAD + assert admitted["exit"] == 0 and admitted["status"] == "independently_reproduced_comparable" + assert len(admitted["stages"]) == 4 and admitted["inputs"]["WORD.json.gz"] == WORD + assert occupancy["pins"]["inputs/7334-WORD.json.gz"] == WORD + assert readback["word_git_blob"] == stock["word_git_blob"] if "word_git_blob" in readback else stock["word_git_blob"] == "73f43007192eb5a38eb5abb591b871df3e52c7cd" + cohort = occupancy["endpoint_cohort"] + assert len(cohort) == len(set(cohort)) == 615 and cohort == sorted(cohort) + assert not set(cohort).intersection({319, 863, 1355, 1568}) + assert stock["old_complete_paid"] == readback["paid"] and stock["complete_targets"] == readback["targets"] + paid, targets = [Counter({int(rank): n for rank,n in readback[key].items()}) for key in ("paid","targets")] + assert (sum(paid.values()), sum(targets.values()), targets[9], readback["copies"]) == (110519, 22461, 10888, 17) + assert not readback["empty_root_credits"] + old = targets.copy() + old.subtract(paid) + assert sum(r*n for r,n in old.items()) == readback["rank_surplus"] == 1424 + k_lo,k_hi = map(Fraction, admitted["crossing"]) + bit = Fraction(readback["bit_premise"]) + assert 0 < k_lo < k_hi == Fraction(stock["crossing_upper"]) < bit < MOONSHOT + math = run_path(str(ROOT/"inputs/pricing.py")) + cost,power,log = (math[key] for key in ("cost","power_bounds","log_bounds")) + delta = {4:17, 5:17, 9:-17} + uniform_derivative_lower = 17 * (power(9,bit)[0]*log(Fraction(9))[0] + - sum(power(r,k_lo)[1]*log(Fraction(r))[1] for r in (4,5))) + assert uniform_derivative_lower > 0 and cost(delta,bit)[1] < 1 + + def scaled(edits, k): + change = {r: edits*n for r,n in delta.items()} + updated = targets.copy() + updated.update(change) + assert min(updated.values()) >= 0 and sum(updated.values()) == 22461+17*edits + signed = updated.copy() + signed.subtract(paid) + assert sum(r*n for r,n in signed.items()) == 1424 + before = cost(old,k) + credit = cost(change,k) + margin = cost(signed,k) + return dict(edits=edits,paid=paid,targets=updated,paid_delta={},target_delta=change, + old_complete_margin=list(map(str,before)),gross_credit=list(map(str,credit)), + complete_margin=list(map(str,margin)),complete_margin_with_one_extra_paid_rank1_upper=str(margin[1]-1)) + + one, whole = (scaled(n,k_hi) for n in (1,len(cohort))) + one_moon, whole_moon = (scaled(n,MOONSHOT) for n in (1,len(cohort))) + assert Fraction(one["complete_margin"][0]) > 0 and Fraction(one["complete_margin_with_one_extra_paid_rank1_upper"]) < 0 + required = (-Fraction(one_moon["old_complete_margin"][1])) // Fraction(one_moon["gross_credit"][1]) + 1 + assert required > 0 + print(dumps(dict(head=HEAD, kappa=admitted["kappa"], word_sha256=WORD, + caller_head=admitted["caller"], caller_sha256=admitted["caller_sha256"], input_sha256=PINS, + old_crossing_lower=str(k_lo), old_crossing_upper=str(k_hi), retained_bit_premise=str(bit), moonshot=str(MOONSHOT), + endpoint_cohort=cohort, cohort_cap=len(cohort), selected_bank_cap=24, build_cap=1, native_copies=17, + old_paid=paid, old_targets=targets, signed_rank_surplus=1424, empty_root_credits=0, + one_split=one, all_distinct_splits_optimistic=whole, one_split_at_moonshot=one_moon, + all_distinct_splits_optimistic_at_moonshot=whole_moon, moonshot_minimum_edits_necessary=int(required), + one_split_uniform_credit_through_bit_upper=str(cost(delta,bit)[1]), + one_split_credit_derivative_lower=str(uniform_derivative_lower), + scope="Fixed paid 4+5 on chart rank 4 or 5 for a chart-3 to chart-127 rank-nine helper. Grant one split per distinct cohort role and all ancillary costs free. Price only, no word decoding or support."), + indent=2,sort_keys=True)) + + +if __name__ == "__main__": + assert __debug__ + main() diff --git a/research/p104-rank-four-five-bank-bound/receipts/SHA256.json b/research/p104-rank-four-five-bank-bound/receipts/SHA256.json new file mode 100644 index 0000000000..0baf2c0f54 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/receipts/SHA256.json @@ -0,0 +1,21 @@ +{ + "independent/COMPARE.json": "3d0d418c317ea43cf10a24ea7fd9b5486f4cc04da05ac12aa1cccf4293964aa2", + "independent/EXACT.json": "f68c7033ed1840704c5b66edb9dc6ad223628c80879b1862796de6735a41b961", + "independent/RESULT.json": "fa35b69613ad4af03eada14f251827464dba0d002f67da085817422ec3351649", + "inputs/R86-PRIOR.json": "60ccc6007510c1125a5dee8612f0a3474c2d7e5c21f931745a58a8d4e2077d7b", + "lead/EXACT.json": "6c89dc61732e9f3dd0bd6bf7b3653c0aae555543959919b6955c3d49e8caf3c6", + "lead/GEOMETRY.json": "238135413a5646cb39b34dd65dad73b3032f28352f114da9d67b854ffff39250", + "lead/R86-RATIONAL.json": "4000abaf88ad7ecb1f76a59b9eb5bafc64d0c3db75e6af159826a4431ca8f884", + "lead/RESULT.json": "a3505dd0cfd3ee9e242f804e12e3c4705ea6548080d537f597cec355f358e92c", + "lead/SELECTION.json": "a4877749084f276d00917c137fda2b2593894daca1e10629a4a27de7914b4574", + "price/PRICE.json": "b4bf8e00a8289f03b1da731fb3ab563a771d88d875e0da73acf70954df2f2c56", + "r89/independent/COMPARE.json": "ca6d9bf4f8eb278e45e30e3b85b5f8de1ac3274df008ca8eb7afcfd5ea0451b2", + "r89/independent/EXACT-COMPARE.json": "66632762d4e9529a5772aea6fb4b2eabe3bea17364b058a1d34fa2a06ab97814", + "r89/independent/EXACT.json": "6821bf1f2df591d076528757fd02ce32e35743557ac33ee8b6a6810f4c81b4a3", + "r89/independent/RESULT.json": "560a22da8219d5ca3d5ec9cb8fa25bdd32f068ca28242cdd4383351dbed82f67", + "r89/lead/EXACT.json": "d2369e9657a8bb99cd07813f354a44e9fb02a74245a2ff188723d295d93ce609", + "r89/lead/PAIR.json": "4b8f2963ae0ef7bd357c3129e8287f79c5c1fccca6375c41e35fa01c476cb2ae", + "r89/lead/RESULT.json": "340d1beb37477198e4690a56153d1a225c8ad70e00cf470c07a5bc080c0255ad", + "r89/lead/SELECTION.json": "27a14af96296f0f2d162c77aa38e4051f3aaf8a8156dd654b414dd1196a6d597", + "r89/price/KEYS.json": "a131ec5bf96baac89f0f6623cf7d9dff06601b36ea720474311ee7ecb394f6e2" +} diff --git a/research/p104-rank-four-five-bank-bound/receipts/UNRESOLVED.json b/research/p104-rank-four-five-bank-bound/receipts/UNRESOLVED.json new file mode 100644 index 0000000000..fffd047a84 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/receipts/UNRESOLVED.json @@ -0,0 +1 @@ +[[32956,117],[32957,117],[33898,114],[33899,114],[33900,114],[33901,114],[33902,114],[33903,114],[33904,114],[33905,114],[33906,114],[33907,114],[33908,114],[33909,114],[33910,114],[33911,114],[33912,114],[33913,114],[33914,114],[33915,114],[33916,114],[33917,114],[33918,114],[33919,114],[33920,114],[33921,114],[33922,114],[33923,114],[33924,114],[33925,114],[33926,114],[33927,114],[33928,114],[33929,114],[33930,114],[33931,114],[33932,114],[33933,114],[33934,114],[33935,114],[33936,114],[33937,114],[33938,114],[33939,114],[33940,114],[33941,114],[33942,114],[33943,114],[33944,114],[33945,114],[33946,114],[33947,114],[33956,114],[33997,114],[33998,114],[33999,114],[34000,114],[34656,114],[35068,1090],[35592,1048],[35593,1048],[35594,1048],[35595,1048],[35596,1048],[35597,1048],[35598,1048],[35599,1048],[35600,1048],[35601,1048],[35602,1048],[35603,1048],[35604,1048],[35605,1048],[35606,1048],[35607,1048],[35608,1048],[35609,1048],[35610,1048],[35611,1048],[35612,1048],[35613,1048],[35614,1048],[35615,1048],[35616,1048],[35617,1048],[35618,1048],[35619,1048],[35620,1048],[35621,1048],[35622,1048],[35623,1048],[35624,1048],[35625,1048],[35626,1048],[35627,1048],[35628,1048],[35680,1031],[35681,1031],[35682,1031],[35683,1031],[35684,1031],[35685,1031],[35686,1031],[35687,1031],[35688,1031],[35689,1031],[35690,1031],[35691,1031],[35692,1031],[35693,1031],[35694,1031],[35695,1031],[35696,1031],[35697,1031],[35698,1031],[35699,1031],[35700,1031],[35701,1031],[35702,1031],[35703,1031],[35704,1031],[35705,1031],[35706,1031],[35707,1031],[35708,1031],[35709,1031],[35710,1031],[35711,1031],[35712,1031],[35713,1031],[35714,1031],[35715,1031],[35851,1052],[35852,1052],[35853,1052],[35854,1052],[35855,1052],[35856,1052],[35857,1052],[35858,1052],[35859,1052],[35860,1052],[35861,1052],[35862,1052],[35863,1052],[35864,1052],[35865,1052],[35866,1052],[35867,1052],[35868,1052],[35869,1052],[35870,1052],[35871,1052],[35872,1052],[35873,1052],[35874,1052],[35875,1052],[35876,1052],[35932,1052],[35933,1052],[35934,1052],[35935,1052],[35936,1052],[35937,1052],[35938,1052],[35939,1052],[35940,1052],[35941,1031],[35942,1031],[35943,1031],[35944,1031],[35945,1031],[35991,116],[35992,116],[35993,116],[35994,116],[35995,116],[35996,116],[35997,116],[35998,116],[35999,116],[36000,116],[36001,116],[36002,116],[36003,116],[36004,116],[36005,116],[36006,116],[36007,116],[36008,116],[36009,116],[36010,116],[36223,240],[36224,240],[36225,240],[36226,240],[36227,240],[36228,240],[36229,240],[36230,240],[36231,240],[36232,240],[36233,240],[36234,240],[36235,240],[36236,240],[36237,240],[36238,240],[36239,240],[36240,240],[36241,240],[36242,240],[36243,240],[36244,240],[36245,240],[36246,240],[36247,240],[36248,240],[36249,240],[36250,240],[36251,240],[36252,240],[36253,240],[36254,240],[36255,240],[36256,240],[36257,240],[36258,240],[36259,240],[36260,240],[36261,240],[36262,240],[36263,240],[36264,240],[36265,240],[36266,240],[36267,240],[36268,240],[36269,240],[36270,240],[36271,240],[36272,240],[36273,240],[36274,240],[36275,240],[36276,240],[36277,240],[36278,240],[36279,240],[36280,240],[36281,240],[36282,240],[36283,240],[36284,240],[36285,240],[36286,240],[36287,240],[36288,240],[36289,240],[36290,240],[36291,240],[36292,240],[36293,240],[36294,240],[36295,240],[36296,240],[36300,240],[36316,240],[36317,240],[36318,240],[36319,240],[36320,240],[36350,240],[36351,240],[36352,240],[36353,240],[36356,240],[36357,240],[36358,240],[36359,240],[36360,240],[36361,240],[36362,240],[36363,240],[36364,240],[36365,240],[36366,240],[36367,240],[36369,1031],[36370,1031],[36472,1049],[36473,1049],[36474,1049],[36475,1049],[36640,1091],[36641,1091],[36642,1091],[36643,1091],[36644,1091],[36645,1091],[36646,1091],[36647,1091],[36648,1091],[36649,1091],[36650,1091],[36651,1091],[36652,1091],[36653,1091],[36654,1091],[36655,1091],[36656,1091],[36657,1091],[36658,1091],[36659,1091],[36660,1091],[36661,1091],[36662,1091],[36663,1091],[36664,1091],[36665,1091],[36666,1091],[36667,1091],[36668,1091],[36669,1091],[36670,1091],[36671,1091],[36672,1091],[36673,1091],[36674,1091],[36675,1091],[36676,1091],[36677,1091],[36678,1091],[36679,1091],[36680,1091],[36681,1091],[36682,1091],[36683,1091],[36684,1091],[36685,1091],[36686,1091],[36687,1091],[36688,1091],[36689,1091],[36690,1091],[36691,1091],[36692,1091],[36693,1091],[36694,1091],[36695,1091],[36696,1091],[36697,1091],[36698,1091],[36699,1091],[36700,1091],[36701,1091],[36702,1091],[36703,1091],[36704,1091],[36705,1091],[36706,1091],[36707,1091],[36708,1091],[36709,1091],[36710,1091],[36711,1091],[36712,1091],[36713,1091],[36714,1091],[36715,1091],[36716,1091],[36719,1091],[36724,1091],[36808,288],[36809,288],[36810,288],[36811,288],[36812,288],[36813,288],[36814,288],[36815,288],[36816,288],[36817,288],[36818,288],[36819,288],[36820,288],[36821,288],[36822,288],[36823,288],[36824,288],[36825,288],[36826,288],[36827,288],[36828,288],[36829,288],[36830,288],[36831,288],[36832,288],[36833,288],[36834,288],[36835,288],[36836,288],[36837,288],[36838,288],[36839,288],[36840,288],[36841,288],[36895,306],[36896,306],[36897,306],[36898,306],[36908,306],[36909,306],[36910,306],[36911,306],[36912,306],[36913,306],[36914,306],[36915,306],[36916,306],[36917,306],[36918,306],[36919,306],[36920,306],[36921,306],[36922,306],[36923,306],[36924,306],[36925,306],[36926,306],[36927,306],[36928,306],[36929,306],[36930,306],[36931,306],[36932,306],[36933,306],[36934,306],[36935,306],[36936,306],[36937,306],[36938,306],[36939,306],[36940,306],[36941,306],[36942,306],[36943,306],[36944,306],[36945,306],[37014,232],[37015,232],[37016,232],[37017,232],[37018,232],[37019,232],[37020,232],[37021,232],[37022,232],[37023,232],[37024,232],[37025,232],[37026,232],[37027,232],[37028,232],[37029,232],[37030,232],[37031,232],[37032,232],[37033,232],[37034,232],[37035,232],[37036,232],[37037,232],[37038,232],[37039,232],[37040,232],[37041,232],[37042,232],[37043,232],[37044,232],[37045,232],[37046,232],[37047,232],[37048,232],[37049,232],[37050,232],[37051,232],[37052,232],[37053,232],[37054,232],[37055,232],[37056,232],[37057,232],[37058,232],[37059,232],[37060,232],[37061,232],[37062,232],[37063,232],[37064,232],[37065,232],[37066,232],[37067,232],[37068,232],[37069,232],[37070,232],[37071,232],[37072,232],[37073,232],[37074,232],[37075,232],[37076,232],[37077,232],[37078,232],[37079,232],[37080,232],[37081,232],[37082,232],[37083,232],[37084,232],[37121,234],[37122,234],[37123,234],[37124,234],[37125,234],[37126,234],[37127,234],[37128,234],[37129,234],[37130,234],[37131,234],[37132,234],[37133,234],[37134,234],[37135,234],[37136,234],[37137,234],[37138,234],[37139,234],[37140,234],[37141,234],[37142,234],[37143,234],[37144,234],[37145,234],[37146,234],[37147,234],[37148,234],[37149,234],[37150,234],[37151,234],[37152,234],[37153,234],[37154,234],[37155,234],[37156,234],[37157,234],[37158,234],[37159,234],[37160,234],[37161,234],[37162,234],[37163,234],[37164,234],[37165,234],[37166,234],[37167,234],[37168,234],[37169,234],[37170,234],[37171,234],[37172,234],[37173,234],[37174,234],[37175,234],[37176,234],[37177,234],[37178,234],[37185,234],[37192,234],[37217,234],[37252,235],[37253,235],[37254,235],[37255,235],[37256,235],[37257,235],[37258,235],[37259,235],[37260,235],[37261,235],[37262,235],[37263,235],[37264,235],[37265,235],[37266,235],[37267,235],[37268,235],[37269,235],[37270,235],[37271,235],[37272,235],[37273,235],[37274,235],[37275,235],[37276,235],[37277,235],[37278,235],[37279,235],[37280,235],[37281,235],[37282,235],[37283,235],[37284,235],[37285,235],[37286,235],[37287,235],[37288,235],[37289,235],[37290,235],[37291,235],[37292,235],[37293,235],[37294,235],[37295,235],[37296,235],[37297,235],[37298,235],[37299,235],[37300,235],[37301,235],[37302,235],[37303,235],[37304,235],[37305,235],[37306,235],[37307,235],[37308,235],[37309,235],[37310,235],[37311,235],[37312,235],[37313,235],[37314,235],[37315,235],[37316,235],[37317,235],[37318,235],[37319,235],[37320,235],[37324,235],[37325,235],[37326,235],[37327,235],[37339,306],[37340,235],[37465,240],[37468,235],[37525,242],[37526,242],[37527,242],[37528,242],[37529,242],[37530,242],[37531,242],[37532,242],[37533,242],[37534,242],[37535,242],[37536,242],[37537,242],[37538,242],[37539,242],[37540,242],[37541,242],[37542,242],[37543,242],[37544,242],[37545,242],[37546,242],[37547,242],[37548,242],[37549,242],[37550,242],[37551,242],[37552,242],[37553,242],[37554,242],[37555,242],[37556,242],[37557,242],[37558,242],[37559,242],[37560,242],[37561,242],[37562,242],[37563,242],[37564,234],[37565,242],[37566,242],[37567,242],[37568,242],[37569,242],[37570,242],[37571,242],[37572,242],[37573,242],[37574,242],[37575,242],[37576,242],[37577,242],[37578,242],[37579,242],[37580,242],[37581,242],[37582,242],[37583,242],[37584,242],[37585,242],[37586,242],[37587,242],[37588,242],[37589,242],[37590,242],[37591,242],[37592,242],[37593,242],[37594,242],[37595,242],[37596,242],[37597,242],[37598,242],[37604,240],[37612,232],[37618,234],[37626,234],[37673,244],[37674,244],[37675,244],[37676,244],[37677,244],[37678,244],[37679,244],[37680,244],[37681,244],[37682,244],[37684,244],[37685,244],[37686,244],[37687,244],[37688,244],[37689,244],[37690,244],[37691,244],[37692,244],[37693,244],[37694,244],[37695,244],[37696,244],[37697,244],[37698,244],[37699,244],[37700,244],[37701,244],[37703,244],[37704,244],[37705,244],[37706,244],[37707,244],[37708,244],[37709,244],[37710,244],[37711,244],[37712,244],[37713,244],[37714,244],[37715,244],[37716,244],[37717,244],[37718,244],[37719,244],[37720,244],[37721,244],[37722,244],[37723,244],[37724,244],[37725,244],[37726,244],[37727,244],[37728,244],[37729,244],[37730,244],[37731,244],[37732,244],[37733,244],[37734,244],[37735,244],[37736,244],[37737,244],[37738,244],[37739,244],[37740,244],[37741,244],[37742,244],[37743,244],[37744,244],[37745,244],[37746,244],[37747,244],[37748,244],[37749,244],[37750,244],[37751,234],[37762,240],[37764,240],[37765,240],[37778,244],[37780,244],[37781,232],[37802,244],[37885,516],[37886,516],[37887,516],[37888,516],[37889,516],[37890,516],[37891,242],[37893,1091],[37894,234],[37895,288],[37900,242],[37902,306],[37903,232],[37904,306],[37909,306],[37911,306],[38002,234],[38023,1031],[38024,1031],[38025,1031],[38026,1031],[38027,1031],[38140,1031],[38141,1031],[38145,242],[38187,1049],[38188,1049],[38189,1049],[38190,1049],[38191,1049],[38192,1049],[38193,1049],[38194,1049],[38195,1049],[38196,1049],[38197,1049],[38198,1049],[38199,1049],[38200,1049],[38226,1053],[38227,1053],[38228,1053],[38229,1053],[38230,1053],[38231,1053],[38232,1053],[38233,1053],[38234,1053],[38235,1053],[38236,1053],[38237,1053],[38238,1053],[38239,1053],[38240,1053],[38248,116],[38249,116],[38250,116],[38251,116],[38343,116],[38363,116],[38407,116],[38467,116],[38476,116],[38477,116],[38505,116],[38506,116],[38551,235],[38552,235],[38553,237],[38554,237],[38555,235],[38556,235],[38557,235],[38558,235],[38560,237],[38562,237],[38564,242],[38565,242],[38566,237],[38567,244],[38568,244],[38569,244],[38570,244],[38571,244],[38572,244],[38573,244],[38574,244],[38575,232],[38576,232],[38579,237],[38580,237],[38581,235],[38582,235],[38584,244],[38585,244],[38586,244],[38587,237],[38588,242],[38589,242],[38590,234],[38591,234],[38592,244],[38593,244],[38594,244],[38595,244],[38596,244],[38597,244],[38598,1091],[38637,288],[38638,288],[38648,306],[38649,306],[38656,234],[38657,1091],[38682,235],[38698,240],[38713,242],[38721,234],[38808,244],[38824,516],[38825,516],[38826,516],[38827,516],[38828,516],[38829,516],[38830,516],[38831,516],[38832,516],[38833,516],[38834,516],[38835,516],[38836,516],[38837,516],[38838,516],[38839,516],[38840,516],[38841,516],[38842,516],[38843,516],[38844,516],[38845,516],[38846,516],[38847,516],[38848,516],[38849,516],[38850,516],[38851,516],[38852,516],[38853,516],[38854,516],[38855,516],[38857,516],[38859,516],[38865,516],[38866,516],[38867,516],[38869,516],[38874,244],[38900,516],[38901,242],[38902,1091],[38904,1091],[38905,1091],[38906,1091],[38907,1091],[38908,1091],[38909,1091],[38910,1091],[38965,242],[38966,242],[38967,242],[39004,1049],[39110,232],[39111,232],[39112,232],[39115,306],[39116,306],[39117,306],[39118,306],[39119,306],[39120,306],[39121,306],[39122,306],[39123,306],[39124,306],[39125,306],[39273,1031],[39274,1031],[39275,1031],[39276,1031],[39277,1031],[39278,1031],[39279,1031],[39306,234],[39307,234],[39308,234],[39404,1031],[39572,240],[39573,240],[39602,1048],[39603,1031],[39604,1048],[39605,1031],[39606,1048],[39608,1048],[39610,1048],[39612,1048],[39624,1051],[39625,1051],[39626,1051],[39627,1051],[39628,1051],[39629,1051],[39630,1051],[39631,1051],[39632,1051],[39633,1051],[39634,1051],[39635,1051],[39647,240],[39648,240],[39660,1051],[39662,1051],[39663,1051],[39664,1051],[39665,1051],[39666,1051],[39667,1051],[39668,1051],[39669,1051],[39670,1051],[39671,1051],[39672,1051],[39673,1051],[39674,1051],[39675,1051],[39676,1051],[39679,1052],[39680,1052],[39681,1052],[39684,1052],[39685,1052],[39687,1052],[39701,118],[39702,118],[39703,118],[39704,118],[39754,235],[39755,235],[39763,1053],[39985,240],[39992,118],[39993,118],[39994,118],[39995,118],[39996,118],[39997,118],[39998,118],[39999,118],[40000,118],[40001,118],[40002,118],[40003,118],[40004,118],[40005,118],[40006,118],[40007,118],[40008,118],[40009,118],[40010,118],[40011,118],[40012,118],[40013,118],[40014,118],[40015,118],[40016,118],[40017,118],[40018,118],[40019,118],[40020,118],[40021,118],[40022,118],[40023,118],[40024,118],[40025,118],[40026,118],[40027,118],[40028,118],[40029,118],[40030,118],[40031,118],[40032,118],[40033,118],[40034,118],[40035,118],[40036,118],[40037,118],[40038,118],[40039,118],[40040,118],[40041,118],[40042,118],[40043,118],[40044,118],[40045,118],[40046,118],[40047,118],[40048,118],[40049,118],[40050,118],[40051,118],[40052,118],[40053,118],[40055,118],[40056,118],[40057,118],[40065,243],[40066,243],[40067,243],[40070,118],[40071,118],[40072,118],[40074,1053],[40075,1053],[40076,1053],[40077,1053],[40078,1053],[40079,1053],[40080,1053],[40081,1053],[40082,1053],[40083,1053],[40084,1053],[40085,1053],[40086,1053],[40087,1053],[40094,1052],[40097,116],[40098,116],[40099,116],[40100,116],[40217,240],[40218,240],[40242,242],[40243,242],[40244,242],[40245,242],[40246,242],[40247,242],[40248,242],[40255,1052],[40271,243],[40272,243],[40273,243],[40274,243],[40275,243],[40288,1048],[40349,116],[40385,1052],[40483,1052],[40707,232],[40708,232],[40709,232],[40778,118],[40786,116],[40843,116],[40853,118],[40880,234],[40881,234],[40882,234],[40883,234],[40884,234],[40885,234],[40976,237],[40977,237],[40992,237],[40993,237],[40994,237],[41206,1052],[41207,1052],[41208,1052],[41209,1052],[41249,232],[41250,232],[41296,244],[41575,1048],[41576,1048],[41577,1048],[41579,1048],[41648,243],[41649,243],[41650,243],[41651,243],[41652,243],[41653,243],[41654,243],[41655,243],[41656,243],[41665,243],[41666,243],[41740,242],[41741,242],[42083,240],[42084,240],[42085,240],[42086,240],[42087,240],[42093,240],[42094,240],[42433,240],[42434,240],[42435,240],[45181,232],[45182,232],[45221,232],[45222,232],[45224,232],[45225,232],[45226,232],[45227,232],[45246,235],[45247,235],[45252,235],[45253,235],[45254,235],[45255,235],[45261,240],[45262,240],[45263,240],[45264,240],[45265,240],[45266,242],[45267,242],[45268,242],[45269,242],[45270,242],[45273,242],[45276,242],[45277,242],[45278,243],[45280,243],[45281,243],[45282,243],[45283,243],[45284,243],[45285,244],[45286,244],[45289,244],[45290,244],[45291,244],[45292,244],[45295,244],[45296,244],[45339,1091],[45340,1091],[45350,240],[45355,1091],[45356,1091],[45357,1091],[45358,240],[45374,240],[45388,243],[45391,1091],[45392,1091],[45395,243],[45396,243],[45397,243],[45398,243],[45399,243],[45400,243],[45401,243],[45402,243],[45403,243],[45404,243],[45434,242],[45435,242],[45438,232],[45439,232],[45446,240],[45452,235],[45453,235],[45456,243],[45458,244],[45459,244],[45460,244],[45462,235],[45463,235],[45465,240],[45467,242],[45468,242],[45469,242],[45470,242],[45471,242],[45472,242],[45478,244],[45479,244],[45480,244],[45481,244],[45482,244],[45483,244],[45505,232],[45515,232],[45590,244],[45592,242],[45594,1091],[45595,1091],[45596,1091],[45597,1091],[45598,1091],[45599,1091],[45600,1091],[45601,1091],[45602,1091],[45603,1091],[45604,1091],[45605,1091],[45606,1091],[45607,1091],[45608,1091],[45609,1091],[45610,1091],[45611,1091],[45612,1091],[45613,1091],[45614,1091],[45615,1091],[45616,1091],[45617,1091],[45618,1091],[45619,1091],[45620,1091],[45621,1091],[45622,1091],[45623,1091],[45624,1091],[45625,1091],[45626,1091],[45627,1091],[45628,1091],[45629,235],[45630,1091],[45634,232],[45636,306],[45637,306],[45642,288],[45645,1091],[45646,1091],[45647,1091],[45648,1091],[45649,1091],[45650,1091],[45651,1091],[45652,1091],[45653,1091],[45654,1091],[45655,1091],[45656,1091],[45657,1091],[45658,1091],[45659,1091],[45660,1091],[45661,1091],[45662,1091],[45663,1091],[45664,1091],[45665,1091],[45666,1091],[45667,1091],[45668,1091],[45669,1091],[45670,1091],[45671,1091],[45672,1091],[45673,1091],[45674,1091],[45675,1091],[45676,1091],[45677,1091],[45678,1091],[45679,1091],[45680,1091],[45681,1091],[45682,1091],[45683,1091],[45684,1091],[45685,1091],[45686,1091],[45687,1091],[45688,1091],[45690,1091],[45692,1091],[45693,1091],[45698,1091],[45702,1091],[45703,1091],[45704,1091],[45705,1091],[45706,1091],[45707,1091],[45708,1091],[45709,242],[45712,1091],[45714,1091],[45716,1091],[45720,516],[45721,516],[45722,516],[45723,516],[45809,240],[45810,243],[45811,243],[45859,240],[45934,516],[45956,1091],[45959,306],[46138,1091],[46140,1091],[46142,243],[46143,243],[46179,240],[46180,240],[46279,232],[46536,288],[46833,243],[46863,240],[46870,235],[46963,516],[46992,243],[46996,243],[47185,235],[47199,243],[47203,243],[47211,235],[47227,240],[47231,240],[47406,235],[47435,240],[47964,288],[47992,288]] diff --git a/research/p104-rank-four-five-bank-bound/replay.py b/research/p104-rank-four-five-bank-bound/replay.py new file mode 100644 index 0000000000..72e6a61398 --- /dev/null +++ b/research/p104-rank-four-five-bank-bound/replay.py @@ -0,0 +1,238 @@ +"""Replay the fixed-paid rank-four/five public-bank support results.""" +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 +import shutil +import subprocess +import sys +from tempfile import TemporaryDirectory + +HERE = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" + + +def unique(pairs): + result = dict(pairs) + if len(result) != len(pairs): + raise ValueError("duplicate JSON key") + return result + + +def decode(raw): + return loads(raw, object_pairs_hook=unique) + + +def digest(raw): + return sha256(raw).hexdigest() + + +def checked_path(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(): + raw = (HERE / checked_path(name)).read_bytes() + if digest(raw) != expected: + raise ValueError("changed dependency: " + name) + sources = decode((HERE / "PROVENANCE.json").read_bytes())["files"] + for name, source in sources.items(): + raw = (HERE / checked_path(name)).read_bytes() + assert not source["uncompress"] and pins[name] == source["sha256"] == digest(raw) + assert sha1(f"blob {len(raw)}\0".encode() + raw).hexdigest() == source["git_blob"] + for name, source in decode((HERE / "PROVENANCE.json").read_bytes())["derived_inputs"].items(): + raw = (HERE / checked_path(name)).read_bytes() + assert name in pins and source["published_receipt"] in sources + if source.get("compression") == "gzip": + raw = decompress(raw) + published = decode((HERE / checked_path(source["published_receipt"])).read_bytes()) + assert digest(raw) == published[source["receipt_key"]] + + +def command(script, *args, timeout=35, check=True): + argv = [sys.executable, "-I", "-B", str(HERE / script), *map(str, args)] + return subprocess.run(argv, capture_output=True, check=check, timeout=timeout) + + +def replay_suffix(scratch, record, expected): + """Continue on the exact R87 unresolved bank list without changing its receipts.""" + root = scratch / "r89" + for name in ("price", "inputs", "lead", "independent/reused"): + (root / name).mkdir(parents=True) + for name in ("7334-WORD.json.gz", "PRICE.json", "paired_rank.py", "paired_support.py"): + shutil.copyfile(scratch / "inputs" / name, root / "inputs" / name) + shutil.copyfile(HERE / "engines/modular_primary.py", root / "inputs/exterior_minor.py") + shutil.copyfile(HERE / "engines/r89/suffix_sweep.py", root / "lead/suffix_sweep.py") + independent_exact = root / "independent/exact_selection.py" + shutil.copyfile(HERE / "engines/r89/exact_independent.py", independent_exact) + for local, source in (("exact_six.py", "exact_independent.py"), + ("rolling_exterior.py", "rolling_exterior.py")): + shutil.copyfile(HERE / "engines" / source, root / "independent/reused" / local) + + def stage(name, script, *args, timeout=35): + return record("r89/" + name, command(script, *args, timeout=timeout).stdout) + + frozen = stage("price/KEYS.json", "engines/r89/freeze.py", scratch, timeout=10) + assert frozen["cases"] == 2128 and frozen["one_split_per_literal_pivot_cap"] == 129 + primary = stage("lead/RESULT.json", "engines/r89/suffix_sweep.py", root) + assert primary["status"] == "EXHAUSTED" and not primary["unvisited"] + assert primary["counts"] == {"excluded":663, "rank drop":1465} + keys_path = root / "price/KEYS.json" + price_path = root / "inputs/PRICE.json" + word_path = root / "inputs/7334-WORD.json.gz" + suffix_script = "engines/r89/reverse_suffix.py" + modular_args = ("--keys", keys_path, "--price", price_path, "--word", word_path) + other = stage("independent/RESULT.json", suffix_script, *modular_args) + assert len(other["denominator_units"]) == 98 and not other["unvisited"] + assert not other["control_discrepancies"] and not other["control_unvisited"] + compare = stage("independent/COMPARE.json", "engines/r89/compare_modular.py", keys_path, + root / "lead/RESULT.json", root / "independent/RESULT.json", timeout=10) + assert compare["agreed_keys"] == 2128 and compare["full_suffix_exclusions"] == 663 + assert compare["suffix_rank_drops"] == 1465 and len(compare["remaining_pivots"]) == 109 + assert Fraction(compare["moonshot_optimistic_complete_upper"]) < 0 + + heuristic = stage("lead/PAIR.json", "engines/r89/rank_pairs.py", root) + assert heuristic["cases"] == 1465 and heuristic["modular_pairs"] == 0 and not heuristic["unvisited"] + selection = stage("lead/SELECTION.json", "engines/r89/select.py", root, timeout=10) + assert len(selection["selected"]) == selection["case_cap"] == 6 + exact = stage("lead/EXACT.json", "engines/r89/exact_primary.py", root) + assert exact["counts"] == {"no unit pairing":6} and not exact["selected_unresolved"] + selection_path = root / "lead/SELECTION.json" + selection_hash = expected["r89/lead/SELECTION.json"] + exact_args = (*modular_args, "--suffix", root / "independent/RESULT.json", + "--selection", selection_path, "--selection-sha", selection_hash) + independent = stage("independent/EXACT.json", independent_exact, *exact_args) + assert independent["counts"] == {"no_exact_unit_pair":6} and not independent["unresolved"] + checked = stage("independent/EXACT-COMPARE.json", "engines/r89/compare_exact.py", + selection_path, root / "lead/EXACT.json", root / "independent/EXACT.json", + root / "independent/RESULT.json", timeout=10) + assert checked["exact_agreements"] == 6 and checked["exact_unit_pairs"] == 0 + assert checked["remaining_modular_drops"] == 1459 and len(checked["remaining_literal_pivots"]) == 109 + + unresolved = decode((HERE / "receipts/UNRESOLVED.json").read_bytes()) + checked_keys = {tuple(row["key"]) for row in independent["results"]} + independently_remaining = [row["key"] for row in other["tested"] + if row["status"] == "modular_suffix_rank_drop" and tuple(row["key"]) not in checked_keys] + assert unresolved == exact["unselected"] == selection["unselected"] == independently_remaining + assert len(unresolved) == len(set(map(tuple, unresolved))) == 1459 + assert 4207 - (24 + 2049 + 6 + 663 + 6) == len(unresolved) + + for target, message, args, index, script in ( + (keys_path, b"Changed input keys", modular_args, 1, suffix_script), + (word_path, b"Changed input word", modular_args, 5, suffix_script), + (selection_path, b"Changed input bad-SELECTION.json", exact_args, 9, independent_exact), + ): + bad = root / ("bad-" + target.name) + bad.write_bytes(target.read_bytes() + b"\n") + changed = [*args] + changed[index] = bad + negative = command(script, *changed, timeout=10, check=False) + assert negative.returncode == 1 and message in negative.stderr and not negative.stdout + + +def replay(scratch, output): + authenticate() + expected = decode((HERE / "receipts/SHA256.json").read_bytes()) + generated = {} + + def record(name, raw): + if digest(raw) != expected[name]: + raise ValueError("changed receipt: " + name) + generated[name] = raw + (scratch / checked_path(name)).write_bytes(raw) + return decode(raw) + + for name in ("lead", "independent"): + (scratch / name).mkdir() + for name in ("price", "inputs"): + shutil.copytree(HERE / name, scratch / name) + compressed = scratch / "price/inputs/R72-OCCUPANCY.json.gz" + (compressed.parent / "R72-OCCUPANCY.json").write_bytes(decompress(compressed.read_bytes())) + price_path = scratch / "price/PRICE.json" + price = record("price/PRICE.json", command(scratch / "price/quote.py", timeout=15).stdout) + assert price["head"] == HEAD and price["native_copies"] == 17 + split = price["one_split"] + assert not split["paid_delta"] and split["target_delta"] == {"4":17, "5":17, "9":-17} + assert sum(split["paid"].values()) == 110519 + assert (sum(price["old_targets"].values()), sum(split["targets"].values())) == (22461,22478) + assert price["signed_rank_surplus"] == 1424 and price["empty_root_credits"] == 0 + assert 0 < Fraction(split["complete_margin"][0]) and Fraction(split["complete_margin_with_one_extra_paid_rank1_upper"]) < 0 + + geometry_path = scratch / "lead/GEOMETRY.json" + geom = record("lead/GEOMETRY.json", command("engines/geometry.py", scratch, timeout=20).stdout) + assert geom["head"] == HEAD and geom["status"] == "EXHAUSTED" + assert (geom["visited_events"],geom["eligible_bank_count"],geom["eligible_chart_count"]) == (76466,4207,90) + assert len(geom["selected"]) == 24 and len(geom["unvisited_keys"]) == 4183 + assert len(price["endpoint_cohort"]) == 615 + old_rational = record("lead/R86-RATIONAL.json", command("engines/prior_rational.py", scratch, + expected["lead/GEOMETRY.json"],timeout=25).stdout) + assert old_rational["counts"] == {"no nonzero pure prefix":24} and not old_rational["selected_unresolved"] + word = scratch / "inputs/7334-WORD.json.gz" + prior = record("inputs/R86-PRIOR.json", command("engines/prior_minors.py", "--price", price_path, + "--geometry", geometry_path, "--word", word, + "--primary", scratch / "lead/R86-RATIONAL.json",timeout=25).stdout) + assert prior["head"] == HEAD + shutil.copyfile(price_path, scratch / "inputs/PRICE.json") + shutil.copyfile(geometry_path, scratch / "inputs/GEOMETRY.json") + + modular = record("lead/RESULT.json", command("engines/modular_primary.py", scratch).stdout) + assert modular["status"] == "EXHAUSTED" and not modular["unvisited"] + assert modular["counts"] == {"excluded":2049, "rank drop":2134} + other = record("independent/RESULT.json", command("engines/rolling_exterior.py", "--price", price_path, + "--geometry", geometry_path, "--prior", scratch / "inputs/R86-PRIOR.json", + "--word", word).stdout) + assert len(other["denominator_units"]) == 98 and not other["unvisited"] + selection = record("lead/SELECTION.json", command("engines/select_six.py", scratch, timeout=10).stdout) + assert len(selection["selected"]) == 6 + exact = record("lead/EXACT.json", command("engines/exact_primary.py", scratch).stdout) + assert exact["counts"] == {"no nonzero pure suffix":4, "no unit pairing":2} + assert not exact["selected_unresolved"] + assert len(exact["unselected"]) == len(set(map(tuple, exact["unselected"]))) == 2128 + record("independent/EXACT.json", command("engines/exact_independent.py", "--price", price_path, "--word", word, + "--selection", scratch / "lead/SELECTION.json", "--modular", scratch / "independent/RESULT.json").stdout) + compare = record("independent/COMPARE.json", command("engines/compare.py", scratch / "lead/RESULT.json", + scratch / "independent/RESULT.json", scratch / "lead/EXACT.json", + scratch / "independent/EXACT.json", timeout=10).stdout) + assert compare["modular_exact_bank_agreements"] == 4207 + assert compare["new_full_rank_exclusions"] == 2049 and compare["exact_scope_exclusions"] == 6 + assert compare["remaining_unresolved"] == 2128 + + replay_suffix(scratch, record, expected) + + # Check that the actual scientific entry points reject changed receipts before replaying the word. + for target, script, message in (("inputs/GEOMETRY.json", "engines/modular_primary.py", b"changed dependency"), + ("lead/RESULT.json", "engines/select_six.py", b"changed modular support receipt")): + changed = scratch / target + changed.write_bytes(changed.read_bytes() + b"\n") + negative = command(script, scratch, timeout=10, check=False) + assert negative.returncode == 1 and message in negative.stderr and not negative.stdout + + assert generated.keys() == expected.keys() + if output is not None: + output.mkdir(parents=True) + for name, raw in generated.items(): + target = output / name + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(raw) + print("PASS_RANK_FOUR_FIVE_BANK_BOUND prior=24 new=2724 unresolved=1459 kappa_change=0") + + +def main(): + if sys.version_info[:2] != (3, 12) or not __debug__: + raise RuntimeError("Use CPython 3.12 with assertions enabled") + parser = ArgumentParser(description=__doc__) + parser.add_argument("--out", type=Path, help="new directory to retain regenerated receipts") + args = parser.parse_args() + with TemporaryDirectory() as temporary: + replay(Path(temporary), args.out) + + +if __name__ == "__main__": + main()