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-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))