From bb36fc65ee0b161229169505f4840c436c5ca2b9 Mon Sep 17 00:00:00 2001 From: Clear1nsight <22630354+Clear1nsight@users.noreply.github.com> Date: Wed, 11 Nov 2026 14:22:27 +1100 Subject: [PATCH 1/3] Reuse #7147 selected replay navigation for onboarding This is the exact documentation prerequisite retained by #7156. It points the onboarding check to the selected #7000/#7001 review. Credit to Rohan Arun and the source authors. --- docs/ci-verification.md | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) 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). From d2e54af81f9dda6487636b79d4964a2385d89b2b Mon Sep 17 00:00:00 2001 From: Clear1nsight <22630354+Clear1nsight@users.noreply.github.com> Date: Wed, 11 Nov 2026 21:53:51 +1100 Subject: [PATCH 2/3] Replay the historical selected check at its inspected commit MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The PR #6292 rejection census and package plan are statements about 2485805. Load its exact sources and planner in a private sparse checkout, keeping all source hashes, 19 expected rejections, nine package selections and the empty-plan control. Subsequent edits to the live Makefile and CI guide no longer invalidate this historical check. The original audit is by unpaidmoon, building on Dennis’s historical replay gate. The pinned repository view follows the precedent of Matarener’s PR #5434. Repair prepared with substantial OpenAI Codex assistance. --- .../historical-selected-replay-gap/README.md | 6 +- .../SOURCES.json | 60 +++++++++--------- .../VERIFY.json | 31 +-------- .../historical-selected-replay-gap/verify.py | 63 ++++++++++++++----- 4 files changed, 82 insertions(+), 78 deletions(-) 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") From da481f3d12bf0a346a82411bddd9e075d72ed3db Mon Sep 17 00:00:00 2001 From: Clear1nsight <22630354+Clear1nsight@users.noreply.github.com> Date: Thu, 12 Nov 2026 00:21:14 +1100 Subject: [PATCH 3/3] Archive fixed-output validation of PR #7244 --- .../README.md | 25 ++ .../RECEIPT.json | 169 ++++++++++ .../check.py | 300 ++++++++++++++++++ 3 files changed, 494 insertions(+) create mode 100644 research/p104-two-cut-fixed-output-crosscheck/README.md create mode 100644 research/p104-two-cut-fixed-output-crosscheck/RECEIPT.json create mode 100644 research/p104-two-cut-fixed-output-crosscheck/check.py diff --git a/research/p104-two-cut-fixed-output-crosscheck/README.md b/research/p104-two-cut-fixed-output-crosscheck/README.md new file mode 100644 index 0000000000..cc0beebc13 --- /dev/null +++ b/research/p104-two-cut-fixed-output-crosscheck/README.md @@ -0,0 +1,25 @@ +# Fixed-output validation of #7244 + +This archive records the cross-check of [#7244](https://github.com/CrocSwap/integer-mult-bounds/pull/7244) at `215f67247f395c0e15f5ea3980f6a3e4aed155af` against the #7161 scientific commit `e3f8d39c43b07063dfc5b800f71c5d21015259e6`. Both use the signed #7113 caller at `07a76c5e2738882c0cb322278e56f6cae3c9885d`. The checker and receipt are byte-identical to the [original evidence export](https://github.com/Clear1nsight/integer-mult-bounds/tree/db81f377beac072c16d7fa2c6e2bc5f9b5781c7b/research/p104-two-cut-fixed-output-crosscheck). + +The [receipt](RECEIPT.json) records exact scalar endpoints and a dirty COPY control, the [#7245](https://github.com/CrocSwap/integer-mult-bounds/pull/7245) census on both words, the complete 17-stage rank counts and directed rational price intervals. Both words have full row rank in all 2,229 quotient classes and all 978 target classes, with zero contact-free MOVE pairs. The verified conditional κ of 0.003645372367832 uses the changed productive fields and charges both new exits at every stage. [#7246](https://github.com/CrocSwap/integer-mult-bounds/pull/7246) addresses a complementary decoder that crosses target classes. + +## Reproduction + +Fetch the exact public source commits into the checkout. Use CPython 3.12 with assertions. The checker uses the pinned main-branch Clifford classifier and implements its own exact scalar replay, elimination modulo 65,521, invoice count and directed price arithmetic. The committed JSON records the SHA-256 digests of the input words, caller and classifier. The archive uses a manual replay because the exact candidate and caller come from public PR commits. + +```sh +git fetch --no-tags https://github.com/CrocSwap/integer-mult-bounds.git \ + e3f8d39c43b07063dfc5b800f71c5d21015259e6 \ + 07a76c5e2738882c0cb322278e56f6cae3c9885d \ + 215f67247f395c0e15f5ea3980f6a3e4aed155af +GIT_NO_REPLACE_OBJECTS=1 python3.12 -I -B \ + research/p104-two-cut-fixed-output-crosscheck/check.py . > /tmp/p104-7244-cross-check.json +cmp /tmp/p104-7244-cross-check.json research/p104-two-cut-fixed-output-crosscheck/RECEIPT.json +``` + +## Open next questions + +Use this replay alongside the registered #7244 replay to review the conditional frontier proposal. Maintainer selection and independent human or formal review of the [five retained assumptions](https://github.com/Clear1nsight/integer-mult-bounds/blob/215f67247f395c0e15f5ea3980f6a3e4aed155af/research/p104-two-cut-funded-split/PROPOSED-CLAIM.json) remain open. The [frontier review discussion](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19542237) records the handoff. + +Credit ToikY for #7245 and #7246, Clear1nsight and the retained #7161/#7244 lineages, Rohan Arun for #7113, and the canonical Clifford authors. Prepared for Clear1nsight with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/p104-two-cut-fixed-output-crosscheck/RECEIPT.json b/research/p104-two-cut-fixed-output-crosscheck/RECEIPT.json new file mode 100644 index 0000000000..d065433579 --- /dev/null +++ b/research/p104-two-cut-fixed-output-crosscheck/RECEIPT.json @@ -0,0 +1,169 @@ +{ + "census": { + "after": { + "signed_quotients": { + "classes": 2229, + "exact_defects": [], + "maximum_size": 48, + "modular_full_classes": 2229 + }, + "target_cosets": { + "classes": 978, + "exact_defects": [], + "maximum_size": 1052, + "modular_full_classes": 978 + } + }, + "before": { + "signed_quotients": { + "classes": 2229, + "exact_defects": [], + "maximum_size": 48, + "modular_full_classes": 2229 + }, + "target_cosets": { + "classes": 978, + "exact_defects": [], + "maximum_size": 1050, + "modular_full_classes": 978 + } + }, + "contact_free_pairs": [ + 0, + 0 + ], + "moves": [ + 6279, + 6281 + ], + "prime": 65521 + }, + "heads": { + "after": "215f67247f395c0e15f5ea3980f6a3e4aed155af", + "base": "e54523517d0f03e58352e647c403a5af3e525a57", + "before": "e3f8d39c43b07063dfc5b800f71c5d21015259e6", + "caller": "07a76c5e2738882c0cb322278e56f6cae3c9885d" + }, + "invoice": { + "after": { + "P": { + "1": 68401, + "2": 14501, + "3": 14093, + "4": 3825, + "5": 5848, + "6": 238, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "T": { + "1": 306, + "2": 357, + "3": 799, + "4": 3808, + "5": 1360, + "6": 731, + "7": 323, + "8": 561, + "9": 10888, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208, + "137": 208 + }, + "paid": 110553, + "productive": 22461 + }, + "before": { + "P": { + "1": 68367, + "2": 14501, + "3": 14093, + "4": 3825, + "5": 5848, + "6": 238, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "T": { + "1": 289, + "2": 357, + "3": 799, + "4": 3791, + "5": 1343, + "6": 731, + "7": 323, + "8": 578, + "9": 10888, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208, + "137": 208 + }, + "paid": 110519, + "productive": 22427 + } + }, + "price": { + "at_lower_endpoint": [ + "0.0000000000000182338656538385248256", + "0.0000000000000182338656538385248257" + ], + "at_upper_endpoint": [ + "-0.0000000000000205373774348370202244", + "-0.0000000000000205373774348370202243" + ], + "candidate_crossing_bracket": [ + "0.0036453723678327048000", + "0.0036453723678327049000" + ], + "claim": "455671545979/125000000000000", + "new_at_test": [ + "0.0000000002461380849925665196973280", + "0.0000000002461380849925665196973281" + ], + "old_at_claim": [ + "-0.1870183852628409991294809242338744", + "-0.1870183852628409991294809242338743" + ], + "tested": "364537236783207/100000000000000000" + }, + "scalar_check": { + "closed_lifetimes_after": 70, + "dirty_copy_rejected": true, + "new_identity_rows": 2, + "old_output_rows_match": 1499 + }, + "sha256": { + "after": "75061d1e4b354e4cf36b690f30ddb2b257ed2f4e86509f87e17bb0f63eca126f", + "before": "c1caec11ca3ee264ef03018dd91037eac10c3e28950c4c525ee1b4bf5ee210e2", + "caller": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "tableau": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38" + } +} diff --git a/research/p104-two-cut-fixed-output-crosscheck/check.py b/research/p104-two-cut-fixed-output-crosscheck/check.py new file mode 100644 index 0000000000..a05e8ce3a9 --- /dev/null +++ b/research/p104-two-cut-fixed-output-crosscheck/check.py @@ -0,0 +1,300 @@ +"""Recount the pinned signed caller and apply the fixed-output census to both words. + +Run with Python 3.12 and a Git repository containing the named commits. The +Clifford tableau classifier is reused from main. Scalar replay, elimination, +invoice reconstruction, and directed price arithmetic are local to this check. +""" + +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction +from functools import cache +import gzip +from hashlib import sha256 +import json +from pathlib import Path +from subprocess import check_output + + +BASE = "e54523517d0f03e58352e647c403a5af3e525a57" +BEFORE = "e3f8d39c43b07063dfc5b800f71c5d21015259e6" +AFTER = "215f67247f395c0e15f5ea3980f6a3e4aed155af" +CALLER = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +PACKAGE = "research/p104-two-cut-funded-split" +PRIME = 65521 + + +def git_bytes(repo, commit, path): + return check_output(["git", "-C", str(repo), "show", f"{commit}:{path}"]) + + +def span(vectors): + members = {0} + for value in vectors: + members.update(value ^ x for x in tuple(members)) + return frozenset(members) + + +parse = cache(Fraction) + + +def replay(word, spaces): + n = word["public"] + chart = word["initial"] + [None] * word["owned_fields"] + rows = [{r: Fraction(1)} for r in range(n)] + [None] * word["owned_fields"] + last_touch = {} + paid, moves, copies = Counter(), [], [] + contact_free = opens = closes = 0 + for t, (op, r, *args) in enumerate(word["program"]): + touched = (r,) + if op == "INIT": + assert r >= n and chart[r] is None + chart[r], rows[r] = args[0], {} + opens += 1 + elif op == "CLEAR": + assert r >= n and chart[r] == args[0] and rows[r] is not None + chart[r], rows[r] = None, None + closes += 1 + elif op == "MOVE": + source, target, owned = args + assert chart[r] == source and rows[r] is not None and owned == (r >= n) + assert spaces[source] < spaces[target] or owned and spaces[target] < spaces[source] + rank = abs(len(word["frames"][source]) - len(word["frames"][target])) + paid[rank] += 1 + contact_free += last_touch.get(r) == "MOVE" + moves.append((t, source, target, rows[r])) + chart[r] = target + elif op == "SCALE": + coefficient, frame = args + assert chart[r] == frame and rows[r] is not None + rows[r] = {i: value for i, x in rows[r].items() if (value := parse(coefficient) * x)} + else: + assert op in ("ADD", "COPY") + source, coefficient, frame = args + assert chart[r] == chart[source] == frame and rows[r] is not None and rows[source] is not None + touched = (r, source) + if op == "COPY": + if rows[r]: + raise ValueError(f"Dirty COPY destination at event {t}") + copies.append((t, r, source)) + result = rows[r].copy() + for i, x in rows[source].items(): + value = result.get(i, 0) + parse(coefficient) * x + if value: + result[i] = value + else: + result.pop(i, None) + rows[r] = result + last_touch.update((role, op) for role in touched) + assert chart == word["final"] + [None] * word["owned_fields"] + assert rows[n:] == [None] * word["owned_fields"] and opens == closes and len(copies) == 1 + return rows[:n], paid, moves, copies[0], contact_free, opens + + +@cache +def reduce_mod(x): + return x.numerator * pow(x.denominator, -1, PRIME) % PRIME + + +def rank(rows, modular): + basis = {} + for row in rows: + vector = {i: y for i, x in row.items() if (y := reduce_mod(x) if modular else x)} + while vector: + lead = min(vector) + if lead not in basis: + basis[lead] = vector + break + pivot = basis[lead] + multiple = vector[lead] * pow(pivot[lead], -1, PRIME) if modular else vector[lead] / pivot[lead] + for i, x in pivot.items(): + value = vector.get(i, 0) - multiple * x + if modular: + value %= PRIME + if value: + vector[i] = value + else: + vector.pop(i, None) + return len(basis) + + +def census(moves, source, frames): + interpreter = {"__name__": "pinned_clifford"} + exec(compile(source, "pinned native_verify.py", "exec"), interpreter) + circuits = [interpreter["frame"](frame, 9) for frame in frames] + adjoints = [interpreter["adjoint"](circuit) for circuit in circuits] + tableau = interpreter["tableau"] + cosets = [span(x | z << 9 for x, z, _ in tableau(inv)[9:]) for inv in adjoints] + + @cache + def quotient(f, g): + return tableau(adjoints[f] + circuits[g]) + + signed, targets = defaultdict(list), defaultdict(list) + for t, f, g, row in moves: + signed[quotient(f, g)].append((t, row)) + targets[cosets[g]].append((t, row)) + result = {} + for label, groups in (("signed_quotients", signed), ("target_cosets", targets)): + modular_full = 0 + exact_defects = [] + for group in groups.values(): + vectors = [row for _, row in group] + if rank(vectors, modular=True) == len(vectors): + modular_full += 1 + continue + exact = rank(vectors, modular=False) + if exact != len(vectors): + exact_defects.append({"size": len(vectors), "rank": exact, "events": [t for t, _ in group]}) + result[label] = {"classes": len(groups), "maximum_size": max(map(len, groups.values())), + "modular_full_classes": modular_full, "exact_defects": exact_defects} + return result + + +def invoice(word, native_paid, caller): + live = word["live"] + main = {*live, *(r + 112 for r in live), *word["hosted"]["X2"], *word["hosted"]["Y2"]} + assert len(main) == 400 + stages = [event[1] for event in caller["events"] if event[0] == "J"] + assert stages == list(range(1, 18)) == list(range(1, caller["stages"] + 1)) + productive = Counter() + for r, (f, g) in enumerate(zip(word["initial"], word["final"], strict=True)): + if r not in main: + difference = len(word["frames"][g]) - len(word["frames"][f]) + assert difference > 0 + productive[difference] += len(stages) + for spec in caller["types"].values(): + ports = len(spec["ports"]) + for sign, head, *bits in spec["diagonal"]: + assert (sign, head, len(bits)) == (-1, 0, len(stages)) and set(bits) <= {0, 1} + productive[1 + 8 * sum(bits)] += ports + paid = Counter({r: count * len(stages) for r, count in native_paid.items()}) + for event in caller["events"]: + if event[0] == "J": + continue + kind, op, _, *args = event + ports = len(caller["types"][kind]["ports"]) + if op == "QUERY": + paid[1] += ports + elif op in ("IDLE_ONE", "IDLE_ODD"): + paid[8 * len(args[0]) + int(op == "IDLE_ODD")] += ports + return productive, paid + + +def log_series(value): + # With 1 <= value <= 2, bound the remaining atanh series by a geometric tail. + x = (value - 1) / (value + 1) + square = x * x + term, total = x, Fraction(0) + for j in range(64): + total += term / (2 * j + 1) + term *= square + return 2 * total, 2 * (total + term / (129 * (1 - square))) + + +@cache +def log_bounds(n): + exponent = n.bit_length() - 1 + a, b = log_series(Fraction(n, 2**exponent)) + c, d = log_series(Fraction(2)) + scale = 10**49 + return Fraction((a + exponent * c) * scale // 1, scale), Fraction(-(-(b + exponent * d) * scale // 1), scale) + + +def exp_bounds(x): + # Alternating Taylor terms decrease for 0 <= x < 1. Degrees 31 and 32 enclose exp(-x). + assert 0 <= x < 1 + value = term = Fraction(1) + for degree in range(1, 32): + term *= -x / degree + value += term + return value, value - term * x / 32 + + +def moment(signed, k): + lo = hi = Fraction(0) + for r, count in signed.items(): + a, b = log_bounds(r) + lower = r * exp_bounds(k * b)[0] + upper = r * exp_bounds(k * a)[1] + lo += count * (lower if count >= 0 else upper) + hi += count * (upper if count >= 0 else lower) + return lo, hi + + +def interval_text(bounds, digits=34): + scale = 10**digits + integers = (bounds[0] * scale // 1, -(-bounds[1] * scale // 1)) + return [f"{'-' if value < 0 else ''}{abs(value) // scale}.{abs(value) % scale:0{digits}d}" for value in integers] + + +def main(repo): + raw = { + "before": git_bytes(repo, BEFORE, "research/p104-rank8-exit-funded-split/WORD.json.gz"), + "after": git_bytes(repo, AFTER, f"{PACKAGE}/WORD.json.gz"), + "caller": git_bytes(repo, CALLER, "research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json"), + "tableau": git_bytes(repo, BASE, "research/shared-wire-split-composition/frozen/native_verify.py"), + } + assert raw["before"] == git_bytes(repo, AFTER, f"{PACKAGE}/reference/WORD.json.gz") + assert sha256(raw["caller"]).hexdigest() == "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc" + assert sha256(raw["tableau"]).hexdigest() == "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38" + before, after = [json.loads(gzip.decompress(raw[name])) for name in ("before", "after")] + assert sha256(gzip.decompress(raw["after"])).hexdigest() == "56e1a5e60cecf14991b3169b4575f0b7388d48fa39f261d7a20c7627a8d9e540" + assert before["frames"] == after["frames"] and before["initial"] == after["initial"][:-2] + spaces = [span(frame) for frame in before["frames"]] + assert all(len(s) == 2**len(f) for s, f in zip(spaces, before["frames"], strict=True)) + old, new = replay(before, spaces), replay(after, spaces) + assert after["public"] == before["public"] + 2 + assert new[0] == old[0] + [{i: Fraction(1)} for i in range(before["public"], after["public"])] + t, dst, src = new[3] + dirty = dict(after, program=after["program"][:t] + [["ADD", dst, src, "1", after["program"][t][-1]]] + after["program"][t:]) + try: + replay(dirty, spaces) + except ValueError as error: + assert str(error) == f"Dirty COPY destination at event {t + 1}" + else: + raise AssertionError("Dirty COPY control was accepted") + caller = json.loads(raw["caller"]) + invoices = [invoice(word, result[1], caller) for word, result in ((before, old), (after, new))] + receipt = json.loads(git_bytes(repo, AFTER, f"{PACKAGE}/RESULT.json"))["price"] + signed = [] + for label, (productive, paid) in zip(("before", "after"), invoices, strict=True): + expected = receipt[label] + assert {str(r): count for r, count in productive.items()} == expected["T"] + assert {str(r): count for r, count in paid.items()} == expected["P"] + delta = productive.copy() + delta.subtract(paid) + assert sum(r * count for r, count in delta.items()) == expected["S"] == 1424 + signed.append(delta) + claim = parse(receipt["gate"]["claim"]) + tested = parse(receipt["gate"]["tested"]) + candidate_bracket = (parse("0.0036453723678327048"), parse("0.0036453723678327049")) + old_at_claim = moment(signed[0], claim) + new_at_test = moment(signed[1], tested) + at_low, at_high = [moment(signed[1], k) for k in candidate_bracket] + assert old_at_claim[1] < 0 < new_at_test[0] and at_high[1] < 0 < at_low[0] + rank_control = [{0: Fraction(1)}, {1: Fraction(1)}, {0: Fraction(2), 1: Fraction(3)}] + assert rank(rank_control[:2], True) == rank(rank_control, True) == rank(rank_control, False) == 2 + stock = [census(result[2], raw["tableau"], before["frames"]) for result in (old, new)] + assert stock[0]["signed_quotients"]["modular_full_classes"] == 2229 + assert stock[0]["target_cosets"]["modular_full_classes"] == 978 + return { + "heads": {"base": BASE, "before": BEFORE, "after": AFTER, "caller": CALLER}, + "sha256": {name: sha256(content).hexdigest() for name, content in raw.items()}, + "scalar_check": {"old_output_rows_match": before["public"], "new_identity_rows": 2, + "dirty_copy_rejected": True, "closed_lifetimes_after": new[5]}, + "census": {"prime": PRIME, "before": stock[0], "after": stock[1], + "moves": [len(old[2]), len(new[2])], "contact_free_pairs": [old[4], new[4]]}, + "invoice": {label: {"productive": sum(t.values()), "paid": sum(p.values()), "T": dict(t), "P": dict(p)} + for label, (t, p) in zip(("before", "after"), invoices, strict=True)}, + "price": {"claim": str(claim), "tested": str(tested), + "old_at_claim": interval_text(old_at_claim), "new_at_test": interval_text(new_at_test), + "candidate_crossing_bracket": interval_text(candidate_bracket, 22), + "at_lower_endpoint": interval_text(at_low), "at_upper_endpoint": interval_text(at_high)}, + } + + +if __name__ == "__main__": + parser = ArgumentParser(description=__doc__) + parser.add_argument("repo", type=Path) + print(json.dumps(main(parser.parse_args().repo), indent=2, sort_keys=True))