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-owned-move-deletion-bound/CONTACTS.json b/research/p104-owned-move-deletion-bound/CONTACTS.json new file mode 100644 index 0000000000..292f30bc7f --- /dev/null +++ b/research/p104-owned-move-deletion-bound/CONTACTS.json @@ -0,0 +1,492 @@ +{ + "controls": [ + "direct_clear_detected", + "intervening_add_read_excluded", + "intervening_copy_read_excluded", + "owned_reuse_separate" + ], + "direct_clear": [], + "direct_zero": [], + "head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "kappa_change": "0", + "next_contact_counts": { + "ADD": 43, + "SCALE": 4 + }, + "owned_followups": [ + { + "contact": "destination", + "from_chart": 477, + "move": 30527, + "next": 30528, + "next_op": "ADD", + "rank": 4, + "role": 1510, + "to_chart": 1090 + }, + { + "contact": "source", + "from_chart": 1090, + "move": 30535, + "next": 30536, + "next_op": "ADD", + "rank": 1, + "role": 1520, + "to_chart": 470 + }, + { + "contact": "source", + "from_chart": 470, + "move": 30549, + "next": 30550, + "next_op": "ADD", + "rank": 2, + "role": 1521, + "to_chart": 601 + }, + { + "contact": "source", + "from_chart": 601, + "move": 30579, + "next": 30580, + "next_op": "ADD", + "rank": 2, + "role": 1547, + "to_chart": 470 + }, + { + "contact": "source", + "from_chart": 470, + "move": 30591, + "next": 30592, + "next_op": "ADD", + "rank": 1, + "role": 1546, + "to_chart": 1090 + }, + { + "contact": "source", + "from_chart": 267, + "move": 32937, + "next": 32938, + "next_op": "ADD", + "rank": 4, + "role": 1529, + "to_chart": 1091 + }, + { + "contact": "source", + "from_chart": 543, + "move": 33123, + "next": 33124, + "next_op": "ADD", + "rank": 1, + "role": 1528, + "to_chart": 541 + }, + { + "contact": "source", + "from_chart": 1091, + "move": 33131, + "next": 33132, + "next_op": "ADD", + "rank": 1, + "role": 1514, + "to_chart": 260 + }, + { + "contact": "source", + "from_chart": 541, + "move": 33138, + "next": 33139, + "next_op": "ADD", + "rank": 1, + "role": 1502, + "to_chart": 534 + }, + { + "contact": "source", + "from_chart": 534, + "move": 33140, + "next": 33141, + "next_op": "ADD", + "rank": 1, + "role": 1502, + "to_chart": 117 + }, + { + "contact": "source", + "from_chart": 117, + "move": 33147, + "next": 33148, + "next_op": "ADD", + "rank": 4, + "role": 1502, + "to_chart": 594 + }, + { + "contact": "destination", + "from_chart": 517, + "move": 34512, + "next": 34513, + "next_op": "ADD", + "rank": 4, + "role": 1513, + "to_chart": 243 + }, + { + "contact": "source", + "from_chart": 243, + "move": 34516, + "next": 34517, + "next_op": "ADD", + "rank": 1, + "role": 1518, + "to_chart": 431 + }, + { + "contact": "source", + "from_chart": 599, + "move": 35138, + "next": 35139, + "next_op": "ADD", + "rank": 2, + "role": 1541, + "to_chart": 260 + }, + { + "contact": "source", + "from_chart": 431, + "move": 35429, + "next": 35430, + "next_op": "ADD", + "rank": 2, + "role": 1519, + "to_chart": 600 + }, + { + "contact": "source", + "from_chart": 600, + "move": 35434, + "next": 35435, + "next_op": "ADD", + "rank": 2, + "role": 1545, + "to_chart": 431 + }, + { + "contact": "source", + "from_chart": 431, + "move": 35438, + "next": 35439, + "next_op": "ADD", + "rank": 1, + "role": 1544, + "to_chart": 243 + }, + { + "contact": "destination", + "from_chart": 518, + "move": 36307, + "next": 36308, + "next_op": "ADD", + "rank": 4, + "role": 1512, + "to_chart": 240 + }, + { + "contact": "source", + "from_chart": 240, + "move": 36311, + "next": 36312, + "next_op": "ADD", + "rank": 1, + "role": 1516, + "to_chart": 394 + }, + { + "contact": "source", + "from_chart": 394, + "move": 36319, + "next": 36320, + "next_op": "ADD", + "rank": 2, + "role": 1517, + "to_chart": 598 + }, + { + "contact": "source", + "from_chart": 598, + "move": 36329, + "next": 36330, + "next_op": "ADD", + "rank": 2, + "role": 1543, + "to_chart": 394 + }, + { + "contact": "source", + "from_chart": 394, + "move": 36341, + "next": 36342, + "next_op": "ADD", + "rank": 1, + "role": 1542, + "to_chart": 240 + }, + { + "contact": "source", + "from_chart": 243, + "move": 39532, + "next": 39533, + "next_op": "ADD", + "rank": 4, + "role": 1539, + "to_chart": 517 + }, + { + "contact": "source", + "from_chart": 240, + "move": 39559, + "next": 39560, + "next_op": "ADD", + "rank": 4, + "role": 1538, + "to_chart": 518 + }, + { + "contact": "source", + "from_chart": 531, + "move": 39705, + "next": 39706, + "next_op": "ADD", + "rank": 1, + "role": 1526, + "to_chart": 529 + }, + { + "contact": "source", + "from_chart": 529, + "move": 39763, + "next": 39764, + "next_op": "ADD", + "rank": 1, + "role": 1548, + "to_chart": 531 + }, + { + "contact": "source", + "from_chart": 529, + "move": 39792, + "next": 39793, + "next_op": "ADD", + "rank": 1, + "role": 1503, + "to_chart": 520 + }, + { + "contact": "source", + "from_chart": 520, + "move": 39798, + "next": 39799, + "next_op": "ADD", + "rank": 5, + "role": 1503, + "to_chart": 595 + }, + { + "contact": "source", + "from_chart": 260, + "move": 39831, + "next": 39832, + "next_op": "ADD", + "rank": 2, + "role": 1515, + "to_chart": 599 + }, + { + "contact": "destination", + "from_chart": 595, + "move": 39853, + "next": 39854, + "next_op": "ADD", + "rank": 5, + "role": 1532, + "to_chart": 520 + }, + { + "contact": "role", + "from_chart": 520, + "move": 39862, + "next": 39863, + "next_op": "SCALE", + "rank": 1, + "role": 1532, + "to_chart": 529 + }, + { + "contact": "source", + "from_chart": 549, + "move": 40518, + "next": 40519, + "next_op": "ADD", + "rank": 1, + "role": 1549, + "to_chart": 559 + }, + { + "contact": "source", + "from_chart": 559, + "move": 40536, + "next": 40537, + "next_op": "ADD", + "rank": 1, + "role": 1527, + "to_chart": 549 + }, + { + "contact": "destination", + "from_chart": 549, + "move": 40543, + "next": 40544, + "next_op": "ADD", + "rank": 2, + "role": 1501, + "to_chart": 115 + }, + { + "contact": "source", + "from_chart": 115, + "move": 40547, + "next": 40548, + "next_op": "ADD", + "rank": 4, + "role": 1501, + "to_chart": 593 + }, + { + "contact": "source", + "from_chart": 1090, + "move": 41474, + "next": 41475, + "next_op": "ADD", + "rank": 4, + "role": 1537, + "to_chart": 477 + }, + { + "contact": "role", + "from_chart": 593, + "move": 41629, + "next": 41630, + "next_op": "SCALE", + "rank": 6, + "role": 1530, + "to_chart": 549 + }, + { + "contact": "destination", + "from_chart": 594, + "move": 41988, + "next": 41989, + "next_op": "ADD", + "rank": 4, + "role": 1531, + "to_chart": 117 + }, + { + "contact": "source", + "from_chart": 591, + "move": 42460, + "next": 42461, + "next_op": "ADD", + "rank": 3, + "role": 1504, + "to_chart": 1031 + }, + { + "contact": "source", + "from_chart": 1031, + "move": 42465, + "next": 42466, + "next_op": "ADD", + "rank": 4, + "role": 1504, + "to_chart": 597 + }, + { + "contact": "source", + "from_chart": 597, + "move": 42470, + "next": 42471, + "next_op": "ADD", + "rank": 4, + "role": 1533, + "to_chart": 1031 + }, + { + "contact": "role", + "from_chart": 1031, + "move": 42483, + "next": 42484, + "next_op": "SCALE", + "rank": 3, + "role": 1533, + "to_chart": 591 + }, + { + "contact": "source", + "from_chart": 541, + "move": 44249, + "next": 44250, + "next_op": "ADD", + "rank": 1, + "role": 1550, + "to_chart": 543 + }, + { + "contact": "destination", + "from_chart": 117, + "move": 44256, + "next": 44257, + "next_op": "ADD", + "rank": 1, + "role": 1531, + "to_chart": 534 + }, + { + "contact": "role", + "from_chart": 534, + "move": 44258, + "next": 44259, + "next_op": "SCALE", + "rank": 1, + "role": 1531, + "to_chart": 541 + }, + { + "contact": "source", + "from_chart": 1091, + "move": 45607, + "next": 45608, + "next_op": "ADD", + "rank": 4, + "role": 1551, + "to_chart": 267 + }, + { + "contact": "source", + "from_chart": 260, + "move": 45625, + "next": 45626, + "next_op": "ADD", + "rank": 1, + "role": 1540, + "to_chart": 1091 + } + ], + "paid_owned_moves": 47, + "stock_upper": "0", + "unresolved": 0, + "word_sha256": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756" +} diff --git a/research/p104-owned-move-deletion-bound/NOTICE b/research/p104-owned-move-deletion-bound/NOTICE new file mode 100644 index 0000000000..8910a2f9f4 --- /dev/null +++ b/research/p104-owned-move-deletion-bound/NOTICE @@ -0,0 +1,6 @@ +Apache-2.0. +The literal native word and complete comparator come from #7277, with the +signed caller and accounting lineage of #7113. #7298 retained the identical +native word in its separate chronology audit. #6865 and #5557 supply the +related owned-exit and initialized-zero/residual precedents. #7165 supplies +the prior owned-MOVE comparison. OpenAI Codex and subagents materially assisted. diff --git a/research/p104-owned-move-deletion-bound/PROVENANCE.json b/research/p104-owned-move-deletion-bound/PROVENANCE.json new file mode 100644 index 0000000000..6394df4e91 --- /dev/null +++ b/research/p104-owned-move-deletion-bound/PROVENANCE.json @@ -0,0 +1,13 @@ +{ + "files": { + "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", + "uncompress": false + } + }, + "schema_version": 1 +} diff --git a/research/p104-owned-move-deletion-bound/README.md b/research/p104-owned-move-deletion-bound/README.md new file mode 100644 index 0000000000..29337e3bf7 --- /dev/null +++ b/research/p104-owned-move-deletion-bound/README.md @@ -0,0 +1,78 @@ +# Direct deletion bound for paid P104 owned MOVEs + +**NO VERIFIED GAIN. Exact conditional κ change 0%.** On the exact +[#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277) native word, +consider direct deletion of one paid owned MOVE with the rest of the word +fixed. The two tested cases are an identically zero MOVE input and a MOVE +whose first next same-lifetime contact is CLEAR. All 47 paid owned MOVE inputs +are nonzero as exact normalized rational rows. Each of the 47 MOVEs has an +intervening contact before CLEAR. The stock is empty under both predicates, +so the optimistic paid saving is exactly zero per native call and across the +complete caller. Zero cases remain unresolved in this scope. + +## Exact scope and checks + +The signed rational replay initializes all public inputs independently and +propagates exact sparse rows through 76,443 literal instructions. It checks +the chart and ownership guards, including the fresh-zero COPY token, and +removes exactly canceled terms. A nonzero input row has at least one nonzero +coefficient and therefore a nonzero response for some allowed input. +The census checks 70 owned lifetimes and 47 positive-rank owned MOVEs. +The paid rank histogram is `{1: 20, 2: 9, 3: 2, 4: 13, 5: 2, 6: 1}`. + +A separate forward pass follows each active owned role and records the first +later contact of each MOVE. It counts ADD and COPY sources as reads and tracks +INIT/CLEAR lifetimes separately. The next contacts are 36 ADD source reads, +seven ADD destination contacts and four SCALEs. This independently checks the reverse +next-contact census used in discovery. The controls detect an exact rational +cancellation, reject a changed sign, detect a synthetic direct CLEAR, reject +an intervening ADD or COPY source read, and distinguish a reused owned slot. +[RESULT.json](RESULT.json) and [CONTACTS.json](CONTACTS.json) contain the +deterministic replay receipts. + +The fixed-word stock bound covers these two direct deletion predicates. +Changed contacts or lifetimes, broader dead-value analysis after an +intervening write, and a replacement that transports a nonzero field require +separate tests. No physical candidate was built. The strongest independently +reproduced comparable witness remains #7277 at conditional κ = +0.003645669928698. + +## Replay + +From a clean checkout, use CPython 3.12 with assertions enabled and the +standard library. + +~~~sh +python3.12 -B scripts/research_package.py --package research/p104-owned-move-deletion-bound +python3.12 -B scripts/check_research_commit.py --package research/p104-owned-move-deletion-bound --check-modes --check-source-history +~~~ + +A Git-free export can run +`python3.12 -I -B research/p104-owned-move-deletion-bound/replay.py`. +The bundled word is authenticated by SHA-256 and Git blob ID. Its exact +source commit, path and digests are in [PROVENANCE.json](PROVENANCE.json). +No earlier checkout or temporary pointer is required. + +## Predecessors + +[#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277) at +`ed090b57ed88f8859e5ff4643645099e6ba856ea` supplies the literal word +and complete comparator. [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +at `07a76c5e2738882c0cb322278e56f6cae3c9885d` supplies the +signed caller and paid accounting lineage. [#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) +previously bundled the identical literal word in a distinct scalar +chronology audit. [#6865](https://github.com/CrocSwap/integer-mult-bounds/pull/6865) +supplies the related owned-exit and lifetime-shortening precedent. +[#5557](https://github.com/CrocSwap/integer-mult-bounds/pull/5557) +supplies the initialized-zero owned COPY and residual precedent. +[#7165](https://github.com/CrocSwap/integer-mult-bounds/pull/7165) +supplies the earlier paid owned-MOVE replacement comparison with donor +routes. OpenAI Codex and subagents materially assisted. + +## Open next questions + +Can a changed lifetime or consumer graph remove the earliest intervening +contact while preserving the complete signed operator? Start with one exact +owned contact chain and bound the total compatible savings under its changed +contract. A surviving route needs signed forward and adjoint action, +ownership and restoration, and a fully charged caller and tape price. diff --git a/research/p104-owned-move-deletion-bound/RESULT.json b/research/p104-owned-move-deletion-bound/RESULT.json new file mode 100644 index 0000000000..cad68031ac --- /dev/null +++ b/research/p104-owned-move-deletion-bound/RESULT.json @@ -0,0 +1,29 @@ +{ + "checked_copies": 1, + "compressed_word_sha256": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "control": { + "cancellation_detected": true, + "changed_sign_rejected": true, + "test_owned_move_index": 4 + }, + "exact_zero_moves": [], + "first_unvisited_literal_index": null, + "first_unvisited_owned_move_index": null, + "fresh_zero_moves": 0, + "literal_events": 76443, + "literal_events_visited": 76443, + "nonzero_owned_clears": 69, + "owned_lifetimes": 70, + "paid_owned_histogram": { + "1": 20, + "2": 9, + "3": 2, + "4": 13, + "5": 2, + "6": 1 + }, + "paid_owned_moves": 47, + "peak_owned": 49, + "scientific_head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "scope_exhausted": true +} diff --git a/research/p104-owned-move-deletion-bound/SOURCES.json b/research/p104-owned-move-deletion-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-owned-move-deletion-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-owned-move-deletion-bound/TASK.json b/research/p104-owned-move-deletion-bound/TASK.json new file mode 100644 index 0000000000..ff9cff60e5 --- /dev/null +++ b/research/p104-owned-move-deletion-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Direct deletion of one already-paid owned MOVE on the exact retained #7277 word if its normalized input is identically zero or its first next same-lifetime contact is CLEAR.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent audit and packaging.", + "author": "Round 40 research campaign", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Bound the stock of exact direct deletions before building any physical zero-rechart or erasure variant.", + "budget_minutes": 2, + "evidence": "Exact rational signed normalized row replay, independent forward owner-contact recount, old paid rank histogram, exact cancellation/sign, direct-clear and intervening-read controls.", + "open_questions": [ + { + "blocked_by": "An algebraic match needs full signed arbitrary-input equivalence, physical ownership and restoration, and complete paid and tape costs.", + "first_step": "Identify one exact contact graph and price the compatible whole stock under the proposed changed lifetime contract before building a candidate.", + "question": "Can a changed lifetime boundary remove a paid MOVE with an intervening contact?", + "why_it_matters": "The fixed-word direct deletion stock is empty, so another change must account for each intervening read or write." + } + ], + "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": "This changes paid owned MOVE deletion eligibility without changing scalar chronology, any other MOVE or ownership lifetimes.", + "scope_status": "changed", + "stop_rule": "Exhaust every paid owned MOVE or report the first unresolved event. If both necessary filters return empty stock, close the scope without a native build.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-owned-move-deletion-bound/VERIFY.json b/research/p104-owned-move-deletion-bound/VERIFY.json new file mode 100644 index 0000000000..3971acc45d --- /dev/null +++ b/research/p104-owned-move-deletion-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Authenticate the exact #7277 word, exhaust the normalized rational zero stock, and independently check every paid owned MOVE's next owner contact.", + "timeout_seconds": 30 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-owned-move-deletion-bound/inputs/WORD.json.gz b/research/p104-owned-move-deletion-bound/inputs/WORD.json.gz new file mode 100644 index 0000000000..077bf48c35 Binary files /dev/null and b/research/p104-owned-move-deletion-bound/inputs/WORD.json.gz differ diff --git a/research/p104-owned-move-deletion-bound/replay.py b/research/p104-owned-move-deletion-bound/replay.py new file mode 100644 index 0000000000..a893899fab --- /dev/null +++ b/research/p104-owned-move-deletion-bound/replay.py @@ -0,0 +1,116 @@ +"""Authenticate and exhaust direct deletion eligibility on the #7277 word.""" +from argparse import ArgumentParser +from collections import Counter +import gzip +from hashlib import sha1, sha256 +import json +from pathlib import Path +import runpy +import time + +HERE = Path(__file__).resolve().parent +WORD = "inputs/WORD.json.gz" +HEAD = "ed090b57ed88f8859e5ff4643645099e6ba856ea" +SHA256 = "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756" +BLOB = "077bf48c35db0ddafae81f1bfa0ffacc30894b2b" + + +def unique(items): + value = dict(items) + assert len(value) == len(items), "duplicate JSON key" + return value + + +def read_json(data): + return json.loads(data, object_pairs_hook=unique) + + +def owned_followups(word): + public = word["public"] + active = set() + pending = {} + followups = [] + for i, (op, dst, *args) in enumerate(word["program"]): + if op == "INIT": + assert dst >= public and dst not in active and dst not in pending + active.add(dst) + continue + contacts = [(dst, "destination"), (args[0], "source")] if op in ("ADD", "COPY") else [(dst, "role")] + for role, side in contacts: + if role < public: + continue + assert role in active + if role in pending: + record = pending.pop(role) + if op == "CLEAR": + assert args == [record["to_chart"]] + followups.append({**record, "next": i, "next_op": op, "contact": side}) + if op == "CLEAR": + active.remove(dst) + elif op == "MOVE": + src, target, owned = args + assert owned == (dst in active) + if owned: + rank = abs(len(word["frames"][src]) - len(word["frames"][target])) + assert rank > 0 + pending[dst] = { + "move": i, "role": dst, "from_chart": src, + "to_chart": target, "rank": rank, + } + assert not pending and not active + return sorted(followups, key=lambda row: row["move"]) + + +def contact_controls(): + word = {"public": 1, "frames": [[], [1]], "program": [ + ["INIT", 1, 0], ["ADD", 1, 0, "1", 0], ["MOVE", 1, 0, 1, True], + ["CLEAR", 1, 1], ["INIT", 1, 0], ["ADD", 1, 0, "1", 0], + ["MOVE", 1, 0, 1, True], ["ADD", 0, 1, "1", 1], ["CLEAR", 1, 1], + ["INIT", 1, 0], ["MOVE", 1, 0, 1, True], ["INIT", 2, 1], + ["COPY", 2, 1, "1", 1], ["CLEAR", 2, 1], ["CLEAR", 1, 1], + ]} + trace = owned_followups(word) + assert [(r["move"], r["next_op"], r["contact"]) for r in trace] == [ + (2, "CLEAR", "role"), (6, "ADD", "source"), (10, "COPY", "source")] + return ["direct_clear_detected", "intervening_add_read_excluded", + "intervening_copy_read_excluded", "owned_reuse_separate"] + + +def run(): + pin = read_json((HERE / "PROVENANCE.json").read_bytes())["files"][WORD] + assert (pin["commit"], pin["sha256"], pin["git_blob"]) == (HEAD, SHA256, BLOB) + raw = (HERE / WORD).read_bytes() + assert sha256(raw).hexdigest() == SHA256, "changed exact source word" + assert sha1(f"blob {len(raw)}\0".encode() + raw).hexdigest() == BLOB + word = read_json(gzip.decompress(raw)) + verifier = runpy.run_path(str(HERE / "verify_zero.py")) + result = { + "scientific_head": HEAD, "compressed_word_sha256": SHA256, + **verifier["audit"](word, time.monotonic(), 18), + "control": verifier["control"](), + } + assert read_json(json.dumps(result)) == read_json((HERE / "RESULT.json").read_bytes()) + assert result["scope_exhausted"] and not result["exact_zero_moves"] + assert result["fresh_zero_moves"] == 0 + contacts = owned_followups(word) + counts = Counter(row["rank"] for row in contacts) + assert counts == result["paid_owned_histogram"] + assert len(contacts) == result["paid_owned_moves"] == 47 + clear = [row for row in contacts if row["next_op"] == "CLEAR"] + assert not clear + return { + "head": HEAD, "word_sha256": SHA256, + "paid_owned_moves": len(contacts), "direct_zero": result["exact_zero_moves"], + "direct_clear": clear, "next_contact_counts": Counter(row["next_op"] for row in contacts), + "stock_upper": "0", "kappa_change": "0", "unresolved": 0, + "controls": contact_controls(), "owned_followups": contacts, + } + + +if __name__ == "__main__": + assert __debug__, "run with assertions enabled" + parser = ArgumentParser(description=__doc__) + parser.parse_args() + actual = json.dumps(run(), indent=2, sort_keys=True) + "\n" + assert actual == (HERE / "CONTACTS.json").read_text() + print("PASS_OWNED_MOVE_DIRECT_DELETION moves=47 exact_zero=0 direct_clear=0 unresolved=0 stock_upper=0 kappa_change=0") diff --git a/research/p104-owned-move-deletion-bound/verify_zero.py b/research/p104-owned-move-deletion-bound/verify_zero.py new file mode 100644 index 0000000000..a9c212b149 --- /dev/null +++ b/research/p104-owned-move-deletion-bound/verify_zero.py @@ -0,0 +1,180 @@ +"""Audit normalized owned-MOVE inputs using exact signed rational rows.""" + +import argparse +from collections import Counter +from fractions import Fraction +import gzip +from hashlib import sha256 +import json +from math import gcd +from pathlib import Path +import time + +SHA = "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756" +HEAD = "ed090b57ed88f8859e5ff4643645099e6ba856ea" +OWNED_PAID = {1: 20, 2: 9, 3: 2, 4: 13, 5: 2, 6: 1} + + +def reduced(denominator, numerators): + if not numerators: + return 1, {} + factor = denominator + for n in numerators.values(): + factor = gcd(factor, n) + if factor == 1: + return denominator, numerators + return denominator // factor, {k: n // factor for k, n in numerators.items()} + + +def scaled(row, q): + denominator, numerators = row + return reduced(denominator * q.denominator, {k: q.numerator * n for k, n in numerators.items()}) + + +def plus(destination, source, q): + denominator, numerators = destination + s_den, s_num = source + right_denominator = s_den * q.denominator + common_factor = gcd(denominator, right_denominator) + left_scale = right_denominator // common_factor + right_scale = denominator // common_factor * q.numerator + sums = {k: left_scale * n for k, n in numerators.items()} if left_scale != 1 else numerators + for k, n in s_num.items(): + value = sums.get(k, 0) + right_scale * n + if value: + sums[k] = value + else: + sums.pop(k, None) + return reduced(denominator * left_scale, sums) + + +def frame_space(rows): + space = {0} + for row in rows: + space |= {v ^ row for v in space} + assert len(space) == 1 << len(rows) + return space + + +def audit(word, start, seconds): + public = word["public"] + roles = public + word["owned_fields"] + events = word["program"] + frames = [frame_space(f) for f in word["frames"]] + charts = word["initial"] + [None] * (roles - public) + rows = [(1, {r: 1}) for r in range(public)] + [None] * (roles - public) + fresh = set() + live = set() + owned_paid = Counter() + nonzero_clears = owned_copies = lifetimes = peak = visited = 0 + found, token_hits = [], [] + cap = start + seconds + for index, event in enumerate(events): + if index % 64 == 0 and time.monotonic() >= cap: + break + visited = index + 1 + op, d, *args = event + if op == "INIT": + frame, = args + assert d >= public and charts[d] is None and rows[d] is None and d not in live + rows[d], charts[d] = (1, {}), frame + fresh.add(d) + live.add(d) + lifetimes += 1 + peak = max(peak, len(live)) + elif op == "CLEAR": + frame, = args + assert d in live and charts[d] == frame + nonzero_clears += bool(rows[d][1]) + fresh.discard(d) + live.remove(d) + rows[d], charts[d] = None, None + elif op == "MOVE": + source, target, owned = args + assert charts[d] == source and owned == (d in live) == (d >= public) + assert frames[source] < frames[target] or (owned and frames[target] < frames[source]) + if owned: + rank = abs(len(word["frames"][target]) - len(word["frames"][source])) + owned_paid[rank] += 1 + if not rows[d][1]: + found.append({"literal_index": index, "role": d, "from": source, "to": target, "rank": rank}) + if d in fresh: + assert not rows[d][1] + token_hits.append(index) + fresh.discard(d) + charts[d] = target + elif op == "SCALE": + coefficient, frame = args + q = Fraction(coefficient) + assert charts[d] == frame and q + rows[d] = scaled(rows[d], q) + else: + s, coefficient, frame = args + q = Fraction(coefficient) + assert op in ("ADD", "COPY") and d != s and charts[d] == frame == charts[s] and q + if op == "COPY": + assert d in live and d in fresh and not rows[d][1] + rows[d] = scaled(rows[s], q) + owned_copies += 1 + else: + rows[d] = plus(rows[d], rows[s], q) + fresh.discard(d) + first_unvisited = None if visited == len(events) else visited + remaining_move = next((i for i in range(visited, len(events)) if events[i][0] == "MOVE" and events[i][-1]), None) + if first_unvisited is None: + assert not live and not fresh and charts == word["final"] + [None] * (roles - public) + return { + "scope_exhausted": first_unvisited is None, + "literal_events": len(events), "literal_events_visited": visited, + "first_unvisited_literal_index": first_unvisited, + "first_unvisited_owned_move_index": remaining_move, + "paid_owned_histogram": owned_paid, "paid_owned_moves": sum(owned_paid.values()), + "exact_zero_moves": found, "fresh_zero_moves": len(token_hits), + "owned_lifetimes": lifetimes, "peak_owned": peak, "checked_copies": owned_copies, + "nonzero_owned_clears": nonzero_clears, + } + + +def control(): + # Same public input reaches an owned role with two different signed rational paths. + word = { + "public": 1, "owned_fields": 1, "initial": [0], "final": [0], "frames": [[], [1]], + "program": [ + ["INIT", 1, 0], ["COPY", 1, 0, "2/3", 0], + ["ADD", 1, 0, "-1/2", 0], ["ADD", 1, 0, "-1/6", 0], + ["MOVE", 1, 0, 1, True], ["CLEAR", 1, 1], + ], + } + observed = audit(word, time.monotonic(), 1) + assert observed["scope_exhausted"] + assert observed["exact_zero_moves"] == [{"literal_index": 4, "role": 1, "from": 0, "to": 1, "rank": 1}] + assert observed["fresh_zero_moves"] == 0 + word["program"][3][3] = "1/6" + changed = audit(word, time.monotonic(), 1) + assert changed["scope_exhausted"] and not changed["exact_zero_moves"] + return {"cancellation_detected": True, "changed_sign_rejected": True, "test_owned_move_index": 4} + + + +def main(): + if not __debug__: + raise RuntimeError("Run with assertions enabled") + start = time.monotonic() + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--word", required=True, type=Path) + parser.add_argument("--cap", default=22.0, type=float) + args = parser.parse_args() + assert 0 < args.cap <= 22.0 + raw = args.word.read_bytes() + if sha256(raw).hexdigest() != SHA: + raise ValueError("Unexpected compressed word SHA-256") + result = audit(json.loads(gzip.decompress(raw)), start, args.cap) + if result["scope_exhausted"]: + assert result["paid_owned_histogram"] == OWNED_PAID + assert tuple(result[k] for k in ("owned_lifetimes", "peak_owned", "checked_copies")) == (70, 49, 1) + print(json.dumps({"scientific_head": HEAD, "compressed_word_sha256": SHA, + **result, "control": control()}, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()