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-chart238-prefix-bound/LOCAL-PINS.json b/research/p104-rank-five-chart238-prefix-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..375eadd08a --- /dev/null +++ b/research/p104-rank-five-chart238-prefix-bound/LOCAL-PINS.json @@ -0,0 +1,19 @@ +{ + "PROVENANCE.json": "c1faf8946d6065b76979f54080cf6cddf0d751fd4391fc2631c2590399ea1828", + "engines/freeze.py": "84745fc47e460b50e4ba845654ef08ceb8d3773e6b02364fa4a3320574227b46", + "engines/modular.py": "55e5bd81576d7792293b9af84874c63a3896815754775d89cdfde0fde684bba4", + "engines/prefix.py": "c73436f0ec3801186a838fbe7775097494255806825c0965a5069aebea9d1a8b", + "engines/verify_axes.py": "cdc0309980d9a5cad557e1641a34628b4dc9f390ce4a9e352a8451115b6d01c5", + "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": "6d11211dd631cf41a7c5f2c5da5cbe30c8dc4e9a11cc5e31f6cc173c4e11ac3a", + "receipts/SHA256.json": "6f9615c7563d88279f39e0c5d936ec839e3102f6c83fe956b6f22be256741ae5", + "replay.py": "6cbaf4346ddaeb7d71b613addc85487634a5c3eb947fde5bb686b702455ef9b4" +} diff --git a/research/p104-rank-five-chart238-prefix-bound/NOTICE b/research/p104-rank-five-chart238-prefix-bound/NOTICE new file mode 100644 index 0000000000..981c527ea4 --- /dev/null +++ b/research/p104-rank-five-chart238-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-chart238-prefix-bound/PROOF.md b/research/p104-rank-five-chart238-prefix-bound/PROOF.md new file mode 100644 index 0000000000..92e673e9b5 --- /dev/null +++ b/research/p104-rank-five-chart238-prefix-bound/PROOF.md @@ -0,0 +1,63 @@ +# Fixed-paid chart 3→238 rank-five split + +The exact #7370 geometry exhausts all 76,466 events for 80 eligible +rank-five helpers in 28 endpoint cohorts. Its completed support +group is chart 3→241. The inherited manifest pins the full +catalogue and leaves chart 3→238 entirely outside that support +scope. This continuation selects the whole exact chart 3→238 +group, roles 325 and 1087. The source and target chart ranks are +zero and five. A productive 2+3 or 3+2 split uses a strict existing +rank-two or rank-three intermediate chart. Every selected bank +is owned-empty. + +| Productive pivot | Intermediate chart | Literal pre-event clocks | +|---:|---:|---| +| 325 | 370 | 28279, 28280, 28281, 28282 | +| 325 | 375 | 28284, 28285 | +| 1087 | 370 | 32029, 32030, 32032 | +| 1087 | 375 | 32033, 32034, 32035, 32036, 32037, 32038, 33040, 34653, 34658 | + +A cut c is the state after exactly c literal events. Let P be +the normalized prefix-row matrix of the public roles live in +the intermediate chart at the cut. Let E project onto original +input coordinates outside the productive cohort. A nonzero +pure prefix would require some nonzero row a with aPE = 0. +A nonzero full-row-rank minor of PE excludes that necessary +condition. + +The forward modular engines reconstruct each exact bank, including +all scalar signs, public and owned occupancy, and pivot roles. +Both walks visit all 76,466 literal events under 25-second caps. +Every scalar denominator used in the exact rational projection is +a unit at the replay prime. The independent run observes 98 distinct +denominators. It computes independent full minors at 65537 and +re-evaluates the original 65521 column sets on the independently +reconstructed exterior rows. All 18 original column sets remain +nonzero. In either prime a nonzero modular determinant certifies +a nonzero rational minor because the reduced denominators are units. + +All 18 selected cuts fail the necessary prefix test. No transfer +assumption is used for repeated banks. The 31 other representatives +remain outside this continuation. Suffix, exact unit pairing and +signed construction were skipped after the complete prefix result. + +## Complete price + +The 17-copy paid histogram stays fixed at 110,519 positions. +One productive split changes the full target histogram by +{2:+17, 3:+17, 5:−17}, raising the productive count from 22,461 +to 22,478 and conserving the signed rank surplus of 1,424. +The independent replay recomputes the directed #7298 tariff +from the complete #7338 paid/target readback. One edit has +upper credit 0.207666506667591 raw at the previous crossing +upper. The compatible two-role ceiling is 0.415333013335181. +The complete fixed-target upper at κ = 0.0040075385047236 +is about −139.310694990954. One additional raw paid rank-one +position exceeds the two-role envelope. These are price +ceilings before ancillary work, and the tested banks yield +zero verified saving. + +The same native all-column, owned-erasure, compiler, +precision/tape and analytic recovery premises are retained. +A different physical route would require fresh signed proof, +complete accounting and independent caller replay. diff --git a/research/p104-rank-five-chart238-prefix-bound/PROVENANCE.json b/research/p104-rank-five-chart238-prefix-bound/PROVENANCE.json new file mode 100644 index 0000000000..35addfaac5 --- /dev/null +++ b/research/p104-rank-five-chart238-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-chart238-prefix-bound/README.md b/research/p104-rank-five-chart238-prefix-bound/README.md new file mode 100644 index 0000000000..8bee1b4c40 --- /dev/null +++ b/research/p104-rank-five-chart238-prefix-bound/README.md @@ -0,0 +1,73 @@ +# Fixed-paid rank-five prefix bounds on chart 3→238 + +**NO VERIFIED GAIN.** Exact Δκ = 0 relative to independently +reproduced conditional κ = `0.00364665195644` on +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) +`aaeec8c0acf01e99a5f331ef363a698d9c084ace`, with signed +[#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +`07a76c5e2738882c0cb322278e56f6cae3c9885d`. + +A fixed-paid 2+3 or 3+2 split would replace one rank-five +productive target of the chart 3→238 cohort, roles 325 and 1087. +This exhausts the 18 frozen public banks on intermediate charts +370 and 375 that [#7370](https://github.com/CrocSwap/integer-mult-bounds/pull/7370) +left outside its support scope. Both exact prime-field engines +exclude all 18 by full exterior prefix rank. Every primary +minor's coordinate set also gives a nonzero determinant at the +independent prime. No selected bank remains unresolved. +The other 31 representatives from #7370's outside-support list +are still outside this test. +[Exact per-key agreement](receipts/AGREEMENT.json). + +The directed one-edit upper is about 0.207666506667591 raw. +The optimistic two-role upper is about 0.415333013335181. +All 110,519 paid positions stay fixed. [Proof and complete price](PROOF.md). + +## Replay + +From a clean checkout, use CPython 3.12 with assertions: + +```sh +python3.12 -I -B research/p104-rank-five-chart238-prefix-bound/replay.py +``` + +The standard-library replay authenticates the exact #7370 +manifest, price, geometry, and #7334 word. It recomputes the +directed price with the exact tariff, freezes all 18 keys, +replays both primes and checks the primary minor coordinates +at the independent prime. Altered selection and geometry +inputs reject. Use `--out fresh-directory` to retain all four +receipts. No Git metadata, network, external root or prior +temporary state is needed. +[Provenance](PROVENANCE.json) · [Path-keyed pins](LOCAL-PINS.json). + +## Open next questions + +Can a different fixed-paid rank-five cohort supply two-sided +support? The #7370 geometry lists 17 representatives for +chart 3→233, roles 289 and 1052. Freeze that one group and price +its complete invoice before a bounded prefix/suffix replay. +This contribution tests only chart 3→238. + +## Credit + +[#7370](https://github.com/CrocSwap/integer-mult-bounds/pull/7370) +at `a41edc3ae92332a7a1f1ba90e9ea4901d0530185` supplies the exact +geometry and directed productive split stock. +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) +and [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +supply the exact native word and signed caller. +[#7338](https://github.com/CrocSwap/integer-mult-bounds/pull/7338) +supplies the admitted full invoice, and +[#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) +the rational directed tariff. +[#7319](https://github.com/CrocSwap/integer-mult-bounds/pull/7319) +supplies the inherited exact helper census. +[#5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599) +supplies the common-frame split method, +[#7367](https://github.com/CrocSwap/integer-mult-bounds/pull/7367) +the same-word exterior proof method on another cohort, and +[#5994](https://github.com/CrocSwap/integer-mult-bounds/pull/5994) +the earlier broad census on a different word. OpenAI Codex and +subagents materially assisted proof, implementation, independent +verification and packaging. diff --git a/research/p104-rank-five-chart238-prefix-bound/SOURCES.json b/research/p104-rank-five-chart238-prefix-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-rank-five-chart238-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-chart238-prefix-bound/TASK.json b/research/p104-rank-five-chart238-prefix-bound/TASK.json new file mode 100644 index 0000000000..1a19d2a031 --- /dev/null +++ b/research/p104-rank-five-chart238-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 325 and 1087 in the exact 18 chart 3\u2192238 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-238 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 18 owner-empty banks on charts 370 and 375. Every original prime-field minor coordinate set remains nonzero at the independent prime. Thirty-one other representatives remain outside scope.", + "open_questions": [ + { + "blocked_by": "All exact 3\u2192238 public banks fail the prefix gate.", + "first_step": "Freeze the 17 #7370 chart 3\u2192233 bank representatives and price its complete invoice 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\u2192238 rank-five group left untouched by the #7370 catalogue and first support group.", + "scope_status": "changed", + "stop_rule": "Freeze the exact 18 keys from #7370, then 76,466 events per prime and 25 seconds per gate. Skip suffix and signed construction after a full prefix exclusion.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-rank-five-chart238-prefix-bound/VERIFICATION.md b/research/p104-rank-five-chart238-prefix-bound/VERIFICATION.md new file mode 100644 index 0000000000..4b3eddf588 --- /dev/null +++ b/research/p104-rank-five-chart238-prefix-bound/VERIFICATION.md @@ -0,0 +1,18 @@ +# Verification + +The direct CPython 3.12 package replay completed in 2.61 seconds +with exit 0. A relocated Git-free copy with an empty inherited +environment completed in 2.37 seconds with exit 0 and reproduced +all four receipt files byte-for-byte. Altered selection and +geometry inputs each returned exit 1. + +The two modular checks each exhaust the 76,466-event tape and +all 18 selected banks. Both primes give full exterior prefix +rank at every key. The independent row walk and determinant +check certify all original minor coordinate sets at the second +prime. Suffix and physical work were skipped after the scoped +prefix exclusion. The other 31 keys were outside this replay. + +The exact inputs, checkout-relative command and receipt hashes +are in [PROVENANCE.json](PROVENANCE.json), [README.md](README.md) +and [receipts/SHA256.json](receipts/SHA256.json). diff --git a/research/p104-rank-five-chart238-prefix-bound/VERIFY.json b/research/p104-rank-five-chart238-prefix-bound/VERIFY.json new file mode 100644 index 0000000000..0c421f6ccd --- /dev/null +++ b/research/p104-rank-five-chart238-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 18 prefix minors at both primes including primary axes, and reject changed inputs.", + "timeout_seconds": 100 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-rank-five-chart238-prefix-bound/engines/freeze.py b/research/p104-rank-five-chart238-prefix-bound/engines/freeze.py new file mode 100644 index 0000000000..6790b21cdf --- /dev/null +++ b/research/p104-rank-five-chart238-prefix-bound/engines/freeze.py @@ -0,0 +1,60 @@ +"""Select and price the untouched rank-five 3-to-238 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, 238] + cohort = next(g["roles"] for g in price["groups"] if g["endpoints"] == group) + assert cohort == [325, 1087] 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}) == 18 + assert all(r["pivots"] and not r["owned"] for r in rows) + assert {r["key"][1] for r in rows} == {370, 375} + 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])], + "caps": {"representatives": 18, "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-chart238-prefix-bound/engines/modular.py b/research/p104-rank-five-chart238-prefix-bound/engines/modular.py new file mode 100644 index 0000000000..e4e99bc1d3 --- /dev/null +++ b/research/p104-rank-five-chart238-prefix-bound/engines/modular.py @@ -0,0 +1,102 @@ +"""Reconstruct two-sided exterior minors for 18 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":"dd92991605306ba552a4be714fbaf0eb70b4120d4bd2f4ba9cce473e13665796", + "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=={325,1087}==set(selection["cohort"]) + rows=selection["selected"] + assert len(rows)==18 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-chart238-prefix-bound/engines/prefix.py b/research/p104-rank-five-chart238-prefix-bound/engines/prefix.py new file mode 100644 index 0000000000..42fcf7c98a --- /dev/null +++ b/research/p104-rank-five-chart238-prefix-bound/engines/prefix.py @@ -0,0 +1,150 @@ +"""Check the 18 frozen rank-five 3→238 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/GEOMETRY.json": "c2a4406cf7130a819189e8ceefb4bb6e09edd392eb56820f9fcadb0e9415ef4e", + "inputs/PRICE.json": "c04adfb199f6dbc25806d6062562c7d707b8fda8ad73f3ed818901248d25ffbf", + "inputs/second_prime.py": "21dbd96192e1f60c00ceddba01a7e8d0ddd7d6ad7da4ad3ed22ef2e47cc589c4", + "inputs/7334-WORD.json.gz": WORD, +} +GROUP = [3, 238] +COHORT = {325, 1087} +EVENTS, CASES, SECONDS, PRIME = 76466, 18, 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): + 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"] == HEAD and price["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 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 len(chosen) == CASES + 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-chart238-prefix-bound/engines/verify_axes.py b/research/p104-rank-five-chart238-prefix-bound/engines/verify_axes.py new file mode 100644 index 0000000000..89626024db --- /dev/null +++ b/research/p104-rank-five-chart238-prefix-bound/engines/verify_axes.py @@ -0,0 +1,62 @@ +"""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" + + +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"] + by_key = {tuple(row["key"][:2]): row for row in primary["results"]} + assert len(by_key) == len(primary["results"]) == len(independent["rows"]) == 18 + results = [] + for row in independent["rows"]: + item = by_key[tuple(row["key"])] + receipt = item.get("prefix", item) + for field in ("public", "owned", "pivots"): + assert row[field] == (receipt[field] if field in receipt else item[field]) + n = len(row["public"]) + assert receipt["exterior_rank"] <= n + primary_full = receipt["exterior_rank"] == n + second_full = row["disposition"] == "prefix exclusion" + columns = 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=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), results=results), + indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-five-chart238-prefix-bound/inputs/7334-WORD.json.gz b/research/p104-rank-five-chart238-prefix-bound/inputs/7334-WORD.json.gz new file mode 100644 index 0000000000..73f4300719 Binary files /dev/null and b/research/p104-rank-five-chart238-prefix-bound/inputs/7334-WORD.json.gz differ diff --git a/research/p104-rank-five-chart238-prefix-bound/inputs/PR7370-SHA256.json b/research/p104-rank-five-chart238-prefix-bound/inputs/PR7370-SHA256.json new file mode 100644 index 0000000000..695c7c46ca --- /dev/null +++ b/research/p104-rank-five-chart238-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-chart238-prefix-bound/inputs/R115-GEOMETRY.json.gz b/research/p104-rank-five-chart238-prefix-bound/inputs/R115-GEOMETRY.json.gz new file mode 100644 index 0000000000..386bd61611 Binary files /dev/null and b/research/p104-rank-five-chart238-prefix-bound/inputs/R115-GEOMETRY.json.gz differ diff --git a/research/p104-rank-five-chart238-prefix-bound/inputs/R115-PRICE.json.gz b/research/p104-rank-five-chart238-prefix-bound/inputs/R115-PRICE.json.gz new file mode 100644 index 0000000000..8e7559e3e6 Binary files /dev/null and b/research/p104-rank-five-chart238-prefix-bound/inputs/R115-PRICE.json.gz differ diff --git a/research/p104-rank-five-chart238-prefix-bound/inputs/READBACK.json b/research/p104-rank-five-chart238-prefix-bound/inputs/READBACK.json new file mode 100644 index 0000000000..625b508eea --- /dev/null +++ b/research/p104-rank-five-chart238-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-chart238-prefix-bound/inputs/exterior_rank23.py b/research/p104-rank-five-chart238-prefix-bound/inputs/exterior_rank23.py new file mode 100644 index 0000000000..01e69f343b --- /dev/null +++ b/research/p104-rank-five-chart238-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-chart238-prefix-bound/inputs/pricing.py b/research/p104-rank-five-chart238-prefix-bound/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-rank-five-chart238-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-chart238-prefix-bound/inputs/reverse_engine.py b/research/p104-rank-five-chart238-prefix-bound/inputs/reverse_engine.py new file mode 100644 index 0000000000..ebfc82f83f --- /dev/null +++ b/research/p104-rank-five-chart238-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-chart238-prefix-bound/inputs/second_prime.py b/research/p104-rank-five-chart238-prefix-bound/inputs/second_prime.py new file mode 100644 index 0000000000..0be5407fe6 --- /dev/null +++ b/research/p104-rank-five-chart238-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-chart238-prefix-bound/receipts/AGREEMENT.json b/research/p104-rank-five-chart238-prefix-bound/receipts/AGREEMENT.json new file mode 100644 index 0000000000..088e9edf98 --- /dev/null +++ b/research/p104-rank-five-chart238-prefix-bound/receipts/AGREEMENT.json @@ -0,0 +1,269 @@ +{ + "banks": 18, + "independent_sha256": "5f6fd88e30576a90f80176aa7d0164817e5bc16732b50a9f4efd4b5c1779ab7e", + "primary_nonzero_axes_at_second_prime": 18, + "primary_sha256": "08bc106e8d16204a1ce4be0461bc4ef8b0689305fa6c1288c1a3dd07c3988b54", + "prime": 65537, + "results": [ + { + "axes": [ + 34 + ], + "independent_full": true, + "key": [ + 28279, + 370 + ], + "primary_det": 1, + "primary_det_mod_65537": 1, + "primary_full": true + }, + { + "axes": [ + 34, + 23 + ], + "independent_full": true, + "key": [ + 28280, + 370 + ], + "primary_det": 1, + "primary_det_mod_65537": 1, + "primary_full": true + }, + { + "axes": [ + 23, + 34 + ], + "independent_full": true, + "key": [ + 28281, + 370 + ], + "primary_det": 65520, + "primary_det_mod_65537": 65536, + "primary_full": true + }, + { + "axes": [ + 23, + 34 + ], + "independent_full": true, + "key": [ + 28282, + 370 + ], + "primary_det": 65520, + "primary_det_mod_65537": 65536, + "primary_full": true + }, + { + "axes": [ + 23, + 33 + ], + "independent_full": true, + "key": [ + 28284, + 375 + ], + "primary_det": 1, + "primary_det_mod_65537": 1, + "primary_full": true + }, + { + "axes": [ + 23, + 33 + ], + "independent_full": true, + "key": [ + 28285, + 375 + ], + "primary_det": 1, + "primary_det_mod_65537": 1, + "primary_full": true + }, + { + "axes": [ + 34, + 895 + ], + "independent_full": true, + "key": [ + 32029, + 370 + ], + "primary_det": 16380, + "primary_det_mod_65537": 16384, + "primary_full": true + }, + { + "axes": [ + 34, + 895 + ], + "independent_full": true, + "key": [ + 32030, + 370 + ], + "primary_det": 16380, + "primary_det_mod_65537": 16384, + "primary_full": true + }, + { + "axes": [ + 34, + 895 + ], + "independent_full": true, + "key": [ + 32032, + 370 + ], + "primary_det": 16380, + "primary_det_mod_65537": 16384, + "primary_full": true + }, + { + "axes": [ + 23, + 34 + ], + "independent_full": true, + "key": [ + 32033, + 375 + ], + "primary_det": 16380, + "primary_det_mod_65537": 16384, + "primary_full": true + }, + { + "axes": [ + 23, + 34, + 129 + ], + "independent_full": true, + "key": [ + 32034, + 375 + ], + "primary_det": 61426, + "primary_det_mod_65537": 61441, + "primary_full": true + }, + { + "axes": [ + 23, + 34, + 129 + ], + "independent_full": true, + "key": [ + 32035, + 375 + ], + "primary_det": 61426, + "primary_det_mod_65537": 61441, + "primary_full": true + }, + { + "axes": [ + 23, + 129, + 34, + 286 + ], + "independent_full": true, + "key": [ + 32036, + 375 + ], + "primary_det": 34808, + "primary_det_mod_65537": 2048, + "primary_full": true + }, + { + "axes": [ + 23, + 129, + 34, + 286 + ], + "independent_full": true, + "key": [ + 32037, + 375 + ], + "primary_det": 34808, + "primary_det_mod_65537": 2048, + "primary_full": true + }, + { + "axes": [ + 23, + 129, + 34, + 286 + ], + "independent_full": true, + "key": [ + 32038, + 375 + ], + "primary_det": 34808, + "primary_det_mod_65537": 2048, + "primary_full": true + }, + { + "axes": [ + 23, + 34, + 286 + ], + "independent_full": true, + "key": [ + 33040, + 375 + ], + "primary_det": 57331, + "primary_det_mod_65537": 57345, + "primary_full": true + }, + { + "axes": [ + 23, + 34 + ], + "independent_full": true, + "key": [ + 34653, + 375 + ], + "primary_det": 16380, + "primary_det_mod_65537": 16384, + "primary_full": true + }, + { + "axes": [ + 34 + ], + "independent_full": true, + "key": [ + 34658, + 375 + ], + "primary_det": 16380, + "primary_det_mod_65537": 16384, + "primary_full": true + } + ], + "same_full_rank_disposition": 18 +} diff --git a/research/p104-rank-five-chart238-prefix-bound/receipts/SHA256.json b/research/p104-rank-five-chart238-prefix-bound/receipts/SHA256.json new file mode 100644 index 0000000000..b9562dcf8e --- /dev/null +++ b/research/p104-rank-five-chart238-prefix-bound/receipts/SHA256.json @@ -0,0 +1,6 @@ +{ + "AGREEMENT.json": "6d11211dd631cf41a7c5f2c5da5cbe30c8dc4e9a11cc5e31f6cc173c4e11ac3a", + "PRIMARY.json": "08bc106e8d16204a1ce4be0461bc4ef8b0689305fa6c1288c1a3dd07c3988b54", + "SECOND.json": "5f6fd88e30576a90f80176aa7d0164817e5bc16732b50a9f4efd4b5c1779ab7e", + "SELECTION.json": "dd92991605306ba552a4be714fbaf0eb70b4120d4bd2f4ba9cce473e13665796" +} diff --git a/research/p104-rank-five-chart238-prefix-bound/replay.py b/research/p104-rank-five-chart238-prefix-bound/replay.py new file mode 100644 index 0000000000..9eccb77bf3 --- /dev/null +++ b/research/p104-rank-five-chart238-prefix-bound/replay.py @@ -0,0 +1,173 @@ +"""Replay the exact fixed-paid rank-five chart 3-to-238 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") + verify_price(selected,decode(inputs["R115-PRICE"])) + assert selected["selected_group"]==[3,238] and selected["cohort"]==[325,1087] + assert len(selected["selected"])==18 and len(selected["unselected"])==31 + assert all(not r["owned"] for r in selected["selected"]) + assert {r["key"][1] for r in selected["selected"]}=={370,375} + + 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":18} + 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"]==18 + assert first["unselected"]==selected["unselected"] + assert all(row["suffix"] is None for row in first["results"]) + + for path,script in (("SELECTION.json","lead/modular.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_CHART238_PREFIX_BOUND banks=18 primary=18 second=18 unresolved=0 other_cohorts=31") + + +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()