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 b567f9a4f5699c5e447100c38b5745526b15b770 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 11 Nov 2026 16:09:48 -0800 Subject: [PATCH 3/3] Certify the fixed-cut Type A QUERY pair correction --- .../LOCAL-PINS.json | 16 + research/p104-type-a-query-fixed-cut/NOTICE | 6 + .../p104-type-a-query-fixed-cut/PHYSICAL.md | 17 + research/p104-type-a-query-fixed-cut/PROOF.md | 33 + .../PROVENANCE.json | 21 + .../p104-type-a-query-fixed-cut/README.md | 24 + .../p104-type-a-query-fixed-cut/SOURCES.json | 18 + .../p104-type-a-query-fixed-cut/TASK.json | 117 +++ .../VERIFICATION.md | 12 + .../p104-type-a-query-fixed-cut/VERIFY.json | 19 + .../engines/independent/formal_necessity.py | 132 ++++ .../engines/independent/gaussian_necessity.py | 177 +++++ .../engines/independent/symbolic_transport.py | 187 +++++ .../independent/transported_product.py | 201 ++++++ .../engines/lead/fixed_cut.py | 140 ++++ .../engines/lead/full_body.py | 135 ++++ .../engines/price/derivative_check.py | 67 ++ .../engines/price/quote.py | 141 ++++ .../inputs/7113-CALLER.json.gz | Bin 0 -> 11215 bytes .../inputs/7334-ADMITTED.json | 58 ++ .../inputs/7334-READBACK.json | 188 +++++ .../inputs/QUERY-CENSUS.json | 674 ++++++++++++++++++ .../inputs/pricing.py | 82 +++ .../receipts/SHA256.json | 10 + .../p104-type-a-query-fixed-cut/replay.py | 126 ++++ 25 files changed, 2601 insertions(+) create mode 100644 research/p104-type-a-query-fixed-cut/LOCAL-PINS.json create mode 100644 research/p104-type-a-query-fixed-cut/NOTICE create mode 100644 research/p104-type-a-query-fixed-cut/PHYSICAL.md create mode 100644 research/p104-type-a-query-fixed-cut/PROOF.md create mode 100644 research/p104-type-a-query-fixed-cut/PROVENANCE.json create mode 100644 research/p104-type-a-query-fixed-cut/README.md create mode 100644 research/p104-type-a-query-fixed-cut/SOURCES.json create mode 100644 research/p104-type-a-query-fixed-cut/TASK.json create mode 100644 research/p104-type-a-query-fixed-cut/VERIFICATION.md create mode 100644 research/p104-type-a-query-fixed-cut/VERIFY.json create mode 100644 research/p104-type-a-query-fixed-cut/engines/independent/formal_necessity.py create mode 100644 research/p104-type-a-query-fixed-cut/engines/independent/gaussian_necessity.py create mode 100644 research/p104-type-a-query-fixed-cut/engines/independent/symbolic_transport.py create mode 100644 research/p104-type-a-query-fixed-cut/engines/independent/transported_product.py create mode 100644 research/p104-type-a-query-fixed-cut/engines/lead/fixed_cut.py create mode 100644 research/p104-type-a-query-fixed-cut/engines/lead/full_body.py create mode 100644 research/p104-type-a-query-fixed-cut/engines/price/derivative_check.py create mode 100644 research/p104-type-a-query-fixed-cut/engines/price/quote.py create mode 100644 research/p104-type-a-query-fixed-cut/inputs/7113-CALLER.json.gz create mode 100644 research/p104-type-a-query-fixed-cut/inputs/7334-ADMITTED.json create mode 100644 research/p104-type-a-query-fixed-cut/inputs/7334-READBACK.json create mode 100644 research/p104-type-a-query-fixed-cut/inputs/QUERY-CENSUS.json create mode 100644 research/p104-type-a-query-fixed-cut/inputs/pricing.py create mode 100644 research/p104-type-a-query-fixed-cut/receipts/SHA256.json create mode 100644 research/p104-type-a-query-fixed-cut/replay.py diff --git a/research/p104-type-a-query-fixed-cut/LOCAL-PINS.json b/research/p104-type-a-query-fixed-cut/LOCAL-PINS.json new file mode 100644 index 0000000000..aca55d4fff --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/LOCAL-PINS.json @@ -0,0 +1,16 @@ +{ + "engines/independent/formal_necessity.py": "27295ea43d542ea661469d7bf17821eceba29e891fb26252668a2dc70a41697c", + "engines/independent/gaussian_necessity.py": "6aafe5d8fb8ba552c3bad0ea0caf30f037a11430f948758f2dd92b8b21690b03", + "engines/independent/symbolic_transport.py": "8e61e28d2e9d0bcfb8e06bb92b74bae7cfcec886a1adc332c555964760fc558e", + "engines/independent/transported_product.py": "ea1c4e1b1d11f3331bc8a1960779405bffe1839bc5542650f8829c9262244e3d", + "engines/lead/fixed_cut.py": "70de991b8443ed9d4f4455b9755743c6262379fd16adc68763048f5d34298fe3", + "engines/lead/full_body.py": "352c7d594f357333f027dc46eef0e82226b9552ab31d6890b1695fe994e8c3b4", + "engines/price/derivative_check.py": "348c8b2de72f1f112cb1337eca9d29ca96c85a7ad903beecafb1a2a1221f408e", + "engines/price/quote.py": "c492b3f1c566887d39d1a3d599c96cd25a042850fb209494b34bfeab09a5bf83", + "inputs/7113-CALLER.json.gz": "7e8038559cd158f6e32ef6d1a3bf15ab6a8ecc2239af32ab1699511ac28e26d9", + "inputs/7334-ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/7334-READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/QUERY-CENSUS.json": "ae9ae5116091dc73d10a5dad34a38eab7581ae26654ef30af8be0ffb1acbea5c", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "receipts/SHA256.json": "f8d0597520426c27c0f52483b69a93b00fb65e8484b023d1f621d39aec6e850d" +} diff --git a/research/p104-type-a-query-fixed-cut/NOTICE b/research/p104-type-a-query-fixed-cut/NOTICE new file mode 100644 index 0000000000..3578e99d78 --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/NOTICE @@ -0,0 +1,6 @@ +Apache-2.0. + +#7334 supplies the independently reproduced baseline, #7113 the exact signed caller, +#7298 the directed tariff, #7309 the four-QUERY census and relative phase gate, +and #7310 the separate changed-J exclusion. OpenAI Codex and subagents +materially assisted proof, implementation, replay and packaging. diff --git a/research/p104-type-a-query-fixed-cut/PHYSICAL.md b/research/p104-type-a-query-fixed-cut/PHYSICAL.md new file mode 100644 index 0000000000..6884a227e8 --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/PHYSICAL.md @@ -0,0 +1,17 @@ +# Physical admission for the formal correction + +The six-case replay computes the required fixed-cut correction at the two signs of q with all body values one. Its defect has rank two at q=−1 and rank zero at q=+1 for all six pairs. For (1580,1659), the rank-two coefficient matrix has the minor `[[0,1],[1,−1]]` in rows (0,19) and columns (1,18), before the common factor −2. + +## Serial one-return interface + +In the retained normalized caller, a single paid QUERY lowerer takes one arbitrary scalar field on a query scratch owner and returns one scalar field. Allow any linear q-even role setup and readout, including bypass and owned zero scratch, at the fixed cut. Fix the body variables. Factoring the prefix and suffix at the one input and one output writes the exterior map as `E(q²)+a(q²)D(q)b(q²)`. Here D is the single field response, b its source row, a its return column and E the bypass. At q=±1 the even factors coincide. On the corresponding normalized spectral lines the difference is `a(D(−1)−D(+1))b`, of rank at most one. The replayed rank two excludes this interface for each of the six pairs, including a higher Clifford rank on that same one-return field. Newly permitted within-field fibre mixing or a two-return compiler would need its own admission. + +The mixed sign alone has an ordinary algebraic correction. If L is the q-even `LAMBDA(+)`, then `L²=q²` and `q²(q−1)+(q²−1)=q⁻¹−1`. The extra ordinary shear can remove a mixed-sign obstruction under an explicitly expanded wrapper contract. It does not supply the second return of the serial QUERY interface. + +## Retained body J + +The signed J interpreter applies the two central shears and then a fresh body monomial to all four Type A roles. The compiled binding enumerates the literal 17 fresh stages, checks disjoint ownership on the ports and charges every nested MOVE and fresh helper target. The unit-body specialization is a necessary algebraic gate. The retained provider has no body-identity mode at this cut. Adding or repeating a literal J with its full body and helpers is a different invoice. + +See the exact [signed interpreter](https://github.com/CrocSwap/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/replay/supplier7112/short-caller/check_odd_caller_exact_grid.py) and [compiled binding](https://github.com/CrocSwap/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/replay/supplier7112/short-caller/upstream_application.py). Their SHA-256 values are respectively `abd5a5fd011b71e5b382cbc058855594d4f2fe7b049f375506675c0303180f54` and `d98987db98553dc55bfc80e3ca47abfcd51c57af6f8cda61101391d8eae94184`. + +A same-volume two-return provider with fully priced setup, routing, adjoint, erasure, precision and tape remains an open class. In a distinct incremental direction, keep an existing J and its paid stock while testing whether both QUERY changes can be absorbed into its relative phase action. The cheaper first test is the exact q=±1 relative rank for each pair and J host. diff --git a/research/p104-type-a-query-fixed-cut/PROOF.md b/research/p104-type-a-query-fixed-cut/PROOF.md new file mode 100644 index 0000000000..c732355e6f --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/PROOF.md @@ -0,0 +1,33 @@ +# Exact correction before the first changed QUERY + +Write A1,A2 for the phase-even replacements, Q1,Q2 for the original QUERYs, and B for the intervening chronological product. The required insertion is unique. + +```text +G = (A2 B A1)^(-1) Q2 B Q1 +``` + +Let E=e_0 e_1^T and δ=q^(-1)−1. As Q_j=A_j(I+δE), the correction factors as follows. + +```text +G = (I+δuv)(I+δE) +u = A1^(-1) B^(-1)e_0 +v = e_1^T B A1 +``` + +One engine applies the original and changed intervals on all 36 columns and inverts the changed interval. The independent engine transports u and v through literal elementary operations. All six corrections are identity at q=+1. At q=−1 and unit body, the squared defect ranks are 2, 1, 1, 2 respectively for (1516,1580), (1516,1659), (1580,1721), and (1659,1721). Two square-zero axes that mutually annihilate have square-zero sum. Those four pairs fail this provider class. + +For selected pair (1580,1659), exact symbolic transport over Gaussian rationals with q⁴=1 and 17 invertible formal body variables gives + +```text +u = -e_0 + 2(e_2 + ... + e_8) + e_19 +v = e_1^T - ((1+i)/2 + (1-i)q²/2)e_18^T +G = I + (q^(-1)−1)(E+uv) +``` + +The vectors have no body dependence. The contractions u_1, v_0, and vu vanish. The axes are independent, square to zero and mutually annihilate. An independent direct replay verifies all 36 basis columns at each Gaussian character with all body variables formal. The four characters distinguish q modulo q⁴−1, so this is an exact normalized operator identity. + +## Limited mixed-sign obstruction + +A direct provider with q-even wrappers, one nonzero inverse axis A and one nonzero forward axis B, and no separate ordinary q-even correction would give normalized defects A−iB and A+iB after division by q^(-1)−1 at q=i and q=−i. The selected witness has equal normalized defects at these characters. Thus B would be zero, which cannot provide rank two. + +A separate ordinary correction changes the hypothesis. The identity q²(q−1)+(q²−1)=q^(-1)−1 allows a q-even wrapper and a separate q-even correction to convert a forward phase. Its physical field volume, legal routes, restoration and complete price remain open. diff --git a/research/p104-type-a-query-fixed-cut/PROVENANCE.json b/research/p104-type-a-query-fixed-cut/PROVENANCE.json new file mode 100644 index 0000000000..5e28345e49 --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/PROVENANCE.json @@ -0,0 +1,21 @@ +{ + "files": { + "inputs/7113-CALLER.json.gz": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "git_blob": "9451ceaf6e8e037894680b549f3ef41c21b260d7", + "path": "research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json", + "sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json", + "uncompress": true + }, + "inputs/pricing.py": { + "commit": "c522451caf287bb3c16eaece72be4c263315dca4", + "git_blob": "40ec194017bda1d524bba4f07b188c53281419d0", + "path": "research/adjacent-owned-add-exchange-bound/pricing.py", + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/c522451caf287bb3c16eaece72be4c263315dca4/research/adjacent-owned-add-exchange-bound/pricing.py", + "uncompress": false + } + }, + "schema_version": 1 +} diff --git a/research/p104-type-a-query-fixed-cut/README.md b/research/p104-type-a-query-fixed-cut/README.md new file mode 100644 index 0000000000..86168401bb --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/README.md @@ -0,0 +1,24 @@ +# Fixed-cut Type A QUERY pair correction + +**NO VERIFIED GAIN. Exact conditional κ change 0%.** On independently replayed [#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) at `aaeec8c0acf01e99a5f331ef363a698d9c084ace`, κ `0.00364665195644`, test two of the four Type A QUERYs at clocks 1516, 1580, 1659 and 1721 in exact [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) `07a76c5e2738882c0cb322278e56f6cae3c9885d`. Replace two QUERYs by ordinary ADDs and insert one proposed same-volume rank-two correction before the first replacement. All 17 J blocks and other paid calls stay fixed. The scoped provider uses two commuting, mutually annihilating rank-one axes. + +Two exact unit-body implementations agree on all six pairs. At q=+1 the correction is identity. At q=−1 each defect has rank two. Four pairs have nonzero squared defect and fail the scoped shape. Pairs (1516,1721) and (1580,1659) provisionally pass. The one-pair formal cap selects (1580,1659). Two exact reconstructions verify its correction with all 17 body variables formal, including 36 columns at each of four Gaussian characters, 144 total. Pair (1516,1721) remains unresolved. No physical provider or modified multiplication bound is verified. See [PROOF.md](PROOF.md). + +One same-volume edit would change the complete 96-port paid bill by `P1−192,P2+96`, leaving productive targets fixed. The optimistic gross upper is about 0.484699135287 raw at the incumbent crossing. The hypothetical two-disjoint upper is about 0.969398270574. Both are below one extra paid rank-one position. The directed derivative certificate proves that with this debit both edited bills stay negative from the incumbent lower crossing through the retained BIT cap. The two-disjoint grant leaves more than 138.70 raw units of deficit at fixed κ `0.0040075385047236`. No compatible physical saving is certified. The [physical admission note](PHYSICAL.md) derives a rank obstruction for the retained serial one-return interface and identifies the mandatory body in the existing J. + +## Replay + +Use CPython 3.12 with assertions and the standard library. From a clean checkout: + +```sh +python3.12 -I -B research/p104-type-a-query-fixed-cut/replay.py +python3.12 -B scripts/research_package.py --package research/p104-type-a-query-fixed-cut +``` + +Use `--out` with a fresh path to retain the eight regenerated receipts. See [VERIFICATION.md](VERIFICATION.md) for pins and controls. + +## Open next questions + +Can a retained physical service supply both inverse-q axes at one rank-two field volume? Start with the directions in PROOF.md and the signed phase compiler. A mixed-sign service with q-even wrappers and no separate ordinary correction cannot implement it directly. A separately priced q-even correction may change this result. A physical candidate still needs all-width forward and adjoint, exact phase, coframes, ownership, restoration, paid and ordinary routing, compiler, precision, tape, caller and outer verification. The other provisional pair remains open. + +Credit #7334 for the admitted invoice, #7113 for the signed caller, #7298 for the directed tariff, #7309 for the four-query census and q-even obstruction, and #7310 for the distinct one-removal changed-J obstruction. OpenAI Codex and subagents materially assisted. diff --git a/research/p104-type-a-query-fixed-cut/SOURCES.json b/research/p104-type-a-query-fixed-cut/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/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-type-a-query-fixed-cut/TASK.json b/research/p104-type-a-query-fixed-cut/TASK.json new file mode 100644 index 0000000000..e3f90bf632 --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Exact #7334 and #7113, two Type A QUERY even replacements and one proposed same-volume fixed-cut correction. All six unit-body pairs, one full symbolic pair.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "Signed Type A QUERY correction research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Fuse two rank-one children into one rank-two job in the complete signed complex bill, if exact physical service and directed price pass.", + "budget_minutes": 8, + "evidence": "Four square obstructions, two unit-body provisionals, one exact 17-body-variable formal factor confirmed across 144 Gaussian Laurent columns, one unresolved at the cap. No physical candidate.", + "open_questions": [ + { + "blocked_by": "No verified provider, native ownership, precision, tape or signed application replay for this modified caller.", + "first_step": "Pin the actual provider contract and test two inverse axes, or an explicitly charged mixed-phase wrapper with an ordinary q-even correction.", + "question": "Can the retained same-volume service realize the two inverse-q axes at positive complete price?", + "why_it_matters": "The exact formal operator permits a conditional rank-one-pair fusion but lacks a physical and fully charged implementation." + } + ], + "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": "partial", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Direct source reuse is excluded. This tests a distinct signed phase factor by replacing two QUERYs and offering one rank-two service.", + "scope_status": "changed", + "stop_rule": "Six unit-body cases or 20 runner seconds, then one exact symbolic case or 90 runner seconds. No other symbolic case or physical candidate was built.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-type-a-query-fixed-cut/VERIFICATION.md b/research/p104-type-a-query-fixed-cut/VERIFICATION.md new file mode 100644 index 0000000000..10a1c9427c --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/VERIFICATION.md @@ -0,0 +1,12 @@ +# Exact replay coverage + +LOCAL-PINS.json pins paths. PROVENANCE.json gives the exact public #7113 caller and #7298 tariff objects. The #7334 readback and four-stage local admission pin the complete baseline. The #7309 census supplies the four clocks. + +The registered command regenerates eight SHA-256-bound receipts listed in receipts/SHA256.json. + +- PRICE and DERIVATIVE verify the full signed bill, crossing probes, retained BIT interval and the extra rank-one debit. +- DIRECT and UNIT agree on all six exact keys. Controls cover a disjoint two-axis defect, a linked defect and q=+1 identity. +- FORMAL-PROBES and GAUSSIAN check the selected pair at exact single-body specializations and all four q characters. +- SYMBOLIC propagates q mod 4 and all body exponents. FULL-BODY checks 144 arbitrary-input basis actions with all 17 variables formal and rejects a changed sign. The registered replay also rejects changed caller bytes. + +The unit-body gate exhausted six keys and the formal gate spent its one-key budget. Physical service, the modified caller, and a changed exponent remain unverified. diff --git a/research/p104-type-a-query-fixed-cut/VERIFY.json b/research/p104-type-a-query-fixed-cut/VERIFY.json new file mode 100644 index 0000000000..f5c0b8b19a --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Replay exact directed full-bill prices and derivative, six fixed-cut shape checks by two engines, and one exact Gaussian Laurent correction by two engines. Reject a changed caller.", + "timeout_seconds": 90 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-type-a-query-fixed-cut/engines/independent/formal_necessity.py b/research/p104-type-a-query-fixed-cut/engines/independent/formal_necessity.py new file mode 100644 index 0000000000..4d9ab4a745 --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/engines/independent/formal_necessity.py @@ -0,0 +1,132 @@ +"""Necessary fixed-axis test on the single R76 pair (1580, 1659).""" +from fractions import Fraction as Q +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from math import prod +from time import monotonic +import argparse +import runpy + +PAIR = (1580, 1659) +PRICE = "52e05b80069ce01cad3b8e5f3cf9123e930de36987bd398dd43f103953a4674a" +UNIT = "84049bddeed687a28954fa0b8bb993d676900b4eb86ebd6e54ca1f7c60e27887" +ENGINE = "ea1c4e1b1d11f3331bc8a1960779405bffe1839bc5542650f8829c9262244e3d" + + +def load(path, digest): + raw = path.read_bytes() + if sha256(raw).hexdigest() != digest: + raise ValueError("changed pinned file " + path.name) + return raw + + +def transpose(matrix): + result = {} + for i, row in matrix.items(): + for j, x in row.items(): + result.setdefault(j, {})[i] = x + return result + + +def compare(first, second, rank): + first_cols, second_cols = transpose(first), transpose(second) + stack = lambda a, b: dict(enumerate([*a.values(), *b.values()])) + return {"unit_rank": rank(first), "nonunit_rank": rank(second), + "joint_row_rank": rank(stack(first, second)), + "joint_column_rank": rank(stack(first_cols, second_cols))} + + +def nonunit_emit(engine, event, bodies, q, alpha, even): + family, op, *args = event + emitted = engine["emit"](event, q, alpha, even) + if family == "J": + d = bodies[op - 1] + if d != 1: + emitted.extend(("SCALE", role, role, d) for role in args[0]) + if family == "A" and op in ("IDLE_ODD", "IDLE_ONE"): + dst, mask, *_ = args + d = prod(bodies[i - 1] for i in mask) + if d != 1: + emitted.append(("SCALE", dst, dst, d)) + return emitted + + +def probe(engine, caller, q, bodies): + first, second = PAIR + events = caller["events"] + ty = caller["types"]["A"] + dest, source = events[first][2:4] + ops = [item for t in range(first, second) + for item in nonunit_emit(engine, events[t], bodies, q, Q(ty["alpha2"]), t == first)] + u, v = engine["transported"](ops, ty["roles"], dest, source) + N = engine["residual"](u, v, dest, source, Q(1, q) - 1) + return N, [str(v[dest]), str(u[source])] + + +def first_difference(first, second): + for i in sorted(first.keys() | second.keys()): + a, b = first.get(i, {}), second.get(i, {}) + for j in sorted(a.keys() | b.keys()): + if a.get(j, 0) != b.get(j, 0): + return [i, j, str(a.get(j, 0)), str(b.get(j, 0))] + return None + + +def main(args): + started = monotonic() + engine_path = Path(__file__).with_name("transported_product.py") + load(engine_path, ENGINE) + engine = runpy.run_path(str(engine_path)) + rank = engine["rank"] + check = engine["require"] + check(compare({0: {1: Q(1)}}, {2: {1: Q(2)}}, rank)["joint_column_rank"] == 2, + "joint column control") + check(compare({0: {1: Q(1)}}, {0: {3: Q(2)}}, rank)["joint_row_rank"] == 2, + "joint row control") + check(compare({0: {1: Q(1)}}, {0: {1: Q(2)}}, rank)["joint_row_rank"] == 1, + "unchanged span control") + price = loads(load(args.price, PRICE)) + unit = loads(load(args.unit_receipt, UNIT)) + check(price["formal_case_cap"] == 1 and price["formal_runner_seconds"] == 90 and + list(PAIR) in unit["rank_at_most_two_square_zero_keys"], "wrong fixed formal stock or cap") + caller = loads(load(args.caller, engine["CALLER"])) + check(all(caller["events"][t] == ["A", "QUERY", 0, 1, -1] for t in PAIR), "wrong query pair") + base, _ = probe(engine, caller, -1, (Q(1),) * 17) + check(rank(base) == 2 and not engine["product"](base, base), "unit baseline not reproduced") + verdict = "q_minus_single_body_probes_inconclusive" + outputs = [] + for j in range(17): + if monotonic() - started >= 90: + verdict = "runner_cap" + break + bodies = [Q(1)] * 17 + bodies[j] = Q(2) + plus, _ = probe(engine, caller, 1, bodies) + check(not plus, "q=+1 did not give identity") + mutant, cross = probe(engine, caller, -1, bodies) + square = engine["product"](mutant, mutant) + summary = compare(base, mutant, rank) + outputs.append(summary | {"nonunit_variable": j + 1, "value": "2", + "cross_terms": cross, + "first_square_nonzero": engine["first_nonzero"](square), + "first_entry_difference": first_difference(base, mutant)}) + if square: + verdict = "nonzero_square_excludes_provider" + break + if summary["joint_row_rank"] > 2 or summary["joint_column_rank"] > 2: + verdict = "changing_span_excludes_fixed_axes" + break + print(dumps({ + "pair": PAIR, "verdict": verdict, "price_sha256": PRICE, "unit_receipt_sha256": UNIT, + "caller_sha256": engine["CALLER"], "independent_unit_engine_sha256": ENGINE, + "probes": outputs, "unselected_provisional_pair": [1516, 1721], + "scope": "One pair; q=−1 exact single formal body specializations, q=+1 controls. Fixed q-even setup and axes, with no new body-dependent transports." + }, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + p = argparse.ArgumentParser() + for name in ("caller", "price", "unit-receipt"): + p.add_argument("--" + name, type=Path, required=True) + main(p.parse_args()) diff --git a/research/p104-type-a-query-fixed-cut/engines/independent/gaussian_necessity.py b/research/p104-type-a-query-fixed-cut/engines/independent/gaussian_necessity.py new file mode 100644 index 0000000000..9fc55d6f1b --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/engines/independent/gaussian_necessity.py @@ -0,0 +1,177 @@ +"""Exact Gaussian-rational probes for the selected R76 rank-two correction.""" +from dataclasses import dataclass +from fractions import Fraction as Q +from json import dumps, loads +from pathlib import Path +import argparse +import runpy +from math import prod +from time import monotonic + + +@dataclass(frozen=True, eq=False) +class G: + re: Q = Q(0) + im: Q = Q(0) + + def __bool__(self): + return bool(self.re or self.im) + + def __eq__(self, other): + other = lift(other) + return self.re == other.re and self.im == other.im + + def __str__(self): + return f"{self.re}+({self.im})i" if self.im else str(self.re) + + def __add__(self, other): + other = lift(other) + return G(self.re + other.re, self.im + other.im) + + __radd__ = __add__ + + def __neg__(self): + return G(-self.re, -self.im) + + def __sub__(self, other): + return self + -lift(other) + + def __rsub__(self, other): + return lift(other) + -self + + def __mul__(self, other): + other = lift(other) + return G(self.re * other.re - self.im * other.im, self.re * other.im + self.im * other.re) + + __rmul__ = __mul__ + + def __truediv__(self, other): + other = lift(other) + d = other.re * other.re + other.im * other.im + return self * G(other.re / d, -other.im / d) + + def __rtruediv__(self, other): + return lift(other) / self + + +def lift(value): + return value if isinstance(value, G) else G(Q(value)) + + +def qpow(q, power): + return (G(Q(1)), q, G(Q(-1)), -q)[power % 4] + + +def gaussian_ops(event, q, alpha, bodies, even): + family, op, *args = event + if family == "B": + return [] + if family == "J": + u, v, x, y = args[0] + scalar = bodies[op - 1] + return [("ADD", v, u, 1 / q), ("ADD", x, y, alpha * q)] + ( + [("SCALE", r, r, scalar) for r in (u, v, x, y)] if scalar != 1 else []) + if family != "A": + raise ValueError("unknown caller family") + dst, *tail = args + if op == "ADD": + return [(op, dst, tail[0], Q(tail[1]))] + if op == "SCALE": + return [(op, dst, dst, Q(tail[0]))] + if op == "SWAP": + return [(op, dst, tail[0], Q(1))] + if op == "LAMBDA": + # (1+i sign)/2 + (1-i sign)q²/2 at q=±i. + return [("SCALE", dst, dst, G(Q(0), Q(tail[0])))] + if op == "QUERY": + return [("ADD", dst, tail[0], Q(1) if even else qpow(q, tail[1]))] + if op in ("IDLE_ODD", "IDLE_ONE"): + c = prod(bodies[s - 1] for s in tail[0]) + if op == "IDLE_ODD": + c *= qpow(q, tail[1]) + return [("SCALE", dst, dst, c)] if c != 1 else [] + raise ValueError("unknown Type A operation") + + +def probe(engine, caller, pair, q, bodies): + first, second = pair + events = caller["events"] + ty = caller["types"]["A"] + d, s = events[first][2:4] + tape = [op for t in range(first, second) + for op in gaussian_ops(events[t], q, Q(ty["alpha2"]), bodies, t == first)] + u, v = engine["transported"](tape, ty["roles"], d, s) + N = engine["residual"](u, v, d, s, qpow(q, -1) - 1) + return N, [str(v[d]), str(u[s])] + + +def main(args): + start = monotonic() + root = Path(__file__).resolve().parent + formal = runpy.run_path(str(root / "formal_necessity.py")) + pinned, pair = formal["load"], formal["PAIR"] + engine_path = root / "transported_product.py" + pinned(engine_path, formal["ENGINE"]) + engine = runpy.run_path(str(engine_path)) + rank, check = engine["rank"], engine["require"] + price = loads(pinned(args.price, formal["PRICE"])) + unit = loads(pinned(args.unit_receipt, formal["UNIT"])) + check(price["formal_case_cap"] == 1 and price["formal_runner_seconds"] == 90 and + list(pair) in unit["rank_at_most_two_square_zero_keys"], "wrong fixed pair") + caller = loads(pinned(args.caller, engine["CALLER"])) + i = G(Q(0), Q(1)) + check(i * i == -1 and 1 / i == -i and (Q(1, 3) + i) / (Q(1, 3) + i) == 1, "Gaussian field control") + check(gaussian_ops(["A", "LAMBDA", 1, -1], i, Q(-1), (Q(1),) * 17, False)[0][-1] == -i, + "Gaussian LAMBDA control") + verdict = "gaussian_necessary_probes_inconclusive" + receipts = [] + baseline = {} + for stage in (0, *range(1, 18)): + if monotonic() - start >= 90: + verdict = "runner_cap" + break + bodies = [Q(1)] * 17 + if stage: + bodies[stage - 1] = Q(2) + matrices, details = {}, {} + for name, q in (("i", i), ("minus_i", -i)): + N, cross = probe(engine, caller, pair, q, bodies) + matrices[name] = N + sq = engine["product"](N, N) + details[name] = {"rank": rank(N), "square_rank": rank(sq), + "first_square_nonzero": engine["first_nonzero"](sq), "cross_terms": cross} + if stage: + details[name]["vs_unit"] = formal["compare"](baseline[name], N, rank) + details[name]["first_entry_difference_vs_unit"] = formal["first_difference"](baseline[name], N) + comparison = formal["compare"](matrices["i"], matrices["minus_i"], rank) + receipts.append({"nonunit_variable": stage or None, "characters": details, "q_even_shape": comparison}) + if any(v["square_rank"] for v in details.values()): + verdict = "nonzero_square_excludes_provider" + break + if any(v["rank"] > 2 for v in details.values()): + verdict = "rank_excludes_provider" + break + if comparison["joint_row_rank"] > 2 or comparison["joint_column_rank"] > 2: + verdict = "changing_span_at_same_q_squared_excludes_fixed_q_even_axes" + break + if stage and any( + v["vs_unit"]["joint_row_rank"] > 2 or v["vs_unit"]["joint_column_rank"] > 2 for v in details.values() + ): + verdict = "changing_body_span_excludes_fixed_axes" + break + if not stage: + baseline = matrices + print(dumps({ + "pair": pair, "verdict": verdict, "probes": receipts, "price_sha256": formal["PRICE"], + "caller_sha256": engine["CALLER"], "unit_receipt_sha256": formal["UNIT"], + "controls": ["exact Gaussian rational arithmetic", "q²=−1 signed LAMBDA"], + "unselected_provisional_pair": [1516, 1721], + "scope": "One selected pair, q=±i with exact rational Gaussian characters. Same q-even axes at the two characters." + }, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + p = argparse.ArgumentParser() + for name in ("caller", "price", "unit-receipt"): + p.add_argument("--" + name, type=Path, required=True) + main(p.parse_args()) diff --git a/research/p104-type-a-query-fixed-cut/engines/independent/symbolic_transport.py b/research/p104-type-a-query-fixed-cut/engines/independent/symbolic_transport.py new file mode 100644 index 0000000000..1abcfaee7a --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/engines/independent/symbolic_transport.py @@ -0,0 +1,187 @@ +"""Exact Laurent transport of the selected R76 pair, without a physical build.""" +from argparse import ArgumentParser +from fractions import Fraction as Q +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from time import monotonic +import runpy + +PAIR = (1580, 1659) +PRICE = "52e05b80069ce01cad3b8e5f3cf9123e930de36987bd398dd43f103953a4674a" +CALLER = "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc" +GAUSS = "5bc0f4fd3fece7223551be76d7e4343631e7ee3156b73d3d01c81446a9e7e214" +ZERO = (0,) * 17 +ENGINE_PATH = Path(__file__).with_name("gaussian_necessity.py") +G = runpy.run_path(str(ENGINE_PATH))["G"] + + +class Capped(Exception): + pass + + +def pinned(path, sha): + data = path.read_bytes() + if sha256(data).hexdigest() != sha: + raise ValueError("changed input " + path.name) + return data + + +def mono(k=1, phase=0, powers=ZERO): + return {(phase % 4, powers): k} if k else {} + + +def add(a, b, sign=1): + out = a.copy() + for m, c in b.items(): + x = out.get(m, 0) + sign * c + if x: + out[m] = x + else: + out.pop(m, None) + return out + + +def mul(a, b): + out = {} + for (q, v), x in a.items(): + for (r, w), y in b.items(): + key = ((q + r) % 4, tuple(i + j for i, j in zip(v, w, strict=True))) + z = out.get(key, 0) + x * y + if z: + out[key] = z + else: + out.pop(key, None) + return out + + +def scalar(role, coeff=Q(1), phase=0, mask=()): + powers = tuple(mask.count(i) for i in range(1, 18)) + return ("SCALE", role, role, mono(coeff, phase, powers), + mono(1 / coeff, -phase, tuple(-x for x in powers))) + + +def emit(event, alpha, even): + family, op, *args = event + if family == "B": + return [] + if family == "J": + u, v, x, y = args[0] + return [("ADD", v, u, mono(1, -1), None), ("ADD", x, y, mono(alpha, 1), None), + *(scalar(r, mask=(op,)) for r in (u, v, x, y))] + assert family == "A" + d, *tail = args + if op == "ADD": + return [(op, d, tail[0], mono(Q(tail[1])), None)] + if op == "SCALE": + return [scalar(d, Q(tail[0]))] + if op == "SWAP": + return [(op, d, tail[0], None, None)] + if op == "QUERY": + return [("ADD", d, tail[0], mono(1, 0 if even else tail[1]), None)] + if op == "LAMBDA": + s = Q(tail[0], 2) + a, b = G(Q(1, 2), s), G(Q(1, 2), -s) + return [("SCALE", d, d, add(mono(a), mono(b, 2)), add(mono(b), mono(a, 2)))] + if op in ("IDLE_ONE", "IDLE_ODD"): + return [scalar(d, phase=tail[1] if op == "IDLE_ODD" else 0, mask=tuple(tail[0]))] + raise ValueError("unknown Type A event") + + +def transport(ops, n, dest, source, deadline): + u = [mono(Q(i == dest)) for i in range(n)] + v = [mono(Q(i == source)) for i in range(n)] + for kind, d, s, scale, inv in reversed(ops): + if monotonic() >= deadline: + raise Capped + if kind == "ADD": + u[d] = add(u[d], mul(scale, u[s]), -1) + v[s] = add(v[s], mul(scale, v[d])) + elif kind == "SCALE": + u[d] = mul(inv, u[d]) + v[d] = mul(scale, v[d]) + else: + assert kind == "SWAP" + u[d], u[s] = u[s], u[d] + v[d], v[s] = v[s], v[d] + return u, v + + +def describe(poly): + return [{"q": phase, "body": {j + 1: n for j, n in enumerate(powers) if n}, "coefficient": str(c)} + for (phase, powers), c in sorted(poly.items())] + + +def proof(caller, deadline): + first, second = PAIR + events = caller["events"] + ty = caller["types"]["A"] + assert all(events[t] == ["A", "QUERY", 0, 1, -1] for t in PAIR) + tape = [item for t in range(first, second) + for item in emit(events[t], Q(ty["alpha2"]), t == first)] + u, v = transport(tape, ty["roles"], 0, 1, deadline) + dot = {} + for x, y in zip(u, v, strict=True): + dot = add(dot, mul(x, y)) + assert not dot, "transported shear lost own square-zero property" + outer = {} + for i, x in enumerate(u): + if monotonic() >= deadline: + raise Capped + if x: + for j, y in enumerate(v): + if y and (p := mul(x, y)): + outer[i, j] = p + bad_body = [(i, j, describe(p)) for (i, j), p in outer.items() if any(m[1] != ZERO for m in p)] + odd = [(i, j) for (i, j), p in outer.items() if any(m[0] % 2 for m in p)] + corrected = {} + delta = add(mono(1, -1), mono(-1)) + for key, p in outer.items(): + if result := mul(delta, p): + corrected[key] = result + for i, x in enumerate(u): + if x and (p := mul(mul(delta, delta), mul(x, v[0]))): + key = (i, 1) + corrected[key] = add(corrected.get(key, {}), p) + corrected[0, 1] = add(corrected.get((0, 1), {}), delta) + corrected = {k: p for k, p in corrected.items() if p} + return { + "status": "EXACT_SYMBOLIC_AXES" if not (u[1] or v[0] or bad_body or odd) else "FORMAL_SHAPE_OPEN", + "pair": PAIR, "literal_between_event_count": len(range(first, second)), + "elementary_operation_count": len(tape), "vector_support": [sum(map(bool, u)), sum(map(bool, v))], + "vectors": {"u": {i: describe(p) for i, p in enumerate(u) if p}, + "v": {i: describe(p) for i, p in enumerate(v) if p}}, + "cross_actions": {"u_source": describe(u[1]), "v_dest": describe(v[0]), "v_u": describe(dot)}, + "outer_body_dependency": bad_body, "outer_q_odd_entries": odd, + "outer_axis": {f"{i},{j}": describe(p) for (i, j), p in outer.items()}, + "normalized_delta_entries": {f"{i},{j}": describe(p) for (i, j), p in corrected.items()}, + "condition_if_success": "G=I+(q^-1−1)(e0 e1^T+u v) over Q(i)[q,D_1^±1,...,D_17^±1]/(q^4−1). Formal axes only, with no physical provider or cost admission." + } + + +def main(args): + start = monotonic() + controls = [ + mul(add(mono(G(Q(1, 2), Q(1, 2))), mono(G(Q(1, 2), Q(-1, 2)), 2)), + add(mono(G(Q(1, 2), Q(-1, 2))), mono(G(Q(1, 2), Q(1, 2)), 2))) == mono(), + mul(mono(3, -1, (1,) + ZERO[1:]), mono(Q(1, 3), 1, (-1,) + ZERO[1:])) == mono(), + ] + assert all(controls) + price = loads(pinned(args.price, PRICE)) + gaussian = loads(pinned(args.gaussian, GAUSS)) + assert price["formal_case_cap"] == 1 and price["formal_runner_seconds"] == 90 and tuple(gaussian["pair"]) == PAIR + caller = loads(pinned(args.caller, CALLER)) + try: + result = proof(caller, start + 87) + except Capped: + result = {"status": "CAPPED", "pair": PAIR, "pending": "Finish exact Laurent rank-one transport/product"} + result.update({"caller_sha256": CALLER, "price_sha256": PRICE, "gaussian_receipt_sha256": GAUSS, + "controls": ["LAMBDA inverse", "Laurent monomial inverse"], "unvisited_pair": [1516, 1721]}) + print(dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + p = ArgumentParser() + for name in ("price", "caller", "gaussian"): + p.add_argument("--" + name, type=Path, required=True) + main(p.parse_args()) diff --git a/research/p104-type-a-query-fixed-cut/engines/independent/transported_product.py b/research/p104-type-a-query-fixed-cut/engines/independent/transported_product.py new file mode 100644 index 0000000000..0d6b72d0ba --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/engines/independent/transported_product.py @@ -0,0 +1,201 @@ +"""Independent unit-body rank-two signed correction via transported shears.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import combinations +from json import dumps, loads +from pathlib import Path +from time import monotonic + +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc" +CLOCKS = (1516, 1580, 1659, 1721) +PAIRS = tuple(combinations(CLOCKS, 2)) +CAP, SECONDS = 6, 20 + + +def require(ok, reason): + if not ok: + raise ValueError(reason) + + +def pinned(path, expected): + raw = path.read_bytes() + require(len(expected) == 64 and sha256(raw).hexdigest() == expected, "changed input " + path.name) + return raw + + +def unit(n, at): + return [Q(i == at) for i in range(n)] + + +def emit(event, q, alpha, even=False): + family, op, *args = event + if family == "J": + u, v, x, y = args[0] + return [("ADD", v, u, Q(1, q)), ("ADD", x, y, alpha * q)] + if family == "B": + return [] + require(family == "A", "unknown event family") + dst, *tail = args + if op == "ADD": + src, value = tail + return [(op, dst, src, Q(value))] + if op == "SCALE": + return [(op, dst, dst, Q(tail[0]))] + if op == "SWAP": + return [(op, dst, tail[0], Q(1))] + if op == "QUERY": + src, power = tail + return [("ADD", dst, src, Q(1) if even else Q(q) ** power)] + if op == "IDLE_ODD": + return [("SCALE", dst, dst, Q(q) ** tail[1])] + require(op in ("LAMBDA", "IDLE_ONE"), "unknown Type A event") + # Body=1 and q²=1 give identity for these two operations. + return [] + + +def transported(ops, n, dst, src): + u, v = unit(n, dst), unit(n, src) + for op, d, s, a in reversed(ops): + if op == "ADD": + u[d] -= a * u[s] + v[s] += a * v[d] + elif op == "SCALE": + u[d] /= a + v[d] *= a + else: + require(op == "SWAP", "unknown elementary op") + u[d], u[s] = u[s], u[d] + v[d], v[s] = v[s], v[d] + require(sum(x * y for x, y in zip(u, v, strict=True)) == 0, "transported shear lost square-zero") + return u, v + + +def residual(u, v, dst, src, delta): + # (I+delta*u*v)(I+delta*e_dst*e_src^T)-I. + rows = {} + for i, a in enumerate(u): + row = {j: delta * a * b for j, b in enumerate(v) if delta * a * b} + extra = delta * (i == dst) + delta * delta * a * v[dst] + if extra: + row[src] = row.get(src, Q(0)) + extra + row = {j: c for j, c in row.items() if c} + if row: + rows[i] = row + return rows + + +def product(A, B): + output = {} + for i, left in A.items(): + row = Counter() + for k, a in left.items(): + for j, b in B.get(k, {}).items(): + row[j] += a * b + row = {j: c for j, c in row.items() if c} + if row: + output[i] = row + return output + + +def rank(rows): + pivots = {} + for row in rows.values(): + r = row.copy() + while r: + j = max(r) + if j not in pivots: + scale = r[j] + pivots[j] = {k: c / scale for k, c in r.items()} + break + multiplier = r[j] + for k, c in pivots[j].items(): + x = r.get(k, Q(0)) - multiplier * c + if x: + r[k] = x + else: + r.pop(k, None) + return len(pivots) + + +def first_nonzero(matrix): + for i in sorted(matrix): + for j, value in sorted(matrix[i].items()): + if value: + return [i, j, str(value)] + return None + + +def analyze(events, start, stop, n, alpha, q): + d, s = events[start][2:4] + ops = [row for t in range(start, stop) + for row in emit(events[t], q, alpha, even=(t == start))] + u, v = transported(ops, n, d, s) + N = residual(u, v, d, s, Q(1, q) - 1) + square = product(N, N) + return dict(rank=rank(N), square_rank=rank(square), first_square_nonzero=first_nonzero(square), + trace=str(sum(row.get(i, 0) for i, row in N.items())), + transport_cross_terms=[str(v[d]), str(u[s])], + rank_one_directions={"column": {i: str(c) for i, c in enumerate(u) if c}, + "row": {i: str(c) for i, c in enumerate(v) if c}}) + + +def controls(): + query = ["A", "QUERY", 0, 1, -1] + disjoint = [query, ["A", "SWAP", 0, 2], ["A", "SWAP", 1, 3], query] + linked = [query, ["A", "SWAP", 0, 1], query] + good = analyze(disjoint, 0, 3, 4, Q(-1), -1) + bad = analyze(linked, 0, 2, 4, Q(-1), -1) + even = analyze(linked, 0, 2, 4, Q(-1), 1) + require(good["rank"] == 2 and good["square_rank"] == 0, "disjoint rank-two control") + require(bad["rank"] == 2 and bad["square_rank"] > 0, "linked square control") + require(even["rank"] == even["square_rank"] == 0, "q=+1 control") + return ["disjoint square-zero rank two", "linked non-square-zero rank two", "q=+1 identity"] + + +def main(args): + tests = controls() + if args.controls_only: + return {"controls": tests} + # The lead's explicit launch supplies the sealed price digest. Read it before the caller. + price = loads(pinned(args.price, args.price_sha)) + require(price["head"] == HEAD and price["caller_sha256"] == CALLER, "wrong comparator price") + require(price["eligible_pairs_before_support"] == [list(pair) for pair in PAIRS] and + price["support_pair_cap"] == CAP and price["support_runner_seconds"] == SECONDS, + "wrong frozen pair scope") + start = monotonic() + caller = loads(pinned(args.caller, CALLER)) + data = caller["types"]["A"] + require((caller["stages"], data["roles"], data["offset"], len(data["ports"])) == (17, 36, 0, 96), + "wrong exact caller signature") + events = caller["events"] + require([i for i, e in enumerate(events) if e[:2] == ["A", "QUERY"]] == list(CLOCKS), "wrong QUERY inventory") + require(all(events[i] == ["A", "QUERY", 0, 1, -1] for i in CLOCKS), "wrong QUERY source or power") + outcomes, possible = [], [] + for pair in PAIRS: + if len(outcomes) == CAP or monotonic() - start >= SECONDS: + break + first, second = pair + probes = [analyze(events, first, second, data["roles"], Q(data["alpha2"]), q) for q in (1, -1)] + require(probes[0]["rank"] == probes[0]["square_rank"] == 0, "q=+1 correction is not identity") + odd = probes[1] + if odd["rank"] <= 2 and odd["square_rank"] == 0: + possible.append(list(pair)) + outcomes.append({"pair": pair, "q_plus": probes[0], "q_minus": odd}) + return {"head": HEAD, "caller_sha256": CALLER, "price_sha256": args.price_sha, "controls": tests, + "case_cap": CAP, "runner_cap_seconds": SECONDS, "body": "all 17 body variables equal one", + "outcomes": outcomes, "unvisited": PAIRS[len(outcomes):], "rank_at_most_two_square_zero_keys": possible, + "next_gate_if_any": "one exact key/90s formal necessary test only; no physical candidate established"} + + +if __name__ == "__main__": + p = ArgumentParser() + p.add_argument("--controls-only", action="store_true") + p.add_argument("--price", type=Path) + p.add_argument("--price-sha") + p.add_argument("--caller", type=Path) + args = p.parse_args() + require(args.controls_only or (args.price and args.price_sha and args.caller), "missing exact launch inputs") + print(dumps(main(args), indent=2, sort_keys=True)) diff --git a/research/p104-type-a-query-fixed-cut/engines/lead/fixed_cut.py b/research/p104-type-a-query-fixed-cut/engines/lead/fixed_cut.py new file mode 100644 index 0000000000..5e81a6ac70 --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/engines/lead/fixed_cut.py @@ -0,0 +1,140 @@ +"""Direct exact fixed-cut compensator action on all 36 basis columns.""" +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path +import sys +from time import monotonic + +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +PRICE = "52e05b80069ce01cad3b8e5f3cf9123e930de36987bd398dd43f103953a4674a" +CALLER = "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc" +CLOCKS = (1516, 1580, 1659, 1721) +N = 36 + + +def checked(path, expected): + value = path.read_bytes() + if sha256(value).hexdigest() != expected: + raise ValueError(f"changed dependency {path.name}") + return json.loads(value) + + +def trace(caller, first, second, q, even): + factors = [] + assert Q(caller["types"]["A"]["alpha2"]) == -1 + for clock in range(first, second + 1): + kind, op, *args = caller["events"][clock] + if kind == "J": + x, y, u, v = args[0] + assert len({x, y, u, v}) == 4 + factors.extend([("ADD", y, x, Q(q)), ("ADD", u, v, Q(-q))]) + elif kind == "A": + d, *tail = args + if op in ("ADD", "QUERY"): + s, k = tail + if op == "QUERY": + if clock in (first, second): + assert (d, s, k) == (0, 1, -1) + k = Q(1 if even and clock in (first, second) else q) ** k + factors.append(("ADD", d, s, Q(k))) + elif op == "SCALE": + k = Q(tail[0]) + assert k + factors.append((op, d, d, k)) + elif op == "SWAP": + factors.append((op, d, tail[0], Q(0))) + elif op == "LAMBDA": + assert q*q == 1 + elif op == "IDLE_ODD": + factors.append(("SCALE", d, d, Q(q) ** tail[1])) + elif op != "IDLE_ONE": + raise ValueError(op) + elif kind != "B": + raise ValueError(kind) + return factors + + +def apply(factors, vector, inverse=False): + for op, d, s, k in reversed(factors) if inverse else factors: + if op == "ADD": + vector[d] += (-k if inverse else k) * vector[s] + elif op == "SCALE": + vector[d] *= 1/k if inverse else k + elif op == "SWAP": + vector[d], vector[s] = vector[s], vector[d] + else: + raise ValueError(op) + return vector + + +def defect(original, even, dimension=N): + columns = [] + for i in range(dimension): + vector = [Q(j == i) for j in range(dimension)] + changed = apply(even, apply(original, vector.copy()), inverse=True) + assert apply(even, changed.copy()) == apply(original, vector.copy()) + columns.append([b-a for a, b in zip(vector, changed)]) + return columns + + +def square_entry(columns): + n = len(columns) + for j, col in enumerate(columns): + for i in range(n): + value = sum(columns[k][i]*a for k, a in enumerate(col) if a) + if value: + return [i, j, str(value)] + return None + + +def rank(columns): + basis = {} + for column in columns: + v = column.copy() + for i, row in sorted(basis.items()): + if v[i]: + v = [a-v[i]*b for a,b in zip(v,row)] + i = next((i for i,x in enumerate(v) if x), None) + if i is not None: + basis[i] = [x/v[i] for x in v] + return len(basis) + + +def controls(): + disjoint = [("ADD", 0, 1, Q(-2)), ("ADD", 2, 3, Q(-2))] + shared = [("ADD", 0, 1, Q(-2)), ("ADD", 1, 0, Q(-2))] + assert rank(defect(disjoint, [], 4)) == 2 + assert square_entry(defect(disjoint, [], 4)) is None + assert square_entry(defect(shared, [], 4)) is not None + assert defect(disjoint, disjoint, 4) == [[0]*4 for _ in range(4)] + return ["commuting disjoint rank two", "cross-acting rank two", "exact predecessor cancellation"] + + +def main(): + root = Path(sys.argv[1]) + price = checked(root / "price/PRICE.json", PRICE) + caller = checked(root / "price/inputs/7113-CALLER.json", CALLER) + assert (caller["stages"], len(caller["types"]["A"]["ports"])) == (17, 96) + keys = list(combinations(CLOCKS, 2)) + checks = controls() + deadline = monotonic() + 18 + records = [] + for first, second in keys: + if monotonic() >= deadline: + break + even_plus, orig_plus = (trace(caller, first, second, 1, flag) for flag in (True, False)) + assert even_plus == orig_plus and rank(defect(orig_plus, even_plus)) == 0 + even_minus, orig_minus = (trace(caller, first, second, -1, flag) for flag in (True, False)) + columns = defect(orig_minus, even_minus) + r, square = rank(columns), square_entry(columns) + records.append(dict(key=[first, second], rank=r, square_witness=square, + decision="excluded" if square is not None or r > 2 else "provisional", + defect_columns=[{i:str(x) for i,x in enumerate(col) if x} for col in columns])) + print(json.dumps(dict(head=HEAD, caller_sha256=CALLER, price_sha256=PRICE, scope="fixed first cut, commuting mutually annihilating rank-one axes", body_values="all one", + controls=checks, cap_cases=6, cap_runner_seconds=18, decisions=records, unvisited=keys[len(records):]), indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-type-a-query-fixed-cut/engines/lead/full_body.py b/research/p104-type-a-query-fixed-cut/engines/lead/full_body.py new file mode 100644 index 0000000000..5352fe3812 --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/engines/lead/full_body.py @@ -0,0 +1,135 @@ +"""Replay every basis column of the chosen correction over Gaussian Laurent polynomials.""" +from fractions import Fraction as Q +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path +import sys + +DIRECT = "70de991b8443ed9d4f4455b9755743c6262379fd16adc68763048f5d34298fe3" +FIRST, SECOND = 1580, 1659 +ZERO = (0,) * 17 + + +def checked_code(path, digest): + if sha256(path.read_bytes()).hexdigest() != digest: + raise ValueError("changed direct predecessor") + return run_path(str(path)) + + +def term(stage_list=()): + assert len(stage_list) == len(set(stage_list)) + return tuple(int(j in stage_list) for j in range(1,18)) + + +def add_scaled(dst, src, scalar=Q(1), turn=0, exponent=ZERO): + for (source_turn, powers), value in src.items(): + combined = (turn + source_turn) % 4 + new_powers = tuple(a+b for a,b in zip(powers,exponent)) + key = combined%2, new_powers + new_value = dst.get(key,0) + value*scalar*(-1 if combined>=2 else 1) + if new_value: + dst[key] = new_value + else: + dst.pop(key,None) + + +def operators(caller, phase, replace): + gates = [] + for clock in range(FIRST, SECOND+1): + kind, op, *args = caller["events"][clock] + if kind=="J": + a,b,c,d = args[0] + gates.extend([("ADD",b,a,Q(1),-phase,ZERO),("ADD",c,d,Q(-1),phase,ZERO)]) + gates.extend(("SCALE",r,r,Q(1),0,term((op,))) for r in (a,b,c,d)) + elif kind=="A": + d,*params = args + if op=="ADD": + gates.append((op,d,params[0],Q(params[1]),0,ZERO)) + elif op=="QUERY": + s,power=params + if clock in (FIRST,SECOND): + assert (d,s,power)==(0,1,-1) + gates.append(("ADD",d,s,Q(1),0 if replace and clock in (FIRST,SECOND) else phase*power,ZERO)) + elif op=="SWAP": + gates.append((op,d,params[0],Q(1),0,ZERO)) + elif op=="SCALE": + gates.append((op,d,d,Q(params[0]),0,ZERO)) + elif op=="LAMBDA": + assert params[0] in (-1,1) + gates.append(("SCALE",d,d,Q(1),params[0] if phase%2 else 0,ZERO)) + elif op in ("IDLE_ONE","IDLE_ODD"): + gates.append(("SCALE",d,d,Q(1),phase*params[1] if op=="IDLE_ODD" else 0,term(params[0]))) + else: + raise ValueError(op) + else: + assert kind=="B" + return gates + + +def apply(gates, v, undo=False): + for op,d,s,c,t,b in reversed(gates) if undo else gates: + if op=="SWAP": + v[d],v[s]=v[s],v[d] + elif op=="ADD": + assert d!=s + add_scaled(v[d],v[s],-c if undo else c,t,b) + else: + assert op=="SCALE" and c + new={} + if undo: + add_scaled(new,v[d],1/c,-t,tuple(-x for x in b)) + else: + add_scaled(new,v[d],c,t,b) + v[d]=new + return v + + +def basis(j): + return [{(0,ZERO):Q(1)} if r==j else {} for r in range(36)] + + +def predicted(j, phase, mut=False): + v=basis(j) + for i in range(36): + u = -1 if i==0 else 2 if 2<=i<=8 else 1 if i==19 else 0 + if j==1: + c,turn = u+(i==0),0 + elif j==18: + c,turn = (-1 if not mut else 1)*u, (1 if phase%2 else 0) + else: + continue + one={(0,ZERO):Q(1)} + add_scaled(v[i],one,c,turn-phase) + add_scaled(v[i],one,-c,turn) + return v + + +def main(): + root=Path(sys.argv[1]) + p=checked_code(root/"lead/fixed_cut.py",DIRECT) + price=p["checked"](root/"price/PRICE.json",p["PRICE"]) + caller=p["checked"](root/"price/inputs/7113-CALLER.json",p["CALLER"]) + assert price["head"]==p["HEAD"] and price["caller_sha256"]==p["CALLER"] + counts=[] + for phase in range(4): + original,even=(operators(caller,phase,flag) for flag in (False,True)) + corrections=[] + for j in range(36): + original_col=apply(original,basis(j)) + actual=apply(even,[v.copy() for v in original_col],undo=True) + assert actual==predicted(j,phase),(phase,j,actual) + assert apply(even,[v.copy() for v in actual])==original_col + if actual!=basis(j): + corrections.append(j) + assert corrections==([] if phase==0 else [1,18]) + if phase: + assert predicted(18,phase,mut=True)!=predicted(18,phase) + counts.append(dict(q_i_power=phase,columns=36,nonzero_correction_columns=corrections)) + print(json.dumps(dict(head=p["HEAD"],caller_sha256=p["CALLER"],price_sha256=p["PRICE"], + fixed_cut=FIRST, later=SECOND, phase_checks=counts, independent_basis_columns=144, + arbitrary_body_variables=17, unchanged_recovered_action=True, sign_control="passed"),indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-type-a-query-fixed-cut/engines/price/derivative_check.py b/research/p104-type-a-query-fixed-cut/engines/price/derivative_check.py new file mode 100644 index 0000000000..ce5cdf3779 --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/engines/price/derivative_check.py @@ -0,0 +1,67 @@ +"""Check decrease of the complete priced moments through the retained BIT cap.""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from json import dumps,loads +from pathlib import Path +from runpy import run_path + +ROOT = Path(__file__).resolve().parent +PINS = { + 'PRICE.json':'52e05b80069ce01cad3b8e5f3cf9123e930de36987bd398dd43f103953a4674a', + 'inputs/pricing.py':'f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182', + 'inputs/7334-READBACK.json':'337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82', +} + + +def derivative(histogram,low,high,tariff): + log,power = tariff['log_bounds'],tariff['power_bounds'] + ln2_low,ln2_high = log(Q(2)) + lower = upper = Q(0) + for rank,count in histogram.items(): + shift = rank.bit_length()-1 + a,b = log(Q(rank,1<0 and type(n) is int and n>0 for r,n in result.items()) + return result + + +def interval(values): + return list(map(str,values)) + + +def main(): + assert __debug__ + raw={} + for rel,pin in PINS.items(): + value=(ROOT/rel).read_bytes() + if sha256(value).hexdigest()!=pin: + raise ValueError(f'Changed dependency {rel}') + raw[rel]=value + read=lambda key:loads(raw[key],object_pairs_hook=unique) + census=read('inputs/QUERY-CENSUS.json') + base=read('inputs/7334-READBACK.json') + admission=read('inputs/7334-ADMITTED.json') + assert base['head']==admission['head']==HEAD and admission['exit']==0 + assert admission['status']=='independently_reproduced_comparable' and len(admission['stages'])==4 + assert base['caller_head']==admission['caller']==CALLER + assert census['caller_sha256']==admission['caller_sha256']==PINS['inputs/7113-CALLER.json'] + assert set(base['assumptions'])==set(admission['assumptions'])=={ + 'native_all_columns','owned_erasure','compiler','precision_tape','analytic_recovery'} + queries=census['query_events'] + clocks=sorted(map(int,queries)) + assert clocks==[1516,1580,1659,1721] + assert all(q=={'destination':0,'q_power':-1,'relative_defect_rank':1,'source':1} for q in queries.values()) + ports=len(set(census['ports'])) + assert ports==len(census['ports'])==96 and len(clocks)==4 + paid,targets=(hist(base[k]) for k in ('paid','targets')) + assert (sum(paid.values()),sum(targets.values()),paid[1])==(110519,22461,68384) + old=targets.copy(); old.subtract(paid) + assert sum(r*n for r,n in old.items())==base['rank_surplus']==1424 and not base['empty_root_credits'] + crossing=Q(base['new_raw_interval'][1]); bit=Q(base['bit_premise']); claim=Q(base['claim']) + assert claim==Q(admission['kappa'])0 + assert sum(delta.values())==-ports*fusions and sum(r*n for r,n in delta.items())==0 + assert sum(new.values())==110519-ports*fusions + signed=targets.copy() + signed.subtract(new) + assert sum(r*n for r,n in signed.items())==1424 + credit=Counter({rank:-change for rank,change in delta.items()}) + assert sum(r*n for r,n in credit.items())==0 + raw_credit=cost(credit,crossing) + new_cross,new_probe,new_bit,new_target=(cost(signed,k) for k in (crossing,probe,bit,target)) + with_extra=signed.copy() + with_extra[1]-=1 + extra=cost(with_extra,crossing) + assert extra==tuple(x-1 for x in new_cross) + assert 0nb_8iZQHo9Z9c#MK3iM+V!OINb-MaZ z*XizWcO4=C%#Z(R;NO=yws8le2|GRG|Ma(TiZWlb+n{?^8%stSh+oOTvHVb-wzxJRp-*Yi^g+l*tS3mY37I~z;yw-09wKPKxeI6IX)wmBBx>h8<#d%ty`>hFvU9}lNdxX3cf z*2y}^o_LN>6j2;dBvZJ_vdT8ey2w7rUhL4YGqEvo)U%dbCtALNC|AgLie`(xnw68B zlBAM4D6%LvC^{(KDZ(j6D4q+)W$9&4GmSEhvi36fvQRTovl27sk-e~81uklc+*go0 zoz*`dzF!uQS6cEG-Ch`XwtR5E=N|pPw>HiNI{n>0jRgXCT1s#zZb$Pf!-y`BzHNvu zmIYR;{p+;94O+kY>^_6H-k>`kk^2kZ1RKBpAHB^%U;X7A&Yy(lLP z?~LvK-(O9CB>x?11++{()eSw+>+mD)G<)}o3FwSJWpL|xUD#$ke6^sx0HPa$QbyBHh5U91P~I=b7!_xP-~>!|0|`PwKhubBfp6Hx2_bq|>H zzjXD%_2ccx9I4c9NO|lW%$XAZG^@jaaHpOQEck#zC4OrPKGA^qVHP;2E%?=s|=_KdbA1$Mt-_uI$J3 z!2n<0Qk&Lp-@V@N1uOLM^=Kg4S^Zt!-y7UrC&o6J*LA67tsiRrxjs%d=HLhoXyeh< z*^*L$>4)n0BMYG3dr%`hdI?T`8w9wwzUvbgJA_7kn^c#}LVl+PX~GieI<3Wk(jd&A zhB|D|m9+_CcD-Lh>n`scKCOor$k*wol#O`r%y;o>bjop(yMAxRuFd|%@Y+dNJIAE( zvIey$r|e{xm=ST{q&2Ei-bx1cavn(9>N9p6zGVY=t(hg6+gqftMhO~@l)BvYG6nH7 zC?j+JPAYdL1w@`5GBhOn9}67U0_u}M^ovOAzNn#Jjf~vfKF`q*Lz<4Am`@b9e`!S? zhYIWHDp%MsKRY{M^NXjUqTCwK@XKR zrL8z!<^;}N|4?T5DG)%&GW_nfr8{?jlk2ysPpA*QW3~zu(| zUMN+KYSn|=YFh7P{1c^hXh>&N-)2)?N8;@2JHWjxcF;8YSzH%wQ!Z0zEX_A*F=e(1 z7ra>0d>R4;tjG4WZ0;T?rdsyox6CltJN%%~!=Cr6UaO9N2=Qaminr?+-;{*UPVF^Y z^QfO*rw^?kM zJ!F6#R1{J!NWgfWZ4rfon>hGT?W*8&(K`f7ksd4?Tv5gaJ>5aq{5*i=8 z8lz@2k`DFIcb&V^k=4)V`!7H&9)2Z55S95U`JY@4%Nm4uql-B$uR?kjaam4D>$YPtK{U4cw1 zJM{tEwb0iqLC@C5+qFcf#2nkTy8EAAcYe0Usrrt0eth0NZbQV!EdBiTpFVl3<*Tc3 z0&9(V7uUGL@Yurl=)!n(P;TW@uzhVF*L_?)w41TUwsA+P-l4&bjb9OM!4 z4DetXyZ>e8Y*Lr~$yntgU?!vxd_WO2ZHWh4zdec!z1cvRKsgQV89x|THfW>3(fK!h z8o4hjLKTW#mJfP`AY7V|!(0^B`f?jGrEyPHX9D)aoa^_ypxF*BEm&zK0^{KXA$kcv*{$?=&+79krN^2{Y#RM;g50IXmoxRb6Daeb`-TS z)o3&c19O<(eIg+%!kWq z`SBMlSY0Otz{#>V#djo&VmY?A_&2he~~>(bs537;7Tv5Jc+QYr?>_(O#QQ z>s$jt1vcYcVr7F(NlN13u|!3MD?dYKJTr?G=p#rU zN6=rkpSO^F@*gT@loP2Hrf3~Z1-d3lU$x}Mn)~ivUVNESKgb29ONv0Vl{47$6m|xsuRwCU-T^)J-kOs% z5<~n!_&J-U84YbrCWMSOpKO#NU0m*2j!h{imst&EhBm;_gR2ZE)(aF10*VCy#nMOE zlsSesrt=XETAnjx)*EkhpaSr*ie2cZXa`vpp>3dG3S; zA2ZUPnuHldI*A>l)#L&xy^VHH!S)o}Vi^w_0pi8SC`H_z_^KDwMiW;D()XEod>lb2Cx~8$ZLm0u?Gce*!7q6mCiQM-0kcu^viu7;f&>e@%DNMp> zMk_s9C*cX1KFtkD408>_-YkM+@~W?W<#x5 ziG6hOPQV`_ySMNmyj9>NOa0&(3Ur}T27dQ5`rrFQWl%^xj^S_(!k?@8UKa{HZe{p9 zi!lTh!=IH|C=WYb_z~n*@^-_RVUMDKIBu`S{lY-Pm=}xw$_yBEuf>FzLj-=SQ^oK& zFRx@}Q?u&d{-5$aFH=3y@Gw=uugzmfyDLR&&YW|x-H`(`$0yP}dg!5M0+lo2`nW41 zfOBYdEkGse3IlI@E5%@HU6BOsDW!DOOaY=0+(rT4Y(4H->d@Sk6p5mV0y+-5=ugoE z!T&A8)zS2(Jep@!!;PIe+5Zn({3JoSK^T$m$!@Gs!s~LtTLnzq#L%Cu5&2st4*NLk zg+E&x^KaK|f4?Mqwq3P&FxZ=TnK4M}lLT)|31;ppTV!W*Llb_>mYJ z=V-`&afb6$*`uY?g?hKX6nY-7UZvXw@6hA$d8e-GqF-^+*EC(}*Jl6OFz@9|sS#?{ z)jXD3UT3rbyX?r>cjiW^ac}dwzlsn`N0WScs<@ex3h8ShL6mtI7O#;?BrOE`0}Gil z0^qC<69D&P3=U@Iqz)cnzL?(aodk^%O7QM6(N(d8zae+@CCafC`68ZL3ghOe2&}=d z;^QJB{%q!7Bk7k5Q6vu8V%tfj(F#j7gO*Is75T2D(P~MhAS_=+O!*2|ZpJ=W$P)OM7`JN&4deJBcEJq zB&b)V9xus`S+e=m0k&T4q)My_LK9O?MeDAKvFC$9&iGqyVoA(iV_Zm4JeB2ZL!!r= z*;m;VC$V%qBlRA~Y_dH@Agm697GiT8;)UqqiZ*B+Ve_QVymgvDYM#+Ru zS>#}F#9f1j$yio7O_LtwrbL<9u*RfB%I$v6|#nRrTS~(`l z#2334p6#Fzg3`DBX3FLuh!}`YHJ;Gr*P;KN5(d2QCAFq8(^s^aaov^adfh!K8DgMW zCc+UORTDiB5K-uVo3uWhT>c&q)9TjnaA`T`y`Jqq1G@6xu3^=fP@NG>49kujptd-i z0gX40$egA`@WlkK_Fl;2do;Li#gBYnvl#sEytN%Vx8rD^$+V|xwvr|~o+EZO=nT~a zfLiSt-sZNsSAF-@mWe8oN#<%`kmqL63b9pL^~A5)6^w?WpV7{hy!AXBRwnsj4_c*$ zsyRQ&Po}GDzz9I@@Q+|k0$d-o&Xw#%gcxnt;@B-Sd0FuJu29d4<745jX|z4QB_PAf|^HXaWHVs^t(%1|BxyD{LxAF zXNy1Bh(8tZ%4n9hgqa()5;8hueX)jBYpJ}8%LJ|O-Xnrg6LqXfaU@+$ouQ&Qwqg{g zFz{=uv*|z{E;KJWH?}|R104SMThXIe^3|F3XFo%}9|@|AzLKt>Q^!J(J;P*b$dMSj z-{(Zd>~Vd^Yl|5neLX|D)3$Z~r81oD3ZeBYszJQ?pNyDa5}LzWvlrBG=40UIo^%$z z_~U=T$H(BtJ?UgVtyZ^;4Xs2-#^HNQ2peXb4uuv_pN018VJ2zdC(os+p>@fuOu-Z< zq$Ad?1CNy_7lR+M-Bgp2?SbV3O^pR;t$}XGsS6oFS)~bA+N2b*Bi0`ti^H)acI_oP zD3PgLPL>C1(PdkB^FF8+GAzFbW5yQ_^Fx2REd>#D_8rNguo===li40E_Inbyrcv-` zEjBqRaj>2}J>cc4Emlu)mb}IvH7dyW*YxoqK8;deJ|~RCt!H5_<=9qLy{#Lb)w8}2 z&86_Q69V6e{W)!Xg5JCsvIuy$0e9rBBbi-HCqd{5`sXj7Cyy6G+%6ieBmFI&H81#d zK5^PSO>cA61h}7nc$_~Np^yMF#x5zcYdu3A3`=5G-)DGzYFRCx9wXYOe&eQ@{}fr5 zd}z&DAJaw5LP#;`SW9Fx}b=@tS_u@b99YX+^RqOC#`tQbIk&6w9F32?_n8=pq6_ z_g3m4OYzwp3au$C5F0JlL;*(4uvaxg+Cl+7KXnKiJP2mPgXWR!90qTtB6(ne4PMFn z9)s8C28gi{+r!~&*Hioy8sW8@NS;;|ky6^Ep5pYYJ+O>YkdGy$p-3XNSpr3i9Nsil zH};tLL3;wO=CN!y!o!Tz zRFQ!GyuZJlv5;F%sC4BRs#yx_?R&agPO)1qwSwsn6i~IPR_f_1nRb&ZNctjV1#^n! ze*MA=Djnmq|G}8Dv)?ZfGr4W~VBlIJX+-WNIMgZ|LJ_m!)!iO0$B+x`%p2$LR$onbO5>U7fvxg z*I}q^KJ6rfp#tpvc>>>;Jy3r5fr*YTxvP+x3QF_lAMN;TDsFuS)pWKc+7lul03R2=4#VkodVU=nPsCwz6DF^ zvn8{4a2xiPl>qskPI9Jaa0PP1<7S%^u-iGk%E&lUqzIsBqrzH9tgR5>XSrb|yPE|> zp<*TNF3WIN$&$vt-U3_+ludGE3mZp|iE`sO#ZK|LY4TW2`_<6BqKKEaPKJgovkAW!8>vn1r{U*x zP3+Mts)q&YZYJ`?YnHp{c*AN132d*im2ZfoR53qktp51J7F&I*e!V~DsOl1Os=1?} z?9Ib%$gsi@^(K|mZn%i}*zU;DY%LY7F8Y3CorvXNt+@)dO&CUCwCyRu!*Uta1pTL% zG}r=}l%no0>3Z-E^56jfEn5&{?`^y!KQ3mE%ARv_d|+`025REtPeme86N6@x&icaEQ;_tKqpv{nFHAT#>QzeD%NDwCQV%UFF6p^{)G@uY` zL@I=C9d7nd%{HH&K};Z$rHnUM&GxIN0)vcivan zE;L7g=j&az96M!d6;S~V#3(R*h>~tnA!H=Y*t9{y3YXe$XQ5==Y~lYn%a-YQh6YNS zFn$PYlOgj|Bl}W^@f5e$L%^Q%*qxiHy7xnZ($3_P7ZZz8DXrKv24#LaL}nlaptD3` zW{6N`yiDa}&YRt^*>gPral8&K>9{ipW9j#?+YQb@ugKFB5nFNJiY19alxIZtkuwPzRFKF!;b3!$j>9P>bz4}6)MVZ&N)6drL#^5ghK?2I~_dySSE`GqTkc)znme+ZcnNLyb4e@(?EMcI_J$Gx#P{Z~$t0%eU&OwfSj zNB`Y^(l#64$IJ=(|2?s{C#pjpVIj834BH=$Yz@xV@iZ!W$n4b1!i93n+7^*s>OMZg zfd3>ysCh>fH1ZRI3jc$gun;A3Y-)>Ih$4 z$PxV$=(sAZM<t7(QnBF8GTH!2t^}_}yd*JQ3R8tq z1BWS7cp^@ZMn>$3QH61*Z`&0yhPwS8Ko`}domPPm7|?ylpm zg7dG0(*VbdUcu{Lk~?D3GqC+@um$hZp$HLLls>Pmef9|hcDW48cW=vXC`;(DYDe{* z^(eO0i`ZF!WOh93+9)xqAYPy7UHz{(N!COYnWz!+kjU_~#q1(8jAq*=F!TxbT7b)3 z+0T_%M(Bu_=ekcN)edn^ zZm`iN!CyCW|F*a`4G#PUkxy=ExzPK-oMG5|`RCUDL3@n+LDCZ=ikDMKK>VP;JY&4t z+V9Bni1jR~-;A!`JjQCi>=7bRnEKT+bzf)uU1>jZ%`qr{pV@2s?IInG`7%k`TCzWD z>*tuifrV1YM}l9O=qRyA3uVH!RV*tM(lF>MB-R+g9_1(gF!J_SXreArGRUttItRrJ z)hqFoM|4N&xTKxvtY|-m5$^1~RuBXY1BdKFiaUyLxXTSz4QCKx{H=4HG=bMd{ew*I z)A^99W_-5dMbQ3R;PRb20Pn6uh8@J0yNAHW9*Kr?1&(2SFnzdT^nDI_? zPs|-6p5-29e{XAdCmT(u^1jdYqd*=E*jko!^EuNLSi(gF)V!(}^fB{y+h8sDUURhq z8L{*jRdaKK))QA!vS39d*Z55h#q5DdJ=sawj1}9Mr0Tbf0 zgu$UJgQF9A!33+KCs3rmO+IYv|I7Qw_{}ki~gZmzcHO5?BN6X|RJ4 z%Bb?4&LzXTp4x}eIF^&uK6Gd_ZVvMSr}5|?5=`_KYnS=>{cI9(Mfn5JVr0fv>3te| zKH~X)v16cg<{`p!iE>coX#r3%?$Ct(Auq+^ya z|ET0PApT);+LrWRY^{Zbig__2$I>9Q3wv9AM>rhZaOlL!gi<4LD;mx^h6;{g{3KAv zc1glPP{BuoUbO?_19`0cD^YJ2_Je>!9FZ^E59=B&vxaLz;im8eX>=|HHu(b$p-2;$ z-1OQfR6z~4Qc=<^`gOa>c6NP8>2gK$N2?cq)|IkyBJk#B9Sba53pM^kO^|CU)a~XM zOL~!{5x03v4M}-vTLd25Enf*6e&J^G{^rC<4T>R+Yk#!f(m$ky_WhWzb=^ow(toIz z>A|#9*bP}2VN>rTuN53j3XZ6T{2{7P$Hzpip`tR&je&tsDhdUNf@2OR<)jt)A4MAO zh!eh05EKaZG=lJe1NV?)C{wE-bKP0!{qMA?y2&MrtD{VS~9UIlF?=LhORH;2zZ- zRo9HeR)T`UQk)QQSjn}JH(bc_mKV-5~7V*I!A%mUC{ByF#aRqCzT$nKwwJq zPKV)gx{ypKSMd%(>(sBYwaq?V7r?O|QCP=62R!b%3wk4eR4eU0$OBIH;ejK{AP;LG z5x`=bwEfs|MSpycz)Zm<2gSUSSG|&T^T+QR+cf98J}kAJ7RfkJ3Dplou%fnABq$nY zWDfj)S|MrlkAi&#^D_8-tCBigibQKK3{{VjXEZJD<_s(3M3p{u;M-_h@)ajTm^*;d zUGIW#SX74S7Rvy6m%o7cq^?53CjfHUA8(qA3x=D z4K@dtD5u@xS+j4^s|oa-IFjtYUeEorkB}odO-aKZ#fls1g;jVH_Y&gR1yH!e+%{oh3fUm-i0_aT?Ih#MU>VVAnC&>QwzX>kzFThy!D;5OIoW`Q&KEv+ycME_+r zb)Rc{_u}y{hm9V@U#%~%>qbFEAruilu1tMp918z2M0JmuP*I+2M0MZUxTSn_Rvloi z9rgu@^_wGrA_}2x5>1kRXE{|^!{r=5(}!#$S-+zCKZfTd)dFr)uSaU(I-NZwwOrm6|OIF5dhhnLrt+1%9)UlsN^NBGbUnb)> zl7Dkglz&H6=7d~x4L>uN!unHOxI^}Lvcw+4jCiw-P7|9vpX_EsI86WGG=J)C0}ZBT z^>Q`BWjjMoXZ+8;WjiBGXE=i&PyYzjj%(e*5Tc3j7xbZWWRwKA27~n`zeukO+R&PK z$q1O4l%9lUE2|5Sn*{N@y7<}>&q-7DRv|d$LfR8N3V+@=>Ep(;+)z)4krFe?%XAM_srOv8Bs_J+3{0hLgUV5zw_Qot2A# z?L127bBJA&9{-NA2B$vGEjeUWyT4#AL;95pJ>z#5lF1AC*9e8!^DosP1iBFzT)nqK z1kvIoWaz4@LIfq%AUnLzkwSzy)gV7C`dwN2NKQi}tC3@D`Cp#0K&W(~(is|M^FO@= z`XbyhA;@|Qx>xB}1t0$!XM_{hNI_A#t>&3?`NpZ^^1gGYn5Ugih+qw*QtUr*2R>!B@5L_;-6rw_vceO)L(360tx){MRQJA<1g{uRpHx z1b_JKcKD8AN)=J2#gPQPt{lq2LvN$9C;$ez{!IpYyAyhl_tVVVB|5W|QAv@}dIaN9 z>Z>m*9%x_nd$NMEwNIaU`tc{Q;GB+#=#Jr>fQ9Af{jk6N`(X^E86)R(hHU4i~~h%ZJNQ}O7Lg&~+(NdbK2w;Qt&v@xUe z|37T@*w-$dGW=;tL&DP-W1tPqng%MTzB1BJBcF_EoESp*BJ%BH@Y*{xJ;Y<;3q6SB zcCU;I02%a{z!RQ!i<5$4KrFpiyM%QALIiKj=>LFfHUj+rjrj=D7^?ppdz=N8M|+?0 zME>trpQTxVT6(|FDF(ks{qG}&sVsr7OLcp{`%C?r?T^y$k0br>XQC{Q>z%F6*VDJl z>un#P-}A_F=c~YV&v|W3n!x4<=yF7!gJ}C>sw2za`~Iu6$9qB9`~GPwOI`qhLqNC3 z*ZsbOV@2TWVc^l7Bk$|U-2eG#|NZ+N^q%#V@TKnG{WTZ<(3lsB{ub{4cKi1J1-kzF zoO1oXN9N$Tto=U4>UmA$;PCJET=8@NyuBRZ=;`_TT6jmc|K52lZN1(>?A(sF_q|>D PMn*AXLoONv`|UQv! literal 0 HcmV?d00001 diff --git a/research/p104-type-a-query-fixed-cut/inputs/7334-ADMITTED.json b/research/p104-type-a-query-fixed-cut/inputs/7334-ADMITTED.json new file mode 100644 index 0000000000..464c89e45c --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/inputs/7334-ADMITTED.json @@ -0,0 +1,58 @@ +{ + "assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "base": "e54523517d0f03e58352e647c403a5af3e525a57", + "caller": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "caller_sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "crossing": [ + "0.00364665195644044790699554028334161", + "0.00364665195644044790699554028334162" + ], + "end": "2026-11-11T23:04:43Z", + "exit": 0, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "hosted_at_admission": "plan and historical success; candidate replay in progress", + "inputs": { + "EARLY-RESULT.json": "ad1ca9b2e2febbf80d9bf8b6ceef14ff90fcc29ef9358310e551628eb1706649", + "INPUTS.json": "abedac59097a1c35c27d91cbdb07207bc562a64743bc406d13c94a8bc970592d", + "NATIVE-RESULT.json": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812", + "PROPOSED-CLAIM.json": "6e31241944c123d2bd4aa8bc94d833b44b3d889bd6d9aafc579108f416b45f03", + "RESULT.json": "7f2d587c59f063b01f1e8b320084a7f0943f2f05d65e3e0f5e80448c6c8e8194", + "SOURCES.json": "ac7b4473035af648d6073e78b6c39675e706e8194b346bb55ed62a0adc81d593", + "VERIFY.json": "ede7dd2dd3733b9a73f72af9dd7edfe819b49b859c5c76e227ec82cb9c220513", + "WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" + }, + "kappa": "0.00364665195644", + "ours": "0", + "peer_gain": "0.000000430519994", + "prior_kappa": "0.003646221436446", + "receipt": { + "peer-prep/IDENTITIES.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "peer-prep/STATIC.json": "500cc563b7dac8b1de1faf1dee9b820e73152dfddc15a650cd1191edd39e8c79", + "peer-price/RANK-STOCK.json": "4a7841699dd17688f6aada5c902a2a91e94558b2b1b4460c46b0e55aa95b3f9f", + "peer-price/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "peer/COMMAND.txt": "714bfab024155d8216f3ef99f3ee7627ddc35ab341c486ac6bd53c476b757130", + "peer/COMMIT.stdout": "597470d8132a3812deb3624a859546c0c13d52b094fd6fc61e7416941130bd70", + "peer/END-UTC.txt": "9c46923c616c14da5b8ed503e1652021d7bd409a10ec91a78a03263013fba08a", + "peer/METADATA.stdout": "5873404cb4424dca918a00d503569f3c29a3190fd029a007e1afb2006399f647", + "peer/RUN.exit": "9a271f2a916b0b6ee6cecb2426f0b3206ef074578be55d9bc94f6f3fe3ab86aa", + "peer/RUN.stderr": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "peer/RUN.stdout": "d589626c7581fbb9928bc615364cfee49deb62dfc0a39a903417ca62be89cf8c", + "peer/START-UTC.txt": "5b78fd6d42a2b42206891318c08e6014de57d7ca46b0201cd11a166f452210f7" + }, + "source_history": "exact anchored base and recursive package provenance, sparse shallow stock wrapper not executed", + "stages": { + "caller": "PASS_HELPER_319_FUSED_CALLER 91166298911/25000000000000", + "early": "PASS_HELPER_319_EXACT_NATIVE_AND_SIGNED_PRICE 0.00364665195644", + "frontier": "PASS_HELPER_319_FUSED_FRONTIER_PROPOSAL 91166298911/25000000000000", + "native": "PASS_HELPER_319_FUSED_NATIVE 3646017316711/1000000000000000" + }, + "start": "2026-11-11T22:54:48Z", + "status": "independently_reproduced_comparable", + "tree": "fa98712a459b20c10240450097c87de433f8a750" +} diff --git a/research/p104-type-a-query-fixed-cut/inputs/7334-READBACK.json b/research/p104-type-a-query-fixed-cut/inputs/7334-READBACK.json new file mode 100644 index 0000000000..625b508eea --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/inputs/7334-READBACK.json @@ -0,0 +1,188 @@ +{ + "assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "bit_admitted": "12039/3125000", + "bit_claim_headroom": "3000951089/25000000000000", + "bit_premise": "376669/100000000", + "caller_head": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "claim": "91166298911/25000000000000", + "context_c": 2430, + "context_headroom": 1666, + "copies": 17, + "directed_bounds": { + "new_at_claim": [ + "347195197206460540909548691538238227127/2000000000000000000000000000000000000000000000000", + "1735975986032302704547743457691191192207/10000000000000000000000000000000000000000000000000" + ], + "new_at_old_crossing_upper": [ + "333717954993733063339209580360321337006028706669/2000000000000000000000000000000000000000000000000", + "1668589774968665316696047901801606685030143589709/10000000000000000000000000000000000000000000000000" + ], + "new_at_raw_lower": [ + "8890529086421014119/10000000000000000000000000000000000000000000000000", + "8890529086421080299/10000000000000000000000000000000000000000000000000" + ], + "new_at_raw_upper": [ + "-29866980917152322049/10000000000000000000000000000000000000000000000000", + "-29866980917152266101/10000000000000000000000000000000000000000000000000" + ], + "new_at_tested": [ + "1464673416007288863003441470091977383033/10000000000000000000000000000000000000000000000000", + "1464673416007288863003441470091977438357/10000000000000000000000000000000000000000000000000" + ], + "old_at_claim": [ + "-1668785950738799647054310634446839861363893886031/10000000000000000000000000000000000000000000000000", + "-66751438029551985882172425377873594454555753177/400000000000000000000000000000000000000000000000" + ], + "old_at_old_crossing_upper": [ + "-357270001119021587349/10000000000000000000000000000000000000000000000000", + "-357270001119021530951/10000000000000000000000000000000000000000000000000" + ] + }, + "empty_root_credits": 0, + "exact_gain": "215259997/500000000000000", + "exact_relative_percent": "21525999700/1823110718223", + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "incumbent": "1823110718223/500000000000000", + "main_boundaries": 104, + "native_grid": [ + 1125, + 25 + ], + "native_ingredient_claim": "3646017316711/1000000000000000", + "new_raw_interval": [ + "364665195644044790699554028334161/100000000000000000000000000000000000", + "182332597822022395349777014167081/50000000000000000000000000000000000" + ], + "old_raw_upper": "36462214364462343366888845568981/10000000000000000000000000000000000", + "ordinary": 782715464, + "ordinary_delta": 52088, + "ordinary_headroom": 217284536, + "outer_functional": 4, + "outer_strict": 54, + "outer_strict_slack": "299635334804355997/10000000000000000000000000000000000", + "owned_lifetimes": 73, + "owned_peak": 50, + "paid": { + "1": 68384, + "2": 14501, + "3": 14093, + "4": 3791, + "5": 5865, + "6": 238, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "paid_delta": { + "1": -17, + "5": -17, + "6": 17 + }, + "paid_positions": 110519, + "parent": "9d0119eb12fbd9fa534b48cd37b68e7099757b91", + "path_pins": { + "dependencies/7298/pricing.py": { + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182" + }, + "dependencies/7314/NATIVE-RESULT.json": { + "sha256": "336f463da5afe5b60bfd3b9f0ce8aeea5a5feb1f854613bf4218ba0b28b3371b" + }, + "dependencies/7314/PROPOSED-CLAIM.json": { + "sha256": "41a08c4b7d0b2de4af22bc778948a143027eb3065fff47b0400b6ded1cc52778" + }, + "dependencies/7314/RESULT.json": { + "sha256": "432191ca572c9221935787ebe392699e3a1ef4512b0bf4fbc704657321cc87ca" + }, + "dependencies/round65/price.json": { + "sha256": "25205ad2cf4230bd2b2b704eec9f96ec4a5486fd575b5599861b28ffdd15b00b" + }, + "receipts/EARLY-RESULT.json": { + "git_blob": "675d6cf2374f3384019dfd53b2bdffd845005f13", + "sha256": "ad1ca9b2e2febbf80d9bf8b6ceef14ff90fcc29ef9358310e551628eb1706649" + }, + "receipts/INPUTS.json": { + "git_blob": "95c53f4594287a72d9b586f10ee136d0a1686984", + "sha256": "abedac59097a1c35c27d91cbdb07207bc562a64743bc406d13c94a8bc970592d" + }, + "receipts/NATIVE-RESULT.json": { + "git_blob": "eb101307d4d0399efed96d88cf6d4c01ec9c7369", + "sha256": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812" + }, + "receipts/PROOF.md": { + "git_blob": "7644e5571d583183ee93b686612b5ec4555f6911", + "sha256": "560de573bfd4563c16ca3c7308fa729b4188fabe802d8830f343c3873f75b59d" + }, + "receipts/PROPOSED-CLAIM.json": { + "git_blob": "6b491894580741e3e2c11a453722a0302db7b5d6", + "sha256": "6e31241944c123d2bd4aa8bc94d833b44b3d889bd6d9aafc579108f416b45f03" + }, + "receipts/README.md": { + "git_blob": "b3a055f4e0d334ce2e7df3310caaa0849eb3eba1", + "sha256": "b4db0eb83ab6a2f7151bed2da955a487f4816ec9d1976eccc21e54c2725490b0" + }, + "receipts/REFERENCE.json": { + "git_blob": "8859e243cc39546bcb1e257d95c19a658c455dc7", + "sha256": "3e66e054b803551f18b8670da0b2990a7d0eeb689dfc45b56dbcba295551da70" + }, + "receipts/REPLAY.txt": { + "git_blob": "0b8d8048c18740060f4b7f6d380a5f3a0f30ee53", + "sha256": "230984f4b8206ae4d0c0f18fbba86ff43a1a9623f8ed337cf1285360f9a67c0c" + }, + "receipts/RESULT.json": { + "git_blob": "3034a490f5b0656ae71495c99493c4ab1ac1f5c6", + "sha256": "7f2d587c59f063b01f1e8b320084a7f0943f2f05d65e3e0f5e80448c6c8e8194" + }, + "receipts/SOURCES.json": { + "git_blob": "6b97e903a6df8de437068a0e2907823885928053", + "sha256": "ac7b4473035af648d6073e78b6c39675e706e8194b346bb55ed62a0adc81d593" + }, + "receipts/VERIFY.json": { + "git_blob": "cc98ee2a5c5a79e670094a6f55c7cacda8fd330c", + "sha256": "ede7dd2dd3733b9a73f72af9dd7edfe819b49b859c5c76e227ec82cb9c220513" + }, + "receipts/construct.py": { + "git_blob": "89e923bd738dfc404ca76b7ae36f13844ac4bfbb", + "sha256": "ecb39578063d7f09153a85370a3b9bb7cbf8b36ff9891033a1cce7a2fe7f7fda" + } + }, + "physical_maps": 3037, + "productive_fields": 22461, + "rank_surplus": 1424, + "raw_strict_separation": "43051999421357030665572644351/100000000000000000000000000000000000", + "scope": "Exact receipt and directed-price readback. No native or caller execution in this audit.", + "source_archive_sha256": "0589953b3886d96eacf3bda3d38d8d574bb739fba1056af7f32f56047b6061e2", + "targets": { + "1": 306, + "2": 357, + "3": 799, + "4": 3825, + "5": 1360, + "6": 731, + "7": 323, + "8": 544, + "9": 10888, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208, + "137": 208 + }, + "tested": "364665195644007/100000000000000000" +} diff --git a/research/p104-type-a-query-fixed-cut/inputs/QUERY-CENSUS.json b/research/p104-type-a-query-fixed-cut/inputs/QUERY-CENSUS.json new file mode 100644 index 0000000000..9e3320bb7c --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/inputs/QUERY-CENSUS.json @@ -0,0 +1,674 @@ +{ + "caller_sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "controls": { + "negative_determinant_one_slack_one": true, + "positive_exact_slack_two": true + }, + "dimension": 36, + "head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "mutants": [ + { + "minus_endpoint_difference_rank": 1, + "proof": "slack_one", + "remaining_defect_rank_budget": 37, + "removed": [ + 1516 + ] + }, + { + "minus_endpoint_difference_rank": 1, + "proof": "slack_one", + "remaining_defect_rank_budget": 37, + "removed": [ + 1580 + ] + }, + { + "minus_endpoint_difference_rank": 1, + "proof": "slack_one", + "remaining_defect_rank_budget": 37, + "removed": [ + 1659 + ] + }, + { + "minus_endpoint_difference_rank": 1, + "proof": "slack_one", + "remaining_defect_rank_budget": 37, + "removed": [ + 1721 + ] + }, + { + "minus_endpoint_difference_rank": 2, + "proof": "slack_zero", + "remaining_defect_rank_budget": 36, + "removed": [ + 1516, + 1580 + ] + }, + { + "minus_endpoint_difference_rank": 2, + "proof": "slack_zero", + "remaining_defect_rank_budget": 36, + "removed": [ + 1516, + 1659 + ] + }, + { + "minus_endpoint_difference_rank": 2, + "proof": "slack_zero", + "remaining_defect_rank_budget": 36, + "removed": [ + 1516, + 1721 + ] + }, + { + "minus_endpoint_difference_rank": 2, + "proof": "slack_zero", + "remaining_defect_rank_budget": 36, + "removed": [ + 1580, + 1659 + ] + }, + { + "minus_endpoint_difference_rank": 2, + "proof": "slack_zero", + "remaining_defect_rank_budget": 36, + "removed": [ + 1580, + 1721 + ] + }, + { + "minus_endpoint_difference_rank": 2, + "proof": "slack_zero", + "remaining_defect_rank_budget": 36, + "removed": [ + 1659, + 1721 + ] + }, + { + "minus_endpoint_difference_rank": 3, + "proof": "rank", + "remaining_defect_rank_budget": 35, + "removed": [ + 1516, + 1580, + 1659 + ] + }, + { + "minus_endpoint_difference_rank": 3, + "proof": "rank", + "remaining_defect_rank_budget": 35, + "removed": [ + 1516, + 1580, + 1721 + ] + }, + { + "minus_endpoint_difference_rank": 3, + "proof": "rank", + "remaining_defect_rank_budget": 35, + "removed": [ + 1516, + 1659, + 1721 + ] + }, + { + "minus_endpoint_difference_rank": 3, + "proof": "rank", + "remaining_defect_rank_budget": 35, + "removed": [ + 1580, + 1659, + 1721 + ] + }, + { + "minus_endpoint_difference_rank": 4, + "proof": "rank", + "remaining_defect_rank_budget": 34, + "removed": [ + 1516, + 1580, + 1659, + 1721 + ] + } + ], + "ports": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 16, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 28, + 29, + 30, + 31, + 32, + 33, + 36, + 37, + 38, + 39, + 40, + 41, + 43, + 44, + 45, + 46, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103 + ], + "proof_census": { + "rank": 5, + "slack_one": 4, + "slack_zero": 6 + }, + "q_minus_endpoint": "-I", + "q_plus_endpoint": "+I", + "query_events": { + "1516": { + "destination": 0, + "q_power": -1, + "relative_defect_rank": 1, + "source": 1 + }, + "1580": { + "destination": 0, + "q_power": -1, + "relative_defect_rank": 1, + "source": 1 + }, + "1659": { + "destination": 0, + "q_power": -1, + "relative_defect_rank": 1, + "source": 1 + }, + "1721": { + "destination": 0, + "q_power": -1, + "relative_defect_rank": 1, + "source": 1 + } + }, + "relative_j_blocks": [ + { + "axes": [ + 1, + 0, + 18, + 19 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 1, + "-2" + ], + [ + 18, + 19, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 1 + }, + { + "axes": [ + 2, + 0, + 18, + 20 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 2, + "-2" + ], + [ + 18, + 20, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 2 + }, + { + "axes": [ + 3, + 0, + 18, + 21 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 3, + "-2" + ], + [ + 18, + 21, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 3 + }, + { + "axes": [ + 4, + 0, + 18, + 22 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 4, + "-2" + ], + [ + 18, + 22, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 4 + }, + { + "axes": [ + 5, + 0, + 18, + 23 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 5, + "-2" + ], + [ + 18, + 23, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 5 + }, + { + "axes": [ + 6, + 0, + 18, + 24 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 6, + "-2" + ], + [ + 18, + 24, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 6 + }, + { + "axes": [ + 7, + 0, + 18, + 25 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 7, + "-2" + ], + [ + 18, + 25, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 7 + }, + { + "axes": [ + 8, + 0, + 18, + 26 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 8, + "-2" + ], + [ + 18, + 26, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 8 + }, + { + "axes": [ + 9, + 0, + 18, + 27 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 9, + "-2" + ], + [ + 18, + 27, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 9 + }, + { + "axes": [ + 10, + 0, + 18, + 28 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 10, + "-2" + ], + [ + 18, + 28, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 10 + }, + { + "axes": [ + 11, + 0, + 18, + 29 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 11, + "-2" + ], + [ + 18, + 29, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 11 + }, + { + "axes": [ + 12, + 0, + 18, + 30 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 12, + "-2" + ], + [ + 18, + 30, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 12 + }, + { + "axes": [ + 13, + 0, + 18, + 31 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 13, + "-2" + ], + [ + 18, + 31, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 13 + }, + { + "axes": [ + 14, + 0, + 18, + 32 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 14, + "-2" + ], + [ + 18, + 32, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 14 + }, + { + "axes": [ + 15, + 0, + 18, + 33 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 15, + "-2" + ], + [ + 18, + 33, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 15 + }, + { + "axes": [ + 16, + 0, + 18, + 34 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 16, + "-2" + ], + [ + 18, + 34, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 16 + }, + { + "axes": [ + 17, + 0, + 18, + 35 + ], + "plus_identity_restricted_rank": 2, + "relative_defect_entries": [ + [ + 0, + 17, + "-2" + ], + [ + 18, + 35, + "2" + ] + ], + "relative_defect_rank": 2, + "stage": 17 + } + ], + "subsets_tested": 15, + "unvisited_subsets": [] +} diff --git a/research/p104-type-a-query-fixed-cut/inputs/pricing.py b/research/p104-type-a-query-fixed-cut/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/inputs/pricing.py @@ -0,0 +1,82 @@ +"""Directed interval arithmetic and the retained signed BIT invoice.""" +from collections import Counter +from fractions import Fraction +from functools import cache + +TARGET = "10018846261809/2500000000000000" +SCALE = 10**49 + + +def rounded(x, upper): + scaled = SCALE*x + if upper: + return Fraction(-((-scaled.numerator) // scaled.denominator), SCALE) + return Fraction(scaled.numerator // scaled.denominator, SCALE) + + +@cache +def log_bounds(x): + z = (x-1)/(x+1) + terms = 60 + exact_partial = 2*sum(z**(2*i+1)/(2*i+1) for i in range(terms)) + tail = 2*z**(2*terms+1)/((2*terms+1)*(1-z*z)) + return rounded(exact_partial, False), rounded(exact_partial+tail, True) + + +@cache +def power_bounds(rank, k): + binary = 2**(rank.bit_length()-1) + shift = binary.bit_length()-1 + l2, u2 = log_bounds(Fraction(2)) + lo, hi = log_bounds(Fraction(rank, binary)) + lo, hi = k*(lo+shift*l2), k*(hi+shift*u2) + assert 0 <= lo <= hi < 1 + + def exponential(z, terms): + total = term = Fraction(1) + for i in range(1, terms+1): + term *= -z/i + total += term + return total + + return rounded(rank*exponential(hi, 35), False), rounded(rank*exponential(lo, 34), True) + + +def cost(hist, k): + lower = upper = Fraction(0) + for r, n in hist.items(): + a, b = (n*x for x in power_bounds(r, k)) + lower += min(a, b) + upper += max(a, b) + return lower, upper + + +def profile(invoice, native, word, ranks): + copies = invoice["native_calls"] + assert copies == len(invoice["native_instances"]) == 36 + assert {tuple((r["stage"], r["copy"])) for r in invoice["native_instances"]} == { + (stage, which) for stage in range(1, 19) for which in (0, 1) + } + assert all(r["ports"] == 111 for r in invoice["native_instances"]) + assert native == Counter({int(r): n for r, n in invoice["native_paid"].items()}) + assert sum(native.values()) == 2871 + caller_paid = {1: 444, **{r: 444 for r in range(7, 57, 7)}} + assert invoice["event_counts"]["QUERY"]*111 == caller_paid[1] + assert invoice["event_counts"]["IDLE_ONE"]*111 == 8*444 + full_paid = Counter({r: copies*n for r, n in native.items()}) + full_paid.update(caller_paid) + + helpers = Counter(ranks[word["final"][j]]-ranks[word["start"][j]] + for j in range(222, word["public"])) + assert helpers == Counter({int(r): n for r, n in invoice["native_helpers"].items()}) + caller_targets = {**{r: 444 for r in range(8, 65, 7)}, 127: 222} + full_targets = Counter({r: copies*n for r, n in helpers.items()}) + full_targets.update(caller_targets) + assert full_paid == Counter({int(r): n for r, n in invoice["paid"].items()}) + assert full_targets == Counter({int(r): n for r, n in invoice["targets"].items()}) + assert sum(full_paid.values()) == invoice["paid_jobs"] + assert sum(full_targets.values()) == invoice["productive_fields"] + signed = full_targets.copy() + signed.subtract(full_paid) + assert sum(r*n for r, n in signed.items()) == invoice["rank_surplus"] + return signed, copies diff --git a/research/p104-type-a-query-fixed-cut/receipts/SHA256.json b/research/p104-type-a-query-fixed-cut/receipts/SHA256.json new file mode 100644 index 0000000000..ab202b5854 --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/receipts/SHA256.json @@ -0,0 +1,10 @@ +{ + "DERIVATIVE.json": "54e4985325df8ec772648567648d865811e72e3f65bee1f3777ff65a7ee45c6d", + "DIRECT.json": "380e384841d7d8753de07436f2a9705de267f43d67fb4e5d7c7c8cd62233d4d2", + "FORMAL-PROBES.json": "d7abbc3f5c6462cdc86c13246e439a5d5212e120905618f9a315bcfc8c2e54a8", + "FULL-BODY.json": "9aba50b267aa4c12cc8c6453bb9a4177fde213e520ca78b33a34c2a8cb831838", + "GAUSSIAN.json": "5bc0f4fd3fece7223551be76d7e4343631e7ee3156b73d3d01c81446a9e7e214", + "PRICE.json": "52e05b80069ce01cad3b8e5f3cf9123e930de36987bd398dd43f103953a4674a", + "SYMBOLIC.json": "ee74faa58377e9496de81b1a50057ce62c3c046340a1c9fc19e2c9ae1f15843a", + "UNIT.json": "84049bddeed687a28954fa0b8bb993d676900b4eb86ebd6e54ca1f7c60e27887" +} diff --git a/research/p104-type-a-query-fixed-cut/replay.py b/research/p104-type-a-query-fixed-cut/replay.py new file mode 100644 index 0000000000..7fa1679779 --- /dev/null +++ b/research/p104-type-a-query-fixed-cut/replay.py @@ -0,0 +1,126 @@ +"""Replay the exact signed QUERY pair prices and formal fixed-cut result.""" +from argparse import ArgumentParser +from gzip import decompress +from hashlib import sha1, sha256 +from json import loads +from pathlib import Path +from shutil import copyfile, copytree +from subprocess import run +from sys import executable +from tempfile import TemporaryDirectory + +HERE = Path(__file__).resolve().parent +CALLER = "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc" +CALLER_BLOB = "9451ceaf6e8e037894680b549f3ef41c21b260d7" +SELECTED, UNRESOLVED = [1580, 1659], [1516, 1721] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def unique(pairs): + result = dict(pairs) + require(len(result) == len(pairs), "Duplicate JSON key or input path") + return result + + +def read(raw): + return loads(raw, object_pairs_hook=unique) + + +def digest(raw): + return sha256(raw).hexdigest() + + +def replay(output): + require(__debug__, "CPython assertions must be enabled") + pins = read((HERE / "LOCAL-PINS.json").read_bytes()) + for name, expected in pins.items(): + path = HERE / name + require(path.resolve().is_relative_to(HERE) and digest(path.read_bytes()) == expected, + f"Changed pinned file {name}") + expected = read((HERE / "receipts/SHA256.json").read_bytes()) + raw = decompress((HERE / "inputs/7113-CALLER.json.gz").read_bytes()) + header = f"blob {len(raw)}".encode() + bytes(1) + require(digest(raw) == CALLER and sha1(header + raw).hexdigest() == CALLER_BLOB, + "Changed exact #7113 caller") + output.mkdir(parents=True, exist_ok=False) + with TemporaryDirectory(prefix="p104-query-pair-") as tmp: + work = Path(tmp) + copytree(HERE / "engines", work, dirs_exist_ok=True) + price_root, lead, independent = (work / name for name in ("price", "lead", "independent")) + inputs = price_root / "inputs" + inputs.mkdir() + for name in ("QUERY-CENSUS.json", "7334-READBACK.json", "7334-ADMITTED.json", "pricing.py"): + copyfile(HERE / "inputs" / name, inputs / name) + caller = inputs / "7113-CALLER.json" + caller.write_bytes(raw) + + def stage(name, script, *args, timeout=20): + result = run([executable, "-I", "-B", str(script), *map(str, args)], cwd=work, + capture_output=True, check=True, timeout=timeout) + require(digest(result.stdout) == expected[name], f"Changed receipt {name}") + (output / name).write_bytes(result.stdout) + return read(result.stdout) + + price = stage("PRICE.json", price_root / "quote.py") + price_path = price_root / "PRICE.json" + copyfile(output / "PRICE.json", price_path) + stage("DERIVATIVE.json", price_root / "derivative_check.py") + direct = stage("DIRECT.json", lead / "fixed_cut.py", work) + unit = stage("UNIT.json", independent / "transported_product.py", "--price", price_path, "--price-sha", + expected["PRICE.json"], "--caller", caller) + args = ("--price", price_path, "--caller", caller, "--unit-receipt", output / "UNIT.json") + finite = stage("FORMAL-PROBES.json", independent / "formal_necessity.py", *args) + gaussian = stage("GAUSSIAN.json", independent / "gaussian_necessity.py", *args) + symbolic = stage("SYMBOLIC.json", independent / "symbolic_transport.py", "--price", price_path, + "--caller", caller, "--gaussian", output / "GAUSSIAN.json", timeout=25) + body = stage("FULL-BODY.json", lead / "full_body.py", work, timeout=25) + + require(not direct["unvisited"] and not unit["unvisited"] and len(direct["decisions"]) == 6, + "Incomplete unit-body gate") + for a, b, key in zip(direct["decisions"], unit["outcomes"], price["eligible_pairs_before_support"], strict=True): + require(a["key"] == b["pair"] == key and b["q_plus"]["rank"] == 0 and + a["rank"] == b["q_minus"]["rank"] == 2 and + (a["square_witness"] is None) == (b["q_minus"]["square_rank"] == 0), + "Independent signed shape decisions differ") + require([x["key"] for x in direct["decisions"] if x["decision"] == "provisional"] == + unit["rank_at_most_two_square_zero_keys"] == [UNRESOLVED, SELECTED], + "Wrong provisional pairs") + require(len(finite["probes"]) == 17 and len(gaussian["probes"]) == 18, + "Incomplete exact body-specialization controls") + require(symbolic["status"] == "EXACT_SYMBOLIC_AXES" and symbolic["pair"] == SELECTED and + symbolic["unvisited_pair"] == UNRESOLVED and not any(symbolic["cross_actions"].values()) and + not symbolic["outer_body_dependency"] and not symbolic["outer_q_odd_entries"], + "Wrong formal scope or correction") + require([body["fixed_cut"], body["later"]] == SELECTED and + body["independent_basis_columns"] == 144 and body["arbitrary_body_variables"] == 17 and + body["unchanged_recovered_action"] and body["sign_control"] == "passed", + "Independent all-character body replay incomplete") + + caller.write_bytes(raw + b" ") + negative = run([executable, "-I", "-B", str(independent / "transported_product.py"), "--price", + str(price_path), "--price-sha", expected["PRICE.json"], "--caller", str(caller)], + cwd=work, capture_output=True, timeout=20) + require(negative.returncode and b"changed input 7113-CALLER.json" in negative.stderr and + not negative.stdout, "Changed caller was accepted") + + require({p.name for p in output.iterdir()} == set(expected), "Wrong replay receipt set") + print("PASS_TYPE_A_QUERY_PAIR_FIXED_CUT pairs=6 excluded=4 symbolic=1 unresolved=1 kappa_change=0") + + +def main(): + parser = ArgumentParser(description=__doc__) + parser.add_argument("--out", type=Path) + args = parser.parse_args() + if args.out: + replay(args.out.resolve()) + else: + with TemporaryDirectory(prefix="p104-query-pair-receipts-") as temp: + replay(Path(temp) / "out") + + +if __name__ == "__main__": + main()