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-seven-prefix-bank-bound/COHORT.md b/research/p104-rank-seven-prefix-bank-bound/COHORT.md new file mode 100644 index 0000000000..a6aa8b88d1 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/COHORT.md @@ -0,0 +1,102 @@ +# R102 independent metadata preflight + +The exact comparable native witness is [#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) +`aaeec8c0acf01e99a5f331ef363a698d9c084ace`, κ `0.00364665195644`, +with signed [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +`07a76c5e2738882c0cb322278e56f6cae3c9885d`. This preflight only +reads the inherited exact 1,101-helper census for +[#7314](https://github.com/CrocSwap/integer-mult-bounds/pull/7314) +`9d0119eb12fbd9fa534b48cd37b68e7099757b91`, the #7334 changed-role +certificate, the independently admitted invoice, and the #7334 +constructor source. The constructor deep-copies the old word, replaces +only `program`, and checks restoration to the original final chart +array and all owned erasures. The frame and endpoint metadata therefore +transfer. The exact constructor SHA-256 is +`ecb39578063d7f09153a85370a3b9bb7cbf8b36ff9891033a1cce7a2fe7fda`. +The #7334 native word was neither opened nor decoded here. + +## Cohort and price stock + +Of 19 productive rank-seven helpers, the guard excludes role 1355, +leaving 18 in 11 exact ordered endpoint cohorts. Chart 602→127 is the +unique largest group, with roles **1457, 1458, 1474, 1475, 1476**. +The next-largest groups, chart 252→127, 462→127 and 603→127, each +have two. The complete invoice independently counts 323 rank-seven +target occurrences, exactly 19×17. + +The old census measured each productive rank as the difference +between dimensions of strictly nested endpoint spans. Ambient chart +rank is at most nine, and productive rank nine on chart 3→127 forces +dim(3)=0 and dim(127)=9. The rank-seven cohort at chart 602→127 +therefore has dim(602)=2. A 3+4 split cuts at absolute rank five +and a 4+3 split at rank six. In the rank-seven quotient there are +11,811 abstract subspaces of each required dimension, before +restricting to signed catalogue labels, actual occupancy and exact +support. This count does not certify any candidate. + +Grant at most one split per distinct old productive role, even if a +role can be used at multiple clocks or both cut ranks. The optimistic +compatibility cap is five edits, corresponding to at most 85 +replaced rank-seven occurrences across the 17 copies. One edit +changes the complete histogram by ΔT = {3:+17, 4:+17, 7:−17}, +ΔP = {}, with no empty-root credit and conserved signed rank mass. +Even before checking support, five times the per-edit directed +upper bounds the family. Actual compatible edits still require +two-sided support, signed arbitrary-input action and complete +setup/routing/ownership/restoration/precision/tape pricing. + +The exact [chart-207 study #7339](https://github.com/CrocSwap/integer-mult-bounds/pull/7339) +targets a rank-nine chart 3→127 root at an absolute rank-eight cut +near the helper-319 retimed block. R96 targets the rank-eight +chart 3→245 cohort at an absolute rank-four cut, with a 4+4 split. +This family changes the old endpoint class, split ranks, and +intermediate ranks. The common fixed-paid two-sided support +method is inherited. + +## Metadata replay + +From this package directory with CPython 3.12: + +```sh +python3.12 -I -B - <<'PY' +from collections import defaultdict +from gzip import decompress +from hashlib import sha256 +from json import loads +from pathlib import Path + +pins = { + "7314-HELPERS.json": "bf353b3e05d0bf5fe3e49c15673c4cb9203251329bd594009303541cf7fecc09", + "7334-CHANGED.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", +} +data = {} +for name, expected in pins.items(): + path = Path("inputs") / name + raw = decompress(path.with_suffix(".json.gz").read_bytes()) if name == "7314-HELPERS.json" else path.read_bytes() + assert sha256(raw).hexdigest() == expected, name + data[name] = loads(raw) +h, x, a, b = data.values() +assert h["head"] == "9d0119eb12fbd9fa534b48cd37b68e7099757b91" +assert a["head"] == b["head"] == "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +assert h["caller_head"] == a["caller"] == b["caller_head"] == "07a76c5e2738882c0cb322278e56f6cae3c9885d" +assert h["complete"] and len(h["rows"]) == len({r["role"] for r in h["rows"]}) == 1101 +assert a["exit"] == 0 and b["copies"] == 17 and not b["empty_root_credits"] +assert a["inputs"]["WORD.json.gz"] == "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +assert x["word_sha256"][1] == "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +assert len(x["roles"]) == len(set(x["roles"])) == 14 +protected = set(x["roles"]) | {863, 1355, 1531, 1567, 1568} +groups = defaultdict(list) +rank_seven = [r for r in h["rows"] if r["old_productive_rank"] == 7] +assert len(rank_seven) == 19 and b["targets"]["7"] == 17 * len(rank_seven) +assert [r["role"] for r in rank_seven if r["role"] in protected] == [1355] +for r in rank_seven: + if r["role"] not in protected: + groups[r["initial"], r["final"]].append(r["role"]) +assert groups[602, 127] == [1457, 1458, 1474, 1475, 1476] +assert sorted(map(len, groups.values()), reverse=True) == [5,2,2,2,1,1,1,1,1,1,1] +assert any((r["initial"], r["final"], r["old_productive_rank"]) == (3,127,9) for r in h["rows"]) +print("PASS_R102_COHORT roles=1457,1458,1474,1475,1476 eligible_rank7=18 groups=11") +PY +``` diff --git a/research/p104-rank-seven-prefix-bank-bound/LOCAL-PINS.json b/research/p104-rank-seven-prefix-bank-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..5ba6a5531c --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/LOCAL-PINS.json @@ -0,0 +1,30 @@ +{ + "PROVENANCE.json": "ccfa38b1f7095bd5a3db5e04d8f18727ad38fc550224c9cafa4d4aa99de28713", + "engines/independent/r102_prefix.py": "505eca6677cc4e905494bdbf027d23c7ad288aa26889443db5d99d3ec41488f5", + "engines/independent/second_prime.py": "21dbd96192e1f60c00ceddba01a7e8d0ddd7d6ad7da4ad3ed22ef2e47cc589c4", + "engines/independent/verify.py": "79bcc7d741f3e0c791901cda3a4c859296affbc84c55cde3c1bb271225ba8aae", + "engines/r102/geometry.py": "dba4588b3360ab9fc162736b5933b208e6c1395fd172a9d8cf0114247beb60d9", + "engines/r102/prefix.py": "7a29fb100262030ebb1601a2eec0a5f021bf92c0a0bc28d1445e9cfbf0e2e7d3", + "engines/r102/quote.py": "a60e221ebf42995dd285ed8b1c0c30016657cb34fd16d933089fab86d8c67c9e", + "engines/r105/alias_rank_seven.py": "64163173dbfa26637a319d2ae1b2f8602b053526c5d4e4c065b84d8d862301f7", + "engines/r105/freeze_support.py": "8d2ab192d4863f7895b0a6ce69f34bd0c03c590b5541064b909e7d3ba41dc4b8", + "engines/r105/modular_support.py": "7c5dc578e846f3509aea9637d5b378b15c926a35d6b6cd78c2f5ac488f5ea66d", + "engines/r109/freeze.py": "3ab4e63dab5c34dffedc21a8ba710448a222a6299dc67ab4359fc9beedd335a2", + "engines/r109/modular_support.py": "6396fbc47ed18e197d5da38d2e3edc096adf17ea46beb79cacad7cdcbbddda4a", + "engines/r109/prefix_second_prime.py": "502b1544934e701793b6758a2f22320b639a05d7e7c71b3ade3416bb4a52314b", + "engines/r109/sweep.py": "089192d85154c1f8ff1d1cf6329397fe9d40b3e4b09c18dd9c90eda169f09fd9", + "inputs/7314-HELPERS.json.gz": "e817ac36ffd85b5b8ad7320daf57bedfa5692b4a0f2990570008afe4888bca6d", + "inputs/7334-CHANGED.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/PR7319-SHA256.json": "ca3ed296a19bdd7b2b37608e93d1763d97c7620ac9faef732a01bae4f485114c", + "inputs/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/exterior_rank56.py": "9fceafc627fe3781bcb8d5229eaefebc557de613f0d4723aa1d36ce4ab9954ac", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "inputs/reverse_engine.py": "751d5d0c4c665c8768ff69bcf939700d3be2f989c59f09af3a4aa14d3c1ebbc4", + "receipts/CLOSED.json": "b3e9f0dca3b11d231dbb26650a479e31fcc4e7bc51ef0d108922dcee7bde0e58", + "receipts/R109-SHA256.json": "93368e1f41a2f324b5f614fc9b1cde3675030c22b418a32159701df13f3ddcb3", + "receipts/RECONCILED.json": "fa7b8bba9ae88cb6d66b41b1e28d70d46289e1853da9c8f8f1b52071eb8159bc", + "receipts/SHA256.json": "a4fe2ea47920e3548bc8eabca34f69a60e2dcde3da6c650d9138e255d9fde4d2", + "replay.py": "ab8fe90e4d741e4c7ba9d52c3ec60ec969bf58f37d638ddd3a85290711c4f766" +} diff --git a/research/p104-rank-seven-prefix-bank-bound/NOTICE b/research/p104-rank-seven-prefix-bank-bound/NOTICE new file mode 100644 index 0000000000..708dc8941f --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/NOTICE @@ -0,0 +1,7 @@ +Apache-2.0. + +#7334 supplies the exact native word, #7113 the signed caller, #7314 +and #7319 the inherited helper census, and #7338 and #7298 the +admitted invoice and directed tariff. #5718 and #6040 supply the +chart-602 lineage. #7363 supplies the distinct rank-eight exterior +method. OpenAI Codex and subagents materially assisted. diff --git a/research/p104-rank-seven-prefix-bank-bound/PROOF.md b/research/p104-rank-seven-prefix-bank-bound/PROOF.md new file mode 100644 index 0000000000..458d366013 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/PROOF.md @@ -0,0 +1,84 @@ +# Fixed-paid rank-seven cochart proof + +The exact #7334 constructor preserves the original endpoint charts and +frame catalogue. The independently reproduced #7314 helper census and +the guarded #7334 changed-role certificate identify the chart 602→127 +cohort as roles 1457, 1458, 1474, 1475 and 1476. The endpoint chart ranks +are two and nine. An intermediate rank-five chart gives 3+4 and +rank six gives 4+3. Replaying all 76,466 native events finds five +eligible rank-six charts and 65 occupied-bank representatives with +a cohort pivot. There is no eligible rank-five bank in this exact +catalogue and itinerary. The independently reconstructed reverse +walk validates every frozen public and owned bank and its pivots. +A key `[cut,chart]` uses the state after exactly `cut` literal events. + +## Direct exterior exclusions + +Let (P) be the matrix of normalized input prefix rows of the +public roles in the bank and let (E) project input coordinates to +the complement of the five-role cohort. A nonzero pure public-bank +prefix would require a nonzero row (a) with (aPE=0). Thus a +nonzero full-row-rank minor of (PE) excludes that bank. The signed +native coefficients are reduced only after the engines verify unit +denominators for their respective primes, 65521 and 65537. Each +nonzero modular determinant implies a nonzero rational determinant. +Both engines reconstruct the same public and owned occupancy and +verify 16 original, 16 continuation and 13 residual exclusions. +No suffix or rational pairing is necessary for these 45 direct +prefix exclusions. + +## Transfer through an unchanged bank + +For adjacent frozen keys in the same chart, both chronology engines +verify equal public, owned and pivot sets and inspect every intervening +literal event. A MOVE incident to the bank, owner initialization or +erasure, COPY, or public/owned ADD mixing blocks the conservative +transfer. A signed nonzero SCALE is invertible. A public ADD whose +two distinct public roles are both in the unchanged bank is an +invertible elementary row update. Owned-only ADD or SCALE and +events disjoint from the bank leave its public rows fixed. + +Consequently, across a proved link the public prefix rows satisfy +(P_{2}=UP_{1}) with (U) invertible over the rationals. For the +same exterior coordinate columns, the square minor is multiplied +by (det U), so nonzero rank certificates transfer in either +direction. Transfer requires no new arithmetic support query. The +60 adjacent links yield 20 proved edges and 45 components. Each +certified edge spans one literal event, and chains compose these +edges. A separate fixed-public-row diagnostic found no additional +links. No cross-chart transfer was claimed. + +Sixteen original directly checked components contain nine extra +keys. The next 16 selected components contain eleven more extra keys. +Their selection takes the widest previously unresolved public bank +first within each chart, round-robin across the five charts, with +the earliest cut breaking ties. Thus the two bounded stages exclude +16 + 9 + 16 + 11 = 52 of 65 keys. The exact remaining 13 singleton +keys were outside the second support cap. They consist of nine +one-role banks and four two-role banks, with no owned roles. A +separately frozen 13-case replay exhausts them in each prime +field under the same 25-second limit. Both engines independently +verify nonzero full-row-rank prefix minors on all 13. The original +65521 minor column choices also give nonzero determinants when +recomputed at 65537 on each key. The final receipt certifies +65 of 65 keys, with zero unresolved. No κ improvement follows +from these exclusions and no signed physical candidate was built. + +## Directed complete cost + +The unchanged exact native and caller ledger has 110,519 paid and +22,461 productive positions, rank surplus 1,424, and zero empty +credit. The speculative one-edit delta is +ΔT = {3:+17, 4:+17, 7:−17}, ΔP = {}. It retains the signed rank +surplus and would make 22,478 productive positions. Its direct credit +is (17(3^{1-kappa}+4^{1-kappa}-7^{1-kappa})). One edit per +distinct old productive helper bounds the family even when all five +edits are granted compatibility and free ancillary work. The +directed one-edit upper at the incumbent crossing upper is about +0.294636248924991 raw, the five-edit upper about 1.473181244624955, +and the relaxed complete margin upper at κ = 0.0040075385047236 is +about −138.148881688689. An additional raw paid rank-one position +overruns the one-edit margin. Native all-column action, owned erasure, +compiler, precision/tape and analytic recovery remain inherited +comparator premises. No new routing, compiler or tape contract is +asserted here. diff --git a/research/p104-rank-seven-prefix-bank-bound/PROVENANCE.json b/research/p104-rank-seven-prefix-bank-bound/PROVENANCE.json new file mode 100644 index 0000000000..1e1294f097 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/PROVENANCE.json @@ -0,0 +1,61 @@ +{ + "derived_inputs": { + "inputs/7314-HELPERS.json.gz": { + "compression": "gzip", + "keys": [ + "REVERSE.json" + ], + "receipt": "inputs/PR7319-SHA256.json" + }, + "inputs/7334-CHANGED.json": { + "keys": [ + "receipt", + "peer-prep/IDENTITIES.json" + ], + "receipt": "inputs/ADMITTED.json" + } + }, + "files": { + "inputs/7334-WORD.json.gz": { + "commit": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "git_blob": "73f43007192eb5a38eb5abb591b871df3e52c7cd", + "path": "research/p104-helper-319-fused-return/WORD.json.gz", + "sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "source": "https://github.com/Clear1nsight/integer-mult-bounds/blob/aaeec8c0acf01e99a5f331ef363a698d9c084ace/research/p104-helper-319-fused-return/WORD.json.gz", + "uncompress": false + }, + "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 + }, + "inputs/PR7319-SHA256.json": { + "commit": "b2d3bc4dd584f8d3aacd244505b12286db4d4875", + "git_blob": "3a28905e8d69888617b56578761c16d39fcdf7a6", + "path": "research/p104-helper-entrance-first-contact-bound/receipts/SHA256.json", + "sha256": "ca3ed296a19bdd7b2b37608e93d1763d97c7620ac9faef732a01bae4f485114c", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/b2d3bc4dd584f8d3aacd244505b12286db4d4875/research/p104-helper-entrance-first-contact-bound/receipts/SHA256.json", + "uncompress": false + }, + "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 + }, + "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-seven-prefix-bank-bound/README.md b/research/p104-rank-seven-prefix-bank-bound/README.md new file mode 100644 index 0000000000..e3fc28ed78 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/README.md @@ -0,0 +1,73 @@ +# Fixed-paid rank-seven prefix exclusions on chart 602→127 + +**NO VERIFIED GAIN.** Exact Δκ = 0, a 0% change from conditional +κ = `0.00364665195644` on independently reproduced +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) +head `aaeec8c0acf01e99a5f331ef363a698d9c084ace), with signed +[#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +head `07a76c5e2738882c0cb322278e56f6cae3c9885d`. + +The proposed fixed-paid change splits one of five rank-seven productive +targets into 3+4 or 4+3 at an existing intermediate chart. Exhaustive +geometry finds 65 occupied rank-six bank keys on five charts and zero +eligible rank-five keys. Two exact prime-field engines agree on 45 +direct exterior-prefix exclusions. Independent literal continuity +replay transfers 32 of those certificates to 20 additional keys. +The original two selections excluded 52 keys. A third selection closes +the exact 13 remaining singleton keys at both primes, for **all 65 +excluded and zero unresolved**. [Final key receipt](receipts/CLOSED.json). + +The fixed paid bill has 110,519 positions across 17 signed caller +copies. The relaxed directed upper is 0.294636248924991 raw units +per edit, or 1.473181244624955 across five distinct targets if all +can coexist. One new paid rank-one position defeats a single edit. +[Proof and price](PROOF.md). + +## Replay + +From a clean checkout, use CPython 3.12 with assertions enabled: + +```sh +python3.12 -I -B research/p104-rank-seven-prefix-bank-bound/replay.py +``` + +The replay authenticates the native word and the inherited helper +census, rebuilds the directed price and full geometry, checks both +primes for the two frozen 16-key sets and the exact 13-key residual, +and reconstructs all 60 adjacent links in both directions. It rejects +altered price, word and residual selection inputs. Use +`--out fresh-directory` to retain the ten predecessor receipts and +the four new residual and closure receipts. The standard-library replay needs no Git +metadata, network, external root or prior temporary state. +[Source provenance](PROVENANCE.json) · [Path-keyed pins](LOCAL-PINS.json) · +[Predecessor receipt hashes](receipts/SHA256.json) · +[Residual receipt hashes](receipts/R109-SHA256.json) · [Cohort preflight](COHORT.md). + +## Open next questions + +Could a different chart or a changed paid itinerary supply a new +eligible public bank? Start by specifying one exact change and +pricing its complete bill before a support test. The fixed public +bank, existing catalogue and pinned word in this package are +exhausted. A different mechanism would still need signed +arbitrary-input forward and adjoint action, ownership, restoration, +compiler, precision, tape and independent caller and outer replay. + +## Credit + +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) +supplies the exact current word and comparable result, and +[#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +the signed caller. [#7314](https://github.com/CrocSwap/integer-mult-bounds/pull/7314) +supplies the parent native word. [#7319](https://github.com/CrocSwap/integer-mult-bounds/pull/7319) +supplies the independent helper census. [#7338](https://github.com/CrocSwap/integer-mult-bounds/pull/7338) +supplies the independently admitted price inputs and +[#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) +the directed tariff. [#5718](https://github.com/CrocSwap/integer-mult-bounds/pull/5718) +uses chart 602 as a productive insertion in an older rank-nine +construction, and [#6040](https://github.com/CrocSwap/integer-mult-bounds/pull/6040) +reproduces that calibration and tests a later older-word domain. +[#7363](https://github.com/CrocSwap/integer-mult-bounds/pull/7363) +supplies the exact-word modular exterior method for a distinct +rank-eight cohort. OpenAI Codex and subagents materially assisted +proof, implementation, independent verification and packaging. diff --git a/research/p104-rank-seven-prefix-bank-bound/SOURCES.json b/research/p104-rank-seven-prefix-bank-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-rank-seven-prefix-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-seven-prefix-bank-bound/TASK.json b/research/p104-rank-seven-prefix-bank-bound/TASK.json new file mode 100644 index 0000000000..08a226d8f1 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "On exact #7334, test fixed-paid rank-seven 3+4 or 4+3 splits for the five chart602\u2192127 helpers and 65 original frozen public-bank keys.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "P104 rank-seven split research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "A fixed-paid productive split has positive relaxed complete cost only if exact cochart prefix and suffix support can supply a unit pair while keeping the signed caller and supplier contract.", + "budget_minutes": 15, + "evidence": "Two independent prime-field implementations agree on 45 direct prefix exclusions across three frozen selections. Two literal chronology engines agree on 60 links and 20 additional transfers. The residual 13-key replay closes all 65 keys with zero unresolved.", + "open_questions": [ + { + "blocked_by": "The exact fixed-paid and existing-catalogue public bank scope is exhausted. Any changed route needs signed and full-cost verification.", + "first_step": "Choose one explicit new chart or itinerary change, and price its full signed invoice before selecting a bounded support test.", + "question": "Could a different chart or paid itinerary create an eligible bank outside the fixed path scope?", + "why_it_matters": "A legally realized 3+4 or 4+3 target split can improve the complete directed complex invoice." + } + ], + "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": "Use the distinct chart602\u2192127 endpoint group and rank-five/rank-six intermediate classes. Reuse exact prefix minors only through proved literal bank equivalence.", + "scope_status": "changed", + "stop_rule": "One 76,466-event geometry pass, up to 65 frozen alias keys in 20 seconds, then frozen sets of 16, 16 and 13 modular keys with 25 seconds per gate. No suffix or exact pairing when full prefix rank excludes each tested key.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-rank-seven-prefix-bank-bound/VERIFY.json b/research/p104-rank-seven-prefix-bank-bound/VERIFY.json new file mode 100644 index 0000000000..600727c4f5 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Authenticate exact sources; reproduce complete price and geometry, independent exterior minors at both primes for frozen 16+16+13 keys, literal alias classification, all 65 closed dispositions, and changed price, word and residual selection rejection.", + "timeout_seconds": 240 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-rank-seven-prefix-bank-bound/engines/independent/r102_prefix.py b/research/p104-rank-seven-prefix-bank-bound/engines/independent/r102_prefix.py new file mode 100644 index 0000000000..4299e0810a --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/engines/independent/r102_prefix.py @@ -0,0 +1,163 @@ +"""Verify only the 16 frozen R102 prefix keys at a second exact prime.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from time import monotonic +import sys + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +WORD = "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PINS = { + "inputs/PRICE.json": "4e0d6436eb4fc6a9dfa34c05ba98aacc63e3a8bf7214145dd9f9254763c5a13e", + "inputs/GEOMETRY.json": "2d0dee60998d168d2eff4c16794176c5ec3b4d18ffa8bde247602035f1b68129", + "inputs/PREFIX.json": "65c11b0a42092557fe1c64b4feb2f61e2d16c636cfcaddf7f95ec09dbdd27452", + "inputs/7334-WORD.json.gz": WORD, + "inputs/second_prime.py": "21dbd96192e1f60c00ceddba01a7e8d0ddd7d6ad7da4ad3ed22ef2e47cc589c4", +} +PRIME, CAP, SECONDS, EVENTS = 65537, 16, 25, 76466 + + +def unique(items): + result = dict(items) + if len(result) != len(items): + raise ValueError("duplicate JSON key") + return result + + +def pinned(root, name): + raw = (root / name).read_bytes() + if sha256(raw).hexdigest() != PINS[name]: + raise ValueError(f"changed dependency: {name}") + return raw + + +def freeze(raw): + price, geom, primary = [loads(raw[f"inputs/{name}.json"], object_pairs_hook=unique) + for name in ("PRICE", "GEOMETRY", "PREFIX")] + assert price["head"] == geom["head"] == primary["head"] == HEAD + assert price["caller"] == CALLER and price["word_sha256"] == geom["word_sha256"] == WORD + assert geom["price_sha256"] == primary["pins"]["lead/PRICE.json"] == PINS["inputs/PRICE.json"] + assert primary["pins"]["lead/GEOMETRY.json"] == PINS["inputs/GEOMETRY.json"] + assert primary["pins"]["inputs/7334-WORD.json.gz"] == WORD + assert geom["status"] == "EXHAUSTED" and geom["visited_events"] == primary["event_count"] == EVENTS + assert geom["bank_cap"] == price["support_cap"] == primary["case_cap"] == CAP + assert primary["runner_seconds"] == price["support_runner_seconds"] == SECONDS + assert geom["ranks"] == price["cut_ranks"] == [5, 6] and price["endpoint_charts"] == [602, 127] + assert primary["counts"] == {"excluded": CAP} and not primary["unvisited"] + cohort = set(price["cohort"]) + assert cohort == {1457, 1458, 1474, 1475, 1476} + selected = {tuple(row["key"]): row for row in geom["selected"]} + assert len(selected) == len(geom["selected"]) == CAP + earlier = {tuple(row["key"]): row for row in primary["rows"]} + assert list(selected) == list(earlier) + unselected = list(map(tuple, geom["unvisited_keys"])) + assert list(map(tuple, primary["unselected"])) == unselected and len(set(unselected)) == 49 + assert set(unselected).isdisjoint(selected) and len(geom["all_representative_keys"]) == 65 + assert set(unselected) | selected.keys() == set(map(tuple, geom["all_representative_keys"])) + for key in selected: + a, b = selected[key], earlier[key] + assert all(a[field] == b[field] for field in ("public", "owned", "pivots")) + assert b["exterior_rank"] == len(a["public"]) and b["determinant"] + return cohort, selected, earlier, unselected + + +def sweep(word, cohort, selected, earlier, engine, deadline, progress, results): + n, owned, tape = (word[k] for k in ("public", "owned_fields", "program")) + assert (n, owned, len(tape)) == (1501, 68, EVENTS) + assert all((word["initial"][r], word["final"][r]) == (602, 127) for r in cohort) + frames = word["frames"] + span = engine["span"] + low, high = span(frames[602]), span(frames[127]) + assert len(low) == 4 and len(high) == 512 and low < high + requests = defaultdict(list) + for cut, chart in selected: + assert 0 <= cut <= EVENTS and len(frames[chart]) in (5, 6) and low < span(frames[chart]) < high + requests[cut].append(chart) + + active = word["initial"] + [None] * owned + vectors = [{r: 1} for r in range(n)] + [None] * owned + fresh, denoms = set(), set() + progress.update(events=0, first_unvisited_cut=0) + for cut in range(EVENTS + 1): + progress["first_unvisited_cut"] = cut + if (cut % 128 == 0 or cut in requests) and monotonic() >= deadline: + break + for chart in requests.get(cut, ()): + key = cut, chart + bank = [r for r in range(n) if active[r] == chart] + owners = [r for r in range(n, n + owned) if active[r] == chart] + pivots = sorted(set(bank) & cohort) + assert pivots and bank == selected[key]["public"] and owners == selected[key]["owned"] + assert pivots == selected[key]["pivots"] + if cut: + last = tape[cut - 1] + assert chart in (last[2:4] if last[0] == "MOVE" else last[-1:]) + proof = engine["classify"](bank, vectors, cohort) + primary_columns = earlier[key]["columns"] + assert len(primary_columns) == len(set(primary_columns)) == len(bank) + assert cohort.isdisjoint(primary_columns) + determinant = engine["verify_minor"]([vectors[r] for r in bank], primary_columns) + results[key] = dict(key=key, chart_rank=len(frames[chart]), public=bank, owned=owners, pivots=pivots, + independent_minor=proof, primary_minor_axes=primary_columns, + primary_minor_det_mod_65537=determinant, + disposition="excluded" if not proof["kernel"] else "modular_rank_drop") + if cut == EVENTS: + assert active == word["final"] + [None] * owned and not fresh + assert len(results) == CAP + progress["first_unvisited_cut"] = None + break + engine["apply"](tape[cut], active, vectors, fresh, n, denoms, False) + progress["events"] += 1 + progress["denominator_units"] = sorted(denoms) + + +def main(): + parser = ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=ROOT) + args = parser.parse_args() + assert __debug__ and sys.version_info[:2] == (3, 12) + + def stop(*_): + raise TimeoutError("hard 25-second cap") + + signal(SIGALRM, stop) + alarm(SECONDS) + deadline = monotonic() + SECONDS - 2 + selected, unselected, result, progress, checks = {}, [], {}, {}, [] + timeout = None + try: + raw = {rel: pinned(args.root, rel) for rel in PINS} + cohort, selected, earlier, unselected = freeze(raw) + engine = run_path(str(args.root / "inputs/second_prime.py")) + assert engine["PRIME"] == PRIME + checks = engine["controls"]() + payload = decompress(raw["inputs/7334-WORD.json.gz"]) + assert sha256(payload).hexdigest() == PAYLOAD + word = loads(payload, object_pairs_hook=unique) + sweep(word, cohort, selected, earlier, engine, deadline, progress, result) + except TimeoutError as error: + timeout = str(error) + finally: + alarm(0) + + rows = [result[k] for k in selected if k in result] + visited_all = timeout is None and progress.get("first_unvisited_cut", 0) is None + agreement = visited_all and all(row["disposition"] == "excluded" for row in rows) + print(dumps(dict(head=HEAD, caller=CALLER, pins=PINS, modulus=PRIME, cap_cases=CAP, cap_seconds=SECONDS, + progress=progress, controls=checks, complete=visited_all, primary_agreement=agreement, timeout=timeout, + counts=Counter(row["disposition"] for row in rows), rows=rows, + unvisited_selected=[k for k in selected if k not in result], unselected=unselected), indent=2, sort_keys=True)) + if not agreement: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-seven-prefix-bank-bound/engines/independent/second_prime.py b/research/p104-rank-seven-prefix-bank-bound/engines/independent/second_prime.py new file mode 100644 index 0000000000..0be5407fe6 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/engines/independent/second_prime.py @@ -0,0 +1,339 @@ +"""Independently verify R97's 310 frozen R96 bank keys modulo 65537.""" + +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from math import isqrt +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic +import sys + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +WORD = "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PINS = { + "inputs/PRICE.json": "a78be64c3e3ae8a0e532237c4dd3541aa9ad3fcbbc3c25d79c8a03fb7e07c525", + "inputs/GEOMETRY.json": "c6f9f018df8b58fcdf4f44356bd59bcac6d411b7845104ff4ad372ed4a95cfbd", + "inputs/REMAINING.json": "3597499663a57702856945e91214a65e1d0f94db8643b93c0234c2bbf9291b1a", + "inputs/7334-WORD.json.gz": WORD, +} +PRIME = 65537 +CASES = 310 +SECONDS = 25 +EVENTS = 76466 + + +def unique(items): + data = dict(items) + if len(items) != len(data): + raise ValueError("duplicate JSON key") + return data + + +def authenticate(root): + raw = {} + for rel, expected in PINS.items(): + data = (root / rel).read_bytes() + if sha256(data).hexdigest() != expected: + raise ValueError(f"changed dependency: {rel}") + raw[rel] = data + return raw + + +@cache +def coefficient(value): + q = Fraction(value) + if not q or q.denominator % PRIME == 0: + raise ValueError("zero scalar or denominator divisible by modulus") + return q.numerator * pow(q.denominator, -1, PRIME) % PRIME, q.denominator + + +def axpy(target, source, scale): + if scale: + for role, old in source.items(): + current = (target.get(role, 0) + scale * old) % PRIME + if current: + target[role] = current + else: + target.pop(role, None) + + +def scaled(vector, scale): + return {i: y for i, x in vector.items() if (y := x * scale % PRIME)} + + +def verify_minor(vectors, columns): + """Independently recompute a minor on the original projected rows.""" + matrix = [[row.get(c, 0) for c in columns] for row in vectors] + determinant = 1 + for c in range(len(matrix)): + pivot = next((r for r in range(c, len(matrix)) if matrix[r][c]), None) + if pivot is None: + return 0 + if pivot != c: + matrix[c], matrix[pivot] = matrix[pivot], matrix[c] + determinant = -determinant + diag = matrix[c][c] + determinant = determinant * diag % PRIME + inverse = pow(diag, -1, PRIME) + for r in range(c + 1, len(matrix)): + factor = matrix[r][c] * inverse % PRIME + if factor: + for k in range(c + 1, len(matrix)): + matrix[r][k] = (matrix[r][k] - factor * matrix[c][k]) % PRIME + matrix[r][c] = 0 + return determinant % PRIME + + +def classify(bank, vectors, cohort): + full_rows = [vectors[r] for r in bank] + exterior = [{i: x for i, x in row.items() if i not in cohort} for row in full_rows] + basis, kernel = [], [] + determinant = 1 + for index, vector in enumerate(exterior): + work = vector.copy() + combination = {index: 1} + for col, known, combo in basis: + factor = -work.get(col, 0) + axpy(work, known, factor) + axpy(combination, combo, factor) + if not work: + image = {} + for i, factor in combination.items(): + axpy(image, full_rows[i], factor) + assert image.keys() <= cohort + kernel.append(dict(cut={bank[i]: x for i, x in combination.items()}, endpoint=image)) + continue + col = max(work) + pivot = work[col] + determinant = determinant * pivot % PRIME + inverse = pow(pivot, -1, PRIME) + basis.append((col, scaled(work, inverse), scaled(combination, inverse))) + rank = len(basis) + assert rank + len(kernel) == len(bank) + columns = [col for col, _, _ in basis] + if kernel: + return dict(rank=rank, kernel=kernel, minor_axes=None, determinant=None) + assert columns and verify_minor(exterior, columns) == determinant != 0 + return dict(rank=rank, kernel=[], minor_axes=columns, determinant=determinant) + + +def apply(event, state, vectors, fresh, n, denominators, backward): + op, r, *args = event + current = state[r] + if op == "MOVE": + old, new, owned = args + assert owned == (r >= n) + assert current == (new if backward else old) + state[r] = old if backward else new + fresh.discard(r) + return + if op in ("INIT", "CLEAR"): + assert r >= n + c, = args + entering = (op == "CLEAR") if backward else (op == "INIT") + if entering: + assert current is None and vectors[r] is None + state[r], vectors[r] = c, {} + if not backward: + fresh.add(r) + else: + assert current == c and vectors[r] is not None + state[r] = vectors[r] = None + fresh.discard(r) + return + assert op in ("SCALE", "ADD", "COPY") and current == args[-1] and vectors[r] is not None + factor, denominator = coefficient(args[-2]) + denominators.add(denominator) + if op == "SCALE": + vectors[r] = scaled(vectors[r], factor) + else: + src = args[0] + assert src != r and state[src] == current and vectors[src] is not None + if backward: + axpy(vectors[src], vectors[r], factor) + if op == "COPY": + assert r >= n + vectors[r] = {} + elif op == "COPY": + assert r >= n and r in fresh and not vectors[r] + vectors[r] = scaled(vectors[src], factor) + else: + axpy(vectors[r], vectors[src], factor) + fresh.discard(r) + + +def controls(): + assert all(PRIME % i for i in range(2, isqrt(PRIME) + 1)) + witness = classify([0, 1], [{3: 2, 8: 1}, {3: 3, 8: 4}], set()) + assert witness["minor_axes"] == [8, 3] and witness["determinant"] == PRIME - 5 + dropped = classify([0, 1], [{0: 1, 8: 1}, {1: 1, 8: 1}], {0, 1}) + assert dropped["kernel"] == [dict(cut={0: PRIME - 1, 1: 1}, endpoint={0: PRIME - 1, 1: 1})] + tape = [("ADD", 1, 0, "-3/2", 4), ("SCALE", 0, "2", 4), ("INIT", 2, 4), + ("COPY", 2, 1, "1", 4), ("ADD", 0, 2, "5", 4), ("CLEAR", 2, 4)] + result = [] + for backward in (False, True): + state, vectors, fresh, denoms = [4, 4, None], [{0: 1}, {1: 1}, None], set(), set() + for event in reversed(tape) if backward else tape: + apply(event, state, vectors, fresh, 2, denoms, backward) + assert state == [4, 4, None] and not fresh and denoms == {1, 2} + result.append(vectors) + assert result[0] == [{0: coefficient("-11/2")[0], 1: 5}, {0: coefficient("-3/2")[0], 1: 1}, None] + assert result[1] == [{0: coefficient("-11/2")[0], 1: coefficient("-3/2")[0]}, {0: 5, 1: 1}, None] + try: + coefficient("1/65537") + except ValueError: + pass + else: + raise AssertionError("nonunit denominator admitted") + return ["prime and signed nonzero minor", "planted pure kernel", "owned COPY forward and adjoint", + "nonunit denominator rejection"] + + +def span(frame): + vectors = {0} + for v in frame: + assert v not in vectors + vectors |= {v ^ w for w in vectors} + return vectors + + +def sweep(word, keys, cohort, deadline, result, progress, backward, previous=None): + tape, n, owned = (word[k] for k in ("program", "public", "owned_fields")) + assert (len(tape), n, owned) == (EVENTS, 1501, 68) + origin, target = ("final", "initial") if backward else ("initial", "final") + state = word[origin] + [None] * owned + vectors = [{r: 1} for r in range(n)] + [None] * owned + fresh, denoms = set(), set() + request = defaultdict(list) + frames = word["frames"] + low, high = span(frames[3]), span(frames[245]) + for cut, chart in keys: + assert 0 <= cut <= EVENTS and len(frames[chart]) == 4 and low < span(frames[chart]) < high + request[cut].append(chart) + boundaries = range(EVENTS, -1, -1) if backward else range(EVENTS + 1) + progress.update(events=0, first_unvisited_cut=boundaries.start, denominator_units=[]) + for cut in boundaries: + progress["first_unvisited_cut"] = cut + if (cut % 128 == 0 or cut in request) and monotonic() >= deadline: + break + for chart in request.get(cut, []): + key = (cut, chart) + public_bank = [r for r in range(n) if state[r] == chart] + owned_bank = [r for r in range(n, n + owned) if state[r] == chart] + pivots = sorted(set(public_bank) & cohort) + assert public_bank and pivots + if cut: + event = tape[cut - 1] + assert chart in (event[2:4] if event[0] == "MOVE" else event[-1:]) + bank = dict(public=public_bank, owned=owned_bank, pivots=pivots) + if previous is not None: + assert bank == previous[key]["bank"] + result[key] = dict(bank=bank, **classify(public_bank, vectors, cohort)) + if cut == (0 if backward else EVENTS): + assert state == word[target] + [None] * owned and not fresh + assert set(result) == set(keys) + progress["first_unvisited_cut"] = None + break + apply(tape[cut - 1 if backward else cut], state, vectors, fresh, n, denoms, backward) + progress["events"] += 1 + progress["denominator_units"] = sorted(denoms) + + +def pairing(prefix, suffix): + def dot(left, right): + return sum(v * right.get(i, 0) for i, v in left.items()) % PRIME + + return [[dict(cut=dot(a["cut"], b["cut"]), endpoint=dot(a["endpoint"], b["endpoint"])) + for b in suffix["kernel"]] for a in prefix["kernel"]] + + +def main(): + parser = ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=ROOT) + parser.add_argument("--controls-only", action="store_true") + args = parser.parse_args() + assert __debug__ and sys.version_info[:2] == (3, 12) + checks = controls() + if args.controls_only: + print(dumps(checks)) + return + + def stop(*_): + raise TimeoutError("hard 25-second cap") + + start = monotonic() + signal(SIGALRM, stop) + alarm(SECONDS) + timeout = None + keys, prior, prefix, suffix = [], [], {}, {} + prefix_progress, suffix_progress = {}, {} + try: + raw = authenticate(args.root) + price, geom, remaining = [loads(raw[f"inputs/{name}.json"], object_pairs_hook=unique) + for name in ("PRICE", "GEOMETRY", "REMAINING")] + assert price["head"] == geom["head"] == remaining["head"] == HEAD and price["caller"] == CALLER + assert price["word_sha256"] == geom["word_sha256"] == WORD + assert geom["price_sha256"] == PINS["inputs/PRICE.json"] + assert remaining["input_sha256"]["lead/GEOMETRY.json"] == PINS["inputs/GEOMETRY.json"] + assert geom["status"] == "EXHAUSTED" and geom["visited_events"] == EVENTS + keys = list(map(tuple, remaining["unvisited_prefix"])) + prior = remaining["dual_drops_requiring_rational"] + assert len(keys) == len(set(keys)) == remaining["next_modular_cases"] == CASES + assert remaining["next_modular_runner_seconds"] == SECONDS + assert keys == list(map(tuple, geom["unvisited_keys"])) + selected = {tuple(row["key"]) for row in geom["selected"]} + assert len(selected) == 16 and not set(keys) & selected and set(map(tuple, prior)) <= selected + assert set(keys) | selected == set(map(tuple, geom["all_representative_keys"])) + assert prior == [[41740, 242], [45266, 242]] + payload = decompress(raw["inputs/7334-WORD.json.gz"]) + assert sha256(payload).hexdigest() == PAYLOAD + word = loads(payload, object_pairs_hook=unique) + cohort = set(price["cohort"]) + assert len(cohort) == 15 and all((word["initial"][r], word["final"][r]) == (3, 245) for r in cohort) + deadline = start + SECONDS - 2 + sweep(word, keys, cohort, deadline, prefix, prefix_progress, False) + candidates = [key for key in keys if key in prefix and prefix[key]["kernel"]] + if candidates: + sweep(word, candidates, cohort, deadline, suffix, suffix_progress, True, prefix) + else: + suffix_progress.update(events=0, first_unvisited_cut=None, denominator_units=[]) + except TimeoutError as error: + timeout = str(error) + finally: + alarm(0) + + results = [] + for key in keys: + left, right = prefix.get(key), suffix.get(key) + pair = None + if left and not left["kernel"]: + status = "prefix_exclusion" + elif right and not right["kernel"]: + status = "suffix_exclusion" + elif right: + status = "dual_drop" + pair = pairing(left, right) + else: + status = "unvisited" + results.append(dict(key=key, status=status, prefix=left, suffix=right, modular_pairings=pair)) + complete = (timeout is None and prefix_progress.get("first_unvisited_cut", 0) is None + and suffix_progress.get("first_unvisited_cut", 0) is None) + print(dumps(dict(head=HEAD, caller=CALLER, pins=PINS, modulus=PRIME, controls=checks, + cap_cases=CASES, cap_seconds=SECONDS, prefix_progress=prefix_progress, suffix_progress=suffix_progress, + timeout=timeout, complete=complete, results=results, + counts=Counter(row["status"] for row in results), previously_frozen_exact_keys=prior), + indent=2, sort_keys=True)) + if not complete: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-seven-prefix-bank-bound/engines/independent/verify.py b/research/p104-rank-seven-prefix-bank-bound/engines/independent/verify.py new file mode 100644 index 0000000000..93ec575302 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/engines/independent/verify.py @@ -0,0 +1,256 @@ +"""Reverse chart continuity or second-prime checks on the exact R105 key sets.""" +from argparse import ArgumentParser +from bisect import bisect_left +from collections import Counter, defaultdict +from fractions import Fraction +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from time import monotonic +import sys + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +EVENTS = 76466 +PINS = { + "inputs/GEOMETRY.json": "2d0dee60998d168d2eff4c16794176c5ec3b4d18ffa8bde247602035f1b68129", + "inputs/PRICE.json": "4e0d6436eb4fc6a9dfa34c05ba98aacc63e3a8bf7214145dd9f9254763c5a13e", + "inputs/PREFIX.json": "65c11b0a42092557fe1c64b4feb2f61e2d16c636cfcaddf7f95ec09dbdd27452", + "inputs/PREFIX-SECOND-PRIME.json": "51c9eb3af7b4d5ff60daef468f3bf262cb485bb88f4d0394d91b83d7eba2bffd", + "inputs/ALIASES.json": "ba0120da7b05b948b1e8294c6b3844deade2c40be1f2e0abf4e0beef395f5c85", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", +} +MOD_PINS = { + "inputs/SELECTION.json": "3bd7bdc9859436ef1d75d011e09d9dfc43a731c5b0a8e9c42fc96d9a6481a30c", + "inputs/MODULAR.json": "1d99a9842dc8c42395878eb0c14b0027656041f150672491d65d3f023d9df23d", + "inputs/r102_prefix.py": "505eca6677cc4e905494bdbf027d23c7ad288aa26889443db5d99d3ec41488f5", + "inputs/second_prime.py": "21dbd96192e1f60c00ceddba01a7e8d0ddd7d6ad7da4ad3ed22ef2e47cc589c4", +} + + +def unique(items): + d = dict(items) + if len(d) != len(items): + raise ValueError("duplicate JSON key") + return d + + +def blocked(event, public): + op, dst, *args = event + if op in ("MOVE", "INIT", "CLEAR", "COPY"): + return op + assert op in ("ADD","SCALE") and Fraction(args[-2]) + return "public/owned" if op == "ADD" and ((dst < public) != (args[0] < public)) else None + + +def prefix_blocked(event, roles): + op, dst, *args = event + if dst not in roles: + return False + return not (op == "SCALE" or op == "ADD" and args[0] in roles) + + +def controls(): + assert blocked(["ADD",1,2,"-1/2",8],5) is None + assert blocked(["ADD",7,1,"-1/2",8],5) == "public/owned" + assert not prefix_blocked(["ADD",7,1,"-1/2",8],{1,2}) + assert prefix_blocked(["ADD",1,7,"-1/2",8],{1,2}) + assert prefix_blocked(["MOVE",1,8,9,False],{1,2}) + return ["invertible signed ADD", "owned reads preserve public prefix", "owned writes and public MOVE block"] + + +def span(frame): + xs = {0} + for v in frame: + assert v not in xs + xs |= {v ^ w for w in xs} + return xs + + +def reverse(word, rows, cohort, deadline, state): + n, owned, tape = (word[k] for k in ("public","owned_fields","program")) + assert (n,owned,len(tape)) == (1501,68,EVENTS) + frames=word["frames"] + low,high=span(frames[602]),span(frames[127]) + charts={c for _,c in rows} + assert len(charts)==5 and all(len(frames[c])==6 and low=deadline: + raise TimeoutError("reverse chronology cap") + for c in requests.get(cut,[]): + p=[r for r in range(n) if live[r]==c] + o=[r for r in range(n,n+owned) if live[r]==c] + assert rows[cut,c]==dict(key=[cut,c],public=p,owned=o,pivots=sorted(set(p)&cohort)) + state["checked"].append([cut,c]) + if cut==0: + assert live==word["initial"]+[None]*owned + state["first_unvisited_event"]=None + break + t=cut-1 + op,d,*a=e=tape[t] + if op=="MOVE": + f,z,flag=a + assert live[d]==z and flag==(d>=n) + live[d]=f + incident=f,z + elif op in ("INIT","CLEAR"): + c,=a + assert d>=n and live[d]==(c if op=="INIT" else None) + live[d]=None if op=="INIT" else c + incident=(c,) + else: + assert op in ("ADD","COPY","SCALE") and live[d]==a[-1] + if op!="SCALE": + assert d!=a[0] and live[a[0]]==live[d] + assert op!="COPY" or d>=n + incident=(a[-1],) + if d in public_union: + writes[d].append((t,e)) + for c in incident: + if c in charts: + contacts[c].append((t,e)) + state["events"]+=1 + return n, {c:list(reversed(v)) for c,v in contacts.items()}, {r:list(reversed(v)) for r,v in writes.items()} + + +def between(values,lo,hi): + key=lambda row:row[0] + return values[bisect_left(values,lo,key=key):bisect_left(values,hi,key=key)] + + +def component_summary(groups,known): + return [dict(keys=g,reuses=[k for k in g if k in known]) for g in groups] + + +def alias(word,rows,cohort,known,prior,deadline,state): + n, contacts, writes=reverse(word,rows,cohort,deadline,state) + ordered=sorted(rows,key=lambda k:(k[1],k[0])) + groups, public_groups, links, diagnostic=[],[],[],[] + last=None + for key in ordered: + if monotonic()>=deadline: + raise TimeoutError("alias key cap") + strict_ok=public_ok=False + if last is not None and last[1]==key[1]: + lo,c=last + hi=key[0] + a,b=rows[last],rows[key] + same=all(a[f]==b[f] for f in ("public","owned","pivots")) + events=between(contacts.get(c,[]),lo,hi) + blockers=[t for t,e in events if blocked(e,n)] + strict_ok=same and not blockers + fixed=set(a["public"]) + public_ok=a["public"]==b["public"] and not any( + prefix_blocked(e,fixed) for r in fixed for _,e in between(writes.get(r,[]),lo,hi)) + assert not strict_ok or public_ok + links.append(dict(left=last,right=key,same_bank=same,blockers=blockers,alias=strict_ok)) + if public_ok and not strict_ok: + diagnostic.append(dict(left=last,right=key,events=events,strict_blockers=blockers)) + if not strict_ok: + groups.append([]) + if not public_ok: + public_groups.append([]) + groups[-1].append(key) + public_groups[-1].append(key) + last=key + strict=component_summary(groups,known) + public_only=component_summary(public_groups,known) + assert len(links)==60 and prior["timeout"] is None and not prior["unvisited"] + assert dumps(links,sort_keys=True)==dumps(prior["links"],sort_keys=True) + assert dumps(strict,sort_keys=True)==dumps(prior["classes"],sort_keys=True) + def reuse(components): + return sorted(k for cls in components if cls["reuses"] for k in cls["keys"] if k not in known) + return dict(agreement=True,links=links,strict_classes=strict,strict_new_reuses=reuse(strict), + fixed_public_only_classes=public_only,fixed_public_new_reuses=reuse(public_only), + diagnostic_additional_links=diagnostic) + + +def modular(root,word,rows,cohort,selection,prior,deadline,state): + assert selection["head"]==prior["head"]==HEAD and prior["prime"]==65521 + assert prior["counts"]=={"prefix exclusion":16} + cases={tuple(r["key"]):r for r in selection["selected"]} + primary={tuple(r["key"]):r["prefix"] for r in prior["results"]} + assert list(cases)==list(primary) and len(cases)==16 + assert cases.keys()<=rows.keys() + for k,r in cases.items(): + assert all(r[f]==rows[k][f]==primary[k][f] for f in ("public","owned","pivots")) + engine=run_path(str(root/"inputs/second_prime.py")) + adapter=run_path(str(root/"inputs/r102_prefix.py")) + assert engine["PRIME"]==65537 + checks=engine["controls"]() + result={} + adapter["sweep"](word,cohort,cases,primary,engine,deadline,state,result) + assert len(result)==16 and state["first_unvisited_cut"] is None + assert all(r["disposition"]=="excluded" for r in result.values()) + return dict(agreement=True,modulus=65537,rows=list(result.values()),controls=checks, + certified_primary_axes=sum(bool(r["primary_minor_det_mod_65537"]) for r in result.values()), + counts={"prefix exclusion":16}) + + +def main(): + p=ArgumentParser(description=__doc__) + p.add_argument("mode",choices=("alias","modular","controls")) + p.add_argument("--root",type=Path,default=ROOT) + a=p.parse_args() + assert __debug__ and sys.version_info[:2]==(3,12) + if a.mode=="controls": + print(dumps(controls())) + return + seconds,cap=(20,65) if a.mode=="alias" else (25,16) + pins=PINS if a.mode=="alias" else PINS|MOD_PINS + def stop(*_): + raise TimeoutError("hard runner cap") + signal(SIGALRM,stop) + alarm(seconds) + deadline=monotonic()+seconds-2 + result,reason,state={},None,{} + try: + raw={} + for rel,h in pins.items(): + data=(a.root/rel).read_bytes() + if sha256(data).hexdigest()!=h: + raise ValueError(f"changed dependency: {rel}") + raw[rel]=data + def read(name): + return loads(raw[f"inputs/{name}.json"],object_pairs_hook=unique) + price,geom,old,second=(read(name) for name in ("PRICE","GEOMETRY","PREFIX","PREFIX-SECOND-PRIME")) + assert price["head"]==geom["head"]==old["head"]==second["head"]==HEAD + rows={tuple(r["key"]):r for r in geom["all_representatives"]} + assert len(rows)==len(geom["all_representatives"])==65 and geom["visited_events"]==EVENTS + known={tuple(r["key"]) for r in old["rows"] if r["determinant"]} + assert known=={tuple(r["key"]) for r in second["rows"] if r["independent_minor"]["determinant"]} + assert len(known)==16 and old["counts"]==second["counts"]=={"excluded":16} + cohort=set(price["cohort"]) + assert cohort=={1457,1458,1474,1475,1476} + payload=decompress(raw["inputs/7334-WORD.json.gz"]) + assert sha256(payload).hexdigest()==PAYLOAD + word=loads(payload,object_pairs_hook=unique) + if a.mode=="alias": + result=alias(word,rows,cohort,known,read("ALIASES"),deadline,state) + else: + result=modular(a.root,word,rows,cohort,read("SELECTION"),read("MODULAR"),deadline,state) + except TimeoutError as exc: + reason=str(exc) + finally: + alarm(0) + print(dumps(dict(head=HEAD,pins=pins,mode=a.mode,cap_cases=cap,cap_seconds=seconds,progress=state, + new_support_cases=0 if a.mode=="alias" else 16,complete=reason is None, + timeout=reason,alias_controls=controls(),**result),indent=2,sort_keys=True)) + if reason: + raise SystemExit(2) + + +if __name__=="__main__": + main() diff --git a/research/p104-rank-seven-prefix-bank-bound/engines/r102/geometry.py b/research/p104-rank-seven-prefix-bank-bound/engines/r102/geometry.py new file mode 100644 index 0000000000..2d50a022f9 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/engines/r102/geometry.py @@ -0,0 +1,115 @@ +"""Exact full-word occupied rank-five/six 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="4e0d6436eb4fc6a9dfa34c05ba98aacc63e3a8bf7214145dd9f9254763c5a13e" +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/"lead/PRICE.json",PRICE)) + word=json.loads(decompress(checked(root/"inputs/7334-WORD.json.gz",WORD))) + assert price["word_sha256"]==WORD and price["support_cap"]==16 + n=word["public"] + cohort=set(price["cohort"]) + source, target = price["endpoint_charts"] + assert len(cohort)==5 and all(word["initial"][r]==source and word["final"][r]==target for r in cohort) + spaces=list(map(span,word["frames"])) + intermediate={i for i,w in enumerate(spaces) if len(w) in (32,64) and spaces[source]=n),pivots=sorted(pivots))) + for c in sorted(bank): + save(0,c) + until=monotonic()+18 + visited=0 + for t,e in enumerate(word["program"]): + if t%128==0 and monotonic()>=until: + break + op,r,*args=e + old=chart[r] + if op=="MOVE": + assert old==args[0] and args[2]==(r>=n) + new=args[1] + elif op=="INIT": + assert old is None and r>=n + new=args[0] + elif op=="CLEAR": + assert old==args[0] and r>=n + new=None + else: + assert old==args[-1] and op in ("ADD","COPY","SCALE") + if op in ("ADD","COPY"): + assert chart[args[0]]==old + new=old + if old in intermediate: + bank[old].remove(r) + if new in intermediate: + bank[new].add(r) + chart[r]=new + for c in sorted({v for v in (old,new) if v in intermediate}): + save(t+1,c) + visited=t+1 + complete=visited==len(word["program"]) + if complete: + assert chart==word["final"]+[None]*word["owned_fields"] + def score(r): + return (bool(r["owned"]),len(r["pivots"])<2,len(r["public"])-len(r["pivots"]), + len(r["public"]),r["key"]) + selected=[] + bank_shapes=set() + selected_clocks=set() + if complete: + for row in sorted(rows,key=score): + shape=row["key"][1],tuple(row["public"]),tuple(row["owned"]) + if shape in bank_shapes or row['key'][0] in selected_clocks: + continue + bank_shapes.add(shape) + selected_clocks.add(row['key'][0]) + selected.append(row) + if len(selected)==16: + break + assert len({tuple(row["key"]) for row in rows})==len(rows) + picked={tuple(r["key"]) for r in selected} + print(json.dumps(dict(head=price["head"],word_sha256=WORD,price_sha256=PRICE,visited_events=visited, + status="EXHAUSTED" if complete else "CAPPED",ranks=[5,6],intermediate_charts=sorted(intermediate),bank_cap=16, + eligible_bank_count=len(rows),eligible_chart_count=len({r["key"][1] for r in rows}), + selected=selected,unvisited_keys=[r["key"] for r in rows if tuple(r["key"]) not in picked], + all_representative_keys=[r["key"] for r in rows],all_representatives=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-seven-prefix-bank-bound/engines/r102/prefix.py b/research/p104-rank-seven-prefix-bank-bound/engines/r102/prefix.py new file mode 100644 index 0000000000..0ae58990c2 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/engines/r102/prefix.py @@ -0,0 +1,49 @@ +"""Test the frozen sixteen rank-seven-cohort banks by exact exterior minors.""" +from collections import Counter +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path +import sys +from time import monotonic + +PINS = { + "lead/PRICE.json": "4e0d6436eb4fc6a9dfa34c05ba98aacc63e3a8bf7214145dd9f9254763c5a13e", + "lead/GEOMETRY.json": "2d0dee60998d168d2eff4c16794176c5ec3b4d18ffa8bde247602035f1b68129", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/exterior_rank56.py": "9fceafc627fe3781bcb8d5229eaefebc557de613f0d4723aa1d36ce4ab9954ac", +} + + +def main(): + assert __debug__ + deadline = monotonic() + 22 + root = Path(sys.argv[1]) + raw = {} + for name, digest in PINS.items(): + raw[name] = (root/name).read_bytes() + if sha256(raw[name]).hexdigest() != digest: + raise ValueError(f"changed dependency: {name}") + engine = run_path(str(root/"inputs/exterior_rank56.py")) + unique = engine["unique"] + price = json.loads(raw["lead/PRICE.json"], object_pairs_hook=unique) + geometry = json.loads(raw["lead/GEOMETRY.json"], object_pairs_hook=unique) + word = json.loads(decompress(raw["inputs/7334-WORD.json.gz"]), object_pairs_hook=unique) + assert geometry["head"] == price["head"] == engine["HEAD"] + assert geometry["status"] == "EXHAUSTED" and geometry["eligible_bank_count"] == 65 + assert len(geometry["selected"]) == 16 and len(price["cohort"]) == 5 + selected = {tuple(row["key"]): row for row in geometry["selected"]} + controls = engine["controls"]() + result, events = engine["sweep"](word, list(selected), set(price["cohort"]), deadline) + assert all(all(row[k] == selected[key][k] for k in ("key","public","owned","pivots")) + for key,row in result.items()) + rows = [result[k] for k in selected if k in result] + print(json.dumps({"head":price["head"],"pins":PINS,"event_count":events,"case_cap":16,"runner_seconds":25, + "controls":controls,"rows":rows,"counts":Counter(row["disposition"] for row in rows), + "unvisited":[list(k) for k in selected if k not in result], + "unselected":geometry["unvisited_keys"]},indent=2,sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-seven-prefix-bank-bound/engines/r102/quote.py b/research/p104-rank-seven-prefix-bank-bound/engines/r102/quote.py new file mode 100644 index 0000000000..c295764e6c --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/engines/r102/quote.py @@ -0,0 +1,70 @@ +"""Preprice fixed-paid rank-seven splits for the 602-to-127 helper cohort.""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "inputs/7314-HELPERS.json": "bf353b3e05d0bf5fe3e49c15673c4cb9203251329bd594009303541cf7fecc09", + "inputs/7334-CHANGED.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", +} + + +def unique(pairs): + out = dict(pairs) + if len(out) != len(pairs): + raise ValueError("duplicate input key") + return out + + +def main(): + assert __debug__ + data = {} + for name, pin in PINS.items(): + raw = (ROOT / name).read_bytes() + if sha256(raw).hexdigest() != pin: + raise ValueError(f"changed dependency {name}") + if name.endswith(".json"): + data[Path(name).stem] = json.loads(raw, object_pairs_hook=unique) + a, b, h, x = (data[k] for k in ("ADMITTED", "READBACK", "7314-HELPERS", "7334-CHANGED")) + assert a["head"] == b["head"] == "aaeec8c0acf01e99a5f331ef363a698d9c084ace" + assert a["exit"] == 0 and a["caller"] == b["caller_head"] and b["copies"] == 17 + assert len(h["rows"]) == 1101 and h["complete"] and len(x["roles"]) == 14 + protected = set(x["roles"]) | {863, 1355, 1531, 1567, 1568} + cohort = sorted(r["role"] for r in h["rows"] if r["role"] not in protected + and (r["initial"], r["final"], r["old_productive_rank"]) == (602, 127, 7)) + assert len(cohort) == len(set(cohort)) == 5 + paid, target = [Counter({int(k): v for k, v in b[name].items()}) for name in ("paid", "targets")] + old = target.copy() + old.subtract(paid) + assert (sum(paid.values()),sum(target.values()),sum(k*v for k,v in old.items())) == (110519,22461,1424) + assert target[7] >= 17*len(cohort) and not b["empty_root_credits"] + change = {3:17,4:17,7:-17} + new = old.copy() + new.update(change) + cost = run_path(str(ROOT/"inputs/pricing.py"))["cost"] + crossing = Q(a["crossing"][1]) + probe = crossing + Q(1,10**9) + moonshot = Q("0.0040075385047236") + assert cost(old,probe)[1] < 0 < cost(new,probe)[0] + def price(k): + delta = cost(change,k) + incumbent = cost(old,k) + return {"old_margin":list(map(str,incumbent)), "gross_one":list(map(str,delta)), + "whole_5_upper":str(5*delta[1]),"complete_5_upper":str(incumbent[1]+5*delta[1])} + print(json.dumps({"head":a["head"],"caller":a["caller"],"pins":PINS,"cohort":cohort, + "word_sha256":a["inputs"]["WORD.json.gz"],"productive_delta":change,"paid_delta":{}, + "endpoint_charts":[602,127],"cut_ranks":[5,6],"incumbent":str(crossing),"probe":str(probe),"moonshot":str(moonshot), + "at_incumbent":price(crossing),"at_target":price(moonshot), + "event_cap":76466,"geometry_runner_seconds":20,"support_cap":16,"support_runner_seconds":25, + "exact_cap":4,"exact_runner_seconds":35,"build_cap":1},indent=2,sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-seven-prefix-bank-bound/engines/r105/alias_rank_seven.py b/research/p104-rank-seven-prefix-bank-bound/engines/r105/alias_rank_seven.py new file mode 100644 index 0000000000..eff76de947 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/engines/r105/alias_rank_seven.py @@ -0,0 +1,104 @@ +"""Classify proven equivalences of the 65 frozen rank-seven bank keys.""" +from collections import defaultdict +from fractions import Fraction +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from signal import SIGALRM, alarm, signal +import sys +from time import monotonic + +PINS = { + "lead/PRICE.json": "4e0d6436eb4fc6a9dfa34c05ba98aacc63e3a8bf7214145dd9f9254763c5a13e", + "lead/GEOMETRY.json": "2d0dee60998d168d2eff4c16794176c5ec3b4d18ffa8bde247602035f1b68129", + "lead/PREFIX.json": "65c11b0a42092557fe1c64b4feb2f61e2d16c636cfcaddf7f95ec09dbdd27452", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", +} + + +def checked(root): + items = {} + for path,pin in PINS.items(): + raw = (root/path).read_bytes() + if sha256(raw).hexdigest()!=pin: + raise ValueError(f"changed dependency {path}") + items[path] = json.loads(decompress(raw) if path.endswith(".gz") else raw) + return items + + +def harmless(event,chart,public): + op,d,*args = event + if op=="MOVE": + return chart not in args[:2] + if op in ("INIT","CLEAR"): + return chart!=args[0] + assert op in ("ADD","COPY","SCALE") + if chart!=args[-1]: + return True + if op=="COPY": + return False + assert Fraction(args[-2]) + return op=="SCALE" or (d=deadline: + raise TimeoutError("cooperative alias classification cap") + key = row["key"] + ok = False + if last is not None: + t0,t1 = last["key"][0],key[0] + same = all(last[f]==row[f] for f in ("public","owned","pivots")) + blockers = [j for j in range(t0,t1) if not harmless(word["program"][j],chart,word["public"])] + ok = same and not blockers + links.append({"left":last["key"],"right":key,"same_bank":same,"blockers":blockers,"alias":ok}) + if not ok: + classes.append([]) + classes[-1].append(key) + unvisited.remove(key) + last=row + assert sum(map(len,classes))==65 and len(links)==60 + except TimeoutError as exc: + reason = str(exc) + finally: + alarm(0) + results = [{"keys":keys,"reuses":sorted(k for k in keys if tuple(k) in passed)} for keys in classes] + print(json.dumps({"pins":PINS,"cap_cases":65,"cap_seconds":20,"classes":results, + "links":links,"unvisited":unvisited,"timeout":reason},indent=2,sort_keys=True)) + if reason: + raise SystemExit(2) + + +if __name__=="__main__": + main() diff --git a/research/p104-rank-seven-prefix-bank-bound/engines/r105/freeze_support.py b/research/p104-rank-seven-prefix-bank-bound/engines/r105/freeze_support.py new file mode 100644 index 0000000000..da83747e9c --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/engines/r105/freeze_support.py @@ -0,0 +1,46 @@ +"""Select sixteen previously unresolved rank-seven bank classes.""" +from collections import Counter, defaultdict +from hashlib import sha256 +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +PINS = { + "ALIASES.json":"ba0120da7b05b948b1e8294c6b3844deade2c40be1f2e0abf4e0beef395f5c85", + "round102-input/lead/GEOMETRY.json":"2d0dee60998d168d2eff4c16794176c5ec3b4d18ffa8bde247602035f1b68129", +} + + +def main(): + inputs = {} + for path,pin in PINS.items(): + raw = (ROOT/path).read_bytes() + if sha256(raw).hexdigest()!=pin: + raise ValueError(f"changed dependency {path}") + inputs[path] = json.loads(raw) + alias,geo = inputs.values() + assert alias["timeout"] is None and not alias["unvisited"] + assert len(alias["classes"])==45 and len(geo["all_representatives"])==65 + bank_by_key = {tuple(r["key"]):r for r in geo["all_representatives"]} + by_chart = defaultdict(list) + for cls in alias["classes"]: + if not cls["reuses"]: + row=bank_by_key[tuple(cls["keys"][0])] + assert not row["owned"] + by_chart[row["key"][1]].append(row|{"aliases":cls["keys"][1:]}) + assert len(by_chart)==5 and sum(map(len,by_chart.values()))==29 + for group in by_chart.values(): + group.sort(key=lambda r:(-len(r["public"]),r["key"])) + order = [group[i] for i in range(max(map(len,by_chart.values()))) + for _,group in sorted(by_chart.items()) if i=deadline: + break + for row in requests.get(t,()): + chart=row["key"][1] + bank=[r for r in range(n) if state[r]==chart] + owners=[r for r in range(n,len(state)) if state[r]==chart] + assert bank==row["public"] and owners==row["owned"] + out[tuple(row["key"])]=engine["exterior_minor"](bank,cols,cohort) + if not t: + assert state==word["initial"]+[None]*word["owned_fields"] + break + reverse["reverse_event"](tape[t-1],state,cols,n,engine["scalar"],engine["plus"],engine["P"]) + return out + + +def main(): + assert __debug__ + deadline=monotonic()+22 + docs=checked() + price=json.loads(docs["round102-input/lead/PRICE.json"]) + selection=json.loads(docs["SELECTION.json"]) + word=json.loads(decompress(docs["round102-input/inputs/7334-WORD.json.gz"])) + engine=run_path(str(ROOT/"round102-input/inputs/exterior_rank56.py")) + reverse=run_path(str(ROOT/"round102-input/inputs/reverse_engine.py")) + controls=reverse["controls"](engine) + cohort=set(price["cohort"]) + rows=selection["selected"] + assert len(rows)==16 and selection["head"]==price["head"]==engine["HEAD"] + keys=[tuple(r["key"]) for r in rows] + prefix,n=engine["sweep"](word,keys,cohort,deadline) + for row in rows: + k=tuple(row["key"]) + if k in prefix: + assert all(row[f]==prefix[k][f] for f in ("public","owned","pivots")) + open_rows=[r for r,k in zip(rows,keys,strict=True) if k in prefix and prefix[k]["disposition"]=="rank drop"] + suffix=reverse_side(word,open_rows,cohort,engine,reverse,deadline) if open_rows else {} + results=[] + for row,k in zip(rows,keys,strict=True): + f,s=prefix.get(k),suffix.get(k) + if f and f["disposition"]=="excluded": + status="prefix exclusion" + elif s: + status="suffix exclusion" if s["disposition"]=="excluded" else "dual drop" + else: + status="capped" + results.append(row|dict(status=status,prefix=f,suffix=s)) + print(json.dumps(dict(head=price["head"],pins=PINS,prime=engine["P"],controls=controls,caps=selection["caps"], + prefix_events=n,results=results,counts=Counter(r["status"] for r in results),unselected=selection["unselected"]), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-rank-seven-prefix-bank-bound/engines/r109/freeze.py b/research/p104-rank-seven-prefix-bank-bound/engines/r109/freeze.py new file mode 100644 index 0000000000..090f39e888 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/engines/r109/freeze.py @@ -0,0 +1,35 @@ +"""Freeze exactly the 13 still-unvisited #7367 bank keys.""" +from collections import Counter +from hashlib import sha256 +import json +from pathlib import Path + +ROOT=Path(__file__).resolve().parents[1] +PINS={ + "inputs/R105-SELECTION.json":"3bd7bdc9859436ef1d75d011e09d9dfc43a731c5b0a8e9c42fc96d9a6481a30c", + "inputs/R105-MODULAR.json":"1d99a9842dc8c42395878eb0c14b0027656041f150672491d65d3f023d9df23d", +} + + +def main(): + assert __debug__ + docs=[] + for path,pin in PINS.items(): + raw=(ROOT/path).read_bytes() + if sha256(raw).hexdigest()!=pin: + raise ValueError(f"changed dependency {path}") + docs.append(json.loads(raw)) + select,mod=docs + assert select["head"]==mod["head"] and mod["counts"]=={"prefix exclusion":16} + assert [r["key"] for r in mod["results"]]==[r["key"] for r in select["selected"]] + keys=select["unselected"] + assert keys==mod["unselected"] and len(keys)==13 + assert all(not r["aliases"] and not r["owned"] for r in keys) + assert Counter(len(r["public"]) for r in keys)=={1:9,2:4} + print(json.dumps(dict(head=select["head"],pins=PINS,selected=keys,unselected=[], + caps={"modular_cases":13,"modular_seconds":25,"exact_cases":4,"exact_seconds":35}), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-rank-seven-prefix-bank-bound/engines/r109/modular_support.py b/research/p104-rank-seven-prefix-bank-bound/engines/r109/modular_support.py new file mode 100644 index 0000000000..a7455aa93b --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/engines/r109/modular_support.py @@ -0,0 +1,92 @@ +"""Reconstruct two-sided exterior minors for 13 frozen residual quotient classes.""" +from collections import Counter, defaultdict +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path +from time import monotonic + +ROOT = Path(__file__).resolve().parent +PINS = { + "SELECTION.json":"d2b40a0130616e378bf2d35e12805c647a1132230b632fe3adc3449bc2778dad", + "round102-input/lead/PRICE.json":"4e0d6436eb4fc6a9dfa34c05ba98aacc63e3a8bf7214145dd9f9254763c5a13e", + "round102-input/inputs/7334-WORD.json.gz":"4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "round102-input/inputs/exterior_rank56.py":"9fceafc627fe3781bcb8d5229eaefebc557de613f0d4723aa1d36ce4ab9954ac", + "round102-input/inputs/reverse_engine.py":"751d5d0c4c665c8768ff69bcf939700d3be2f989c59f09af3a4aa14d3c1ebbc4", +} + + +def checked(): + output={} + for path,digest in PINS.items(): + raw=(ROOT/path).read_bytes() + if sha256(raw).hexdigest()!=digest: + raise ValueError(f"changed dependency {path}") + output[path]=raw + return output + + +def reverse_side(word,rows,cohort,engine,reverse,deadline): + n=word["public"] + state=word["final"]+[None]*word["owned_fields"] + cols=[{i:1} for i in range(n)]+[None]*word["owned_fields"] + requests=defaultdict(list) + for row in rows: + requests[row["key"][0]].append(row) + out={} + tape=word["program"] + for t in range(len(tape),-1,-1): + if (t%128==0 or t in requests) and monotonic()>=deadline: + break + for row in requests.get(t,()): + chart=row["key"][1] + bank=[r for r in range(n) if state[r]==chart] + owners=[r for r in range(n,len(state)) if state[r]==chart] + assert bank==row["public"] and owners==row["owned"] + out[tuple(row["key"])]=engine["exterior_minor"](bank,cols,cohort) + if not t: + assert state==word["initial"]+[None]*word["owned_fields"] + break + reverse["reverse_event"](tape[t-1],state,cols,n,engine["scalar"],engine["plus"],engine["P"]) + return out + + +def main(): + assert __debug__ + deadline=monotonic()+22 + docs=checked() + price=json.loads(docs["round102-input/lead/PRICE.json"]) + selection=json.loads(docs["SELECTION.json"]) + word=json.loads(decompress(docs["round102-input/inputs/7334-WORD.json.gz"])) + engine=run_path(str(ROOT/"round102-input/inputs/exterior_rank56.py")) + reverse=run_path(str(ROOT/"round102-input/inputs/reverse_engine.py")) + controls=reverse["controls"](engine) + cohort=set(price["cohort"]) + rows=selection["selected"] + assert len(rows)==13 and selection["head"]==price["head"]==engine["HEAD"] + keys=[tuple(r["key"]) for r in rows] + prefix,n=engine["sweep"](word,keys,cohort,deadline) + for row in rows: + k=tuple(row["key"]) + if k in prefix: + assert all(row[f]==prefix[k][f] for f in ("public","owned","pivots")) + open_rows=[r for r,k in zip(rows,keys,strict=True) if k in prefix and prefix[k]["disposition"]=="rank drop"] + suffix=reverse_side(word,open_rows,cohort,engine,reverse,deadline) if open_rows else {} + results=[] + for row,k in zip(rows,keys,strict=True): + f,s=prefix.get(k),suffix.get(k) + if f and f["disposition"]=="excluded": + status="prefix exclusion" + elif s: + status="suffix exclusion" if s["disposition"]=="excluded" else "dual drop" + else: + status="capped" + results.append(row|dict(status=status,prefix=f,suffix=s)) + print(json.dumps(dict(head=price["head"],pins=PINS,prime=engine["P"],controls=controls,caps=selection["caps"], + prefix_events=n,results=results,counts=Counter(r["status"] for r in results),unselected=selection["unselected"]), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-rank-seven-prefix-bank-bound/engines/r109/prefix_second_prime.py b/research/p104-rank-seven-prefix-bank-bound/engines/r109/prefix_second_prime.py new file mode 100644 index 0000000000..af7215d614 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/engines/r109/prefix_second_prime.py @@ -0,0 +1,110 @@ +"""Check exactly the 13 frozen R109 prefix banks at prime 65537.""" +from argparse import ArgumentParser +from collections import Counter +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from time import monotonic +import sys + +ROOT=Path(__file__).resolve().parent +HEAD="aaeec8c0acf01e99a5f331ef363a698d9c084ace" +WORD="4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PAYLOAD="9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PINS={ + "inputs/SELECTION.json":"d2b40a0130616e378bf2d35e12805c647a1132230b632fe3adc3449bc2778dad", + "inputs/MODULAR.json":"792eeb7e32a9e4c980bbf4597cd166bc92cf6c25aac0ba12faeb45b26bb49199", + "inputs/R105-SELECTION.json":"3bd7bdc9859436ef1d75d011e09d9dfc43a731c5b0a8e9c42fc96d9a6481a30c", + "inputs/R105-MODULAR.json":"1d99a9842dc8c42395878eb0c14b0027656041f150672491d65d3f023d9df23d", + "inputs/GEOMETRY.json":"2d0dee60998d168d2eff4c16794176c5ec3b4d18ffa8bde247602035f1b68129", + "inputs/PRICE.json":"4e0d6436eb4fc6a9dfa34c05ba98aacc63e3a8bf7214145dd9f9254763c5a13e", + "inputs/sweep.py":"089192d85154c1f8ff1d1cf6329397fe9d40b3e4b09c18dd9c90eda169f09fd9", + "inputs/second_prime.py":"21dbd96192e1f60c00ceddba01a7e8d0ddd7d6ad7da4ad3ed22ef2e47cc589c4", + "inputs/7334-WORD.json.gz":WORD, +} +CAP, SECONDS, EVENTS, PRIME=13,25,76466,65537 + + +def unique(items): + d=dict(items) + if len(d)!=len(items): + raise ValueError("duplicate JSON key") + return d + + +def freeze(raw): + def read(name): + return loads(raw[f"inputs/{name}.json"],object_pairs_hook=unique) + price,geom,selection,primary,prior_s,prior_m=(read(k) for k in + ("PRICE","GEOMETRY","SELECTION","MODULAR","R105-SELECTION","R105-MODULAR")) + assert all(d["head"]==HEAD for d in (price,geom,selection,primary,prior_s,prior_m)) + assert geom["price_sha256"]==PINS["inputs/PRICE.json"] and geom["word_sha256"]==price["word_sha256"]==WORD + assert geom["eligible_bank_count"]==65 and geom["visited_events"]==primary["prefix_events"]==EVENTS + assert primary["prime"]==65521 and primary["counts"]=={"prefix exclusion":CAP} + assert primary["caps"]==selection["caps"] and selection["caps"]["modular_cases"]==CAP + assert selection["caps"]["modular_seconds"]==SECONDS and not selection["unselected"] and not primary["unselected"] + assert all(selection["pins"][k]==PINS[k] for k in ("inputs/R105-SELECTION.json","inputs/R105-MODULAR.json")) + assert primary["pins"]["SELECTION.json"]==PINS["inputs/SELECTION.json"] + assert selection["selected"]==prior_s["unselected"]==prior_m["unselected"] + assert len(selection["selected"])==CAP and all(not row["aliases"] for row in selection["selected"]) + assert prior_m["counts"]=={"prefix exclusion":16} + chosen={tuple(r["key"]):r for r in selection["selected"]} + earlier={tuple(r["key"]):r["prefix"] for r in primary["results"]} + geometry={tuple(r["key"]):r for r in geom["all_representatives"]} + assert list(chosen)==list(earlier) and len(chosen)==CAP + for k,r in chosen.items(): + assert earlier[k]["determinant"] and earlier[k]["exterior_rank"]==len(r["public"]) + assert all(r[f]==earlier[k][f]==geometry[k][f] for f in ("public","owned","pivots")) + cohort=set(price["cohort"]) + assert cohort=={1457,1458,1474,1475,1476} + return cohort,chosen,earlier + + +def main(): + p=ArgumentParser(description=__doc__) + p.add_argument("--root",type=Path,default=ROOT) + args=p.parse_args() + assert __debug__ and sys.version_info[:2]==(3,12) + def stop(*_): + raise TimeoutError("hard 25-second cap") + signal(SIGALRM,stop) + alarm(SECONDS) + deadline=monotonic()+23 + chosen,out,progress,checks={},{},{},[] + timeout=None + try: + raw={} + for rel,digest in PINS.items(): + data=(args.root/rel).read_bytes() + if sha256(data).hexdigest()!=digest: + raise ValueError(f"changed dependency: {rel}") + raw[rel]=data + cohort,chosen,earlier=freeze(raw) + engine=run_path(str(args.root/"inputs/second_prime.py")) + sweep=run_path(str(args.root/"inputs/sweep.py")) + assert engine["PRIME"]==PRIME + checks=engine["controls"]() + payload=decompress(raw["inputs/7334-WORD.json.gz"]) + assert sha256(payload).hexdigest()==PAYLOAD + word=loads(payload,object_pairs_hook=unique) + sweep["sweep"](word,cohort,chosen,earlier,engine,deadline,progress,out) + except TimeoutError as exc: + timeout=str(exc) + finally: + alarm(0) + rows=[out[k] for k in chosen if k in out] + complete=timeout is None and progress.get("first_unvisited_cut",0) is None and len(rows)==CAP + agreement=complete and all(r["disposition"]=="excluded" for r in rows) + print(dumps(dict(head=HEAD,pins=PINS,prime=PRIME,controls=checks,cap_cases=CAP,cap_seconds=SECONDS, + counts=Counter(r["disposition"] for r in rows),rows=rows,complete=complete,agreement=agreement, + progress=progress,timeout=timeout,original_minor_axes_nonzero=sum(bool(r["primary_minor_det_mod_65537"]) for r in rows), + remaining=[k for k in chosen if k not in out or out[k]["disposition"]!="excluded"]),indent=2,sort_keys=True)) + if not agreement: + raise SystemExit(2) + + +if __name__=="__main__": + main() diff --git a/research/p104-rank-seven-prefix-bank-bound/engines/r109/sweep.py b/research/p104-rank-seven-prefix-bank-bound/engines/r109/sweep.py new file mode 100644 index 0000000000..a9f8541c4d --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/engines/r109/sweep.py @@ -0,0 +1,55 @@ +"""Literal prefix walk reused from the first bounded chart-602 gate.""" +from collections import defaultdict +from time import monotonic + +EVENTS = 76466 + + +def sweep(word, cohort, selected, earlier, engine, deadline, progress, results): + n, owned, tape = (word[k] for k in ("public", "owned_fields", "program")) + assert (n, owned, len(tape)) == (1501, 68, EVENTS) + assert all((word["initial"][r], word["final"][r]) == (602, 127) for r in cohort) + frames = word["frames"] + span = engine["span"] + low, high = span(frames[602]), span(frames[127]) + assert len(low) == 4 and len(high) == 512 and low < high + requests = defaultdict(list) + for cut, chart in selected: + assert 0 <= cut <= EVENTS and len(frames[chart]) in (5, 6) and low < span(frames[chart]) < high + requests[cut].append(chart) + + active = word["initial"] + [None] * owned + vectors = [{r: 1} for r in range(n)] + [None] * owned + fresh, denoms = set(), set() + progress.update(events=0, first_unvisited_cut=0) + for cut in range(EVENTS + 1): + progress["first_unvisited_cut"] = cut + if (cut % 128 == 0 or cut in requests) and monotonic() >= deadline: + break + for chart in requests.get(cut, ()): + key = cut, chart + bank = [r for r in range(n) if active[r] == chart] + owners = [r for r in range(n, n + owned) if active[r] == chart] + pivots = sorted(set(bank) & cohort) + assert pivots and bank == selected[key]["public"] and owners == selected[key]["owned"] + assert pivots == selected[key]["pivots"] + if cut: + last = tape[cut - 1] + assert chart in (last[2:4] if last[0] == "MOVE" else last[-1:]) + proof = engine["classify"](bank, vectors, cohort) + primary_columns = earlier[key]["columns"] + assert len(primary_columns) == len(set(primary_columns)) == len(bank) + assert cohort.isdisjoint(primary_columns) + determinant = engine["verify_minor"]([vectors[r] for r in bank], primary_columns) + results[key] = dict(key=key, chart_rank=len(frames[chart]), public=bank, owned=owners, pivots=pivots, + independent_minor=proof, primary_minor_axes=primary_columns, + primary_minor_det_mod_65537=determinant, + disposition="excluded" if not proof["kernel"] else "modular_rank_drop") + if cut == EVENTS: + assert active == word["final"] + [None] * owned and not fresh + assert len(results) == len(selected) + progress["first_unvisited_cut"] = None + break + engine["apply"](tape[cut], active, vectors, fresh, n, denoms, False) + progress["events"] += 1 + progress["denominator_units"] = sorted(denoms) diff --git a/research/p104-rank-seven-prefix-bank-bound/inputs/7314-HELPERS.json.gz b/research/p104-rank-seven-prefix-bank-bound/inputs/7314-HELPERS.json.gz new file mode 100644 index 0000000000..04698c9459 Binary files /dev/null and b/research/p104-rank-seven-prefix-bank-bound/inputs/7314-HELPERS.json.gz differ diff --git a/research/p104-rank-seven-prefix-bank-bound/inputs/7334-CHANGED.json b/research/p104-rank-seven-prefix-bank-bound/inputs/7334-CHANGED.json new file mode 100644 index 0000000000..b1644106d9 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/inputs/7334-CHANGED.json @@ -0,0 +1,72 @@ +{ + "body_clocks": [ + 40222, + 40840, + 42609, + 43022, + 43023, + 43024, + 43025, + 43026, + 43028, + 43030, + 43403, + 43491, + 43535, + 43696, + 43698, + 43887, + 45365, + 45396 + ], + "copy_and_chart_local_ownership_checked": true, + "dirty_readout": { + "319": 1 + }, + "exact_basis_columns": 14, + "forward_direction": { + "1081": -1, + "1467": 1 + }, + "literal_candidate_clocks": [ + 44588, + 44627 + ], + "paid_delta_per_word": { + "1": -1, + "5": -1, + "6": 1 + }, + "ranks": [ + 3, + 8, + 9 + ], + "roles": [ + 198, + 205, + 319, + 532, + 652, + 654, + 962, + 969, + 1081, + 1250, + 1303, + 1305, + 1453, + 1467 + ], + "scope": "Local normalized rational block, literal chart availability and nesting. Absolute Gaussian phase and whole caller separate.", + "status": "PASS_INDEPENDENT_319_BLOCK", + "window": [ + 44616, + 45718 + ], + "word_sha256": [ + "0358b9f6e0340fb3e5aa46c747c558b32a5280cbf9cd92c3b9de627dd18a9a4f", + "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + ], + "wrong_sign_and_omitted_readout_rejected": true +} diff --git a/research/p104-rank-seven-prefix-bank-bound/inputs/7334-WORD.json.gz b/research/p104-rank-seven-prefix-bank-bound/inputs/7334-WORD.json.gz new file mode 100644 index 0000000000..73f4300719 Binary files /dev/null and b/research/p104-rank-seven-prefix-bank-bound/inputs/7334-WORD.json.gz differ diff --git a/research/p104-rank-seven-prefix-bank-bound/inputs/ADMITTED.json b/research/p104-rank-seven-prefix-bank-bound/inputs/ADMITTED.json new file mode 100644 index 0000000000..464c89e45c --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/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-seven-prefix-bank-bound/inputs/PR7319-SHA256.json b/research/p104-rank-seven-prefix-bank-bound/inputs/PR7319-SHA256.json new file mode 100644 index 0000000000..3a28905e8d --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/inputs/PR7319-SHA256.json @@ -0,0 +1,6 @@ +{ + "COMPARE.json": "58d851ca486ec84ea0d1f063eb427ed0204b1b1e49219376d0ab20f6692e043e", + "CONTACT.json": "6d6cb681db29501aec002bd620514b4c48db03424243bf71686ba023dd8d6507", + "PRICE.json": "8d70669e720faabc932366dafbc1bd1fdaef6f088c4eb02b0ea3707ba309ab53", + "REVERSE.json": "bf353b3e05d0bf5fe3e49c15673c4cb9203251329bd594009303541cf7fecc09" +} diff --git a/research/p104-rank-seven-prefix-bank-bound/inputs/READBACK.json b/research/p104-rank-seven-prefix-bank-bound/inputs/READBACK.json new file mode 100644 index 0000000000..625b508eea --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/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-seven-prefix-bank-bound/inputs/exterior_rank56.py b/research/p104-rank-seven-prefix-bank-bound/inputs/exterior_rank56.py new file mode 100644 index 0000000000..427845137e --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/inputs/exterior_rank56.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 (5, 6) + 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-seven-prefix-bank-bound/inputs/pricing.py b/research/p104-rank-seven-prefix-bank-bound/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/inputs/pricing.py @@ -0,0 +1,82 @@ +"""Directed interval arithmetic and the retained signed BIT invoice.""" +from collections import Counter +from fractions import Fraction +from functools import cache + +TARGET = "10018846261809/2500000000000000" +SCALE = 10**49 + + +def rounded(x, upper): + scaled = SCALE*x + if upper: + return Fraction(-((-scaled.numerator) // scaled.denominator), SCALE) + return Fraction(scaled.numerator // scaled.denominator, SCALE) + + +@cache +def log_bounds(x): + z = (x-1)/(x+1) + terms = 60 + exact_partial = 2*sum(z**(2*i+1)/(2*i+1) for i in range(terms)) + tail = 2*z**(2*terms+1)/((2*terms+1)*(1-z*z)) + return rounded(exact_partial, False), rounded(exact_partial+tail, True) + + +@cache +def power_bounds(rank, k): + binary = 2**(rank.bit_length()-1) + shift = binary.bit_length()-1 + l2, u2 = log_bounds(Fraction(2)) + lo, hi = log_bounds(Fraction(rank, binary)) + lo, hi = k*(lo+shift*l2), k*(hi+shift*u2) + assert 0 <= lo <= hi < 1 + + def exponential(z, terms): + total = term = Fraction(1) + for i in range(1, terms+1): + term *= -z/i + total += term + return total + + return rounded(rank*exponential(hi, 35), False), rounded(rank*exponential(lo, 34), True) + + +def cost(hist, k): + lower = upper = Fraction(0) + for r, n in hist.items(): + a, b = (n*x for x in power_bounds(r, k)) + lower += min(a, b) + upper += max(a, b) + return lower, upper + + +def profile(invoice, native, word, ranks): + copies = invoice["native_calls"] + assert copies == len(invoice["native_instances"]) == 36 + assert {tuple((r["stage"], r["copy"])) for r in invoice["native_instances"]} == { + (stage, which) for stage in range(1, 19) for which in (0, 1) + } + assert all(r["ports"] == 111 for r in invoice["native_instances"]) + assert native == Counter({int(r): n for r, n in invoice["native_paid"].items()}) + assert sum(native.values()) == 2871 + caller_paid = {1: 444, **{r: 444 for r in range(7, 57, 7)}} + assert invoice["event_counts"]["QUERY"]*111 == caller_paid[1] + assert invoice["event_counts"]["IDLE_ONE"]*111 == 8*444 + full_paid = Counter({r: copies*n for r, n in native.items()}) + full_paid.update(caller_paid) + + helpers = Counter(ranks[word["final"][j]]-ranks[word["start"][j]] + for j in range(222, word["public"])) + assert helpers == Counter({int(r): n for r, n in invoice["native_helpers"].items()}) + caller_targets = {**{r: 444 for r in range(8, 65, 7)}, 127: 222} + full_targets = Counter({r: copies*n for r, n in helpers.items()}) + full_targets.update(caller_targets) + assert full_paid == Counter({int(r): n for r, n in invoice["paid"].items()}) + assert full_targets == Counter({int(r): n for r, n in invoice["targets"].items()}) + assert sum(full_paid.values()) == invoice["paid_jobs"] + assert sum(full_targets.values()) == invoice["productive_fields"] + signed = full_targets.copy() + signed.subtract(full_paid) + assert sum(r*n for r, n in signed.items()) == invoice["rank_surplus"] + return signed, copies diff --git a/research/p104-rank-seven-prefix-bank-bound/inputs/reverse_engine.py b/research/p104-rank-seven-prefix-bank-bound/inputs/reverse_engine.py new file mode 100644 index 0000000000..ebfc82f83f --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/inputs/reverse_engine.py @@ -0,0 +1,148 @@ +"""Check the 2,128 frozen public banks by exact modular suffix minors.""" +from collections import Counter, defaultdict +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path +import sys +from time import monotonic + +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +PINS = { + "price/KEYS.json": "a131ec5bf96baac89f0f6623cf7d9dff06601b36ea720474311ee7ecb394f6e2", + "inputs/PRICE.json": "b4bf8e00a8289f03b1da731fb3ab563a771d88d875e0da73acf70954df2f2c56", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/exterior_minor.py": "b25fef5432d8ea9cff9eecc422cf07ccf7473568084de3e8d3d1b5224793504d", +} + + +def authenticated(root): + raw = {} + for path, expected in PINS.items(): + raw[path] = (root / path).read_bytes() + if sha256(raw[path]).hexdigest() != expected: + raise ValueError(f"changed dependency: {path}") + return raw + + +def reverse_event(event, active, columns, public, scalar, plus, prime): + op, dst, *args = event + if op == "MOVE": + old, new, owned = args + assert active[dst] == new and owned == (dst >= public) + active[dst] = old + elif op == "CLEAR": + assert dst >= public and active[dst] is None and columns[dst] is None + active[dst], columns[dst] = args[0], {} + elif op == "INIT": + assert dst >= public and active[dst] == args[0] + active[dst] = columns[dst] = None + elif op == "SCALE": + coefficient, chart = args + assert active[dst] == chart + factor = scalar(coefficient) + columns[dst] = {k: factor * v % prime for k, v in columns[dst].items() + if factor * v % prime} + else: + src, coefficient, chart = args + assert op in ("ADD", "COPY") and dst != src + assert active[dst] == active[src] == chart + # The source contributes to both post-event fields. A guarded COPY + # replaces the destination, whose required pre-event value is zero. + plus(columns[src], columns[dst], scalar(coefficient)) + if op == "COPY": + assert dst >= public + columns[dst] = {} + + +def controls(engine): + scalar, plus, prime = (engine[name] for name in ("scalar", "plus", "P")) + active = [4, 4, None] + cols = [{0: 1}, {1: 1}, None] + tape = [ + ("ADD", 1, 0, "-3/2", 4), + ("SCALE", 0, "2", 4), + ("INIT", 2, 4), + ("COPY", 2, 1, "1", 4), + ("ADD", 0, 2, "5", 4), + ("CLEAR", 2, 4), + ] + for event in reversed(tape): + reverse_event(event, active, cols, 2, scalar, plus, prime) + assert cols == [{0: scalar("-11/2"), 1: scalar("-3/2")}, {0: 5, 1: 1}, None] + assert active == [4, 4, None] + minor = engine["exterior_minor"] + assert minor([0, 1], cols, set())["disposition"] == "excluded" + assert minor([0, 1], cols, {0})["disposition"] == "rank drop" + return ["signed two-output impulse with owned COPY and CLEAR", + "full exterior rank", "planted pure suffix", *engine["controls"]()] + + +def sweep(word, records, cohort, engine, deadline): + public = word["public"] + active = word["final"] + [None] * word["owned_fields"] + columns = [{i: 1} for i in range(public)] + [None] * word["owned_fields"] + requests = defaultdict(list) + for record in records: + requests[record["key"][0]].append(record) + scalar, plus, prime, minor = (engine[name] for name in ("scalar", "plus", "P", "exterior_minor")) + seen, visited = {}, 0 + for cut in range(len(word["program"]), -1, -1): + if (cut % 128 == 0 or cut in requests) and monotonic() >= deadline: + break + for record in requests.get(cut, ()): + chart = record["key"][1] + public_bank = [r for r in range(public) if active[r] == chart] + owned_bank = [r for r in range(public, len(active)) if active[r] == chart] + assert public_bank == record["public"] and owned_bank == record["owned"] + assert sorted(set(public_bank) & cohort) == record["pivots"] + result = minor(public_bank, columns, cohort) + seen[tuple(record["key"])] = { + "key": record["key"], "public": public_bank, "owned": owned_bank, + "pivots": record["pivots"], "prefix_rank_mod_65521": record["exterior_rank"], + "suffix_rank_mod_65521": result["exterior_rank"], "output_minor_rows": result["columns"], + "determinant_mod_65521": result["determinant"], "disposition": result["disposition"], + } + if not cut: + assert active == word["initial"] + [None] * word["owned_fields"] + break + reverse_event(word["program"][cut - 1], active, columns, public, scalar, plus, prime) + visited += 1 + return seen, visited + + +def main(): + assert __debug__ + deadline = monotonic() + 32 + root = Path(sys.argv[1]) + raw = authenticated(root) + engine = run_path(str(root / "inputs/exterior_minor.py")) + unique = engine["unique"] + frozen = json.loads(raw["price/KEYS.json"], object_pairs_hook=unique) + price = json.loads(raw["inputs/PRICE.json"], object_pairs_hook=unique) + word = json.loads(decompress(raw["inputs/7334-WORD.json.gz"]), object_pairs_hook=unique) + assert frozen["head"] == price["head"] == HEAD + assert frozen["source_sha256"]["inputs/7334-WORD.json.gz"] == PINS["inputs/7334-WORD.json.gz"] + assert frozen["source_sha256"]["inputs/PRICE.json"] == PINS["inputs/PRICE.json"] + records = frozen["keys"] + keys = [tuple(row["key"]) for row in records] + assert len(keys) == len(set(keys)) == frozen["reverse_case_cap"] == 2128 + cohort = set(price["endpoint_cohort"]) + assert len(cohort) == 615 + checks = controls(engine) + found, visited = sweep(word, records, cohort, engine, deadline) + results = [found[k] for k in keys if k in found] + pending = [list(k) for k in keys if k not in found] + print(json.dumps({ + "head": HEAD, "pins": PINS, "scope": "normalized suffix on the frozen public bank only", + "prime": engine["P"], "cases_cap": 2128, "seconds_cap": 32, "events_processed": visited, + "status": "CAPPED" if pending or visited != len(word["program"]) else "EXHAUSTED", + "controls": checks, "counts": Counter(row["disposition"] for row in results), + "results": results, "unvisited": pending, + "rank_drops": [row["key"] for row in results if row["disposition"] == "rank drop"], + }, separators=(",", ":"), sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-seven-prefix-bank-bound/receipts/CLOSED.json b/research/p104-rank-seven-prefix-bank-bound/receipts/CLOSED.json new file mode 100644 index 0000000000..c099783cc7 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/receipts/CLOSED.json @@ -0,0 +1,730 @@ +{ + "counts": { + "continuation direct minor": 16, + "continuation minor via alias": 11, + "original direct minor": 16, + "original minor via alias": 9, + "residual direct minor": 13 + }, + "excluded": 65, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "original": 65, + "rows": [ + { + "disposition": "original direct minor", + "key": [ + 40313, + 647 + ], + "witness": [ + 40313, + 647 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40314, + 647 + ], + "witness": [ + 40314, + 647 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40315, + 647 + ], + "witness": [ + 40314, + 647 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40316, + 647 + ], + "witness": [ + 40316, + 647 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40317, + 647 + ], + "witness": [ + 40316, + 647 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40319, + 647 + ], + "witness": [ + 40319, + 647 + ] + }, + { + "disposition": "residual direct minor", + "key": [ + 40322, + 647 + ], + "witness": [ + 40322, + 647 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40332, + 647 + ], + "witness": [ + 40332, + 647 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40333, + 647 + ], + "witness": [ + 40332, + 647 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40338, + 645 + ], + "witness": [ + 40338, + 645 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40339, + 645 + ], + "witness": [ + 40339, + 645 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40340, + 645 + ], + "witness": [ + 40339, + 645 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40341, + 645 + ], + "witness": [ + 40341, + 645 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40342, + 645 + ], + "witness": [ + 40341, + 645 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40344, + 645 + ], + "witness": [ + 40344, + 645 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40347, + 645 + ], + "witness": [ + 40347, + 645 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40348, + 645 + ], + "witness": [ + 40347, + 645 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40352, + 645 + ], + "witness": [ + 40352, + 645 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40353, + 645 + ], + "witness": [ + 40352, + 645 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40372, + 647 + ], + "witness": [ + 40372, + 647 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40373, + 647 + ], + "witness": [ + 40372, + 647 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40374, + 645 + ], + "witness": [ + 40374, + 645 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40637, + 645 + ], + "witness": [ + 40637, + 645 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40715, + 694 + ], + "witness": [ + 40715, + 694 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40716, + 694 + ], + "witness": [ + 40716, + 694 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40717, + 694 + ], + "witness": [ + 40716, + 694 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40718, + 694 + ], + "witness": [ + 40718, + 694 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40719, + 694 + ], + "witness": [ + 40718, + 694 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40721, + 694 + ], + "witness": [ + 40721, + 694 + ] + }, + { + "disposition": "residual direct minor", + "key": [ + 40724, + 694 + ], + "witness": [ + 40724, + 694 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40730, + 695 + ], + "witness": [ + 40730, + 695 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40731, + 695 + ], + "witness": [ + 40731, + 695 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40732, + 695 + ], + "witness": [ + 40731, + 695 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40733, + 695 + ], + "witness": [ + 40733, + 695 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40734, + 695 + ], + "witness": [ + 40733, + 695 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40736, + 695 + ], + "witness": [ + 40736, + 695 + ] + }, + { + "disposition": "residual direct minor", + "key": [ + 40742, + 695 + ], + "witness": [ + 40742, + 695 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40751, + 693 + ], + "witness": [ + 40751, + 693 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40752, + 693 + ], + "witness": [ + 40752, + 693 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40753, + 693 + ], + "witness": [ + 40752, + 693 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40754, + 693 + ], + "witness": [ + 40754, + 693 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40755, + 693 + ], + "witness": [ + 40754, + 693 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40757, + 693 + ], + "witness": [ + 40757, + 693 + ] + }, + { + "disposition": "residual direct minor", + "key": [ + 40762, + 693 + ], + "witness": [ + 40762, + 693 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40768, + 695 + ], + "witness": [ + 40768, + 695 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40769, + 695 + ], + "witness": [ + 40768, + 695 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40772, + 693 + ], + "witness": [ + 40772, + 693 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40773, + 693 + ], + "witness": [ + 40772, + 693 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40774, + 693 + ], + "witness": [ + 40774, + 693 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40775, + 693 + ], + "witness": [ + 40774, + 693 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40776, + 694 + ], + "witness": [ + 40776, + 694 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40777, + 694 + ], + "witness": [ + 40776, + 694 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40779, + 695 + ], + "witness": [ + 40779, + 695 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40780, + 695 + ], + "witness": [ + 40779, + 695 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40781, + 694 + ], + "witness": [ + 40781, + 694 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40782, + 694 + ], + "witness": [ + 40781, + 694 + ] + }, + { + "disposition": "residual direct minor", + "key": [ + 40783, + 693 + ], + "witness": [ + 40783, + 693 + ] + }, + { + "disposition": "residual direct minor", + "key": [ + 40787, + 695 + ], + "witness": [ + 40787, + 695 + ] + }, + { + "disposition": "residual direct minor", + "key": [ + 40796, + 694 + ], + "witness": [ + 40796, + 694 + ] + }, + { + "disposition": "residual direct minor", + "key": [ + 40802, + 645 + ], + "witness": [ + 40802, + 645 + ] + }, + { + "disposition": "residual direct minor", + "key": [ + 40840, + 695 + ], + "witness": [ + 40840, + 695 + ] + }, + { + "disposition": "residual direct minor", + "key": [ + 41059, + 694 + ], + "witness": [ + 41059, + 694 + ] + }, + { + "disposition": "residual direct minor", + "key": [ + 42156, + 693 + ], + "witness": [ + 42156, + 693 + ] + }, + { + "disposition": "residual direct minor", + "key": [ + 42192, + 647 + ], + "witness": [ + 42192, + 647 + ] + }, + { + "disposition": "residual direct minor", + "key": [ + 42279, + 647 + ], + "witness": [ + 42279, + 647 + ] + } + ], + "unresolved": 0 +} diff --git a/research/p104-rank-seven-prefix-bank-bound/receipts/R109-SHA256.json b/research/p104-rank-seven-prefix-bank-bound/receipts/R109-SHA256.json new file mode 100644 index 0000000000..6b94fea6d3 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/receipts/R109-SHA256.json @@ -0,0 +1,5 @@ +{ + "R109-MODULAR.json": "792eeb7e32a9e4c980bbf4597cd166bc92cf6c25aac0ba12faeb45b26bb49199", + "R109-SECOND.json": "aa1213904c70a852a4b65053ea27d97a8b374d5aeccc9fe0832fdf4fb13268d1", + "R109-SELECTION.json": "d2b40a0130616e378bf2d35e12805c647a1132230b632fe3adc3449bc2778dad" +} diff --git a/research/p104-rank-seven-prefix-bank-bound/receipts/RECONCILED.json b/research/p104-rank-seven-prefix-bank-bound/receipts/RECONCILED.json new file mode 100644 index 0000000000..b160f432e5 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/receipts/RECONCILED.json @@ -0,0 +1,691 @@ +{ + "counts": { + "continuation direct minor": 16, + "continuation minor via alias": 11, + "original direct minor": 16, + "original minor via alias": 9, + "unresolved after cap": 13 + }, + "excluded": 52, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "original": 65, + "rows": [ + { + "disposition": "original direct minor", + "key": [ + 40313, + 647 + ], + "witness": [ + 40313, + 647 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40314, + 647 + ], + "witness": [ + 40314, + 647 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40315, + 647 + ], + "witness": [ + 40314, + 647 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40316, + 647 + ], + "witness": [ + 40316, + 647 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40317, + 647 + ], + "witness": [ + 40316, + 647 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40319, + 647 + ], + "witness": [ + 40319, + 647 + ] + }, + { + "disposition": "unresolved after cap", + "key": [ + 40322, + 647 + ], + "witness": null + }, + { + "disposition": "original direct minor", + "key": [ + 40332, + 647 + ], + "witness": [ + 40332, + 647 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40333, + 647 + ], + "witness": [ + 40332, + 647 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40338, + 645 + ], + "witness": [ + 40338, + 645 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40339, + 645 + ], + "witness": [ + 40339, + 645 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40340, + 645 + ], + "witness": [ + 40339, + 645 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40341, + 645 + ], + "witness": [ + 40341, + 645 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40342, + 645 + ], + "witness": [ + 40341, + 645 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40344, + 645 + ], + "witness": [ + 40344, + 645 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40347, + 645 + ], + "witness": [ + 40347, + 645 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40348, + 645 + ], + "witness": [ + 40347, + 645 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40352, + 645 + ], + "witness": [ + 40352, + 645 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40353, + 645 + ], + "witness": [ + 40352, + 645 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40372, + 647 + ], + "witness": [ + 40372, + 647 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40373, + 647 + ], + "witness": [ + 40372, + 647 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40374, + 645 + ], + "witness": [ + 40374, + 645 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40637, + 645 + ], + "witness": [ + 40637, + 645 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40715, + 694 + ], + "witness": [ + 40715, + 694 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40716, + 694 + ], + "witness": [ + 40716, + 694 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40717, + 694 + ], + "witness": [ + 40716, + 694 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40718, + 694 + ], + "witness": [ + 40718, + 694 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40719, + 694 + ], + "witness": [ + 40718, + 694 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40721, + 694 + ], + "witness": [ + 40721, + 694 + ] + }, + { + "disposition": "unresolved after cap", + "key": [ + 40724, + 694 + ], + "witness": null + }, + { + "disposition": "original direct minor", + "key": [ + 40730, + 695 + ], + "witness": [ + 40730, + 695 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40731, + 695 + ], + "witness": [ + 40731, + 695 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40732, + 695 + ], + "witness": [ + 40731, + 695 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40733, + 695 + ], + "witness": [ + 40733, + 695 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40734, + 695 + ], + "witness": [ + 40733, + 695 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40736, + 695 + ], + "witness": [ + 40736, + 695 + ] + }, + { + "disposition": "unresolved after cap", + "key": [ + 40742, + 695 + ], + "witness": null + }, + { + "disposition": "original direct minor", + "key": [ + 40751, + 693 + ], + "witness": [ + 40751, + 693 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40752, + 693 + ], + "witness": [ + 40752, + 693 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40753, + 693 + ], + "witness": [ + 40752, + 693 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40754, + 693 + ], + "witness": [ + 40754, + 693 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40755, + 693 + ], + "witness": [ + 40754, + 693 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40757, + 693 + ], + "witness": [ + 40757, + 693 + ] + }, + { + "disposition": "unresolved after cap", + "key": [ + 40762, + 693 + ], + "witness": null + }, + { + "disposition": "original direct minor", + "key": [ + 40768, + 695 + ], + "witness": [ + 40768, + 695 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40769, + 695 + ], + "witness": [ + 40768, + 695 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40772, + 693 + ], + "witness": [ + 40772, + 693 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40773, + 693 + ], + "witness": [ + 40772, + 693 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40774, + 693 + ], + "witness": [ + 40774, + 693 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40775, + 693 + ], + "witness": [ + 40774, + 693 + ] + }, + { + "disposition": "original direct minor", + "key": [ + 40776, + 694 + ], + "witness": [ + 40776, + 694 + ] + }, + { + "disposition": "original minor via alias", + "key": [ + 40777, + 694 + ], + "witness": [ + 40776, + 694 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40779, + 695 + ], + "witness": [ + 40779, + 695 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40780, + 695 + ], + "witness": [ + 40779, + 695 + ] + }, + { + "disposition": "continuation direct minor", + "key": [ + 40781, + 694 + ], + "witness": [ + 40781, + 694 + ] + }, + { + "disposition": "continuation minor via alias", + "key": [ + 40782, + 694 + ], + "witness": [ + 40781, + 694 + ] + }, + { + "disposition": "unresolved after cap", + "key": [ + 40783, + 693 + ], + "witness": null + }, + { + "disposition": "unresolved after cap", + "key": [ + 40787, + 695 + ], + "witness": null + }, + { + "disposition": "unresolved after cap", + "key": [ + 40796, + 694 + ], + "witness": null + }, + { + "disposition": "unresolved after cap", + "key": [ + 40802, + 645 + ], + "witness": null + }, + { + "disposition": "unresolved after cap", + "key": [ + 40840, + 695 + ], + "witness": null + }, + { + "disposition": "unresolved after cap", + "key": [ + 41059, + 694 + ], + "witness": null + }, + { + "disposition": "unresolved after cap", + "key": [ + 42156, + 693 + ], + "witness": null + }, + { + "disposition": "unresolved after cap", + "key": [ + 42192, + 647 + ], + "witness": null + }, + { + "disposition": "unresolved after cap", + "key": [ + 42279, + 647 + ], + "witness": null + } + ], + "unresolved": 13 +} diff --git a/research/p104-rank-seven-prefix-bank-bound/receipts/SHA256.json b/research/p104-rank-seven-prefix-bank-bound/receipts/SHA256.json new file mode 100644 index 0000000000..653bb906ce --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/receipts/SHA256.json @@ -0,0 +1,11 @@ +{ + "R102-GEOMETRY.json": "2d0dee60998d168d2eff4c16794176c5ec3b4d18ffa8bde247602035f1b68129", + "R102-PREFIX.json": "65c11b0a42092557fe1c64b4feb2f61e2d16c636cfcaddf7f95ec09dbdd27452", + "R102-PRICE.json": "4e0d6436eb4fc6a9dfa34c05ba98aacc63e3a8bf7214145dd9f9254763c5a13e", + "R102-SECOND.json": "51c9eb3af7b4d5ff60daef468f3bf262cb485bb88f4d0394d91b83d7eba2bffd", + "R105-ALIASES.json": "ba0120da7b05b948b1e8294c6b3844deade2c40be1f2e0abf4e0beef395f5c85", + "R105-MODULAR.json": "1d99a9842dc8c42395878eb0c14b0027656041f150672491d65d3f023d9df23d", + "R105-REVERSE.json": "ec0e9e642e8525f8d9d91e481e3f03a73539f3683b3adffef8cb399fcc7e13bf", + "R105-SECOND.json": "86dc10932eae8abebf8e122bfcb5d96209a1f9e61838f6f6d55f6e9c4ade1ce6", + "R105-SELECTION.json": "3bd7bdc9859436ef1d75d011e09d9dfc43a731c5b0a8e9c42fc96d9a6481a30c" +} diff --git a/research/p104-rank-seven-prefix-bank-bound/replay.py b/research/p104-rank-seven-prefix-bank-bound/replay.py new file mode 100644 index 0000000000..a518a2b399 --- /dev/null +++ b/research/p104-rank-seven-prefix-bank-bound/replay.py @@ -0,0 +1,273 @@ +"""Replay the fixed-paid rank-seven bank and prefix exclusion receipts.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction +from gzip import decompress +from hashlib import sha1, sha256 +from json import dumps, loads +from pathlib import Path, PurePosixPath +from shutil import copyfile +from subprocess import run +import sys +from tempfile import TemporaryDirectory + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" + + +def unique(items): + result = dict(items) + if len(result) != len(items): + raise ValueError("duplicate JSON key") + return result + + +def decode(data): + return loads(data, object_pairs_hook=unique) + + +def digest(data): + return sha256(data).hexdigest() + + +def relative(name): + path = PurePosixPath(name) + if path.is_absolute() or path.as_posix() != name or ".." in path.parts: + raise ValueError(f"invalid relative path: {name}") + return path + + +def authenticate(): + pins = decode((ROOT / "LOCAL-PINS.json").read_bytes()) + for path, expected in pins.items(): + if digest((ROOT / relative(path)).read_bytes()) != expected: + raise ValueError(f"changed package dependency: {path}") + provenance = decode((ROOT / "PROVENANCE.json").read_bytes()) + for path, record in provenance["files"].items(): + raw = (ROOT / relative(path)).read_bytes() + assert digest(raw) == record["sha256"] == pins[path] + assert sha1(f"blob {len(raw)}\0".encode() + raw).hexdigest() == record["git_blob"] + for path, record in provenance["derived_inputs"].items(): + raw = (ROOT / relative(path)).read_bytes() + if record.get("compression") == "gzip": + raw = decompress(raw) + expected = decode((ROOT / relative(record["receipt"])).read_bytes()) + for key in record["keys"]: + expected = expected[key] + assert digest(raw) == expected + + +def command(script, *args, timeout=25, check=True): + result = run([sys.executable, "-I", "-B", str(script), *map(str,args)], capture_output=True, timeout=timeout) + if check and result.returncode: + sys.stderr.write(result.stderr.decode(errors="replace")) + result.check_returncode() + return result + + +def materialize(scratch): + r102 = scratch / "round102-input" + ind = scratch / "independent" + for d in (r102/"inputs",r102/"lead",ind/"inputs"): + d.mkdir(parents=True) + for name in ("7334-CHANGED.json", "7334-WORD.json.gz", "ADMITTED.json", "READBACK.json", + "exterior_rank56.py", "pricing.py", "reverse_engine.py"): + copyfile(ROOT/"inputs"/name,r102/"inputs"/name) + (r102/"inputs/7314-HELPERS.json").write_bytes(decompress((ROOT/"inputs/7314-HELPERS.json.gz").read_bytes())) + for name in ("quote.py","geometry.py","prefix.py"): + copyfile(ROOT/"engines/r102"/name,r102/"lead"/name) + for name in ("alias_rank_seven.py","freeze_support.py","modular_support.py"): + copyfile(ROOT/"engines/r105"/name,scratch/name) + for name in ("verify.py","r102_prefix.py"): + copyfile(ROOT/"engines/independent"/name,ind/name) + for name in ("r102_prefix.py","second_prime.py"): + copyfile(ROOT/"engines/independent"/name,ind/"inputs"/name) + copyfile(ROOT/"inputs/7334-WORD.json.gz",ind/"inputs/7334-WORD.json.gz") + return r102,ind + + +def reconcile(geometry,old,old_second,alias,reverse,selection,modular,second): + all_keys = {tuple(k) for k in geometry["all_representative_keys"]} + assert len(all_keys) == geometry["eligible_bank_count"] == 65 + assert geometry["eligible_chart_count"] == 5 and geometry["status"] == "EXHAUSTED" + old_keys = {tuple(r["key"]) for r in old["rows"] if r["determinant"]} + assert old_keys == {tuple(r["key"]) for r in old_second["rows"] if r["independent_minor"]["determinant"]} + assert len(old_keys) == 16 and old["counts"] == old_second["counts"] == {"excluded":16} + assert all(r["chart_rank"] == 6 for r in old_second["rows"] + second["rows"]) + assert alias["classes"] == reverse["strict_classes"] == reverse["fixed_public_only_classes"] + assert not reverse["diagnostic_additional_links"] and len(alias["classes"]) == 45 + assert len(alias["links"]) == 60 and sum(r["alias"] for r in alias["links"]) == 20 + chosen = {tuple(r["key"]):r for r in selection["selected"]} + left = {tuple(r["key"]) for r in selection["unselected"]} + assert chosen.keys() == {tuple(r["key"]) for r in modular["results"] if r["status"] == "prefix exclusion"} + assert chosen.keys() == {tuple(r["key"]) for r in second["rows"] if r["independent_minor"]["determinant"]} + assert len(chosen) == second["certified_primary_axes"] == 16 + assert modular["counts"] == second["counts"] == {"prefix exclusion":16} + assert not old_keys & chosen.keys() + disposition = {} + for component in alias["classes"]: + keys = list(map(tuple,component["keys"])) + original = list(map(tuple,component["reuses"])) + new = [k for k in keys if k in chosen] + assert not (original and new) and len(original) <= 1 and len(new) <= 1 + if original: + witness = original[0] + for key in keys: + disposition[key] = ("original direct minor" if key == witness else "original minor via alias",witness) + elif new: + witness = new[0] + assert chosen[witness]["aliases"] == [list(k) for k in keys if k != witness] + for key in keys: + disposition[key] = ("continuation direct minor" if key == witness else "continuation minor via alias",witness) + else: + assert len(keys) == 1 and keys[0] in left + disposition[keys[0]] = ("unresolved after cap",None) + assert disposition.keys() == all_keys + assert left == {k for k,(status,_) in disposition.items() if status == "unresolved after cap"} + counts = Counter(s for s,_ in disposition.values()) + assert counts == {"original direct minor":16,"original minor via alias":9,"continuation direct minor":16, + "continuation minor via alias":11,"unresolved after cap":13} + rows = [dict(key=k,disposition=disposition[k][0],witness=disposition[k][1]) for k in sorted(disposition)] + return dict(head=HEAD,counts=counts,original=65,excluded=52,unresolved=13,rows=rows) + + + +def close_residual(previous,selection,primary,second): + chosen={tuple(r["key"]):r for r in selection["selected"]} + first={tuple(r["key"]):r for r in primary["results"]} + other={tuple(r["key"]):r for r in second["rows"]} + pending={tuple(r["key"]) for r in previous["rows"] if r["disposition"]=="unresolved after cap"} + assert len(chosen)==len(pending)==13 and pending==chosen.keys()==first.keys()==other.keys() + assert not selection["unselected"] and not primary["unselected"] and not second["remaining"] + assert primary["prime"]==65521 and second["prime"]==65537 and second["agreement"] + assert primary["prefix_events"]==second["progress"]["events"]==76466 + assert second["original_minor_axes_nonzero"]==13 + for key in chosen: + a,b,c=chosen[key],first[key],other[key] + assert not a["owned"] and not a["aliases"] and c["chart_rank"]==6 + assert all(a[field]==b[field]==c[field] for field in ("public","owned","pivots")) + assert b["status"]=="prefix exclusion" and c["disposition"]=="excluded" + assert b["prefix"]["determinant"] and c["independent_minor"]["determinant"] + rows=[] + for row in previous["rows"]: + if tuple(row["key"]) in pending: + row=dict(row,disposition="residual direct minor",witness=row["key"]) + rows.append(row) + counts=Counter(r["disposition"] for r in rows) + assert counts=={"original direct minor":16,"original minor via alias":9, + "continuation direct minor":16,"continuation minor via alias":11, + "residual direct minor":13} + return dict(head=HEAD,counts=counts,original=65,excluded=65,unresolved=0,rows=rows) + + +def replay_residual(scratch,r102,ind,prior,produced): + expected=decode((ROOT/"receipts/R109-SHA256.json").read_bytes()) + r109=scratch/"r109" + for target in ("inputs","lead","round102-input/inputs","round102-input/lead","independent/inputs"): + (r109/target).mkdir(parents=True) + for rel in ("lead/PRICE.json","inputs/7334-WORD.json.gz","inputs/exterior_rank56.py","inputs/reverse_engine.py"): + copyfile(r102/rel,r109/"round102-input"/rel) + for filename,target in (("freeze.py","lead/freeze.py"),("modular_support.py","modular_support.py"), + ("prefix_second_prime.py","independent/prefix_second_prime.py"), + ("sweep.py","independent/inputs/sweep.py")): + copyfile(ROOT/"engines/r109"/filename,r109/target) + for filename in ("PRICE.json","GEOMETRY.json","7334-WORD.json.gz","second_prime.py"): + copyfile(ind/"inputs"/filename,r109/"independent/inputs"/filename) + for name in ("SELECTION.json","MODULAR.json"): + copyfile(scratch/name,r109/"inputs"/f"R105-{name}") + copyfile(scratch/name,r109/"independent/inputs"/f"R105-{name}") + + def record(name,response,target=None): + raw=response.stdout + assert digest(raw)==expected[name],("changed residual receipt",name) + produced[name]=raw + if target is not None: + target.write_bytes(raw) + return decode(raw) + + chosen=record("R109-SELECTION.json",command(r109/"lead/freeze.py"),r109/"SELECTION.json") + mod=record("R109-MODULAR.json",command(r109/"modular_support.py"),r109/"MODULAR.json") + for name in ("SELECTION.json","MODULAR.json"): + copyfile(r109/name,r109/"independent/inputs"/name) + second=record("R109-SECOND.json",command(r109/"independent/prefix_second_prime.py")) + closed=close_residual(prior,chosen,mod,second) + raw=(dumps(closed,indent=2,sort_keys=True)+"\n").encode() + assert raw==(ROOT/"receipts/CLOSED.json").read_bytes() + produced["CLOSED.json"]=raw + + selection=r109/"independent/inputs/SELECTION.json" + selection.write_bytes(selection.read_bytes()+b"\n") + rejection=command(r109/"independent/prefix_second_prime.py",check=False) + assert rejection.returncode==1 and not rejection.stdout + assert b"changed dependency: inputs/SELECTION.json" in rejection.stderr + +def replay(scratch,out): + authenticate() + expected = decode((ROOT / "receipts/SHA256.json").read_bytes()) + r102,ind = materialize(scratch) + produced = {} + + def record(name, target, response): + raw = response.stdout + assert digest(raw) == expected[name], ("changed receipt",name) + target.write_bytes(raw) + produced[name] = raw + return decode(raw) + + price = record("R102-PRICE.json",r102/"lead/PRICE.json",command(r102/"lead/quote.py")) + assert price["head"] == HEAD and price["paid_delta"] == {} and price["productive_delta"] == {"3":17,"4":17,"7":-17} + one = list(map(Fraction,price["at_incumbent"]["gross_one"])) + margin = list(map(Fraction,price["at_incumbent"]["old_margin"])) + assert 0 < one[0] <= one[1] < 1 and one[1]+margin[1] < 1 + assert Fraction(price["at_incumbent"]["whole_5_upper"]) == 5*one[1] + assert Fraction(price["at_target"]["complete_5_upper"]) < 0 + geometry = record("R102-GEOMETRY.json",r102/"lead/GEOMETRY.json", + command(r102/"lead/geometry.py",r102,timeout=20)) + old = record("R102-PREFIX.json",r102/"lead/PREFIX.json",command(r102/"lead/prefix.py",r102)) + for name in ("PRICE.json","GEOMETRY.json","PREFIX.json"): + copyfile(r102/"lead"/name,ind/"inputs"/name) + old_second = record("R102-SECOND.json",ind/"inputs/PREFIX-SECOND-PRIME.json",command(ind/"r102_prefix.py")) + alias = record("R105-ALIASES.json",scratch/"ALIASES.json",command(scratch/"alias_rank_seven.py",r102,timeout=20)) + copyfile(scratch/"ALIASES.json",ind/"inputs/ALIASES.json") + reverse = record("R105-REVERSE.json",scratch/"REVERSE.json",command(ind/"verify.py","alias",timeout=20)) + selection = record("R105-SELECTION.json",scratch/"SELECTION.json",command(scratch/"freeze_support.py")) + modular = record("R105-MODULAR.json",scratch/"MODULAR.json",command(scratch/"modular_support.py")) + for name in ("SELECTION.json","MODULAR.json"): + copyfile(scratch/name,ind/"inputs"/name) + second = record("R105-SECOND.json",scratch/"SECOND.json",command(ind/"verify.py","modular")) + summary = reconcile(geometry,old,old_second,alias,reverse,selection,modular,second) + raw = (dumps(summary,indent=2,sort_keys=True)+"\n").encode() + assert raw == (ROOT/"receipts/RECONCILED.json").read_bytes() + assert set(produced) == set(expected) + produced["RECONCILED.json"] = raw + replay_residual(scratch,r102,ind,summary,produced) + + for victim,script,args in ( + (ind/"inputs/PRICE.json",ind/"verify.py",("alias",)), + (r102/"inputs/7334-WORD.json.gz",r102/"lead/geometry.py",(r102,)), + ): + before = victim.read_bytes() + victim.write_bytes(before+b"\n") + failure = command(script,*args,check=False) + assert failure.returncode == 1 and not failure.stdout + assert b"changed dependency" in failure.stderr and victim.name.encode() in failure.stderr + victim.write_bytes(before) + + if out is not None: + out.mkdir(parents=True) + for name,content in produced.items(): + (out / relative(name)).write_bytes(content) + print("PASS_RANK_SEVEN_PREFIX_BANK_BOUND original=65 direct=45 transfers=20 excluded=65 unresolved=0") + + +def main(): + assert sys.version_info[:2] == (3,12) and __debug__ + parser = ArgumentParser(description=__doc__) + parser.add_argument("--out",type=Path,help="new directory for the fourteen regenerated receipts") + args = parser.parse_args() + with TemporaryDirectory() as directory: + replay(Path(directory),args.out) + + +if __name__ == "__main__": + main()