diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 63ba3e9aa8..52b62d0481 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,25 @@ # CI verification -## Current selected-family replay: #6030 +## Current selected-family replay: #7000 with #7001 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.00363005817 to the [application review](research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md), +[validation receipts](research/pr-intake-evidence/pr7000-application/VALIDATION.json), +and [explicit source closure](../certificates/frontier7000-source.json). +`make frontier7000-verify` follows that exact-source selected replay. The review +reuses eleven authenticated preceding executions and records seven fresh serial +application, scalar and complete native-catalogue executions. The earlier +monolithic timeout is retained separately and is not completed coverage. +Consult the receipts for exact commands, source heads and limits. + +The five inherited framework assumptions remain. No complete uniform word, +literal multiplier execution, independent human proof or formal-kernel proof +is asserted. Routine research submissions do not need to rerun this +selected-family replay. The sections below preserve historical checkpoints. + +## Historical selected-family replay: #6030 + +The [historical checkpoint](../certificates/checkpoints/frontier6030.json) binds conditional κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md), [validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json), and [explicit source closure](../certificates/frontier6030-source.json). diff --git a/research/historical-selected-replay-gap/README.md b/research/historical-selected-replay-gap/README.md index 55d8cc3b49..36d9a873ca 100644 --- a/research/historical-selected-replay-gap/README.md +++ b/research/historical-selected-replay-gap/README.md @@ -69,7 +69,11 @@ python3 -B scripts/research_package.py --package research/historical-selected-re The direct command prints `PASS_HISTORICAL_SELECTED_REPLAY_GAP`. A registered replay prints `PASS_REGISTERED_RESEARCH_PACKAGE`. Both require Git history -containing the two inspected commits. +containing the two inspected commits and the source and manifest objects at +`2485805a6d47f36ea83ddde6327d453ac82d44dc`. The verifier uses a temporary +sparse checkout of that commit, checks the declared source digests there, and +uses its planner and manifest inventory. The recorded rejections and selection +therefore remain reproducible after later changes to the live Makefile or CI guide. ## Open next questions diff --git a/research/historical-selected-replay-gap/SOURCES.json b/research/historical-selected-replay-gap/SOURCES.json index c1010eec95..62bb8b3950 100644 --- a/research/historical-selected-replay-gap/SOURCES.json +++ b/research/historical-selected-replay-gap/SOURCES.json @@ -4,13 +4,13 @@ "files": [ { "path": "Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "0d683a06b9e7ee162496108ce9a7c5d2ee94fccf", "sha256": "4f2d4f2dcd15139ec82658a975f85ed300897385f85799218539f4c8d60567da" }, { "path": "certificates/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "eccafa830c16170c36faf93045ddf1f638f7bcd4", "sha256": "4c0b9d37e1034b2076e30a70f8e514416298c462d9ee98bc87fe6556b14df786" }, @@ -22,7 +22,7 @@ }, { "path": "docs/ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "63ba3e9aa8bdc5e942b56e34244b92b16f854085", "sha256": "c7d3027e9ad8bcbff68f07aa9576b30fb2f3c76c44d876d40c7fdbf4a3e2228a" }, @@ -34,163 +34,163 @@ }, { "path": "research/clifford-state-performance/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "6f98a0061a5104dfab82c9e806f819b41811f684", "sha256": "396d0f08df24952248140d5c65c51b8c902ef1c580892ff7ea182890530f67ee" }, { "path": "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "5e0f92af463ec12c5e1dcc3effd44081a88af647", "sha256": "07a9daeaf2bda308a92e9a4684f13d5fc766c7772d74801fceb7f4599fdab226" }, { "path": "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "9e13266bf85e627f1b7dc225e9530ea69fd2c7f0", "sha256": "421e1211fb1897c45621dc6801c276e53f2e6f335583c9c9049e535f87c0a3b1" }, { "path": "research/community-batch932-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "cc4d03eb59b9ab3f952735f7e88ff18c2d15d7af", "sha256": "184629cac91a5cfaca50330a88596008b824221433867dcf8117539c913c284a" }, { "path": "research/community-batch970-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8b9f4111badf7de5d97684799560b55110e9da79", "sha256": "23188ed920e38a54006cb883e181585620821c63bf7e8b5e05d32719417cc37e" }, { "path": "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "a5300d4e7a5381a3f443fc54c768ca6f0f236d68", "sha256": "3c820fb30e1b4d9bcfc6a7ab524375e5b2abd66b940af2c509146104f0bcd79c" }, { "path": "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "d7ff6d777b01d69b6ce84caf25d3b7e4a4d2f211", "sha256": "6b185a9902652f893f3ebd8ada92d2f11b6de6533a9a4d11718a8a4496101128" }, { "path": "research/community-hyperplane599-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "546f37d326d10a99910ae8f908e71ef768524d98", "sha256": "65099d764bfcc39bda5e4d9966783611b094c3522dbdd1435cd498d657a8ef8e" }, { "path": "research/community-k492-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "e538481e4cb16ed936d3195f2dfb5b5a9ca0a76b", "sha256": "2c0f4fa5bc150d05658af2e7c54c4d2c337dd52b7efd3d69530ae73bcbdf452a" }, { "path": "research/community-reconciliation92-audit/MANIFEST.json", - "usage": "input", + "usage": "provenance", "git_blob": "2a2e93685173d5f13cbb5abe740f5d90352e0228", "sha256": "5f501f3c118131e7d069f30ad77186eb2ad6961f9680a0ef105f4514ed41808a" }, { "path": "research/partial-swap-digest/baseline.py", - "usage": "input", + "usage": "provenance", "git_blob": "a2f0190704db83bd8ef48e46e723c49b925804fe", "sha256": "81e9af92cdf38243a540cdcff2062778e449467848d444da37a9553c12ca4c34" }, { "path": "research/r420-two-sided-basis/SOURCES.json", - "usage": "input", + "usage": "provenance", "git_blob": "5d718e11e62f4bcadecf1e02d6b61f87dbe190b0", "sha256": "d9810b0d139c5a1211fd2c1f0d142187cc1fca30026e1e7bc4f9ecfacf1596d1" }, { "path": "research/skip-clones/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8d1bb3b9c8189e35e5d8bfdfa632d7473e8be0d5", "sha256": "0b68e63e35a97ce6b0cdb6e291b88ebaa8f2dd4afb70b2498f10ee89428258dc" }, { "path": "research/split-skip/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "2ab610b6ea2edd2865fda793ef2168b0c76afb4f", "sha256": "7c2b4646a3ecfef6f881da5c43e4bd0fa9a4d1b00548b8ab458d897e16735134" }, { "path": "scripts/historical-ci-inputs/Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "aff68409021c9d401a6f8013b9dfd7dbcc30f2a8", "sha256": "ea8830dd79da493e2d75baf753d733ff7efbcf2b4794afe41fae0ac8f3055646" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "65db599ab0b1dea0312c4ca048e0bd0f44c3736f", "sha256": "96ea543e6c707424afe247e77bd86c82152f90fc76a0773c4232145da5cdf8d1" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "34820a8f24678f918f4d0e7a35380d8013fc3495", "sha256": "628391b6abfbc8674ceec1751867a4392f2cc0b5b66886243e139af86cf355ac" }, { "path": "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "c755b76e0d44ba4917aa94440ebe54daefce5b2a", "sha256": "d7fd929726b326aeeaf0a3996475adec88eee9aac09ae0bebeeaa0bc1fc8f199" }, { "path": "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "7f3c012504187917a728b9fe87043f0fc8cd006a", "sha256": "a854022e0e1d5d4db4d60e586be3ea56005013ef14a1fc06d02bc06e8529c4b0" }, { "path": "scripts/historical-ci-inputs/partial-swap-context.json", - "usage": "input", + "usage": "provenance", "git_blob": "ad65114886bf34a4fd27e79f3be502389e689faa", "sha256": "833a9642f33aeab2ffea17ec9c6b82e0a953f90192b2c82e10bef21538dccba9" }, { "path": "scripts/historical-ci-inputs/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "52075f2463f60af5e16571347f24274fce73a1ea", "sha256": "f3c4be597b2f2136da4ae2cc80c7454f63c90aa01f84e5b8131cee4dd55de815" }, { "path": "scripts/partial_swap/shared.py", - "usage": "input", + "usage": "provenance", "git_blob": "44a0e454c70f9c4b98e258b8443612e6a119904b", "sha256": "5a0646a50b9f3e8ea55168620a78e8853b0ab810517cefc8cfb8696aedee278a" }, { "path": "scripts/replay_historical_check.py", - "usage": "input", + "usage": "provenance", "git_blob": "1e92fff2782970ef71378f594f2350d245a4db26", "sha256": "5467619c78183d3adc82b0cb55af28e5c1a01fca2b0588677816244b53e2bafd" }, { "path": "scripts/research_package.py", - "usage": "input", + "usage": "provenance", "git_blob": "091b4c8f58bac9a9580d76025b887dc5c873d05f", "sha256": "e1256016e7f51827d04fa2179255989f639ae1d97afaa9c16265f85a0c6abd70" }, { "path": "scripts/run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "a96ab35b315ce492e7fbbfd6c5ae211aa066b541", "sha256": "49eb56dd0fc0d8d8ffdb209970a7adf2176223580646f575d5c22e59543b381c" }, { "path": "scripts/verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "6882a4700e410dec569b51ae2eaf1a19cc019195", "sha256": "d6b305eac5b9bdb8172c469ad30a1655a60fa0aceac8b1bf610e1b73f51babd8" }, { "path": "tests/test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "343b24abf6719b81805eba5a84c74e57634c8288", "sha256": "3a5470d0b139828b90e19bf9583ddeafcd69f8e34f2824664eb3a2958a52e34d" } diff --git a/research/historical-selected-replay-gap/VERIFY.json b/research/historical-selected-replay-gap/VERIFY.json index 98553e72ed..ab7efa3471 100644 --- a/research/historical-selected-replay-gap/VERIFY.json +++ b/research/historical-selected-replay-gap/VERIFY.json @@ -4,36 +4,7 @@ "python": "3.12", "requirements": [], "inputs": [ - "Makefile", - "certificates/partial-swap-network.json", - "docs/ci-verification.md", - "research/clifford-state-performance/SOURCE.json", - "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "research/community-batch932-audit/CONTENT-COVERAGE.json", - "research/community-batch970-audit/CONTENT-COVERAGE.json", - "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "research/community-hyperplane599-audit/SOURCE.json", - "research/community-k492-audit/SOURCE.json", - "research/community-reconciliation92-audit/MANIFEST.json", - "research/partial-swap-digest/baseline.py", - "research/r420-two-sided-basis/SOURCES.json", - "research/skip-clones/SOURCE.json", - "research/split-skip/SOURCE.json", - "scripts/historical-ci-inputs/Makefile", - "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "scripts/historical-ci-inputs/partial-swap-context.json", - "scripts/historical-ci-inputs/partial-swap-network.json", - "scripts/partial_swap/shared.py", - "scripts/replay_historical_check.py", - "scripts/research_package.py", - "scripts/run_isolated_tests.py", - "scripts/verify_selected_result.py", - "tests/test_isolated_test_runner.py" + "scripts/research_package.py" ], "commands": [ { diff --git a/research/historical-selected-replay-gap/verify.py b/research/historical-selected-replay-gap/verify.py index 83b995941a..9d266c5a4e 100644 --- a/research/historical-selected-replay-gap/verify.py +++ b/research/historical-selected-replay-gap/verify.py @@ -6,8 +6,10 @@ """ import hashlib import importlib.util +import json import subprocess import sys +import tempfile from pathlib import Path ROOT = Path(__file__).resolve().parents[2] @@ -61,31 +63,47 @@ def require(ok, message): raise SystemExit(message) -def load_checker(): - path = ROOT / "scripts/replay_historical_check.py" - spec = importlib.util.spec_from_file_location("historical_selected_replay_gap_checker", path) +def load_module(path): + spec = importlib.util.spec_from_file_location(path.stem, path) module = importlib.util.module_from_spec(spec) spec.loader.exec_module(module) return module +def checkout_snapshot(snapshot, sources, runner, env): + paths = [runner.canonical_relative_path(row["path"]) for row in sources["files"]] + git = ["git", "-c", "maintenance.auto=false", "-c", "gc.auto=0", + "-c", "core.autocrlf=false"] + subprocess.run([*git, "clone", "--quiet", "--shared", "--no-tags", "--no-checkout", + "--", str(ROOT), str(snapshot)], cwd=ROOT, env=env, check=True) + subprocess.run([*git, "update-ref", "--no-deref", "HEAD", INSPECTED], + cwd=snapshot, env=env, check=True) + # The pinned planner reads omitted manifests from the sparse HEAD/index. + patterns = "".join(f"/{path.as_posix()}\n" for path in paths) + subprocess.run([*git, "sparse-checkout", "set", "--no-cone", "--stdin"], + cwd=snapshot, env=env, input=patterns.encode("utf-8"), check=True) + subprocess.run([*git, "read-tree", "-mu", "HEAD"], cwd=snapshot, env=env, check=True) + for path, row in zip(paths, sources["files"], strict=True): + require(hashlib.sha256((snapshot / path).read_bytes()).hexdigest() == row["sha256"], + "historical checkout source digest changed: " + path.as_posix()) + + def entries(checker): for name, config in checker.CONFIG.items(): for entry in [config, *config.get("additional_inputs", [])]: yield name, entry -def reject(checker, entry): +def reject(root, checker, entry): try: - checker.authenticated_input(ROOT, entry) + checker.authenticated_input(root, entry) except ValueError as exc: return str(exc) raise SystemExit("historical input was admitted: " + entry["path"]) -def main(): - require(not sys.flags.optimize, "assertions must stay enabled") - checker = load_checker() +def check_snapshot(root, env): + checker = load_module(root / "scripts/replay_historical_check.py") selected = [entry for name, entry in entries(checker) if name == "tooling-ledger" and entry["path"] == SELECTED_PATH] require(len(selected) == 1, "selected-result checker overlay is not unique") @@ -94,7 +112,7 @@ def main(): require(entry["accepted_live_sha256"] == [SELECTED_ACCEPTED], "accepted selected-checker successors changed") frozen = (checker.INPUTS / entry["input"]).read_bytes() - live = (ROOT / SELECTED_PATH).read_bytes() + live = (root / SELECTED_PATH).read_bytes() require(hashlib.sha256(frozen).hexdigest() == SELECTED_PIN, "frozen selected checker bytes changed") require(hashlib.sha256(live).hexdigest() == SELECTED_LIVE, "live selected checker digest changed") require(SELECTED_LIVE not in (SELECTED_PIN, SELECTED_ACCEPTED), "live checker was already admitted") @@ -102,7 +120,7 @@ def main(): # live successor, not a broken comparison. require(SELECTED_PIN in (SELECTED_PIN, *entry["accepted_live_sha256"]), "pin membership control failed") - require(reject(checker, entry) == REJECTIONS[SELECTED_PATH][1], + require(reject(root, checker, entry) == REJECTIONS[SELECTED_PATH][1], "selected checker rejection text changed") counts = {path: 0 for path in REJECTIONS} @@ -110,7 +128,7 @@ def main(): for _name, item in entries(checker): if item["path"] not in REJECTIONS: continue - message = reject(checker, item) + message = reject(root, checker, item) counts[item["path"]] += 1 messages.setdefault(item["path"], message) for path, (count, message) in REJECTIONS.items(): @@ -118,20 +136,31 @@ def main(): require(messages[path] == message, "rejection text changed for " + path) require(sum(counts.values()) == 19, "rejection total changed") ci = [item for _name, item in entries(checker) if item["path"] == CI_PATH] - require(len(ci) == 1 and hashlib.sha256((ROOT / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, + require(len(ci) == 1 and hashlib.sha256((root / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, "selected CI note digest changed") diff = subprocess.check_output( - ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=ROOT, text=True) + ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=root, env=env, text=True) changed = sorted(name for name in diff.splitlines() if name) require(changed == CHANGED, "inspected commit diff changed") - sys.path.insert(0, str(ROOT / "scripts")) - from research_package import plan_details - details = plan_details(ROOT, set(changed)) + planner = load_module(root / "scripts/research_package.py") + details = planner.plan_details(root, set(changed)) require([row["package"] for row in details] == PLAN_PACKAGES, "helper plan selection changed") matched = {name for row in details for names in row["causes"].values() for name in names} require(sorted(set(changed) - matched) == UNMATCHED, "unmatched plan paths changed") - require(plan_details(ROOT, set()) == [], "empty change set selected a package") + require(planner.plan_details(root, set()) == [], "empty change set selected a package") + + +def main(): + require(not sys.flags.optimize, "assertions must stay enabled") + sources = json.loads(Path(__file__).with_name("SOURCES.json").read_bytes()) + require(sources["base_commit"] == INSPECTED, "historical checkout base changed") + runner = load_module(ROOT / "scripts/research_package.py") + env = runner.git_source_env() + with tempfile.TemporaryDirectory(prefix="historical-selected-replay-") as temporary: + snapshot = Path(temporary) / "snapshot" + checkout_snapshot(snapshot, sources, runner, env) + check_snapshot(snapshot, env) print("PASS_HISTORICAL_SELECTED_REPLAY_GAP") print("selected_checker_live=" + SELECTED_LIVE) print("rejections=19 distinct_paths=7 plan_packages=9") diff --git a/research/p104-rank-eight-residual-closure/README.md b/research/p104-rank-eight-residual-closure/README.md new file mode 100644 index 0000000000..21c1784f00 --- /dev/null +++ b/research/p104-rank-eight-residual-closure/README.md @@ -0,0 +1,125 @@ +# Exact closure of the fixed-paid P104 rank-eight split + +**No verified κ gain.** This package closes the 29 cases left open by +[#7363](https://github.com/CrocSwap/integer-mult-bounds/pull/7363). The full +frozen census now excludes **326 of 326** public banks for one productive +rank-eight split into 4+4. Four new exact checks suffice; the other 25 cuts +are linked to exact checks by certified reversible changes of coordinates. + +The literal paid itinerary is held fixed to +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334), with +[#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113)'s signed +caller and the same 15 productive roles from chart 3 to chart 245. The +intermediate bank is public on chart 242, 772 or 1091; public axes outside +the productive cohort may take part in the bank, but prefix and suffix +endpoint images must be supported on the cohort. Original owned fields keep +their operations and stay outside the chosen public bank. The [signed price +replay](https://github.com/CrocSwap/integer-mult-bounds/pull/7363) has +110,519 paid positions and 22,461 targets before editing. In its directed +units the optimistic gross credit for one split is about 0.342 at the +comparator; one extra rank-one paid position would erase it. No edited +word or caller was constructed. The conditional comparator κ stays +0.00364665195644, the repository's selected κ stays 0.00363005817, and the +contribution's Δκ is zero. + +## Exact result + +Each key is (event index, chart), with the cut **before** the indexed event. + +| New exact key | Prefix / suffix exterior rank | Productive prefix / suffix image dimensions | Obstruction | Residual cuts covered | +| --- | ---: | ---: | --- | ---: | +| (45270, 242) | 17 / 17 | 1 / 1 | Both pairing matrices are zero | 2 | +| (45277, 242) | 18 / 18 | 1 / 1 | Both pairing matrices are zero | 1 | +| (45435, 242) | 19 / 19 | 1 / 1 | Both pairing matrices are zero | 7 | +| (45676, 1091) | 25 / 24 | 0 / 2 | Every pure prefix has zero productive image | 11 | + +The eight other residual cuts transfer to three exact zero-pairing seeds +already checked by #7363: (40243, 242), (41740, 242) and (45266, 242). +Thus the partition is 8 inherited by transfer plus 21 covered by the four +new checks; 25 of these 29 keys use a transfer. Together with the 297 +predecessor exclusions, this covers the whole census. + +For a verified interval on a fixed public bank, let `P_i` map initial +coordinates to bank coordinates at cut `i`; let `S_i` map a perturbation +supported on that bank to the final coordinates. Every operation in the +interval is either disjoint from the bank or an invertible public ADD or +SCALE within it. If their bank matrix is `M`, then `P_2 = M P_1` and +`S_1 = S_2 M`. With cut row `a` and cut column `b`, the bijections +`a_1 = a_2 M` and `b_2 = M b_1` preserve both endpoint images +(`a_i P_i`, `S_i b_i`) and the cut pairing `a_i b_i`. Thus they +preserve both the support test and every pairing test, including the +absence of a nonzero productive prefix. The verifier checks every event +in each interval, reconstructs the chart and owned lifecycle, builds +`M` and its inverse over the rationals, and checks both products. It +rejects mixed contacts, bank COPY and zero SCALE. In particular event +45675 reads owned role 1564 into the public bank; the cut at 45676 is +checked directly rather than transferred across that event. + +At each new representative, the pinned backward covector / forward +impulse trace and the pinned full forward / reverse trace reconstruct +the exact coefficient and endpoint-image spaces separately. The verifier +compares canonical row spaces of the stacked coefficients and images, +checks both pairing matrices, and runs the inherited positive and +negative pairing controls. These are two trace paths on the same +source and arithmetic model, not two independently sourced words. +A synthetic nonidentity bank transform also tests the transfer check. + +## Reproduce + +Run with CPython 3.12 and the standard library. The same command works +from a Git-free export: + +```sh +python3.12 -I -B replay.py --output RESULT.json +``` + +The output file must be new; omit `--output` for the registered replay. +The wrapper validates the retained source before extraction, reproduces +#7363's 17 original receipts and then regenerates the complete residual +receipt (all four exact forms and all 25 transfer matrices and inverses). +Its SHA256 is +`bd130ab860c7c605c47059d4a3e43852608acc2d31ffa7c9f80799b88600bc6e`. +A changed source bundle is a failure control. No network, Lean, or +unbounded search is needed. + +The retained source is the unchanged `research/p104-rank-eight-fixed-paid-bank-bound` +subtree (Git tree `ff3642284311ba255be219e5828defd044d215f6`) of +[#7363 at a0502b0](https://github.com/CrocSwap/integer-mult-bounds/tree/a0502b0b30a4a4a0e9a37c08e83febbd515c5955/research/p104-rank-eight-fixed-paid-bank-bound). +The tar is retained because the exact prior replay produces the original +297 exclusions used by this package; it avoids reliance on a live PR ref +or a second package installation. Its SHA256 is +`a7b02b2dab1f5de4b81566b3d04627f543c7cf1264491013aa887675a914f37d`. +To authenticate separately, fetch `refs/pull/7363/head` from the canonical +repo, confirm the stated commit, and compare the extracted subtree to +`git archive --format=tar a0502b0b30a4a4a0e9a37c08e83febbd515c5955 research/p104-rank-eight-fixed-paid-bank-bound`. +The unchanged caller and paid word are pinned at +`07a76c5e2738882c0cb322278e56f6cae3c9885d` and +`aaeec8c0acf01e99a5f331ef363a698d9c084ace`, respectively. +[SOURCES.json](SOURCES.json) records the canonical task and selected-record +provenance at base `e54523517d0f03e58352e647c403a5af3e525a57`. + +## Open next questions + +This exact scope is exhausted. Different paid itineraries, a bank using +owned fields, other helper cohorts, and multiple interacting edits remain +outside the result. The smallest follow-up is to price one separately +claimed and source-pinned route change with a neutral or compensating +paid delta before attempting an exact construction. There is no such +route or complete supplier in this package. See [TASK.json](TASK.json). + +## Credit + +ToikY's [#7363](https://github.com/CrocSwap/integer-mult-bounds/pull/7363) +supplies the frozen census and both trace implementations. +[#7367](https://github.com/CrocSwap/integer-mult-bounds/pull/7367) supplies +the reversible bank approach in the rank-seven cohort. +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) and +[#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) supply the +word and signed caller. [#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) +and [#7338](https://github.com/CrocSwap/integer-mult-bounds/pull/7338) supply +the directed price and admitted invoice, and +[#7314](https://github.com/CrocSwap/integer-mult-bounds/pull/7314) and +[#7319](https://github.com/CrocSwap/integer-mult-bounds/pull/7319) the +inherited helper census. See the retained predecessor's NOTICE for +additional credit. OpenAI Codex materially assisted this proof, +implementation, verification and packaging. diff --git a/research/p104-rank-eight-residual-closure/SOURCES.json b/research/p104-rank-eight-residual-closure/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-rank-eight-residual-closure/SOURCES.json @@ -0,0 +1,18 @@ +{ + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "path": "certificates/selected-result.json", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1", + "usage": "provenance" + }, + { + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "path": "docs/research/agent-task-catalog.json", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "usage": "provenance" + } + ], + "schema_version": 1 +} diff --git a/research/p104-rank-eight-residual-closure/TASK.json b/research/p104-rank-eight-residual-closure/TASK.json new file mode 100644 index 0000000000..3d28f02421 --- /dev/null +++ b/research/p104-rank-eight-residual-closure/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Close exactly the 29 unresolved pre-event/chart pairs from #7363 for a single literal fixed-paid rank-eight chart-3 to chart-245 4+4 split. Four new exact checks, with the other 25 cases linked by certified reversible public-bank transfers. No paid path or caller change.", + "ai_assistance": "OpenAI Codex materially assisted the proof, implementation, verification and packaging.", + "author": "Clear1nsight", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "A legal 4+4 split needs nonzero productive prefix and suffix images with a unit pairing on the same public bank and at the endpoints. The directed price is positive only before any added paid position. The exact closure rules out this fixed-paid, single-split route on the frozen source.", + "budget_minutes": 25, + "evidence": "Full #7363 predecessor replay reproduced all 17 receipts and 297 exclusions. Two exact traces agree on all four new representatives: three zero cut and endpoint pairings, one zero productive prefix. Explicit matrix/inverse certificates transfer the exclusion to the other 25 keys. All 326 frozen representatives are excluded.", + "open_questions": [ + { + "blocked_by": "No such route is supplied here. One added rank-one paid position erases the optimistic one-split credit, and changed routes need separate coordination and a full replay.", + "first_step": "Before construction, pin one source and one route change with a neutral or compensating signed paid delta; price the complete boundary and check the exterior kernels after its first changed event.", + "question": "Can a distinct legal paid itinerary create a productive pair without consuming the split's price allowance?", + "why_it_matters": "The fixed public-bank route is exhausted in this cohort. A changed itinerary has to improve the complete directed cost, not just produce a pair." + } + ], + "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": "Keeps #7363's changed literal chart-245 hypothesis and restricts new exact work to its frozen residual; #7367 supplies the reversible same-bank transfer idea for a different cohort.", + "scope_status": "changed", + "stop_rule": "Replay the immutable predecessor, then evaluate at most the four frozen new representatives with a 34-second deadline per exact engine. Certify transfers on the original tape. Stop without materialization when every representative is excluded.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-rank-eight-residual-closure/VERIFY.json b/research/p104-rank-eight-residual-closure/VERIFY.json new file mode 100644 index 0000000000..f5b299cc63 --- /dev/null +++ b/research/p104-rank-eight-residual-closure/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Replay the exact #7363 source to regenerate 17 predecessor receipts, certify 25 reversible public-bank transfers, compare two exact support and pairing reconstructions on four new cuts, and check the full residual receipt digest.", + "timeout_seconds": 175 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-rank-eight-residual-closure/check_residual.py b/research/p104-rank-eight-residual-closure/check_residual.py new file mode 100644 index 0000000000..189d324457 --- /dev/null +++ b/research/p104-rank-eight-residual-closure/check_residual.py @@ -0,0 +1,370 @@ +#!/usr/bin/env python3 +"""Complete #7363's residual using at most four new exact support evaluations. + +The transfer argument reuses ToikY's reversible bank method in #7367. +The two pinned trace and pairing implementations come from #7363. +""" + +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as Q +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path +from time import monotonic + +ROOT = Path(__file__).resolve().parent +SOURCE = "a0502b0b30a4a4a0e9a37c08e83febbd515c5955" +BASE = "e54523517d0f03e58352e647c403a5af3e525a57" +WORD_HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER_HEAD = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +PACKAGE = "research/p104-rank-eight-fixed-paid-bank-bound" +MANIFEST_SHA = "99aab01167c7306be2fa62281c225f3bf74fcfdadf107516d3253edd5e46d15a" +SEEDS = ((40243, 242), (41740, 242), (45266, 242)) +NEW = ((45270, 242), (45277, 242), (45435, 242), (45676, 1091)) +ANCHORS = SEEDS + NEW + + +def need(value, reason): + if not value: + raise ValueError(reason) + + +def digest(data): + return sha256(data).hexdigest() + + +def unique(pairs): + out = dict(pairs) + need(len(out) == len(pairs), "duplicate JSON key") + return out + + +def decode(data): + return json.loads(data, object_pairs_hook=unique) + + +def checked(path, expected): + data = path.read_bytes() + need(digest(data) == expected, f"source digest changed: {path.name}") + return data + + +def add(a, b, factor): + for k, v in b.items(): + z = a.get(k, 0) + factor * v + if z: + a[k] = z + else: + a.pop(k, None) + + +def as_text(v): + return {str(i): str(q) for i, q in sorted(v.items())} + + +def coord(v): + return {int(i): Q(x) for i, x in v.items()} + + +def dot(a, b): + return sum((q * b.get(i, 0) for i, q in a.items()), Q(0)) + + +def span(basis): + s = {0} + for x in basis: + need(x not in s, "independent chart basis") + s |= {x ^ y for y in s} + return s + + +def barrier(event, live, f, n): + """An event outside the bank is neutral; only internal public shears/scales may touch it.""" + op, r, *a = event + here = r < n and live[r] == f + if op == "MOVE": + return r < n and (here or a[1] == f) + if op in ("ADD", "COPY"): + src = a[0] + peer = src < n and live[src] == f + return (here or peer) if op == "COPY" else here != peer + if op == "SCALE": + return here and not Q(a[0]) + need(op in ("INIT", "CLEAR") and r >= n, "owned lifecycle") + return False + + +def layout(word, keys, cohort): + """Track actual coframes; collect public banks and start-of-epoch cuts.""" + n = word["public"] + live = word["initial"] + [None] * word["owned_fields"] + fs = {f for _, f in keys} + target = span(word["frames"][245]) + need(all(len(word["frames"][f]) == 4 and span(word["frames"][3]) < + span(word["frames"][f]) < target for f in fs), "rank-four geometry") + request = defaultdict(list) + for t, f in sorted(keys): + request[t].append(f) + epochs = dict.fromkeys(fs, 0) + facts, history = {}, {} + start, end = min(request), max(request) + for t, e in enumerate(word["program"]): + for f in request.get(t, ()): + here = [i for i, chart in enumerate(live) if chart == f] + facts[t, f] = {"key": [t, f], "public": [i for i in here if i < n], + "owned": [i for i in here if i >= n], + "pivots": sorted(cohort.intersection(here)), + "epoch": epochs[f]} + need(facts[t, f]["pivots"], "productive bank pivot") + op, r, *a = e + if start <= t < end: + history[t] = (live[r], live[a[0]] if op in ("ADD", "COPY") else None) + for f in fs: + if barrier(e, live, f, n): + epochs[f] = t + 1 + if op == "MOVE": + need(live[r] == a[0] and a[2] == (r >= n), "literal MOVE binding") + live[r] = a[1] + elif op == "INIT": + need(live[r] is None and r >= n, "literal INIT binding") + live[r] = a[0] + elif op == "CLEAR": + need(live[r] == a[0] and r >= n, "literal CLEAR binding") + live[r] = None + else: + need(live[r] == a[-1], "literal scalar binding") + if op in ("ADD", "COPY"): + need(live[a[0]] == live[r] and a[0] != r, "literal pair binding") + need(set(facts) == set(keys), "missing cut") + need(live == word["final"] + [None] * word["owned_fields"], "literal final chart vector") + return facts, history + + +def transfer(tape, history, old, new): + """Check the interval directly and construct both the basis change and its inverse.""" + start, f = old["key"] + end, other = new["key"] + bank = set(old["public"]) + need(f == other and old["public"] == new["public"] and start < end, "same-bank interval") + mat = {r: {r: Q(1)} for r in bank} + ops = [] + for t in range(start, end): + op, r, *a = tape[t] + dest_chart, src_chart = history[t] + if op == "MOVE": + need(r not in bank and not (not a[2] and f in a[:2]), "public MOVE across bank boundary") + elif op in ("ADD", "COPY"): + src = a[0] + if r in bank or src in bank: + need(op == "ADD" and r in bank and src in bank and + r != src and dest_chart == src_chart == f, "mixed or noninvertible bank contact") + q = Q(a[1]) + add(mat[r], mat[src], q) + ops.append((t, op, r, src, q)) + elif op == "SCALE" and r in bank: + q = Q(a[0]) + need(dest_chart == f and q != 0, "invertible bank scale") + mat[r] = {i: q * v for i, v in mat[r].items()} + ops.append((t, op, r, None, q)) + elif op in ("INIT", "CLEAR"): + need(r not in bank, "public lifecycle inside interval") + inv = {r: {r: Q(1)} for r in bank} + for _, op, r, src, q in reversed(ops): + if op == "ADD": + add(inv[r], inv[src], -q) + else: + inv[r] = {i: v / q for i, v in inv[r].items()} + for a, b in ((mat, inv), (inv, mat)): + for r, v in a.items(): + z = {} + for k, q in v.items(): + add(z, b[k], q) + need(z == {r: Q(1)}, "interval inverse") + return dict(chart=f, start=start, stop=end, + elementary_events=[list(tape[t]) + [t] for t, *_ in ops], + matrix={str(r): as_text(row) for r, row in sorted(mat.items())}, + inverse={str(r): as_text(row) for r, row in sorted(inv.items())}) + + +def paired_space(basis): + """Canonical row space of the cut coefficients stacked with productive image.""" + pivots = {} + for bank, image in basis: + row = {(0, i): q for i, q in bank.items()} | {(1, i): q for i, q in image.items()} + for p in sorted(pivots): + if row.get(p, 0): + add(row, pivots[p], -row[p]) + need(bool(row), "independent exact kernel basis") + p = min(row) + a = row[p] + row = {i: v / a for i, v in row.items()} + for old in pivots.values(): + if old.get(p, 0): + add(old, row, -old[p]) + pivots[p] = row + return sorted((i, sorted(v.items())) for i, v in pivots.items()) + + +def primary(word, banks, cohort, files, deadline): + rank = run_path(str(files / "inputs/paired_rank.py")) + paired = run_path(str(files / "inputs/paired_support.py")) + controls = paired["controls"]() + by_time = {k[0]: row["public"] for k, row in banks.items()} + f = rank["side"](word, by_time, cohort, deadline, False) + r = rank["side"](word, by_time, cohort, deadline, True) + need(set(f) == set(r) == set(by_time), "primary trace timed out or missed a cut") + answer = {} + for (t, chart) in banks: + a, b = f[t], r[t] + hit = paired["paired"](a, b, deadline) if any(c for _, c in a) and any(d for _, d in b) else None + answer[t, chart] = (a, b, hit) + return answer, controls + + +def checks(): + # Same-bank invertible shear and scale; a transfer into an outside role must fail. + a = {"key": [0, 0], "public": [0, 1]} + b = {"key": [2, 0], "public": [0, 1]} + program = [["ADD", 0, 1, "-2", 0], ["SCALE", 1, "3/2", 0]] + info = {0: (0, 0), 1: (0, None)} + good = transfer(program, info, a, b) + need(good["matrix"] == {"0": {"0": "1", "1": "-2"}, "1": {"1": "3/2"}}, "transfer control") + for replacement, msg in [(["ADD", 2, 1, "-2", 0], "mixed or noninvertible"), + (["COPY", 0, 1, "-2", 0], "mixed or noninvertible"), + (["SCALE", 0, "0", 0], "invertible bank scale")]: + try: + transfer([replacement, program[1]], info, a, b) + except ValueError as err: + need(msg in str(err), "wrong control rejection") + else: + raise ValueError("unsafe transfer accepted") + return ["shear_and_scale_inverse", "mixed_bank_contact", "copy_inside_bank", "zero_scale"] + + +def run(files, receipts): + need(__debug__, "run with assertions enabled") + pins = decode(checked(files / "LOCAL-PINS.json", MANIFEST_SHA)) + for rel, pin in pins.items(): + checked(files / rel, pin) + fixed = decode((files / "receipts/SHA256.json").read_bytes()) + price = decode(checked(receipts / "input/price/PRICE.json", fixed["input/price/PRICE.json"])) + remaining = [tuple(x) for x in decode((files / "receipts/UNRESOLVED.json").read_bytes())] + need(len(remaining) == len(set(remaining)) == 29 and set(NEW) <= set(remaining) and + not set(SEEDS) & set(remaining), "frozen residual denominator") + need((price["head"], price["caller"]) == (WORD_HEAD, CALLER_HEAD) and + price["productive_delta"] == {"4": 34, "8": -17} and price["paid_delta"] == {} and + 0 < Q(price["at_incumbent"]["gross_one"][1]) < 1, "inherited one-split economics") + cohort = set(price["cohort"]) + word = decode(decompress((files / "inputs/7334-WORD.json.gz").read_bytes())) + need(len(cohort) == 15 and len(word["program"]) == 76466 and + all((word["initial"][i], word["final"][i]) == (3, 245) for i in cohort), "frozen cohort") + geometry = decode(checked(receipts / "input/lead/GEOMETRY.json", fixed["input/lead/GEOMETRY.json"])) + need(geometry["eligible_bank_count"] == 326 and + set(remaining) <= {tuple(k) for k in geometry["all_representative_keys"]}, "frozen geometry denominator") + past = {} + for rel in ("independent/RESULT.json", "independent/FOLLOWUP.json"): + inherited = decode(checked(receipts / rel, fixed[rel])) + need(not inherited["timeout"] and not inherited["selected_unvisited"], "inherited exact receipt") + for row in inherited["results"]: + k = tuple(row["key"]) + if k in SEEDS: + need(row["status"] == "no_exact_unit_pair" and + row["cut_pairing_matrix"] == row["endpoint_pairing_matrix"] == [["0"]], + "inherited zero pair") + past[k] = row + need(set(past) == set(SEEDS), "exact predecessor controls") + stock = decode(checked(receipts / "lead/CONTINUATION.json", fixed["lead/CONTINUATION.json"])) + modular = {tuple(x["key"]): x for x in stock["rows"]} + facts, history = layout(word, set(remaining) | set(SEEDS), cohort) + groups = defaultdict(list) + for key, row in facts.items(): + groups[key[1], row["epoch"]].append(key) + anchors = {} + for group, keys in groups.items(): + seeds = sorted(set(keys) & set(SEEDS)) + keep = seeds[0] if seeds else min(keys) + need(keep in ANCHORS and keep == min(keys), "frozen representative selection") + anchors[keep] = sorted(k for k in keys if k in remaining) + need(set(anchors) == set(ANCHORS), "four new independent classes and three inherited classes") + controls = checks() + certificate = {} + for key, keys in anchors.items(): + a = facts[key] + certificate[key] = { + "anchor": list(key), "source": "inherited" if key in SEEDS else "new", "residual_keys": [list(k) for k in keys], + "bank": a, "transfers": [transfer(word["program"], history, a, facts[k]) for k in keys if k != key], + } + if key in past: + need(all(a[k] == past[key][k] for k in ("key", "public", "owned", "pivots")), "inherited live bank") + + # The positive 35-second allowance is per engine as in #7363. + banks = {k: facts[k] for k in NEW} + first, primary_controls = primary(word, banks, cohort, files, monotonic() + 34) + exact = run_path(str(files / "engines/rational/exact_six.py")) + rational = run_path(str(files / "engines/rational/r97_independent.py")) + independent_controls = exact["checks"]() + deadline = monotonic() + 34 + independent = exact["trace"](word, [banks[k] for k in NEW], deadline) + evidence = [] + dispositions = dict.fromkeys(SEEDS, "no_exact_unit_pair") + for k, (p, s) in zip(NEW, independent, strict=True): + data = banks[k] + m = modular[k] + need(m["status"] == "dual_drop", "upstream modular residual") + need(all(m[side][fld] == data[fld] for side in ("prefix", "suffix") + for fld in ("public", "owned", "pivots")), "independently rebound bank") + row = rational["evaluate"](exact, data, p, s, cohort, deadline) + fa, fb, candidate = first[k] + aa = [(coord(x["a"]), coord(x["c"])) for x in row["prefix_pure_basis"]] + bb = [(coord(x["b"]), coord(x["d"])) for x in row["suffix_pure_basis"]] + need(paired_space(aa) == paired_space(fa) and paired_space(bb) == paired_space(fb), + "independent exact stacked kernel spaces disagree") + need(bool(candidate) == (row["status"] == "exact_unit_pair"), "independent pairing decision") + need(row["cut_pairing_matrix"] == [[str(dot(a, b)) for b, _ in bb] for a, _ in aa] and + row["endpoint_pairing_matrix"] == [[str(dot(c, d)) for _, d in bb] for _, c in aa], + "separately recomputed pairing forms") + evidence.append(row) + dispositions[k] = row["status"] + + coverage = {k: dispositions[a] for a, cases in anchors.items() for k in cases} + need(set(coverage) == set(remaining) and sum(map(len, anchors.values())) == 29, + "complete residual coverage with no duplicate") + for k, v in certificate.items(): + v["disposition"] = dispositions[k] + positives = [list(k) for k in NEW if dispositions[k] == "exact_unit_pair"] + return { + "source_head": SOURCE, "canonical_main": BASE, "word_head": WORD_HEAD, "caller_head": CALLER_HEAD, + "new_case_cap": 4, "new_case_count": len(evidence), "dispositions_by_new_case": Counter(dispositions[k] for k in NEW), + "residual_in": 29, "residual_covered_by_inherited": sum(len(anchors[k]) for k in SEEDS), + "residual_covered_by_new_exact_checks": sum(len(anchors[k]) for k in NEW), + "transfers": sum(len(row["transfers"]) for row in certificate.values()), + "frozen_representative_count": 326, "excluded_total": 297 + sum(v != "exact_unit_pair" for v in coverage.values()), + "positive_representatives": positives, + "physical_materialization_or_kappa_gain_claimed": False, + "controls": controls, "primary_pairing_controls": primary_controls, + "independent_pairing_controls": independent_controls, + "classes": [certificate[k] for k in sorted(certificate)], "new_exact": evidence, + } + + +def main(): + parser = ArgumentParser(description=__doc__) + parser.add_argument("--source", type=Path, default=ROOT / "exact7363" / PACKAGE) + parser.add_argument("--receipts", type=Path, default=ROOT / "evidence/predecessor") + parser.add_argument("--out", type=Path, required=True) + args = parser.parse_args() + report = run(args.source, args.receipts) + with args.out.open("x") as out: + json.dump(report, out, indent=2, sort_keys=True) + out.write("\n") + print("PASS_P104_RANK_EIGHT_RESIDUAL", json.dumps({ + k: report[k] for k in ("new_case_count", "dispositions_by_new_case", "residual_in", + "transfers", "excluded_total", "positive_representatives") + }, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-rank-eight-residual-closure/predecessor.tar.gz b/research/p104-rank-eight-residual-closure/predecessor.tar.gz new file mode 100644 index 0000000000..f7220aa1e6 Binary files /dev/null and b/research/p104-rank-eight-residual-closure/predecessor.tar.gz differ diff --git a/research/p104-rank-eight-residual-closure/replay.py b/research/p104-rank-eight-residual-closure/replay.py new file mode 100644 index 0000000000..58f1388989 --- /dev/null +++ b/research/p104-rank-eight-residual-closure/replay.py @@ -0,0 +1,75 @@ +#!/usr/bin/env python3 +"""Replay the retained #7363 source and its exact residual without Git or network.""" + +from argparse import ArgumentParser +from hashlib import sha256 +from io import BytesIO +from pathlib import Path, PurePosixPath +import subprocess +import sys +import tarfile +from tempfile import TemporaryDirectory + +HERE = Path(__file__).resolve().parent +PACKAGE = PurePosixPath("research/p104-rank-eight-fixed-paid-bank-bound") +SOURCE_SHA = "a7b02b2dab1f5de4b81566b3d04627f543c7cf1264491013aa887675a914f37d" +RESULT_SHA = "bd130ab860c7c605c47059d4a3e43852608acc2d31ffa7c9f80799b88600bc6e" + + +def check(data, expected): + if sha256(data).hexdigest() != expected: + raise ValueError("pinned SHA256 mismatch") + return data + + +def extract(raw, dest): + with tarfile.open(fileobj=BytesIO(raw), mode="r:gz") as archive: + entries = archive.getmembers() + seen = set() + for entry in entries: + path = PurePosixPath(entry.name) + if (path in seen or path.is_absolute() or ".." in path.parts + or "\\" in entry.name or ":" in entry.name + or (not path.is_relative_to(PACKAGE) + and not (entry.isdir() and path in PACKAGE.parents)) + or not (entry.isdir() or entry.isfile())): + raise ValueError(f"unexpected retained source path: {entry.name}") + seen.add(path) + archive.extractall(dest, members=entries, filter="data") + + +def run(script, *args, timeout): + subprocess.run([sys.executable, "-I", "-B", str(script), *map(str, args)], + check=True, timeout=timeout) + + +def main(): + parser = ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="write the full residual receipt to a new file") + args = parser.parse_args() + if not __debug__: + parser.error("run with assertions enabled") + raw = check((HERE / "predecessor.tar.gz").read_bytes(), SOURCE_SHA) + try: + check(raw[:-1] + bytes([raw[-1] ^ 1]), SOURCE_SHA) + except ValueError: + pass + else: + raise ValueError("changed source bundle accepted") + with TemporaryDirectory(prefix="p104-rank-eight-residual-") as tmp: + dest = Path(tmp) + extract(raw, dest) + source = dest / PACKAGE + receipts, result = dest / "receipts", dest / "RESULT.json" + run(source / "replay.py", "--output", receipts, timeout=90) + run(HERE / "check_residual.py", "--source", source, "--receipts", receipts, + "--out", result, timeout=75) + data = check(result.read_bytes(), RESULT_SHA) + if args.output: + with args.output.open("xb") as out: + out.write(data) + print(f"PASS_P104_RANK_EIGHT_RESIDUAL_RECEIPT sha256={RESULT_SHA}") + + +if __name__ == "__main__": + main()