diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 63ba3e9aa8..52b62d0481 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,25 @@ # CI verification -## Current selected-family replay: #6030 +## Current selected-family replay: #7000 with #7001 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.00363005817 to the [application review](research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md), +[validation receipts](research/pr-intake-evidence/pr7000-application/VALIDATION.json), +and [explicit source closure](../certificates/frontier7000-source.json). +`make frontier7000-verify` follows that exact-source selected replay. The review +reuses eleven authenticated preceding executions and records seven fresh serial +application, scalar and complete native-catalogue executions. The earlier +monolithic timeout is retained separately and is not completed coverage. +Consult the receipts for exact commands, source heads and limits. + +The five inherited framework assumptions remain. No complete uniform word, +literal multiplier execution, independent human proof or formal-kernel proof +is asserted. Routine research submissions do not need to rerun this +selected-family replay. The sections below preserve historical checkpoints. + +## Historical selected-family replay: #6030 + +The [historical checkpoint](../certificates/checkpoints/frontier6030.json) binds conditional κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md), [validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json), and [explicit source closure](../certificates/frontier6030-source.json). diff --git a/research/historical-selected-replay-gap/README.md b/research/historical-selected-replay-gap/README.md index 55d8cc3b49..36d9a873ca 100644 --- a/research/historical-selected-replay-gap/README.md +++ b/research/historical-selected-replay-gap/README.md @@ -69,7 +69,11 @@ python3 -B scripts/research_package.py --package research/historical-selected-re The direct command prints `PASS_HISTORICAL_SELECTED_REPLAY_GAP`. A registered replay prints `PASS_REGISTERED_RESEARCH_PACKAGE`. Both require Git history -containing the two inspected commits. +containing the two inspected commits and the source and manifest objects at +`2485805a6d47f36ea83ddde6327d453ac82d44dc`. The verifier uses a temporary +sparse checkout of that commit, checks the declared source digests there, and +uses its planner and manifest inventory. The recorded rejections and selection +therefore remain reproducible after later changes to the live Makefile or CI guide. ## Open next questions diff --git a/research/historical-selected-replay-gap/SOURCES.json b/research/historical-selected-replay-gap/SOURCES.json index c1010eec95..62bb8b3950 100644 --- a/research/historical-selected-replay-gap/SOURCES.json +++ b/research/historical-selected-replay-gap/SOURCES.json @@ -4,13 +4,13 @@ "files": [ { "path": "Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "0d683a06b9e7ee162496108ce9a7c5d2ee94fccf", "sha256": "4f2d4f2dcd15139ec82658a975f85ed300897385f85799218539f4c8d60567da" }, { "path": "certificates/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "eccafa830c16170c36faf93045ddf1f638f7bcd4", "sha256": "4c0b9d37e1034b2076e30a70f8e514416298c462d9ee98bc87fe6556b14df786" }, @@ -22,7 +22,7 @@ }, { "path": "docs/ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "63ba3e9aa8bdc5e942b56e34244b92b16f854085", "sha256": "c7d3027e9ad8bcbff68f07aa9576b30fb2f3c76c44d876d40c7fdbf4a3e2228a" }, @@ -34,163 +34,163 @@ }, { "path": "research/clifford-state-performance/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "6f98a0061a5104dfab82c9e806f819b41811f684", "sha256": "396d0f08df24952248140d5c65c51b8c902ef1c580892ff7ea182890530f67ee" }, { "path": "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "5e0f92af463ec12c5e1dcc3effd44081a88af647", "sha256": "07a9daeaf2bda308a92e9a4684f13d5fc766c7772d74801fceb7f4599fdab226" }, { "path": "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "9e13266bf85e627f1b7dc225e9530ea69fd2c7f0", "sha256": "421e1211fb1897c45621dc6801c276e53f2e6f335583c9c9049e535f87c0a3b1" }, { "path": "research/community-batch932-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "cc4d03eb59b9ab3f952735f7e88ff18c2d15d7af", "sha256": "184629cac91a5cfaca50330a88596008b824221433867dcf8117539c913c284a" }, { "path": "research/community-batch970-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8b9f4111badf7de5d97684799560b55110e9da79", "sha256": "23188ed920e38a54006cb883e181585620821c63bf7e8b5e05d32719417cc37e" }, { "path": "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "a5300d4e7a5381a3f443fc54c768ca6f0f236d68", "sha256": "3c820fb30e1b4d9bcfc6a7ab524375e5b2abd66b940af2c509146104f0bcd79c" }, { "path": "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "d7ff6d777b01d69b6ce84caf25d3b7e4a4d2f211", "sha256": "6b185a9902652f893f3ebd8ada92d2f11b6de6533a9a4d11718a8a4496101128" }, { "path": "research/community-hyperplane599-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "546f37d326d10a99910ae8f908e71ef768524d98", "sha256": "65099d764bfcc39bda5e4d9966783611b094c3522dbdd1435cd498d657a8ef8e" }, { "path": "research/community-k492-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "e538481e4cb16ed936d3195f2dfb5b5a9ca0a76b", "sha256": "2c0f4fa5bc150d05658af2e7c54c4d2c337dd52b7efd3d69530ae73bcbdf452a" }, { "path": "research/community-reconciliation92-audit/MANIFEST.json", - "usage": "input", + "usage": "provenance", "git_blob": "2a2e93685173d5f13cbb5abe740f5d90352e0228", "sha256": "5f501f3c118131e7d069f30ad77186eb2ad6961f9680a0ef105f4514ed41808a" }, { "path": "research/partial-swap-digest/baseline.py", - "usage": "input", + "usage": "provenance", "git_blob": "a2f0190704db83bd8ef48e46e723c49b925804fe", "sha256": "81e9af92cdf38243a540cdcff2062778e449467848d444da37a9553c12ca4c34" }, { "path": "research/r420-two-sided-basis/SOURCES.json", - "usage": "input", + "usage": "provenance", "git_blob": "5d718e11e62f4bcadecf1e02d6b61f87dbe190b0", "sha256": "d9810b0d139c5a1211fd2c1f0d142187cc1fca30026e1e7bc4f9ecfacf1596d1" }, { "path": "research/skip-clones/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8d1bb3b9c8189e35e5d8bfdfa632d7473e8be0d5", "sha256": "0b68e63e35a97ce6b0cdb6e291b88ebaa8f2dd4afb70b2498f10ee89428258dc" }, { "path": "research/split-skip/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "2ab610b6ea2edd2865fda793ef2168b0c76afb4f", "sha256": "7c2b4646a3ecfef6f881da5c43e4bd0fa9a4d1b00548b8ab458d897e16735134" }, { "path": "scripts/historical-ci-inputs/Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "aff68409021c9d401a6f8013b9dfd7dbcc30f2a8", "sha256": "ea8830dd79da493e2d75baf753d733ff7efbcf2b4794afe41fae0ac8f3055646" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "65db599ab0b1dea0312c4ca048e0bd0f44c3736f", "sha256": "96ea543e6c707424afe247e77bd86c82152f90fc76a0773c4232145da5cdf8d1" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "34820a8f24678f918f4d0e7a35380d8013fc3495", "sha256": "628391b6abfbc8674ceec1751867a4392f2cc0b5b66886243e139af86cf355ac" }, { "path": "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "c755b76e0d44ba4917aa94440ebe54daefce5b2a", "sha256": "d7fd929726b326aeeaf0a3996475adec88eee9aac09ae0bebeeaa0bc1fc8f199" }, { "path": "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "7f3c012504187917a728b9fe87043f0fc8cd006a", "sha256": "a854022e0e1d5d4db4d60e586be3ea56005013ef14a1fc06d02bc06e8529c4b0" }, { "path": "scripts/historical-ci-inputs/partial-swap-context.json", - "usage": "input", + "usage": "provenance", "git_blob": "ad65114886bf34a4fd27e79f3be502389e689faa", "sha256": "833a9642f33aeab2ffea17ec9c6b82e0a953f90192b2c82e10bef21538dccba9" }, { "path": "scripts/historical-ci-inputs/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "52075f2463f60af5e16571347f24274fce73a1ea", "sha256": "f3c4be597b2f2136da4ae2cc80c7454f63c90aa01f84e5b8131cee4dd55de815" }, { "path": "scripts/partial_swap/shared.py", - "usage": "input", + "usage": "provenance", "git_blob": "44a0e454c70f9c4b98e258b8443612e6a119904b", "sha256": "5a0646a50b9f3e8ea55168620a78e8853b0ab810517cefc8cfb8696aedee278a" }, { "path": "scripts/replay_historical_check.py", - "usage": "input", + "usage": "provenance", "git_blob": "1e92fff2782970ef71378f594f2350d245a4db26", "sha256": "5467619c78183d3adc82b0cb55af28e5c1a01fca2b0588677816244b53e2bafd" }, { "path": "scripts/research_package.py", - "usage": "input", + "usage": "provenance", "git_blob": "091b4c8f58bac9a9580d76025b887dc5c873d05f", "sha256": "e1256016e7f51827d04fa2179255989f639ae1d97afaa9c16265f85a0c6abd70" }, { "path": "scripts/run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "a96ab35b315ce492e7fbbfd6c5ae211aa066b541", "sha256": "49eb56dd0fc0d8d8ffdb209970a7adf2176223580646f575d5c22e59543b381c" }, { "path": "scripts/verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "6882a4700e410dec569b51ae2eaf1a19cc019195", "sha256": "d6b305eac5b9bdb8172c469ad30a1655a60fa0aceac8b1bf610e1b73f51babd8" }, { "path": "tests/test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "343b24abf6719b81805eba5a84c74e57634c8288", "sha256": "3a5470d0b139828b90e19bf9583ddeafcd69f8e34f2824664eb3a2958a52e34d" } diff --git a/research/historical-selected-replay-gap/VERIFY.json b/research/historical-selected-replay-gap/VERIFY.json index 98553e72ed..ab7efa3471 100644 --- a/research/historical-selected-replay-gap/VERIFY.json +++ b/research/historical-selected-replay-gap/VERIFY.json @@ -4,36 +4,7 @@ "python": "3.12", "requirements": [], "inputs": [ - "Makefile", - "certificates/partial-swap-network.json", - "docs/ci-verification.md", - "research/clifford-state-performance/SOURCE.json", - "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "research/community-batch932-audit/CONTENT-COVERAGE.json", - "research/community-batch970-audit/CONTENT-COVERAGE.json", - "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "research/community-hyperplane599-audit/SOURCE.json", - "research/community-k492-audit/SOURCE.json", - "research/community-reconciliation92-audit/MANIFEST.json", - "research/partial-swap-digest/baseline.py", - "research/r420-two-sided-basis/SOURCES.json", - "research/skip-clones/SOURCE.json", - "research/split-skip/SOURCE.json", - "scripts/historical-ci-inputs/Makefile", - "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "scripts/historical-ci-inputs/partial-swap-context.json", - "scripts/historical-ci-inputs/partial-swap-network.json", - "scripts/partial_swap/shared.py", - "scripts/replay_historical_check.py", - "scripts/research_package.py", - "scripts/run_isolated_tests.py", - "scripts/verify_selected_result.py", - "tests/test_isolated_test_runner.py" + "scripts/research_package.py" ], "commands": [ { diff --git a/research/historical-selected-replay-gap/verify.py b/research/historical-selected-replay-gap/verify.py index 83b995941a..9d266c5a4e 100644 --- a/research/historical-selected-replay-gap/verify.py +++ b/research/historical-selected-replay-gap/verify.py @@ -6,8 +6,10 @@ """ import hashlib import importlib.util +import json import subprocess import sys +import tempfile from pathlib import Path ROOT = Path(__file__).resolve().parents[2] @@ -61,31 +63,47 @@ def require(ok, message): raise SystemExit(message) -def load_checker(): - path = ROOT / "scripts/replay_historical_check.py" - spec = importlib.util.spec_from_file_location("historical_selected_replay_gap_checker", path) +def load_module(path): + spec = importlib.util.spec_from_file_location(path.stem, path) module = importlib.util.module_from_spec(spec) spec.loader.exec_module(module) return module +def checkout_snapshot(snapshot, sources, runner, env): + paths = [runner.canonical_relative_path(row["path"]) for row in sources["files"]] + git = ["git", "-c", "maintenance.auto=false", "-c", "gc.auto=0", + "-c", "core.autocrlf=false"] + subprocess.run([*git, "clone", "--quiet", "--shared", "--no-tags", "--no-checkout", + "--", str(ROOT), str(snapshot)], cwd=ROOT, env=env, check=True) + subprocess.run([*git, "update-ref", "--no-deref", "HEAD", INSPECTED], + cwd=snapshot, env=env, check=True) + # The pinned planner reads omitted manifests from the sparse HEAD/index. + patterns = "".join(f"/{path.as_posix()}\n" for path in paths) + subprocess.run([*git, "sparse-checkout", "set", "--no-cone", "--stdin"], + cwd=snapshot, env=env, input=patterns.encode("utf-8"), check=True) + subprocess.run([*git, "read-tree", "-mu", "HEAD"], cwd=snapshot, env=env, check=True) + for path, row in zip(paths, sources["files"], strict=True): + require(hashlib.sha256((snapshot / path).read_bytes()).hexdigest() == row["sha256"], + "historical checkout source digest changed: " + path.as_posix()) + + def entries(checker): for name, config in checker.CONFIG.items(): for entry in [config, *config.get("additional_inputs", [])]: yield name, entry -def reject(checker, entry): +def reject(root, checker, entry): try: - checker.authenticated_input(ROOT, entry) + checker.authenticated_input(root, entry) except ValueError as exc: return str(exc) raise SystemExit("historical input was admitted: " + entry["path"]) -def main(): - require(not sys.flags.optimize, "assertions must stay enabled") - checker = load_checker() +def check_snapshot(root, env): + checker = load_module(root / "scripts/replay_historical_check.py") selected = [entry for name, entry in entries(checker) if name == "tooling-ledger" and entry["path"] == SELECTED_PATH] require(len(selected) == 1, "selected-result checker overlay is not unique") @@ -94,7 +112,7 @@ def main(): require(entry["accepted_live_sha256"] == [SELECTED_ACCEPTED], "accepted selected-checker successors changed") frozen = (checker.INPUTS / entry["input"]).read_bytes() - live = (ROOT / SELECTED_PATH).read_bytes() + live = (root / SELECTED_PATH).read_bytes() require(hashlib.sha256(frozen).hexdigest() == SELECTED_PIN, "frozen selected checker bytes changed") require(hashlib.sha256(live).hexdigest() == SELECTED_LIVE, "live selected checker digest changed") require(SELECTED_LIVE not in (SELECTED_PIN, SELECTED_ACCEPTED), "live checker was already admitted") @@ -102,7 +120,7 @@ def main(): # live successor, not a broken comparison. require(SELECTED_PIN in (SELECTED_PIN, *entry["accepted_live_sha256"]), "pin membership control failed") - require(reject(checker, entry) == REJECTIONS[SELECTED_PATH][1], + require(reject(root, checker, entry) == REJECTIONS[SELECTED_PATH][1], "selected checker rejection text changed") counts = {path: 0 for path in REJECTIONS} @@ -110,7 +128,7 @@ def main(): for _name, item in entries(checker): if item["path"] not in REJECTIONS: continue - message = reject(checker, item) + message = reject(root, checker, item) counts[item["path"]] += 1 messages.setdefault(item["path"], message) for path, (count, message) in REJECTIONS.items(): @@ -118,20 +136,31 @@ def main(): require(messages[path] == message, "rejection text changed for " + path) require(sum(counts.values()) == 19, "rejection total changed") ci = [item for _name, item in entries(checker) if item["path"] == CI_PATH] - require(len(ci) == 1 and hashlib.sha256((ROOT / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, + require(len(ci) == 1 and hashlib.sha256((root / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, "selected CI note digest changed") diff = subprocess.check_output( - ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=ROOT, text=True) + ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=root, env=env, text=True) changed = sorted(name for name in diff.splitlines() if name) require(changed == CHANGED, "inspected commit diff changed") - sys.path.insert(0, str(ROOT / "scripts")) - from research_package import plan_details - details = plan_details(ROOT, set(changed)) + planner = load_module(root / "scripts/research_package.py") + details = planner.plan_details(root, set(changed)) require([row["package"] for row in details] == PLAN_PACKAGES, "helper plan selection changed") matched = {name for row in details for names in row["causes"].values() for name in names} require(sorted(set(changed) - matched) == UNMATCHED, "unmatched plan paths changed") - require(plan_details(ROOT, set()) == [], "empty change set selected a package") + require(planner.plan_details(root, set()) == [], "empty change set selected a package") + + +def main(): + require(not sys.flags.optimize, "assertions must stay enabled") + sources = json.loads(Path(__file__).with_name("SOURCES.json").read_bytes()) + require(sources["base_commit"] == INSPECTED, "historical checkout base changed") + runner = load_module(ROOT / "scripts/research_package.py") + env = runner.git_source_env() + with tempfile.TemporaryDirectory(prefix="historical-selected-replay-") as temporary: + snapshot = Path(temporary) / "snapshot" + checkout_snapshot(snapshot, sources, runner, env) + check_snapshot(snapshot, env) print("PASS_HISTORICAL_SELECTED_REPLAY_GAP") print("selected_checker_live=" + SELECTED_LIVE) print("rejections=19 distinct_paths=7 plan_packages=9") diff --git a/research/p104-rank-five-chart233-prefix-bound/LOCAL-PINS.json b/research/p104-rank-five-chart233-prefix-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..fa50a32c1d --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/LOCAL-PINS.json @@ -0,0 +1,19 @@ +{ + "PROVENANCE.json": "c1faf8946d6065b76979f54080cf6cddf0d751fd4391fc2631c2590399ea1828", + "engines/freeze.py": "7d9004d88386aeeb83c35dd9952419da0df4f03de5d5873c3e7a6bfd3c8c0369", + "engines/modular.py": "9a84c502d1cb62aa2f149cc7ca7c409b6ab3098e85d50d7a21f3329b1f82aa07", + "engines/prefix.py": "7f0eb780803ae41ad2fa71794ae1c070e19cccc65ce6fbfd0588a0861a1fb3ae", + "engines/verify_axes.py": "933696292df26ff08a5e63214647c7f4eb8791bbc8fe181198da07dee47f7bc0", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/PR7370-SHA256.json": "ea5a3157a967c01b94fd57ca26f8ace1bfa2c6e8165271af917846eb14f9c0d9", + "inputs/R115-GEOMETRY.json.gz": "6a6e3e576deff0174c928c6929863fa3f3b66698b4394063a98df0f932dcd200", + "inputs/R115-PRICE.json.gz": "2bfd2e221e42363c6aeec7619263a04c39abf711f426f984d090943e0a7bb115", + "inputs/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/exterior_rank23.py": "7a20424d9a554795e89fd7288361529d8d1c91c256f529a63ef2d867a40bd31f", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "inputs/reverse_engine.py": "751d5d0c4c665c8768ff69bcf939700d3be2f989c59f09af3a4aa14d3c1ebbc4", + "inputs/second_prime.py": "21dbd96192e1f60c00ceddba01a7e8d0ddd7d6ad7da4ad3ed22ef2e47cc589c4", + "receipts/AGREEMENT.json": "e85668ebd96c302102fa23b65f35f0bd1629130d433e1c7fc8d1963111fc853e", + "receipts/SHA256.json": "fd334987adac93393bab7578815ec8f9a9cb16ce8dce9b6620613efddde3203d", + "replay.py": "9156c6383a35373910b09c4d082c3fe06823da95af653a124586e96178228315" +} diff --git a/research/p104-rank-five-chart233-prefix-bound/NOTICE b/research/p104-rank-five-chart233-prefix-bound/NOTICE new file mode 100644 index 0000000000..981c527ea4 --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/NOTICE @@ -0,0 +1,8 @@ +Apache-2.0. + +#7370 supplies the exact catalogue, cohort and price. #7334 and +#7113 supply the exact native word and signed caller. #7338, +#7298 and #7319 supply the complete admitted price, directed +tariff and helper census. #5599, #7367 and #5994 supply proof +and census precedents. OpenAI Codex and subagents materially +assisted. diff --git a/research/p104-rank-five-chart233-prefix-bound/PROOF.md b/research/p104-rank-five-chart233-prefix-bound/PROOF.md new file mode 100644 index 0000000000..05050490d8 --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/PROOF.md @@ -0,0 +1,20 @@ +# Fixed-paid chart 3→233 rank-five split + +The authenticated #7370 geometry exhausts 76,466 literal events across 80 eligible rank-five helpers in 28 endpoint cohorts. Its completed support group is chart 3→241. The separate #7373 result covers chart 3→238. This continuation takes all 17 bank representatives for roles 289 and 1052 with chart path 3→233. The endpoint chart ranks are zero and five, so the 2+3 or 3+2 split requires a strict existing rank-two or rank-three intermediate chart. Each selected bank is owned-empty. + +| Productive pivot | Intermediate chart | Literal pre-event clocks | +|---:|---:|---| +| 289 | 329 | 28620, 28621, 28622, 28626 | +| 289 | 340 | 28632, 28633 | +| 1052 | 329 | 34829, 34830, 34831 | +| 1052 | 340 | 34836, 34837, 34838, 34864, 34865, 34866, 34871, 34875 | + +A cut c denotes the state after exactly c literal events. Let P be the normalized prefix-row matrix for the public roles in the intermediate chart, and let E project onto original input coordinates outside the cohort. A pure prefix requires a nonzero row a with aPE = 0. A full-row-rank minor of PE rules out this condition for arbitrary input. + +The 65521 and 65537 engines replay all signed scalar and chart events, reconstruct each public bank, and check owned occupancy and pivot roles. The scalar denominators are units at the replay primes, with 98 distinct denominators in the independent pass. A nonzero determinant modulo a prime gives a nonzero determinant over the rationals because the original rational entries have unit denominators there. The 65537 engine produces its own full minors and evaluates all 17 primary axis sets independently. Every axis set gives a nonzero determinant. All 17 keys are individually verified without using alias equivalence. Suffix, exact unit pairing and signed construction were unnecessary after this prefix exclusion. The 14 other keys stay outside the stated scope. + +## Complete price + +All 110,519 paid positions stay fixed in the 17-copy signed application. One split changes the productive histogram by `{2:+17, 3:+17, 5:−17}`, raises productive positions from 22,461 to 22,478 and conserves signed rank surplus 1,424. The replay recomputes the directed #7298 tariff from the complete #7338 paid and productive readback. At the comparator crossing upper, the one-edit saving is at most 0.207666506667591 raw and the two-role compatible saving at most 0.415333013335181 raw. The complete margin at fixed target κ = 0.0040075385047236 is at most −139.310694990954. One additional raw paid rank-one position exceeds the two-role relaxation. + +The native all-columns, owned-erasure, compiler, precision/tape and analytic recovery premises are retained. A physical survivor would require signed forward and adjoint identities, paid route and restoration proof, and a fresh caller and precision/tape check on the complete invoice. diff --git a/research/p104-rank-five-chart233-prefix-bound/PROVENANCE.json b/research/p104-rank-five-chart233-prefix-bound/PROVENANCE.json new file mode 100644 index 0000000000..35addfaac5 --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/PROVENANCE.json @@ -0,0 +1,46 @@ +{ + "derived_gzip": { + "R115-GEOMETRY": { + "key": "R115-GEOMETRY.json", + "receipt": "inputs/PR7370-SHA256.json" + }, + "R115-PRICE": { + "key": "R115-PRICE.json", + "receipt": "inputs/PR7370-SHA256.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/PR7370-SHA256.json": { + "commit": "a41edc3ae92332a7a1f1ba90e9ea4901d0530185", + "git_blob": "695c7c46ca319b0a6b7ca6154a32021121b22e6a", + "path": "research/p104-rank-five-catalogue-bound/receipts/SHA256.json", + "sha256": "ea5a3157a967c01b94fd57ca26f8ace1bfa2c6e8165271af917846eb14f9c0d9", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/a41edc3ae92332a7a1f1ba90e9ea4901d0530185/research/p104-rank-five-catalogue-bound/receipts/SHA256.json" + }, + "inputs/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-five-chart233-prefix-bound/README.md b/research/p104-rank-five-chart233-prefix-bound/README.md new file mode 100644 index 0000000000..9440f381ee --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/README.md @@ -0,0 +1,29 @@ +# Fixed-paid rank-five prefix bounds on chart 3→233 + +**NO VERIFIED GAIN.** Exact Δκ = 0 relative to independently reproduced conditional κ = `0.00364665195644` on #7334 at `aaeec8c0acf01e99a5f331ef363a698d9c084ace`, with signed #7113 at `07a76c5e2738882c0cb322278e56f6cae3c9885d`. [Comparator #7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) · [Signed caller #7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) + +All 17 frozen public banks for productive roles 289 and 1052 fail the necessary prefix test for a fixed-paid 2+3 or 3+2 split. The banks occupy intermediate charts 329 and 340 with no owned fields. Both prime-field engines produce full exterior prefix rank on every bank. The primary minor's coordinate set remains nonzero at the independent prime in every case. There are no unresolved keys in 3→233. Fourteen keys on endpoint groups 712→127 and 714→127 remain outside this replay. [Exact per-key agreement](receipts/AGREEMENT.json) + +The directed one-edit saving upper is about 0.207666506667591 raw at the comparator crossing. The compatible two-role upper is 0.415333013335181, with all 110,519 paid positions held fixed. The tested scope produces zero verified saving. [Complete price and proof](PROOF.md) + +## Replay + +From a clean checkout with CPython 3.12 and assertions enabled: + +```sh +python3.12 -I -B research/p104-rank-five-chart233-prefix-bound/replay.py +``` + +The standard-library replay authenticates the pinned #7370 manifest, price and geometry, as well as the exact #7334 word. It reconstructs the directed price, freezes all 17 keys, checks the primary minors at both primes and rejects altered selection and geometry. Add `--out fresh-directory` to retain the four receipts. The replay runs with no Git metadata, network, external input root or prior temporary state. [Verification](VERIFICATION.md) · [Provenance](PROVENANCE.json) · [Path-keyed pins](LOCAL-PINS.json) + +## Open next questions + +Can either seven-key group on 712→127 or 714→127 supply a pure prefix and suffix with nonzero unit pairing? Start with the remaining key list in the regenerated selection, price one cohort on the full signed invoice and screen its exterior rank. Any positive support still needs an exact signed construction and complete verification. + +## Credit + +#7370 at `a41edc3ae92332a7a1f1ba90e9ea4901d0530185` supplies the complete catalogue and price. #7373 at `f390469548c0f7a44465bf80476ad7bc5a8e20f5` supplies the two-prime replay workflow and covers the separate 3→238 cohort. [Catalogue #7370](https://github.com/CrocSwap/integer-mult-bounds/pull/7370) · [Predecessor #7373](https://github.com/CrocSwap/integer-mult-bounds/pull/7373) + +#7338 supplies the complete signed invoice, #7298 the directed arithmetic and #7319 the exact helper census. #5599 supplies the common-frame split method, #7367 the exterior proof on a different cohort and #5994 the earlier broad census on another word. [#7338](https://github.com/CrocSwap/integer-mult-bounds/pull/7338) · [#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) · [#7319](https://github.com/CrocSwap/integer-mult-bounds/pull/7319) · [#5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599) · [#7367](https://github.com/CrocSwap/integer-mult-bounds/pull/7367) · [#5994](https://github.com/CrocSwap/integer-mult-bounds/pull/5994) + +OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging. diff --git a/research/p104-rank-five-chart233-prefix-bound/SOURCES.json b/research/p104-rank-five-chart233-prefix-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/SOURCES.json @@ -0,0 +1,18 @@ +{ + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "path": "certificates/selected-result.json", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1", + "usage": "provenance" + }, + { + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "path": "docs/research/agent-task-catalog.json", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "usage": "provenance" + } + ], + "schema_version": 1 +} diff --git a/research/p104-rank-five-chart233-prefix-bound/TASK.json b/research/p104-rank-five-chart233-prefix-bound/TASK.json new file mode 100644 index 0000000000..1c88d1cafd --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "On exact #7334, fixed-paid rank-five 2+3 or 3+2 productive splitting for roles 289 and 1052 in the exact 17 chart 3\u2192233 public-bank keys inherited from #7370.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "P104 chart 3-to-233 rank-five split research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "A productive split may improve the binding complex bill only if an intermediate public bank supplies a pure cohort prefix and suffix with exact unit pairing.", + "budget_minutes": 10, + "evidence": "Both bounded prime-field prefix walks exclude all 17 owner-empty banks on charts 329 and 340. Every original minor coordinate set remains nonzero at the independent prime. Fourteen keys on 712\u2192127 and 714\u2192127 remain outside scope.", + "open_questions": [ + { + "blocked_by": "All exact 3\u2192233 public banks fail the prefix gate.", + "first_step": "Freeze one seven-key cohort from 712\u2192127 or 714\u2192127 using the selection receipt. Price it before a bounded prefix/suffix replay.", + "question": "Can a different fixed-paid rank-five group supply a two-sided exact pair?", + "why_it_matters": "A valid productive split can improve the binding complete recurrence without changing paid stock." + } + ], + "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": "Tests the complete chart 3\u2192233 rank-five group left outside #7370 and the 3\u2192238 result in #7373.", + "scope_status": "changed", + "stop_rule": "Freeze the exact 17 keys from #7370, then at most 76,466 events per prime and 25 seconds per gate. Skip suffix and signed construction after full prefix exclusion.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-rank-five-chart233-prefix-bound/VERIFICATION.md b/research/p104-rank-five-chart233-prefix-bound/VERIFICATION.md new file mode 100644 index 0000000000..0e357b7a4b --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/VERIFICATION.md @@ -0,0 +1,7 @@ +# Verification + +The direct CPython 3.12 replay exited 0 in 2.59 seconds. A relocated Git-free copy with an empty inherited environment exited 0 in 2.33 seconds and reproduced all four receipts byte for byte. The primary selection mutation, independent selection mutation and independent geometry mutation each returned exit 1. + +The two modular engines each exhaust the 76,466-event tape and 17 selected banks. Both primes give full exterior prefix rank at every key. All 17 primary axis sets give nonzero determinants on the independent rows. There are no unresolved selected keys. Suffix and physical work were skipped after the exact prefix exclusion. Fourteen keys in two other endpoint groups remain outside this replay. + +[Exact source provenance](PROVENANCE.json) · [Replay command](README.md) · [Receipt hashes](receipts/SHA256.json) diff --git a/research/p104-rank-five-chart233-prefix-bound/VERIFY.json b/research/p104-rank-five-chart233-prefix-bound/VERIFY.json new file mode 100644 index 0000000000..1058593664 --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Authenticate the exact #7370 geometry and directed price, recompute the full invoice, compare all 17 prefix minors at both primes including primary axes, and reject altered selection and geometry.", + "timeout_seconds": 100 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-rank-five-chart233-prefix-bound/engines/freeze.py b/research/p104-rank-five-chart233-prefix-bound/engines/freeze.py new file mode 100644 index 0000000000..e5cbb40b10 --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/engines/freeze.py @@ -0,0 +1,60 @@ +"""Select and price the untouched rank-five 3-to-233 endpoint group.""" +from fractions import Fraction +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "inputs/R115-PRICE.json": "c04adfb199f6dbc25806d6062562c7d707b8fda8ad73f3ed818901248d25ffbf", + "inputs/R115-GEOMETRY.json": "c2a4406cf7130a819189e8ceefb4bb6e09edd392eb56820f9fcadb0e9415ef4e", +} + + +def unique(items): + out = dict(items) + if len(out) != len(items): + raise ValueError("duplicate JSON key") + return out + + +def read(path): + raw = (ROOT / path).read_bytes() + if sha256(raw).hexdigest() != PINS[path]: + raise ValueError(f"changed dependency {path}") + return loads(raw, object_pairs_hook=unique) + + +def main(): + assert __debug__ + price, geom = map(read, PINS) + assert price["head"] == geom["head"] == "aaeec8c0acf01e99a5f331ef363a698d9c084ace" + assert geom["status"] == "EXHAUSTED" and len(geom["candidate_rows"]) == 68 + group = [3, 233] + cohort = next(g["roles"] for g in price["groups"] if g["endpoints"] == group) + assert cohort == [289, 1052] and geom["selected_group"] == [3, 241] + rows = [r for r in geom["candidate_rows"] if r["key"][2:] == group] + assert len(rows) == len({tuple(r["key"]) for r in rows}) == 17 + assert all(r["pivots"] and not r["owned"] for r in rows) + assert {r["key"][1] for r in rows} <= set(next(g["labels"] for g in geom["groups"] if g["endpoints"] == group)) + at, moon = price["at_incumbent"], price["at_target"] + assert price["paid_delta"] == {} and price["productive_delta"] == {"2": 17, "3": 17, "5": -17} + assert Fraction(at["gross_one"][0]) > 0 + whole = 2 * Fraction(at["gross_one"][1]) + fixed_complete = Fraction(moon["old_margin"][1]) + 2 * Fraction(moon["gross_one"][1]) + print(dumps({ + "head": price["head"], "caller": price["caller"], "pins": PINS, + "selected_group": group, "cohort": cohort, "paid_delta": {}, "productive_delta": price["productive_delta"], + "one_gross": at["gross_one"], "two_compatible_upper": str(whole), + "fixed_target": price["moonshot"], "fixed_target_complete_upper": str(fixed_complete), + "unchanged_paid_positions": 110519, "productive_one": 22478, "surplus": 1424, + "selected": [dict(r, key=r["key"][:2]) for r in rows], + "unselected": [r["key"] for r in geom["candidate_rows"] if r["key"][2:] not in (group, [3, 241], [3, 238])], + "caps": {"representatives": 17, "events_per_direction": 76466, + "modular_seconds": 25, "exact_pairs": 4, "exact_seconds": 35, + "prototype_seconds": 120}, + }, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-five-chart233-prefix-bound/engines/modular.py b/research/p104-rank-five-chart233-prefix-bound/engines/modular.py new file mode 100644 index 0000000000..759d2985b0 --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/engines/modular.py @@ -0,0 +1,102 @@ +"""Reconstruct two-sided exterior minors for 17 frozen rank-five banks.""" +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 signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "SELECTION.json":"910c8881f31721793cb8e8cbf3b3b3789a9986415e0d48dd9c97d146d5b37bcc", + "inputs/R115-PRICE.json":"c04adfb199f6dbc25806d6062562c7d707b8fda8ad73f3ed818901248d25ffbf", + "inputs/7334-WORD.json.gz":"4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/exterior_rank23.py":"7a20424d9a554795e89fd7288361529d8d1c91c256f529a63ef2d867a40bd31f", + "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 timed_out(*_): + raise TimeoutError("25-second hard cap") + + +def main(): + assert __debug__ + signal(SIGALRM,timed_out) + alarm(25) + deadline=monotonic()+22 + docs=checked() + price=json.loads(docs["inputs/R115-PRICE.json"]) + selection=json.loads(docs["SELECTION.json"]) + word=json.loads(decompress(docs["inputs/7334-WORD.json.gz"])) + assert len(word["program"])==selection["caps"]["events_per_direction"] + engine=run_path(str(ROOT/"inputs/exterior_rank23.py")) + reverse=run_path(str(ROOT/"inputs/reverse_engine.py")) + controls=reverse["controls"](engine) + cohort=set(next(g["roles"] for g in price["groups"] if g["endpoints"]==selection["selected_group"])) + assert cohort=={289,1052}==set(selection["cohort"]) + rows=selection["selected"] + assert len(rows)==17 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)) + alarm(0) + 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-five-chart233-prefix-bound/engines/prefix.py b/research/p104-rank-five-chart233-prefix-bound/engines/prefix.py new file mode 100644 index 0000000000..511a97ca56 --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/engines/prefix.py @@ -0,0 +1,163 @@ +"""Check the 17 frozen rank-five 3→233 exterior prefixes at prime 65537.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +WORD = "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PINS = { + "inputs/SELECTION.json": "910c8881f31721793cb8e8cbf3b3b3789a9986415e0d48dd9c97d146d5b37bcc", + "inputs/GEOMETRY.json": "c2a4406cf7130a819189e8ceefb4bb6e09edd392eb56820f9fcadb0e9415ef4e", + "inputs/PRICE.json": "c04adfb199f6dbc25806d6062562c7d707b8fda8ad73f3ed818901248d25ffbf", + "inputs/second_prime.py": "21dbd96192e1f60c00ceddba01a7e8d0ddd7d6ad7da4ad3ed22ef2e47cc589c4", + "inputs/7334-WORD.json.gz": WORD, +} +GROUP = [3, 233] +COHORT = {289, 1052} +EVENTS, CASES, SECONDS, PRIME = 76466, 17, 25, 65537 + + +def unique(pairs): + result = dict(pairs) + if len(result) != len(pairs): + raise ValueError("duplicate JSON key") + return result + + +def checked(root, name): + raw = (root / name).read_bytes() + if sha256(raw).hexdigest() != PINS[name]: + raise ValueError("changed dependency " + name) + return raw + + +def freeze(root): + selection = loads(checked(root, "inputs/SELECTION.json"), object_pairs_hook=unique) + price = loads(checked(root, "inputs/PRICE.json"), object_pairs_hook=unique) + geometry = loads(checked(root, "inputs/GEOMETRY.json"), object_pairs_hook=unique) + assert price["head"] == geometry["head"] == selection["head"] == HEAD + assert price["caller"] == selection["caller"] == CALLER + assert price["word_sha256"] == geometry["pins"]["inputs/7334-WORD.json.gz"] == WORD + assert geometry["pins"]["lead/PRICE.json"] == PINS["inputs/PRICE.json"] + assert selection["pins"]["inputs/R115-PRICE.json"] == PINS["inputs/PRICE.json"] + assert selection["pins"]["inputs/R115-GEOMETRY.json"] == PINS["inputs/GEOMETRY.json"] + assert geometry["status"] == "EXHAUSTED" and geometry["visited_events"] == EVENTS + assert len(price["groups"]) == 28 and len(geometry["candidate_rows"]) == 68 + assert [set(g["roles"]) for g in price["groups"] if g["endpoints"] == GROUP] == [COHORT] + chosen = {tuple(r["key"][:2]): r for r in geometry["candidate_rows"] if r["key"][2:] == GROUP} + assert selection["selected_group"] == GROUP and set(selection["cohort"]) == COHORT + caps = selection["caps"] + assert (caps["representatives"], caps["events_per_direction"], caps["modular_seconds"]) == (CASES, EVENTS, SECONDS) + assert len(chosen) == len(selection["selected"]) == CASES + assert list(chosen) == [tuple(r["key"]) for r in selection["selected"]] + for row in selection["selected"]: + original = chosen[tuple(row["key"])] + assert all(row[f] == original[f] for f in ("public", "owned", "pivots")) + assert not row["owned"] and row["key"][1] in (329, 340) + return chosen + + +def prefix(word, chosen, engine, deadline, progress, results, denoms): + 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]] == GROUP for r in COHORT) + frames = word["frames"] + + @cache + def span(label): + return engine["span"](frames[label]) + + low, high = map(span, GROUP) + assert len(low) == 1 and len(high) == 32 and low < high + by_cut = defaultdict(list) + for cut, chart in chosen: + assert 0 <= cut <= EVENTS and len(frames[chart]) in (2, 3) + assert low < span(chart) < high + by_cut[cut].append(chart) + + active = word["initial"] + [None] * owned + vectors = [{i: 1} for i in range(n)] + [None] * owned + fresh = set() + for cut in range(EVENTS + 1): + progress["first_unvisited_cut"] = cut + if (cut % 128 == 0 or cut in by_cut) and monotonic() >= deadline: + raise TimeoutError("bounded literal prefix") + for chart in by_cut.get(cut, ()): + key = cut, chart + public = [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(public) & COHORT) + assert public == chosen[key]["public"] and owners == chosen[key]["owned"] + assert pivots and pivots == chosen[key]["pivots"] + proof = engine["classify"](public, vectors, COHORT) + exterior = [{i: v for i, v in vectors[r].items() if i not in COHORT} for r in public] + results[key] = dict(key=key, chart_rank=len(frames[chart]), public=public, + owned=owners, pivots=pivots, exterior_rows=exterior, independent_minor=proof, + disposition="prefix exclusion" if not proof["kernel"] else "modular rank drop") + if cut == EVENTS: + assert active == word["final"] + [None] * owned and not fresh + assert len(results) == CASES + progress["first_unvisited_cut"] = None + break + event = tape[cut] + if event[0] == "MOVE": + old, new, is_owned = event[2:] + assert span(old) < span(new) or is_owned and span(new) < span(old) + engine["apply"](event, active, vectors, fresh, n, denoms, False) + progress["events"] += 1 + + +def main(): + parser = ArgumentParser() + parser.add_argument("--root", type=Path, default=ROOT) + parser.add_argument("--controls-only", action="store_true") + args = parser.parse_args() + assert __debug__ + name = "inputs/second_prime.py" + checked(args.root, name) + engine = run_path(str(args.root / name)) + assert engine["PRIME"] == PRIME + controls = engine["controls"]() + chosen = freeze(args.root) + if args.controls_only: + print(dumps(dict(controls=controls, frozen_keys=list(chosen)), indent=2)) + return 0 + + def stop(*_): + raise TimeoutError("hard 25-second cap") + + signal(SIGALRM, stop) + alarm(SECONDS) + deadline = monotonic() + 23 + progress = {"events": 0, "first_unvisited_cut": 0} + output, denoms, timeout = {}, set(), None + try: + payload = decompress(checked(args.root, "inputs/7334-WORD.json.gz")) + assert sha256(payload).hexdigest() == PAYLOAD + prefix(loads(payload, object_pairs_hook=unique), chosen, engine, deadline, progress, output, denoms) + except TimeoutError as error: + timeout = str(error) + finally: + alarm(0) + rows = [output[key] for key in chosen if key in output] + print(dumps(dict(head=HEAD, caller=CALLER, pins=PINS, group=GROUP, cohort=sorted(COHORT), + prime=PRIME, cases=CASES, seconds=SECONDS, controls=controls, timeout=timeout, + rows=rows, progress=progress, denominator_units=sorted(denoms), + counts=Counter(r["disposition"] for r in rows), + unresolved=[key for key in chosen if key not in output or output[key]["disposition"] != "prefix exclusion"]), + indent=2, sort_keys=True)) + return 2 if timeout else 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/p104-rank-five-chart233-prefix-bound/engines/verify_axes.py b/research/p104-rank-five-chart233-prefix-bound/engines/verify_axes.py new file mode 100644 index 0000000000..b0189732ad --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/engines/verify_axes.py @@ -0,0 +1,72 @@ +"""Reevaluate primary full-axis minors using the sealed independent projections.""" +from argparse import ArgumentParser +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path + +ROOT = Path(__file__).resolve().parent +ENGINE = "21dbd96192e1f60c00ceddba01a7e8d0ddd7d6ad7da4ad3ed22ef2e47cc589c4" +SELECTION = "910c8881f31721793cb8e8cbf3b3b3789a9986415e0d48dd9c97d146d5b37bcc" + + +def checked(path, expected): + raw = path.read_bytes() + if sha256(raw).hexdigest() != expected: + raise ValueError("changed input " + path.name) + return raw + + +def main(): + parser = ArgumentParser() + parser.add_argument("--primary", type=Path, required=True) + parser.add_argument("--primary-sha256", required=True) + parser.add_argument("--independent", type=Path, default=ROOT / "RESULT.json") + parser.add_argument("--independent-sha256", required=True) + args = parser.parse_args() + assert __debug__ + primary = loads(checked(args.primary, args.primary_sha256)) + independent = loads(checked(args.independent, args.independent_sha256)) + path = ROOT / "inputs/second_prime.py" + checked(path, ENGINE) + engine = run_path(str(path)) + assert independent["prime"] == engine["PRIME"] == 65537 + assert primary["head"] == independent["head"] + assert primary["pins"]["SELECTION.json"] == independent["pins"]["inputs/SELECTION.json"] == SELECTION + by_key = {tuple(row["key"][:2]): row for row in primary["results"]} + assert len(by_key) == len(primary["results"]) == 17 + assert len({tuple(row["key"]) for row in independent["rows"]}) == len(independent["rows"]) <= 17 + results = [] + for row in independent["rows"]: + item = by_key[tuple(row["key"])] + receipt = item["prefix"] + for field in ("public", "owned", "pivots"): + assert row[field] == item[field] + if receipt is not None: + assert row[field] == receipt[field] + n = len(row["public"]) + if receipt is not None: + assert receipt["exterior_rank"] <= n + primary_full = None if receipt is None else receipt["exterior_rank"] == n + second_full = row["disposition"] == "prefix exclusion" + columns = None if receipt is None else receipt["columns"] + determinant = None + if primary_full: + assert receipt["determinant"] and len(set(columns)) == len(columns) == n + assert set(columns).isdisjoint(independent["cohort"]) + projected = [{int(col): val for col, val in vector.items()} for vector in row["exterior_rows"]] + determinant = engine["verify_minor"](projected, columns) + results.append(dict(key=row["key"], primary_full=primary_full, independent_full=second_full, + axes=columns, primary_det=None if receipt is None else receipt["determinant"], + primary_det_mod_65537=determinant)) + print(dumps(dict(prime=65537, primary_sha256=args.primary_sha256, independent_sha256=args.independent_sha256, + banks=len(results), same_full_rank_disposition=sum(r["primary_full"] == r["independent_full"] for r in results), + primary_nonzero_axes_at_second_prime=sum(bool(r["primary_det_mod_65537"]) for r in results), + unresolved_at_second_prime=independent["unresolved"], + primary_unvisited=[row["key"] for row in primary["results"] if row["prefix"] is None], + results=results), + indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-five-chart233-prefix-bound/inputs/7334-WORD.json.gz b/research/p104-rank-five-chart233-prefix-bound/inputs/7334-WORD.json.gz new file mode 100644 index 0000000000..73f4300719 Binary files /dev/null and b/research/p104-rank-five-chart233-prefix-bound/inputs/7334-WORD.json.gz differ diff --git a/research/p104-rank-five-chart233-prefix-bound/inputs/PR7370-SHA256.json b/research/p104-rank-five-chart233-prefix-bound/inputs/PR7370-SHA256.json new file mode 100644 index 0000000000..695c7c46ca --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/inputs/PR7370-SHA256.json @@ -0,0 +1,11 @@ +{ + "R114-GEOMETRY.json": "00c49b4bd76005b34a60f639b4a7ed8742d36239bb37aa4d8f026b4450e0cf31", + "R114-INDEPENDENT.json": "9b1cb1064349cca75ec04745649eca4d9b943ed4f6c7862b8c8cea2bd34139f0", + "R114-PRICE.json": "86fa60a067496a276d911fd3cb56b78fbb2388138be6e438b754e1573f9cd077", + "R115-AGREEMENT.json": "528f520845e21af0f12256f993a92b69641b8a99d43da07639c8c3c307806109", + "R115-ALIASES.json": "6a79a44ec164d1c1e1b3c276912ff4a37334ef17268e555330b8fe17a126d4e3", + "R115-GEOMETRY.json": "c2a4406cf7130a819189e8ceefb4bb6e09edd392eb56820f9fcadb0e9415ef4e", + "R115-MODULAR.json": "118fda832ce46e8e52e88a321bf0fcfd182b24e358756c956bc29a1944ec62ff", + "R115-PRICE.json": "c04adfb199f6dbc25806d6062562c7d707b8fda8ad73f3ed818901248d25ffbf", + "R115-SECOND.json": "6bb721c8824fd107acefd570cce44d51ecc2baef351075806c6fe91fba329c87" +} diff --git a/research/p104-rank-five-chart233-prefix-bound/inputs/R115-GEOMETRY.json.gz b/research/p104-rank-five-chart233-prefix-bound/inputs/R115-GEOMETRY.json.gz new file mode 100644 index 0000000000..386bd61611 Binary files /dev/null and b/research/p104-rank-five-chart233-prefix-bound/inputs/R115-GEOMETRY.json.gz differ diff --git a/research/p104-rank-five-chart233-prefix-bound/inputs/R115-PRICE.json.gz b/research/p104-rank-five-chart233-prefix-bound/inputs/R115-PRICE.json.gz new file mode 100644 index 0000000000..8e7559e3e6 Binary files /dev/null and b/research/p104-rank-five-chart233-prefix-bound/inputs/R115-PRICE.json.gz differ diff --git a/research/p104-rank-five-chart233-prefix-bound/inputs/READBACK.json b/research/p104-rank-five-chart233-prefix-bound/inputs/READBACK.json new file mode 100644 index 0000000000..625b508eea --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-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-five-chart233-prefix-bound/inputs/exterior_rank23.py b/research/p104-rank-five-chart233-prefix-bound/inputs/exterior_rank23.py new file mode 100644 index 0000000000..01e69f343b --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/inputs/exterior_rank23.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 (2, 3) + 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-five-chart233-prefix-bound/inputs/pricing.py b/research/p104-rank-five-chart233-prefix-bound/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/inputs/pricing.py @@ -0,0 +1,82 @@ +"""Directed interval arithmetic and the retained signed BIT invoice.""" +from collections import Counter +from fractions import Fraction +from functools import cache + +TARGET = "10018846261809/2500000000000000" +SCALE = 10**49 + + +def rounded(x, upper): + scaled = SCALE*x + if upper: + return Fraction(-((-scaled.numerator) // scaled.denominator), SCALE) + return Fraction(scaled.numerator // scaled.denominator, SCALE) + + +@cache +def log_bounds(x): + z = (x-1)/(x+1) + terms = 60 + exact_partial = 2*sum(z**(2*i+1)/(2*i+1) for i in range(terms)) + tail = 2*z**(2*terms+1)/((2*terms+1)*(1-z*z)) + return rounded(exact_partial, False), rounded(exact_partial+tail, True) + + +@cache +def power_bounds(rank, k): + binary = 2**(rank.bit_length()-1) + shift = binary.bit_length()-1 + l2, u2 = log_bounds(Fraction(2)) + lo, hi = log_bounds(Fraction(rank, binary)) + lo, hi = k*(lo+shift*l2), k*(hi+shift*u2) + assert 0 <= lo <= hi < 1 + + def exponential(z, terms): + total = term = Fraction(1) + for i in range(1, terms+1): + term *= -z/i + total += term + return total + + return rounded(rank*exponential(hi, 35), False), rounded(rank*exponential(lo, 34), True) + + +def cost(hist, k): + lower = upper = Fraction(0) + for r, n in hist.items(): + a, b = (n*x for x in power_bounds(r, k)) + lower += min(a, b) + upper += max(a, b) + return lower, upper + + +def profile(invoice, native, word, ranks): + copies = invoice["native_calls"] + assert copies == len(invoice["native_instances"]) == 36 + assert {tuple((r["stage"], r["copy"])) for r in invoice["native_instances"]} == { + (stage, which) for stage in range(1, 19) for which in (0, 1) + } + assert all(r["ports"] == 111 for r in invoice["native_instances"]) + assert native == Counter({int(r): n for r, n in invoice["native_paid"].items()}) + assert sum(native.values()) == 2871 + caller_paid = {1: 444, **{r: 444 for r in range(7, 57, 7)}} + assert invoice["event_counts"]["QUERY"]*111 == caller_paid[1] + assert invoice["event_counts"]["IDLE_ONE"]*111 == 8*444 + full_paid = Counter({r: copies*n for r, n in native.items()}) + full_paid.update(caller_paid) + + helpers = Counter(ranks[word["final"][j]]-ranks[word["start"][j]] + for j in range(222, word["public"])) + assert helpers == Counter({int(r): n for r, n in invoice["native_helpers"].items()}) + caller_targets = {**{r: 444 for r in range(8, 65, 7)}, 127: 222} + full_targets = Counter({r: copies*n for r, n in helpers.items()}) + full_targets.update(caller_targets) + assert full_paid == Counter({int(r): n for r, n in invoice["paid"].items()}) + assert full_targets == Counter({int(r): n for r, n in invoice["targets"].items()}) + assert sum(full_paid.values()) == invoice["paid_jobs"] + assert sum(full_targets.values()) == invoice["productive_fields"] + signed = full_targets.copy() + signed.subtract(full_paid) + assert sum(r*n for r, n in signed.items()) == invoice["rank_surplus"] + return signed, copies diff --git a/research/p104-rank-five-chart233-prefix-bound/inputs/reverse_engine.py b/research/p104-rank-five-chart233-prefix-bound/inputs/reverse_engine.py new file mode 100644 index 0000000000..ebfc82f83f --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-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-five-chart233-prefix-bound/inputs/second_prime.py b/research/p104-rank-five-chart233-prefix-bound/inputs/second_prime.py new file mode 100644 index 0000000000..0be5407fe6 --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/inputs/second_prime.py @@ -0,0 +1,339 @@ +"""Independently verify R97's 310 frozen R96 bank keys modulo 65537.""" + +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from math import isqrt +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic +import sys + +ROOT = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +WORD = "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +PINS = { + "inputs/PRICE.json": "a78be64c3e3ae8a0e532237c4dd3541aa9ad3fcbbc3c25d79c8a03fb7e07c525", + "inputs/GEOMETRY.json": "c6f9f018df8b58fcdf4f44356bd59bcac6d411b7845104ff4ad372ed4a95cfbd", + "inputs/REMAINING.json": "3597499663a57702856945e91214a65e1d0f94db8643b93c0234c2bbf9291b1a", + "inputs/7334-WORD.json.gz": WORD, +} +PRIME = 65537 +CASES = 310 +SECONDS = 25 +EVENTS = 76466 + + +def unique(items): + data = dict(items) + if len(items) != len(data): + raise ValueError("duplicate JSON key") + return data + + +def authenticate(root): + raw = {} + for rel, expected in PINS.items(): + data = (root / rel).read_bytes() + if sha256(data).hexdigest() != expected: + raise ValueError(f"changed dependency: {rel}") + raw[rel] = data + return raw + + +@cache +def coefficient(value): + q = Fraction(value) + if not q or q.denominator % PRIME == 0: + raise ValueError("zero scalar or denominator divisible by modulus") + return q.numerator * pow(q.denominator, -1, PRIME) % PRIME, q.denominator + + +def axpy(target, source, scale): + if scale: + for role, old in source.items(): + current = (target.get(role, 0) + scale * old) % PRIME + if current: + target[role] = current + else: + target.pop(role, None) + + +def scaled(vector, scale): + return {i: y for i, x in vector.items() if (y := x * scale % PRIME)} + + +def verify_minor(vectors, columns): + """Independently recompute a minor on the original projected rows.""" + matrix = [[row.get(c, 0) for c in columns] for row in vectors] + determinant = 1 + for c in range(len(matrix)): + pivot = next((r for r in range(c, len(matrix)) if matrix[r][c]), None) + if pivot is None: + return 0 + if pivot != c: + matrix[c], matrix[pivot] = matrix[pivot], matrix[c] + determinant = -determinant + diag = matrix[c][c] + determinant = determinant * diag % PRIME + inverse = pow(diag, -1, PRIME) + for r in range(c + 1, len(matrix)): + factor = matrix[r][c] * inverse % PRIME + if factor: + for k in range(c + 1, len(matrix)): + matrix[r][k] = (matrix[r][k] - factor * matrix[c][k]) % PRIME + matrix[r][c] = 0 + return determinant % PRIME + + +def classify(bank, vectors, cohort): + full_rows = [vectors[r] for r in bank] + exterior = [{i: x for i, x in row.items() if i not in cohort} for row in full_rows] + basis, kernel = [], [] + determinant = 1 + for index, vector in enumerate(exterior): + work = vector.copy() + combination = {index: 1} + for col, known, combo in basis: + factor = -work.get(col, 0) + axpy(work, known, factor) + axpy(combination, combo, factor) + if not work: + image = {} + for i, factor in combination.items(): + axpy(image, full_rows[i], factor) + assert image.keys() <= cohort + kernel.append(dict(cut={bank[i]: x for i, x in combination.items()}, endpoint=image)) + continue + col = max(work) + pivot = work[col] + determinant = determinant * pivot % PRIME + inverse = pow(pivot, -1, PRIME) + basis.append((col, scaled(work, inverse), scaled(combination, inverse))) + rank = len(basis) + assert rank + len(kernel) == len(bank) + columns = [col for col, _, _ in basis] + if kernel: + return dict(rank=rank, kernel=kernel, minor_axes=None, determinant=None) + assert columns and verify_minor(exterior, columns) == determinant != 0 + return dict(rank=rank, kernel=[], minor_axes=columns, determinant=determinant) + + +def apply(event, state, vectors, fresh, n, denominators, backward): + op, r, *args = event + current = state[r] + if op == "MOVE": + old, new, owned = args + assert owned == (r >= n) + assert current == (new if backward else old) + state[r] = old if backward else new + fresh.discard(r) + return + if op in ("INIT", "CLEAR"): + assert r >= n + c, = args + entering = (op == "CLEAR") if backward else (op == "INIT") + if entering: + assert current is None and vectors[r] is None + state[r], vectors[r] = c, {} + if not backward: + fresh.add(r) + else: + assert current == c and vectors[r] is not None + state[r] = vectors[r] = None + fresh.discard(r) + return + assert op in ("SCALE", "ADD", "COPY") and current == args[-1] and vectors[r] is not None + factor, denominator = coefficient(args[-2]) + denominators.add(denominator) + if op == "SCALE": + vectors[r] = scaled(vectors[r], factor) + else: + src = args[0] + assert src != r and state[src] == current and vectors[src] is not None + if backward: + axpy(vectors[src], vectors[r], factor) + if op == "COPY": + assert r >= n + vectors[r] = {} + elif op == "COPY": + assert r >= n and r in fresh and not vectors[r] + vectors[r] = scaled(vectors[src], factor) + else: + axpy(vectors[r], vectors[src], factor) + fresh.discard(r) + + +def controls(): + assert all(PRIME % i for i in range(2, isqrt(PRIME) + 1)) + witness = classify([0, 1], [{3: 2, 8: 1}, {3: 3, 8: 4}], set()) + assert witness["minor_axes"] == [8, 3] and witness["determinant"] == PRIME - 5 + dropped = classify([0, 1], [{0: 1, 8: 1}, {1: 1, 8: 1}], {0, 1}) + assert dropped["kernel"] == [dict(cut={0: PRIME - 1, 1: 1}, endpoint={0: PRIME - 1, 1: 1})] + tape = [("ADD", 1, 0, "-3/2", 4), ("SCALE", 0, "2", 4), ("INIT", 2, 4), + ("COPY", 2, 1, "1", 4), ("ADD", 0, 2, "5", 4), ("CLEAR", 2, 4)] + result = [] + for backward in (False, True): + state, vectors, fresh, denoms = [4, 4, None], [{0: 1}, {1: 1}, None], set(), set() + for event in reversed(tape) if backward else tape: + apply(event, state, vectors, fresh, 2, denoms, backward) + assert state == [4, 4, None] and not fresh and denoms == {1, 2} + result.append(vectors) + assert result[0] == [{0: coefficient("-11/2")[0], 1: 5}, {0: coefficient("-3/2")[0], 1: 1}, None] + assert result[1] == [{0: coefficient("-11/2")[0], 1: coefficient("-3/2")[0]}, {0: 5, 1: 1}, None] + try: + coefficient("1/65537") + except ValueError: + pass + else: + raise AssertionError("nonunit denominator admitted") + return ["prime and signed nonzero minor", "planted pure kernel", "owned COPY forward and adjoint", + "nonunit denominator rejection"] + + +def span(frame): + vectors = {0} + for v in frame: + assert v not in vectors + vectors |= {v ^ w for w in vectors} + return vectors + + +def sweep(word, keys, cohort, deadline, result, progress, backward, previous=None): + tape, n, owned = (word[k] for k in ("program", "public", "owned_fields")) + assert (len(tape), n, owned) == (EVENTS, 1501, 68) + origin, target = ("final", "initial") if backward else ("initial", "final") + state = word[origin] + [None] * owned + vectors = [{r: 1} for r in range(n)] + [None] * owned + fresh, denoms = set(), set() + request = defaultdict(list) + frames = word["frames"] + low, high = span(frames[3]), span(frames[245]) + for cut, chart in keys: + assert 0 <= cut <= EVENTS and len(frames[chart]) == 4 and low < span(frames[chart]) < high + request[cut].append(chart) + boundaries = range(EVENTS, -1, -1) if backward else range(EVENTS + 1) + progress.update(events=0, first_unvisited_cut=boundaries.start, denominator_units=[]) + for cut in boundaries: + progress["first_unvisited_cut"] = cut + if (cut % 128 == 0 or cut in request) and monotonic() >= deadline: + break + for chart in request.get(cut, []): + key = (cut, chart) + public_bank = [r for r in range(n) if state[r] == chart] + owned_bank = [r for r in range(n, n + owned) if state[r] == chart] + pivots = sorted(set(public_bank) & cohort) + assert public_bank and pivots + if cut: + event = tape[cut - 1] + assert chart in (event[2:4] if event[0] == "MOVE" else event[-1:]) + bank = dict(public=public_bank, owned=owned_bank, pivots=pivots) + if previous is not None: + assert bank == previous[key]["bank"] + result[key] = dict(bank=bank, **classify(public_bank, vectors, cohort)) + if cut == (0 if backward else EVENTS): + assert state == word[target] + [None] * owned and not fresh + assert set(result) == set(keys) + progress["first_unvisited_cut"] = None + break + apply(tape[cut - 1 if backward else cut], state, vectors, fresh, n, denoms, backward) + progress["events"] += 1 + progress["denominator_units"] = sorted(denoms) + + +def pairing(prefix, suffix): + def dot(left, right): + return sum(v * right.get(i, 0) for i, v in left.items()) % PRIME + + return [[dict(cut=dot(a["cut"], b["cut"]), endpoint=dot(a["endpoint"], b["endpoint"])) + for b in suffix["kernel"]] for a in prefix["kernel"]] + + +def main(): + parser = ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=ROOT) + parser.add_argument("--controls-only", action="store_true") + args = parser.parse_args() + assert __debug__ and sys.version_info[:2] == (3, 12) + checks = controls() + if args.controls_only: + print(dumps(checks)) + return + + def stop(*_): + raise TimeoutError("hard 25-second cap") + + start = monotonic() + signal(SIGALRM, stop) + alarm(SECONDS) + timeout = None + keys, prior, prefix, suffix = [], [], {}, {} + prefix_progress, suffix_progress = {}, {} + try: + raw = authenticate(args.root) + price, geom, remaining = [loads(raw[f"inputs/{name}.json"], object_pairs_hook=unique) + for name in ("PRICE", "GEOMETRY", "REMAINING")] + assert price["head"] == geom["head"] == remaining["head"] == HEAD and price["caller"] == CALLER + assert price["word_sha256"] == geom["word_sha256"] == WORD + assert geom["price_sha256"] == PINS["inputs/PRICE.json"] + assert remaining["input_sha256"]["lead/GEOMETRY.json"] == PINS["inputs/GEOMETRY.json"] + assert geom["status"] == "EXHAUSTED" and geom["visited_events"] == EVENTS + keys = list(map(tuple, remaining["unvisited_prefix"])) + prior = remaining["dual_drops_requiring_rational"] + assert len(keys) == len(set(keys)) == remaining["next_modular_cases"] == CASES + assert remaining["next_modular_runner_seconds"] == SECONDS + assert keys == list(map(tuple, geom["unvisited_keys"])) + selected = {tuple(row["key"]) for row in geom["selected"]} + assert len(selected) == 16 and not set(keys) & selected and set(map(tuple, prior)) <= selected + assert set(keys) | selected == set(map(tuple, geom["all_representative_keys"])) + assert prior == [[41740, 242], [45266, 242]] + payload = decompress(raw["inputs/7334-WORD.json.gz"]) + assert sha256(payload).hexdigest() == PAYLOAD + word = loads(payload, object_pairs_hook=unique) + cohort = set(price["cohort"]) + assert len(cohort) == 15 and all((word["initial"][r], word["final"][r]) == (3, 245) for r in cohort) + deadline = start + SECONDS - 2 + sweep(word, keys, cohort, deadline, prefix, prefix_progress, False) + candidates = [key for key in keys if key in prefix and prefix[key]["kernel"]] + if candidates: + sweep(word, candidates, cohort, deadline, suffix, suffix_progress, True, prefix) + else: + suffix_progress.update(events=0, first_unvisited_cut=None, denominator_units=[]) + except TimeoutError as error: + timeout = str(error) + finally: + alarm(0) + + results = [] + for key in keys: + left, right = prefix.get(key), suffix.get(key) + pair = None + if left and not left["kernel"]: + status = "prefix_exclusion" + elif right and not right["kernel"]: + status = "suffix_exclusion" + elif right: + status = "dual_drop" + pair = pairing(left, right) + else: + status = "unvisited" + results.append(dict(key=key, status=status, prefix=left, suffix=right, modular_pairings=pair)) + complete = (timeout is None and prefix_progress.get("first_unvisited_cut", 0) is None + and suffix_progress.get("first_unvisited_cut", 0) is None) + print(dumps(dict(head=HEAD, caller=CALLER, pins=PINS, modulus=PRIME, controls=checks, + cap_cases=CASES, cap_seconds=SECONDS, prefix_progress=prefix_progress, suffix_progress=suffix_progress, + timeout=timeout, complete=complete, results=results, + counts=Counter(row["status"] for row in results), previously_frozen_exact_keys=prior), + indent=2, sort_keys=True)) + if not complete: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-five-chart233-prefix-bound/receipts/AGREEMENT.json b/research/p104-rank-five-chart233-prefix-bound/receipts/AGREEMENT.json new file mode 100644 index 0000000000..1fb6d8277f --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/receipts/AGREEMENT.json @@ -0,0 +1,258 @@ +{ + "banks": 17, + "independent_sha256": "96bdb7a70d247a198a6777fe10e30ce51f7b2e90d4a81f9bf7fea0515f9c1ad0", + "primary_nonzero_axes_at_second_prime": 17, + "primary_sha256": "d00281b59d994fb96e3f60cedc5c6b3b6277a7d050e8ac7bd6b4a24724219669", + "primary_unvisited": [], + "prime": 65537, + "results": [ + { + "axes": [ + 101 + ], + "independent_full": true, + "key": [ + 28620, + 329 + ], + "primary_det": 1, + "primary_det_mod_65537": 1, + "primary_full": true + }, + { + "axes": [ + 19, + 101 + ], + "independent_full": true, + "key": [ + 28621, + 329 + ], + "primary_det": 32761, + "primary_det_mod_65537": 32769, + "primary_full": true + }, + { + "axes": [ + 19, + 101 + ], + "independent_full": true, + "key": [ + 28622, + 329 + ], + "primary_det": 32761, + "primary_det_mod_65537": 32769, + "primary_full": true + }, + { + "axes": [ + 19, + 101 + ], + "independent_full": true, + "key": [ + 28626, + 329 + ], + "primary_det": 32761, + "primary_det_mod_65537": 32769, + "primary_full": true + }, + { + "axes": [ + 19, + 18 + ], + "independent_full": true, + "key": [ + 28632, + 340 + ], + "primary_det": 32761, + "primary_det_mod_65537": 32769, + "primary_full": true + }, + { + "axes": [ + 19, + 18 + ], + "independent_full": true, + "key": [ + 28633, + 340 + ], + "primary_det": 32761, + "primary_det_mod_65537": 32769, + "primary_full": true + }, + { + "axes": [ + 34, + 164 + ], + "independent_full": true, + "key": [ + 34829, + 329 + ], + "primary_det": 57331, + "primary_det_mod_65537": 57345, + "primary_full": true + }, + { + "axes": [ + 164, + 34 + ], + "independent_full": true, + "key": [ + 34830, + 329 + ], + "primary_det": 8190, + "primary_det_mod_65537": 8192, + "primary_full": true + }, + { + "axes": [ + 164, + 34 + ], + "independent_full": true, + "key": [ + 34831, + 329 + ], + "primary_det": 8190, + "primary_det_mod_65537": 8192, + "primary_full": true + }, + { + "axes": [ + 18, + 34 + ], + "independent_full": true, + "key": [ + 34836, + 340 + ], + "primary_det": 49141, + "primary_det_mod_65537": 49153, + "primary_full": true + }, + { + "axes": [ + 18, + 34, + 142 + ], + "independent_full": true, + "key": [ + 34837, + 340 + ], + "primary_det": 61426, + "primary_det_mod_65537": 61441, + "primary_full": true + }, + { + "axes": [ + 18, + 34, + 142 + ], + "independent_full": true, + "key": [ + 34838, + 340 + ], + "primary_det": 61426, + "primary_det_mod_65537": 61441, + "primary_full": true + }, + { + "axes": [ + 18, + 290, + 34, + 142 + ], + "independent_full": true, + "key": [ + 34864, + 340 + ], + "primary_det": 30713, + "primary_det_mod_65537": 63489, + "primary_full": true + }, + { + "axes": [ + 18, + 290, + 34, + 142 + ], + "independent_full": true, + "key": [ + 34865, + 340 + ], + "primary_det": 30713, + "primary_det_mod_65537": 63489, + "primary_full": true + }, + { + "axes": [ + 18, + 290, + 34, + 142 + ], + "independent_full": true, + "key": [ + 34866, + 340 + ], + "primary_det": 30713, + "primary_det_mod_65537": 63489, + "primary_full": true + }, + { + "axes": [ + 18, + 290, + 34 + ], + "independent_full": true, + "key": [ + 34871, + 340 + ], + "primary_det": 57331, + "primary_det_mod_65537": 57345, + "primary_full": true + }, + { + "axes": [ + 18, + 34 + ], + "independent_full": true, + "key": [ + 34875, + 340 + ], + "primary_det": 49141, + "primary_det_mod_65537": 49153, + "primary_full": true + } + ], + "same_full_rank_disposition": 17, + "unresolved_at_second_prime": [] +} diff --git a/research/p104-rank-five-chart233-prefix-bound/receipts/SHA256.json b/research/p104-rank-five-chart233-prefix-bound/receipts/SHA256.json new file mode 100644 index 0000000000..f6da5eb792 --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/receipts/SHA256.json @@ -0,0 +1,6 @@ +{ + "AGREEMENT.json": "e85668ebd96c302102fa23b65f35f0bd1629130d433e1c7fc8d1963111fc853e", + "PRIMARY.json": "d00281b59d994fb96e3f60cedc5c6b3b6277a7d050e8ac7bd6b4a24724219669", + "SECOND.json": "96bdb7a70d247a198a6777fe10e30ce51f7b2e90d4a81f9bf7fea0515f9c1ad0", + "SELECTION.json": "910c8881f31721793cb8e8cbf3b3b3789a9986415e0d48dd9c97d146d5b37bcc" +} diff --git a/research/p104-rank-five-chart233-prefix-bound/replay.py b/research/p104-rank-five-chart233-prefix-bound/replay.py new file mode 100644 index 0000000000..18c357760b --- /dev/null +++ b/research/p104-rank-five-chart233-prefix-bound/replay.py @@ -0,0 +1,176 @@ +"""Replay the exact fixed-paid rank-five chart 3-to-233 prefix exclusions.""" +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 runpy import run_path +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(raw): + return loads(raw,object_pairs_hook=unique) + + +def digest(raw): + return sha256(raw).hexdigest() + + +def relative(name): + path=PurePosixPath(name) + if path.is_absolute() or path.as_posix()!=name or ".." in path.parts: + raise ValueError(f"invalid relative path: {name}") + return path + + +def authenticate(): + pins=decode((ROOT/"LOCAL-PINS.json").read_bytes()) + for name,expected in pins.items(): + if digest((ROOT/relative(name)).read_bytes())!=expected: + raise ValueError(f"changed package dependency: {name}") + provenance=decode((ROOT/"PROVENANCE.json").read_bytes()) + for name,record in provenance["files"].items(): + raw=(ROOT/relative(name)).read_bytes() + assert digest(raw)==record["sha256"]==pins[name] + assert sha1(f"blob {len(raw)}\0".encode()+raw).hexdigest()==record["git_blob"] + inputs={} + for name,record in provenance["derived_gzip"].items(): + raw=decompress((ROOT/"inputs"/f"{name}.json.gz").read_bytes()) + published=decode((ROOT/relative(record["receipt"])).read_bytes()) + assert digest(raw)==published[record["key"]] + inputs[name]=raw + return inputs + + +def command(script,*args,timeout=25,check=True): + response=run([sys.executable,"-I","-B",str(script),*map(str,args)],capture_output=True,timeout=timeout) + if check and response.returncode: + sys.stderr.write(response.stderr.decode(errors="replace")) + response.check_returncode() + return response + + +def verify_price(selection,prior): + readback=decode((ROOT/"inputs/READBACK.json").read_bytes()) + assert readback["head"]==prior["head"]==selection["head"]==HEAD + assert readback["caller_head"]==prior["caller"]==selection["caller"] + assert readback["copies"]==17 and not readback["empty_root_credits"] + assert prior["pins"]["inputs/pricing.py"]==digest((ROOT/"inputs/pricing.py").read_bytes()) + assert prior["pins"]["inputs/READBACK.json"]==digest((ROOT/"inputs/READBACK.json").read_bytes()) + paid,target=(Counter({int(r):n for r,n in readback[k].items()}) for k in ("paid","targets")) + assert (sum(paid.values()),sum(target.values()))==(110519,22461) + old=target.copy() + old.subtract(paid) + delta={int(r):n for r,n in selection["productive_delta"].items()} + assert not selection["paid_delta"] and delta=={2:17,3:17,5:-17} + assert sum(r*v for r,v in old.items())==selection["surplus"]==1424 + assert sum(r*v for r,v in delta.items())==0 + assert selection["productive_one"]==sum(target.values())+sum(delta.values())==22478 + assert selection["unchanged_paid_positions"]==sum(paid.values()) + cost=run_path(str(ROOT/"inputs/pricing.py"))["cost"] + at,probe,moon=map(Fraction,(prior["incumbent"],prior["probe"],selection["fixed_target"])) + one=cost(delta,at) + assert one==tuple(map(Fraction,selection["one_gross"])) and one[0]>0 + assert 2*one[1]==Fraction(selection["two_compatible_upper"]) + assert cost(old,at)[1]+2*one[1]<1 + after=old.copy() + after.update(delta) + assert cost(after,probe)[0]>0 + assert cost(old,moon)[1]+2*cost(delta,moon)[1]==Fraction(selection["fixed_target_complete_upper"])<0 + + +def replay(root,out): + inputs=authenticate() + expected=decode((ROOT/"receipts/SHA256.json").read_bytes()) + outputs={} + for folder in ("inputs","lead","independent/inputs"): + (root/folder).mkdir(parents=True) + for name,target in (("freeze","lead/freeze.py"),("modular","lead/modular.py"), + ("prefix","independent/prefix.py"),("verify_axes","independent/verify_axes.py")): + copyfile(ROOT/"engines"/f"{name}.py",root/target) + for name,raw in inputs.items(): + (root/"inputs"/f"{name}.json").write_bytes(raw) + for name in ("7334-WORD.json.gz","exterior_rank23.py","reverse_engine.py"): + copyfile(ROOT/"inputs"/name,root/"inputs"/name) + for src,dst in (("R115-PRICE.json","PRICE.json"),("R115-GEOMETRY.json","GEOMETRY.json"), + ("7334-WORD.json.gz","7334-WORD.json.gz")): + copyfile(root/"inputs"/src,root/"independent/inputs"/dst) + copyfile(ROOT/"inputs/second_prime.py",root/"independent/inputs/second_prime.py") + + def record(name,result,target=None): + raw=result.stdout + assert digest(raw)==expected[name],("changed receipt",name) + outputs[name]=raw + if target is not None: + target.write_bytes(raw) + return decode(raw) + + selected=record("SELECTION.json",command(root/"lead/freeze.py"),root/"SELECTION.json") + copyfile(root/"SELECTION.json",root/"independent/inputs/SELECTION.json") + verify_price(selected,decode(inputs["R115-PRICE"])) + assert selected["selected_group"]==[3,233] and selected["cohort"]==[289,1052] + assert len(selected["selected"])==17 and len(selected["unselected"])==14 + assert all(not r["owned"] for r in selected["selected"]) + assert {r["key"][1] for r in selected["selected"]}=={329,340} + + p=root/"lead/RESULT.json" + i=root/"independent/RESULT.json" + first=record("PRIMARY.json",command(root/"lead/modular.py"),p) + other=record("SECOND.json",command(root/"independent/prefix.py"),i) + agree=record("AGREEMENT.json",command(root/"independent/verify_axes.py","--primary",p, + "--primary-sha256",expected["PRIMARY.json"],"--independent",i, + "--independent-sha256",expected["SECOND.json"])) + assert outputs["AGREEMENT.json"]==(ROOT/"receipts/AGREEMENT.json").read_bytes() + assert first["prime"]==65521 and other["prime"]==65537 + assert first["counts"]==other["counts"]=={"prefix exclusion":17} + assert first["prefix_events"]==other["progress"]["events"]==76466 + assert len(other["denominator_units"])==98 and not other["unresolved"] + assert agree["banks"]==agree["same_full_rank_disposition"]==agree["primary_nonzero_axes_at_second_prime"]==17 + assert first["unselected"]==selected["unselected"] + assert not agree["primary_unvisited"] and not agree["unresolved_at_second_prime"] + assert {tuple(row[2:]) for row in selected["unselected"]}=={(712,127),(714,127)} + assert all(row["suffix"] is None for row in first["results"]) + + for path,script in (("SELECTION.json","lead/modular.py"),("independent/inputs/SELECTION.json","independent/prefix.py"),("independent/inputs/GEOMETRY.json","independent/prefix.py")): + victim=root/path + raw=victim.read_bytes() + victim.write_bytes(raw+b"\n") + changed=command(root/script,check=False) + assert changed.returncode==1 and not changed.stdout + assert b"changed dependency" in changed.stderr and victim.name.encode() in changed.stderr + victim.write_bytes(raw) + + assert set(outputs)==set(expected) + if out is not None: + out.mkdir(parents=True) + for name,raw in outputs.items(): + (out/relative(name)).write_bytes(raw) + print("PASS_RANK_FIVE_CHART233_PREFIX_BOUND banks=17 primary=17 second=17 unresolved=0 other_cohorts=14") + + +def main(): + assert __debug__ and sys.version_info[:2]==(3,12) + p=ArgumentParser(description=__doc__) + p.add_argument("--out",type=Path,help="new directory for the four regenerated receipts") + args=p.parse_args() + with TemporaryDirectory() as tmp: + replay(Path(tmp),args.out) + + +if __name__=="__main__": + main()