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-singleton-helper-split-bound/CONTINUATION.json b/research/p104-singleton-helper-split-bound/CONTINUATION.json new file mode 100644 index 0000000000..18ffac5e68 --- /dev/null +++ b/research/p104-singleton-helper-split-bound/CONTINUATION.json @@ -0,0 +1,21 @@ +{ + "counts": { + "prefix_projection_pass": 74 + }, + "head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "helpers": 1101, + "prime": 2305843009213693951, + "projection_survivors": 0, + "public": 1501, + "representative_cuts": 11489, + "seconds": 1, + "seed": 7277, + "selected_cuts": 11489, + "selected_signatures": 1396, + "signature_cap": 1396, + "signatures": 1396, + "tested": [], + "unresolved_exact": 0, + "unvisited_signatures": [], + "word_sha256": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756" +} diff --git a/research/p104-singleton-helper-split-bound/NOTICE b/research/p104-singleton-helper-split-bound/NOTICE new file mode 100644 index 0000000000..ac4fbafd29 --- /dev/null +++ b/research/p104-singleton-helper-split-bound/NOTICE @@ -0,0 +1,5 @@ +Apache-2.0. +Exact literal complex word retained from #7277. The signed caller +context is from #7113. PROVENANCE.json records public source identity. +OpenAI Codex and subagents materially assisted the research, proof, +independent validation and packaging. diff --git a/research/p104-singleton-helper-split-bound/PROVENANCE.json b/research/p104-singleton-helper-split-bound/PROVENANCE.json new file mode 100644 index 0000000000..6fa9d287c3 --- /dev/null +++ b/research/p104-singleton-helper-split-bound/PROVENANCE.json @@ -0,0 +1,53 @@ +{ + "inputs": { + "inputs/WORD.json.gz": { + "commit": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "git_blob": "077bf48c35db0ddafae81f1bfa0ffacc30894b2b", + "path": "research/p104-terminal-cut-rechart/WORD.json.gz", + "sha256": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/WORD.json.gz" + } + }, + "scope_sources": [ + { + "commit": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "pr": "#7277", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/7277" + }, + { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "pr": "#7113", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/7113" + }, + { + "commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "pr": "#5599", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5599" + }, + { + "commit": "02685c603861ca2e23ce30f82d07d7c558b05957", + "pr": "#5702", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5702" + }, + { + "commit": "a1534ac45401c9a9c80c07aa65c89e00e33594f8", + "pr": "#5718", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5718" + }, + { + "commit": "1670baa28f5a9631286591068d7cc2934d2c2d37", + "pr": "#7121", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/7121" + }, + { + "commit": "161e482bc2d8c78ecef96135430c60d49b8fc345", + "pr": "#7130", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/7130" + }, + { + "commit": "bfcb85c0b7298392607092f751df4a7b1afb60c6", + "pr": "#7299", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/7299" + } + ] +} diff --git a/research/p104-singleton-helper-split-bound/README.md b/research/p104-singleton-helper-split-bound/README.md new file mode 100644 index 0000000000..3d407fbfb6 --- /dev/null +++ b/research/p104-singleton-helper-split-bound/README.md @@ -0,0 +1,128 @@ +# Exclude fixed-word singleton P104 helper splits + +**NO VERIFIED GAIN. Conditional κ change 0%.** The complete comparable +benchmark remains κ = 0.003645669928698 on #7277. The current selected +record, retained callers, and paid profile are unchanged. + +The literal source is #7277 at ed090b57ed88f8859e5ff4643645099e6ba856ea. +Its complete signed caller is #7113 at 07a76c5e2738882c0cb322278e56f6cae3c9885d. +A productive split changes the target histogram T. The fixed-packing relaxation +retained by #7277 fixes T, all 17 native paid words and the rank mass of the +remainder with ambient cap 145. Its upper crossing does not cover this change. + +## Price gate + +Write H(r)=r^(1−κ). Any one two-way split with ranks a,b>0 and a+b=r≤9 has +gross gain H(a)+H(b)−H(r) ≤ H(r)(2^κ−1) by concavity. Since log 2<1 and +e^x ≤ 1/(1−x) for 0≤x<1, all 17 copies together gain at most +153κ/(1−κ) ≤ 153/199 < 1 for 0≤κ≤1/200. This includes the incumbent +crossing and fixed moonshot probe. One additional positive integral-rank +child in the complete invoice costs at least 1. Hence a one-split change +with a new paid child and no paid removals cannot improve the signed moment. +This grants every new ordinary operation, access, routing and restoration +for free in the optimistic upper. Credit #5702 and #7299 for related +refinement-fee and balanced-split bounds. + +## Exact support condition + +Fix a helper h and a clock with strict chart inclusions U < F < V. +Let P be the literal scalar prefix and S its literal suffix. A singleton +split with only endpoint rescalings needs nonzero λ such that + + e_h^T P = λ e_h^T, S e_h = λ^(-1) e_h. + +The left identity is on independent public inputs. The right identity +covers every public output and retained owned scalar endpoint. The old +complete operator already fixes the helper input column and output row. +Start h with λ^(-1) x_h, retire it with x_h at F, and replace every +suffix reference to h with a fresh arbitrary independent public input z +starting at F. The suffix changes by S e_h (z−x_h). A final λ scaling +of its successor returns z. Other outputs are unchanged. Thus an admitted +case replaces a U→V target by two independent U→F and F→V targets while +keeping every literal MOVE. Both scale factors need the inherited finite +alphabet and compiler checks. This is the singleton case of the general +cocharted basis identity of #5599. #7121 and #7130 provide exact successor +constructors on the #7113 lineage; #5718 permits different input and output +basis corrections and is wider than the present scope. + +The scalar proof does not establish signed physical action, all-width +phase, dirty ownership and restoration, or the complete new caller and +compiler invoice. These would be mandatory before a κ claim. Merely +dividing one rank into two numbers supplies no new independent field. + +## Finite screen + +For each h, inspect the clock after every literal contact of h for which +its chart is strictly intermediate. Between these representatives the +chart and prefix row do not change. When a skipped event touches only +other roles, it acts identically on the input vector e_h to the suffix, +so the suffix column does not change either. Before the first contact the +chart equals U and cannot be a strict intermediate. A MOVE changes the +physical chart and is retained as a contact. INIT and CLEAR have their +literal owned scalar meaning. + +The screen uses deterministic vectors x and y over the prime field +q=2305843009213693951, seed 7277. The exact identities imply that the +modular values from public all-ones and x satisfy P_h(x)=x_h P_h(1), +and that P_h(1) (S^T y)_h = y_h. Every literal coefficient has +denominator invertible modulo q. Thus an unequal residue is a definitive +rejection of the exact identity. Equal residues can collide and are +confirmed over the rationals. This use of projections has no probabilistic +assumption in any exclusion. Allowing arbitrary endpoint rational λ makes +the negative result at least as strong as restricting to admissible units. + +The first 128-triple cap left 1,268 triples unvisited. The bounded +continuation below exhausted the entire declared scope. Basis changes, +retiming, changed charts, endpoint corrections using other roles, and +simultaneous splits are outside this scope. + +## Exhausted continuation and independent verification + +A separate one-second bounded continuation exhausted all 1,396 triples +and 11,489 representative cuts in 0.13 s wall. The 74 prefix projection +matches all failed the suffix projection. No signature, exact case, or +site remains inside the singleton scope. + +A separate verifier reconstructs the same support geometry by binary +echelon, uses a different prime and probe, and then checks both scalar +conditions over the rationals for every one of its 74 projection +survivors. Each has a valid scalar prefix row and fails the exact suffix +identity. The independent proof needs only one mismatched projection +to reject the other cuts. The toy controls include a reciprocal +rescale and two contaminated cuts. One contaminated cut retains an +identity whole-word scalar operator, demonstrating that a pure prefix +alone cannot prove an independent split. + +## Reproduction + +From a clean checkout using CPython 3.12 with assertions enabled: + + python3.12 -B scripts/research_package.py --package research/p104-singleton-helper-split-bound + python3.12 -B scripts/check_research_commit.py --package research/p104-singleton-helper-split-bound --check-modes --check-source-history + +The package is self-contained. Its Git-free replay command from the +export root is: + + python3.12 -I -B research/p104-singleton-helper-split-bound/replay.py + +The exact original word is bundled byte for byte. PROVENANCE.json +records the public source path, exact #7277 commit, SHA-256 and Git +blob. The wrapper compares the complete deterministic continuation +and rational verifier with frozen receipts, checks the exact tariff +bound and rejects duplicate JSON keys and a mutated source word. +No Git process, temporary pointer, network or machine-specific root +is required. The replay does not build a new physical supplier. + +## Open next questions + +The next larger scope allows a cocharted middle basis or a distinct +boundary correction. Its exact prefix and suffix support should be +checked jointly before materializing a candidate. The scalar exclusion +and price lemma support a pivot. Neither changes the conditional κ. +Material AI assistance by OpenAI Codex. + +#7110/#7112 provide earlier zero-new-MOVE cocharted constructions. +#7175 bounds free refinement on older #7000, and #7299 supplies +generic rank-dependent fees. #7142 moves an input boundary and +increases productive rank mass while charging a new H1. Its changed +rank mass is outside the price lemma here. diff --git a/research/p104-singleton-helper-split-bound/RESULT.json b/research/p104-singleton-helper-split-bound/RESULT.json new file mode 100644 index 0000000000..9969a4e545 --- /dev/null +++ b/research/p104-singleton-helper-split-bound/RESULT.json @@ -0,0 +1,32 @@ +{ + "controls": [ + "REJECT_DUPLICATE_MANIFEST_KEYS", + "REJECT_CHANGED_WORD" + ], + "singleton": { + "controls": [ + "UNIT_RECIPROCAL_POSITIVE", + "SUFFIX_CONTAMINATION_REJECTED", + "PREFIX_CONTAMINATION_REJECTED" + ], + "dependencies": { + "CONTINUATION.json": "d72b12f4b5c24e9d64d6a267dd63baab4bccfd08ebc1ec3b2e7abff762d21eda", + "inputs/WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756" + }, + "different_prime": 1000000007, + "rational_checks": 74, + "rational_reject_prefix": 0, + "rational_reject_suffix": 74, + "representatives": 11489, + "signatures": 1396, + "status": "PASS_FIXED_WORD_SINGLETON_EXCLUSION" + }, + "status": "PASS_FIXED_WORD_SINGLETON_SPLIT_BOUND", + "tariff": { + "copies": 17, + "gross_upper": "153/199", + "kappa_upper": "1/200", + "positive_paid_child_lower": 1, + "rank_upper": 9 + } +} diff --git a/research/p104-singleton-helper-split-bound/SOURCES.json b/research/p104-singleton-helper-split-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-singleton-helper-split-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-singleton-helper-split-bound/TASK.json b/research/p104-singleton-helper-split-bound/TASK.json new file mode 100644 index 0000000000..4562fdb501 --- /dev/null +++ b/research/p104-singleton-helper-split-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Exact #7277 fixed-word singleton helper splits at every strict existing intermediate chart, allowing endpoint rescalings only, plus a uniform paid-child tariff bound for one fixed-mass split.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent audit and packaging.", + "author": "Round 36 research campaign", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Tests whether one exact productive helper split can raise the incumbent complete signed invoice without adding an unaffordable recursive child.", + "budget_minutes": 1, + "evidence": "Exact pinned literal word, deterministic modular exclusions, independent rational rejection of every one of 74 prefix projection survivors, reciprocal-rescale and contamination controls, and exact 153/199 upper against one full-invoice paid child.", + "open_questions": [ + { + "blocked_by": "A survivor needs exact input/output support, native signed phase, returned ownership, restoration and the complete caller and compiler invoice.", + "first_step": "On the same exact word, test paired prefix and suffix subspaces at one bounded cocharted helper group. Price any additional recursive debit before materializing a word.", + "question": "Can a cocharted middle basis or distinct endpoint correction give a new independent productive output?", + "why_it_matters": "All fixed-word singleton cuts failed, but a new jointly supported boundary could preserve the paid MOVE inventory or change it with a fully priced gain." + } + ], + "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": "The prior round altered contact chronology. This screen fixes chronology and chart stock and asks whether new independent productive targets can follow from literal singleton boundary support.", + "scope_status": "changed", + "stop_rule": "Exhaust 1396 chart triples and 11489 representatives. Independently test exact rational survivors. Stop if none pass the two-sided singleton identity. No construction until a support survivor exists.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-singleton-helper-split-bound/VERIFY.json b/research/p104-singleton-helper-split-bound/VERIFY.json new file mode 100644 index 0000000000..0659b59b83 --- /dev/null +++ b/research/p104-singleton-helper-split-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Authenticate the exact word, exhaust 11,489 singleton cuts, verify all 74 independent survivors over the rationals and reproduce the exact fixed-mass tariff bound.", + "timeout_seconds": 45 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-singleton-helper-split-bound/inputs/WORD.json.gz b/research/p104-singleton-helper-split-bound/inputs/WORD.json.gz new file mode 100644 index 0000000000..077bf48c35 Binary files /dev/null and b/research/p104-singleton-helper-split-bound/inputs/WORD.json.gz differ diff --git a/research/p104-singleton-helper-split-bound/replay.py b/research/p104-singleton-helper-split-bound/replay.py new file mode 100644 index 0000000000..a99e4a3310 --- /dev/null +++ b/research/p104-singleton-helper-split-bound/replay.py @@ -0,0 +1,70 @@ +"""Authenticate and independently replay the fixed-word singleton exclusion.""" +from fractions import Fraction +from hashlib import sha1, sha256 +from pathlib import Path +import gzip +import json +import runpy + +HERE = Path(__file__).resolve().parent +WORD = 'inputs/WORD.json.gz' +CONTINUATION = 'CONTINUATION.json' +PRIMARY = runpy.run_path(str(HERE / 'singleton.py')) +INDEPENDENT = runpy.run_path(str(HERE / 'verify.py')) +read_json = INDEPENDENT['read_json'] + + +def verify_word(raw, pin): + assert sha256(raw).hexdigest() == pin['sha256'] == PRIMARY['WORD_SHA256'] == INDEPENDENT['DIGEST'] + assert sha1(f'blob {len(raw)}\0'.encode() + raw).hexdigest() == pin['git_blob'] + return read_json(gzip.decompress(raw)) + + +def verify_controls(raw, pin): + for check in (lambda: read_json('{"inputs": {}, "inputs": {}}'), + lambda: verify_word(raw + b'\0', pin)): + try: + check() + except AssertionError: + continue + raise AssertionError('Mutation control accepted') + return ['REJECT_DUPLICATE_MANIFEST_KEYS', 'REJECT_CHANGED_WORD'] + + +def tariff(): + # For 0 <= k <= 1/200, 2**k - 1 <= k/(1-k) by + # log(2) < 1 and comparison of the exponential and geometric series. + # The maximum rank and 17-copy caller give the factor 153. + k_max = Fraction(1, 200) + r_max, copies = 9, 17 + maximum = copies * r_max * k_max / (1 - k_max) + assert maximum == Fraction(153, 199) < 1 + return {'kappa_upper': str(k_max), 'copies': copies, 'rank_upper': r_max, + 'gross_upper': str(maximum), 'positive_paid_child_lower': 1} + + +def run(): + provenance = read_json((HERE / 'PROVENANCE.json').read_bytes()) + assert set(provenance['inputs']) == {WORD} + pin = provenance['inputs'][WORD] + assert pin['commit'] == 'ed090b57ed88f8859e5ff4643645099e6ba856ea' + assert pin['path'] == 'research/p104-terminal-cut-rechart/WORD.json.gz' + raw = (HERE / WORD).read_bytes() + word = verify_word(raw, pin) + receipt = (HERE / CONTINUATION).read_bytes() + expected = read_json(receipt) + primary = PRIMARY['assess'](word, 1396, 1) + assert read_json(json.dumps(primary)) == expected + checked = INDEPENDENT['run'](word, expected) + checked['dependencies'] = {WORD: pin['sha256'], CONTINUATION: sha256(receipt).hexdigest()} + return {'singleton': checked, 'tariff': tariff(), 'controls': verify_controls(raw, pin), + 'status': 'PASS_FIXED_WORD_SINGLETON_SPLIT_BOUND'} + + +if __name__ == '__main__': + assert __debug__ + result = json.dumps(run(), sort_keys=True, indent=2) + '\n' + frozen = HERE / 'RESULT.json' + if frozen.exists(): + assert result == frozen.read_text() + print(result, end='') diff --git a/research/p104-singleton-helper-split-bound/singleton.py b/research/p104-singleton-helper-split-bound/singleton.py new file mode 100644 index 0000000000..e9f5b86daf --- /dev/null +++ b/research/p104-singleton-helper-split-bound/singleton.py @@ -0,0 +1,205 @@ +"""Search fixed-word single-helper cuts with no shared change of basis.""" +import argparse +from collections import Counter, defaultdict +from fractions import Fraction +from functools import cache +import gzip +from hashlib import sha256 +import json +from pathlib import Path +from random import Random +from time import monotonic + +WORD_SHA256 = '2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756' +PRIME = 2305843009213693951 +SEED = 7277 + + +def add(vector, r, value): + updated = vector.get(r, 0) + value + if updated: + vector[r] = updated + else: + vector.pop(r, None) + + +def scale(vector, r, factor): + if r in vector: + value = vector[r] * factor + if value: + vector[r] = value + else: + del vector[r] + + +@cache +def residue(value): + q = Fraction(value) + return q.numerator * pow(q.denominator, -1, PRIME) % PRIME + + +@cache +def rational(value): + return Fraction(value) + + +def span(frame): + result = {0} + for b in frame: + assert b not in result + result |= {a ^ b for a in result} + return result + + +def assess(word, cap, seconds): + start = monotonic() + program, n, frames = word['program'], word['public'], word['frames'] + main = set(word['live']) | {r+112 for r in word['live']} | set(word['hosted']['X2'] + word['hosted']['Y2']) + assert len(main) == 400 and n - len(main) == 1101 + spaces = list(map(span, frames)) + current = word['initial'] + [None] * word['owned_fields'] + end = word['final'] + rng = Random(SEED) + public_x = [rng.randrange(1, PRIME) for r in range(n)] + public_y = [rng.randrange(1, PRIME) for r in range(n)] + prefix_x = public_x + [0] * word['owned_fields'] + prefix_one = [1] * n + [0] * word['owned_fields'] + suffix_y = public_y + [0] * word['owned_fields'] + signatures = defaultdict(list) + + @cache + def signature(r, f): + u, v = word['initial'][r], end[r] + if r not in main and spaces[u] < spaces[f] < spaces[v]: + return (u, f, v) + return None + + for t, (op, r, *args) in enumerate(program): + touched = (r,) + if op == 'MOVE': + assert current[r] == args[0] + current[r] = args[1] + elif op in ('INIT', 'CLEAR'): + current[r] = args[0] if op == 'INIT' else None + prefix_x[r] = prefix_one[r] = 0 + elif op == 'SCALE': + q = residue(args[0]) + prefix_x[r] = prefix_x[r] * q % PRIME + prefix_one[r] = prefix_one[r] * q % PRIME + elif op in ('ADD', 'COPY'): + s, q = args[0], residue(args[1]) + assert current[s] == current[r] == args[-1] + if op == 'COPY': + prefix_x[r] = prefix_one[r] = 0 + prefix_x[r] = (prefix_x[r] + q * prefix_x[s]) % PRIME + prefix_one[r] = (prefix_one[r] + q * prefix_one[s]) % PRIME + touched = (r, s) if r != s else (r,) + else: + raise ValueError(op) + for role in touched: + if role < n and (sig := signature(role, current[role])) is not None: + coefficient = prefix_one[role] + passes = prefix_x[role] == public_x[role] * coefficient % PRIME + signatures[sig].append((t, role, coefficient, passes)) + assert current == end + [None] * word['owned_fields'] + + def order(sig): + u, f, v = sig + a, b = len(frames[f])-len(frames[u]), len(frames[v])-len(frames[f]) + return (-(a+b), -min(a,b), sig) + + ordered = sorted(signatures, key=order) + selected = set(ordered[:cap]) + waiting = defaultdict(list) + counts = Counter() + for sig in selected: + for t, role, coefficient, passes in signatures[sig]: + if passes: + waiting[t].append((role, coefficient, sig)) + counts['prefix_projection_pass'] += 1 + survivors = [] + for t in range(len(program)-1, -1, -1): + for role, coefficient, sig in waiting.get(t, ()): + if coefficient * suffix_y[role] % PRIME == public_y[role]: + survivors.append((t, role, sig)) + op, r, *args = program[t] + if op in ('CLEAR', 'INIT'): + suffix_y[r] = 0 + elif op == 'SCALE': + suffix_y[r] = suffix_y[r] * residue(args[0]) % PRIME + elif op in ('ADD', 'COPY'): + s, q = args[0], residue(args[1]) + update = suffix_y[r] * q + if op == 'COPY': + suffix_y[r] = 0 + suffix_y[s] = (suffix_y[s] + update) % PRIME + + def exact(t, role, sig): + prefix = {role: Fraction(1)} + for op, r, *args in reversed(program[:t+1]): + if r not in prefix: + continue + if op in ('INIT', 'CLEAR'): + prefix.pop(r) + elif op == 'SCALE': + scale(prefix, r, rational(args[0])) + elif op in ('ADD', 'COPY'): + coeff = prefix.pop(r) if op == 'COPY' else prefix[r] + add(prefix, args[0], coeff * rational(args[1])) + prefix = {r:q for r,q in prefix.items() if r= seconds: + break + outcome, witness = exact(t, role, sig) + tested.append({'cut':t, 'role':role, 'signature':sig, 'outcome':outcome, 'witness':witness}) + counts[outcome] += 1 + if witness: + break + + return { + 'head':'ed090b57ed88f8859e5ff4643645099e6ba856ea', + 'word_sha256':WORD_SHA256, 'public':n, 'helpers':n-len(main), 'seed':SEED, 'prime':PRIME, + 'signature_cap':cap, 'seconds':seconds, 'signatures':len(ordered), + 'selected_signatures':len(selected), 'unvisited_signatures':ordered[cap:], + 'representative_cuts':sum(map(len,signatures.values())), + 'selected_cuts':sum(len(signatures[s]) for s in selected), + 'counts':dict(counts),'projection_survivors':len(survivors), + 'unresolved_exact':len(survivors)-len(tested),'tested':tested, + } + + +if __name__ == '__main__': + assert __debug__ + parser = argparse.ArgumentParser() + parser.add_argument('word', type=Path) + parser.add_argument('--cap', type=int, default=128) + parser.add_argument('--seconds', type=int, default=25) + args = parser.parse_args() + raw = args.word.read_bytes() + assert sha256(raw).hexdigest() == WORD_SHA256 + print(json.dumps(assess(json.loads(gzip.decompress(raw)),args.cap,args.seconds),sort_keys=True,indent=2)) diff --git a/research/p104-singleton-helper-split-bound/verify.py b/research/p104-singleton-helper-split-bound/verify.py new file mode 100644 index 0000000000..7159a51835 --- /dev/null +++ b/research/p104-singleton-helper-split-bound/verify.py @@ -0,0 +1,189 @@ +"""Independently verify the fixed-word singleton exclusion.""" +import argparse +from fractions import Fraction +from functools import cache +import gzip +from hashlib import sha256 +import json +from pathlib import Path + +DIGEST = '2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756' +MOD = 1000000007 + + +def read_json(raw): + def unique(entries): + result = dict(entries) + assert len(result) == len(entries), 'Duplicate JSON keys' + return result + + return json.loads(raw, object_pairs_hook=unique) + + +def basis(rows): + pivots = {} + for row in rows: + while row and row.bit_length() in pivots: + row ^= pivots[row.bit_length()] + assert row + pivots[row.bit_length()] = row + return pivots + + +def contains(pivots, vectors): + for row in vectors: + while row and row.bit_length() in pivots: + row ^= pivots[row.bit_length()] + if row: + return False + return True + + +def decoded(program): + for event in program: + op, dst = event[:2] + src = event[2] if op in ('ADD', 'COPY') else dst + coefficient = Fraction(event[-2]) if op in ('ADD', 'COPY', 'SCALE') else None + if op == 'COPY': + assert src != dst + yield op, dst, src, coefficient + + +def adjust(values, role, amount): + new = values.get(role, 0) + amount + if new: + values[role] = new + else: + values.pop(role, None) + + +def exact(tape, n, cut, role): + row = {role: Fraction(1)} + for op, dst, src, q in reversed(tape[:cut+1]): + c = row.get(dst, 0) + if not c: + continue + if op in ('INIT', 'CLEAR', 'COPY', 'SCALE'): + del row[dst] + if q is not None: + adjust(row, src, c*q) + row = {r:q for r,q in row.items() if r < n} + column = {role: Fraction(1)} + for op, dst, src, q in tape[cut+1:]: + c = column.get(src, 0) + if op in ('INIT', 'CLEAR', 'COPY', 'SCALE'): + column.pop(dst, None) + if q is not None and c: + adjust(column, dst, c*q) + return row, column + + +def control(): + def singleton(program, cut=0): + row, column = exact(list(decoded(program)), 2, cut, 0) + return row == {0:Fraction(2)} and column == {0:Fraction(1,2)} + + pre = ['SCALE', 0, '2', 0] + post = ['SCALE', 0, '1/2', 0] + assert singleton([pre, post]) + assert not singleton([['ADD', 1, 0, '1', 0], pre, post, ['ADD', 1, 0, '-1', 0]], 1) + assert not singleton([['ADD', 0, 1, '1', 0], pre, post, ['ADD', 0, 1, '-1', 0]], 1) + return ['UNIT_RECIPROCAL_POSITIVE', 'SUFFIX_CONTAMINATION_REJECTED', + 'PREFIX_CONTAMINATION_REJECTED'] + + +def run(word, expected): + program, n = word['program'], word['public'] + tape = list(decoded(program)) + main = set(word['live']) | {r+112 for r in word['live']} + main.update(word['hosted']['X2']) + main.update(word['hosted']['Y2']) + charts = word['frames'] + pivots = list(map(basis, charts)) + dims = list(map(len, charts)) + + @cache + def strict(a, b): + return dims[a] < dims[b] and contains(pivots[b], charts[a]) + + @cache + def probe(role): + raw = sha256(f'singleton independent {role}'.encode()).digest() + return int.from_bytes(raw[:8], 'big') % MOD + + @cache + def reduced(q): + return q.numerator * pow(q.denominator, -1, MOD) % MOD + + def update(vector, entry): + op, d, s, q = entry + if op in ('CLEAR', 'INIT'): + vector[d] = 0 + elif op in ('ADD', 'COPY', 'SCALE'): + extra = vector[d] if op == 'ADD' else 0 + vector[d] = (extra + vector[s]*reduced(q)) % MOD + + owned = word['owned_fields'] + values = [probe(role) for role in range(n)] + [0]*owned + ones = [1]*n + [0]*owned + chart = word['initial'] + [None]*owned + marked = [] + signatures = set() + cuts = 0 + for t, (event, entry) in enumerate(zip(program,tape,strict=True)): + op, d, s, _ = entry + if op == 'MOVE': + assert chart[d] == event[2] + chart[d] = event[3] + elif op == 'INIT': + assert chart[d] is None + chart[d] = event[2] + elif op == 'CLEAR': + assert chart[d] == event[2] + chart[d] = None + else: + assert chart[d] == chart[s] == event[-1] + update(values, entry) + update(ones, entry) + for role in {d,s}: + if role in main or role >= n: + continue + u, f, v = word['initial'][role], chart[role], word['final'][role] + if strict(u,f) and strict(f,v): + signatures.add((u,f,v)) + cuts += 1 + if values[role] == ones[role]*probe(role) % MOD: + marked.append((t,role)) + assert chart == word['final'] + [None]*owned + assert len(main) == 400 and n-len(main) == 1101 + assert len(signatures) == expected['selected_signatures'] == expected['signatures'] == 1396 + assert cuts == expected['selected_cuts'] == expected['representative_cuts'] == 11489 + assert expected['projection_survivors'] == expected['unresolved_exact'] == 0 + + bad_prefix = bad_suffix = 0 + for t, role in marked: + row, column = exact(tape, n, t, role) + if set(row) != {role}: + bad_prefix += 1 + else: + assert column != {role:1/row[role]}, (t,role) + bad_suffix += 1 + return {'dependencies':{'complex/source/inputs/WORD.json.gz':DIGEST}, + 'status':'PASS_FIXED_WORD_SINGLETON_EXCLUSION', + 'representatives':cuts,'signatures':len(signatures),'different_prime':MOD, + 'rational_reject_prefix':bad_prefix,'rational_reject_suffix':bad_suffix, + 'rational_checks':len(marked),'controls':control()} + + +if __name__ == '__main__': + assert __debug__ + parser = argparse.ArgumentParser() + parser.add_argument('word', type=Path) + parser.add_argument('receipt', type=Path) + a = parser.parse_args() + raw = a.word.read_bytes() + assert sha256(raw).hexdigest() == DIGEST, 'Changed source word' + receipt = a.receipt.read_bytes() + answer = run(read_json(gzip.decompress(raw)),read_json(receipt)) + answer['dependencies']['interface/CONTINUATION.json'] = sha256(receipt).hexdigest() + print(json.dumps(answer,sort_keys=True,indent=2))