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 76dc0145fb8ef8457fe96cb961eac162bae8d631 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 11 Nov 2026 08:53:11 -0800 Subject: [PATCH 3/3] Bound independently relabeled P104 owned contacts --- .../p104-owned-contact-tree-bound/AUDIT.json | 207 ++++++++++++++++++ research/p104-owned-contact-tree-bound/NOTICE | 11 + .../p104-owned-contact-tree-bound/PROOF.md | 92 ++++++++ .../PROVENANCE.json | 30 +++ .../p104-owned-contact-tree-bound/README.md | 85 +++++++ .../SOURCES.json | 18 ++ .../p104-owned-contact-tree-bound/TASK.json | 117 ++++++++++ .../p104-owned-contact-tree-bound/VERIFY.json | 19 ++ .../histogram.py | 87 ++++++++ .../inputs/CALLER.json.gz | Bin 0 -> 11215 bytes .../inputs/EARLY-RESULT.json.gz | Bin 0 -> 2087 bytes .../inputs/OWNED-STOCK.json.gz | Bin 0 -> 1615 bytes .../p104-owned-contact-tree-bound/pricing.py | 46 ++++ .../reconstruct.py | 169 ++++++++++++++ .../p104-owned-contact-tree-bound/verify.py | 186 ++++++++++++++++ 15 files changed, 1067 insertions(+) create mode 100644 research/p104-owned-contact-tree-bound/AUDIT.json create mode 100644 research/p104-owned-contact-tree-bound/NOTICE create mode 100644 research/p104-owned-contact-tree-bound/PROOF.md create mode 100644 research/p104-owned-contact-tree-bound/PROVENANCE.json create mode 100644 research/p104-owned-contact-tree-bound/README.md create mode 100644 research/p104-owned-contact-tree-bound/SOURCES.json create mode 100644 research/p104-owned-contact-tree-bound/TASK.json create mode 100644 research/p104-owned-contact-tree-bound/VERIFY.json create mode 100644 research/p104-owned-contact-tree-bound/histogram.py create mode 100644 research/p104-owned-contact-tree-bound/inputs/CALLER.json.gz create mode 100644 research/p104-owned-contact-tree-bound/inputs/EARLY-RESULT.json.gz create mode 100644 research/p104-owned-contact-tree-bound/inputs/OWNED-STOCK.json.gz create mode 100644 research/p104-owned-contact-tree-bound/pricing.py create mode 100644 research/p104-owned-contact-tree-bound/reconstruct.py create mode 100644 research/p104-owned-contact-tree-bound/verify.py diff --git a/research/p104-owned-contact-tree-bound/AUDIT.json b/research/p104-owned-contact-tree-bound/AUDIT.json new file mode 100644 index 0000000000..42a3328eb0 --- /dev/null +++ b/research/p104-owned-contact-tree-bound/AUDIT.json @@ -0,0 +1,207 @@ +{ + "all_regions": 138, + "benchmark_head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "controls": [ + "PASS_EXHAUSTIVE_PARALLEL_EDGE_TOY", + "REJECT_SIMPLE_CYCLE" + ], + "dropped_simple_cycle_edges": 0, + "exact_paid_saving_upper": "0", + "exact_whole_incumbent_margin_upper": "-2004494395516543389/1000000000000000000000000000000000000000000000000", + "incumbent_crossing_upper": "91141748217473298207420876011401/25000000000000000000000000000000000", + "original_margin_upper": "-2004494395516543389/1000000000000000000000000000000000000000000000000", + "owned_contacts": 197, + "paid_regions": 20, + "physical_site_tests": 0, + "region_upper_by_contacts": [ + { + "contacts": [ + 30518, + 30530, + 30532, + 30536 + ], + "per_copy_upper": "0" + }, + { + "contacts": [ + 30541, + 30543, + 30545, + 39925 + ], + "per_copy_upper": "1/1000000000000000000000000000000000000000000000000" + }, + { + "contacts": [ + 30573, + 30580, + 30582, + 39875 + ], + "per_copy_upper": "1/1000000000000000000000000000000000000000000000000" + }, + { + "contacts": [ + 30575, + 30577, + 30588, + 30592, + 41476 + ], + "per_copy_upper": "0" + }, + { + "contacts": [ + 33125, + 33128, + 33129, + 33132, + 45327 + ], + "per_copy_upper": "0" + }, + { + "contacts": [ + 33137 + ], + "per_copy_upper": "0" + }, + { + "contacts": [ + 34507, + 34514, + 34515, + 34517, + 34518, + 34519, + 34520, + 45333 + ], + "per_copy_upper": "1/1000000000000000000000000000000000000000000000000" + }, + { + "contacts": [ + 35408, + 35409, + 35435, + 35436, + 35437, + 35439, + 39841, + 39842, + 39843 + ], + "per_copy_upper": "1/1000000000000000000000000000000000000000000000000" + }, + { + "contacts": [ + 36162, + 36330, + 39822 + ], + "per_copy_upper": "1/1000000000000000000000000000000000000000000000000" + }, + { + "contacts": [ + 36163, + 36164, + 36339, + 36340, + 36342, + 39970, + 39971 + ], + "per_copy_upper": "0" + }, + { + "contacts": [ + 36304, + 36309, + 36310, + 36312, + 36313, + 36314, + 36315 + ], + "per_copy_upper": "1/1000000000000000000000000000000000000000000000000" + }, + { + "contacts": [ + 39791 + ], + "per_copy_upper": "0" + }, + { + "contacts": [ + 39827, + 39828, + 39829, + 39840 + ], + "per_copy_upper": "1/1000000000000000000000000000000000000000000000000" + }, + { + "contacts": [ + 39863 + ], + "per_copy_upper": "0" + }, + { + "contacts": [ + 39962, + 40541, + 40542, + 40544, + 40545, + 43552 + ], + "per_copy_upper": "1/500000000000000000000000000000000000000000000000" + }, + { + "contacts": [ + 41630 + ], + "per_copy_upper": "1/1000000000000000000000000000000000000000000000000" + }, + { + "contacts": [ + 42459, + 42461, + 42471, + 42474 + ], + "per_copy_upper": "1/500000000000000000000000000000000000000000000000" + }, + { + "contacts": [ + 42463, + 42518 + ], + "per_copy_upper": "1/1000000000000000000000000000000000000000000000000" + }, + { + "contacts": [ + 42482, + 42484 + ], + "per_copy_upper": "1/1000000000000000000000000000000000000000000000000" + }, + { + "contacts": [ + 44259 + ], + "per_copy_upper": "0" + } + ], + "resolved_histogram_comparisons": 6100, + "source_sha256": { + "inputs/CALLER.json.gz": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "inputs/EARLY-RESULT.json.gz": "691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7", + "inputs/OWNED-STOCK.json.gz": "df55c81afc652c1d04b3f445efd19aa1d8b151dbb5c6bc369bfa7f1bd3eaa30a" + }, + "status": "PASS_OWNED_CONTACT_TREE_FLOOR", + "unvisited_regions": 0, + "whole_incumbent_margin_upper": "-2004494395516543151/1000000000000000000000000000000000000000000000000", + "whole_saving_upper": "119/500000000000000000000000000000000000000000000000" +} diff --git a/research/p104-owned-contact-tree-bound/NOTICE b/research/p104-owned-contact-tree-bound/NOTICE new file mode 100644 index 0000000000..ea077ff3cf --- /dev/null +++ b/research/p104-owned-contact-tree-bound/NOTICE @@ -0,0 +1,11 @@ +Owned-contact tree floor on the retained P104 word, Apache-2.0. + +The bundled #7113 literal caller and #7277 directed invoice are exact +public source bytes supplied by Rohan Arun. The invoice retains the +#7274 and #7244 native constructions and source-specific notices. +The compact owned-contact projection is regenerated from the exact +public #7277 word and #7113 caller. PROVENANCE.json records the source +commits, paths, Git blobs and SHA-256 values. + +OpenAI Codex and subagents materially assisted the proof, +implementation, independent audit and packaging. diff --git a/research/p104-owned-contact-tree-bound/PROOF.md b/research/p104-owned-contact-tree-bound/PROOF.md new file mode 100644 index 0000000000..973b55a6ed --- /dev/null +++ b/research/p104-owned-contact-tree-bound/PROOF.md @@ -0,0 +1,92 @@ +# Dimension floor for independently relabeled owned contacts + +Fix the literal #7277 scalar chronology, role incidences and all +public or mixed contacts. An eligible vertex is an owned INIT, CLEAR +or SCALE, or an ADD or COPY whose operands are both owned. Each shared +scalar contact receives one chart label. A role edge joins consecutive +contacts of the same lifetime. Edges with one fixed endpoint inherit +that endpoint's original chart. Each component covers all its incident +role edges, and two components cannot touch the same edge. + +## Lower bound for replacement transport + +For two canonical charts corresponding to subspaces U and V, the +relative Clifford rank is bounded below by + +```text +dim(U) + dim(V) − 2 dim(U ∩ V) ≥ |dim(U) − dim(V)|. +``` + +The signed price at the specified probe is +`H(r) = r^(1−κ)` with `H(0) = 0`. A single transport costs at least +`H(|dim(U) − dim(V)|)`. A sequence of intermediate transports also +costs at least this amount. Triangle inequality bounds the sum of +successive dimension differences and subadditivity of H bounds the +price of their sum. This argument grants access to arbitrary chart +labels and charges no incremental phase, ownership, precision, +routing, restoration, tape or scalar work. Any physical replacement +under these fixed contact premises is subject to the lower bound. + +Every fixed endpoint has dimension in `[0,9]`. Clamping any proposed +dimension to this interval preserves those endpoints and cannot +increase any absolute difference. The optimization over dimensions +0 through 9 therefore lower-bounds the minimum paid transport over +every chart dimension. It includes labelings that may lack actual +charts or fail signed operator compatibility. Those extra possibilities +make the computed cost a lower bound. + +## Exact tree recurrence + +Combine each parallel edge into one link with multiplicity m. The +reconstructed 138 components are trees after that step. For a node u +with dimension d, its fixed boundary cost is the sum of +`H(|d−b|)` over the multiset of its fixed endpoint dimensions b. +Orient the component away from one root. A child v contributes + +```text +min over q in [0,9] of (child subtree cost at q + m H(|d−q|)). +``` + +The tree gives disjoint child subproblems conditioned on d. Summing +the boundary and child terms and minimizing at the root therefore +gives the entire relaxed component minimum. The 118 components with +no original paid rank have nonnegative replacement cost and cannot +save. The old edges in the remaining 20 components are nested and +the original paid rank equals the absolute dimension difference. + +The replay first computes a lower bound with downward-rounded +tariffs. Subtracting this lower bound from upward-rounded original +cost yields total apparent saving at most `119/(5 × 10^47)` over all +17 copies. A second leaf-elimination pass compares exact histograms. +For two histograms, subtract their counts and use the lower tariff +for positive differences and the upper tariff for negative ones. +A nonnegative resulting lower bound proves that the chosen +histogram minimizes the actual moment. All 6,100 comparisons resolve +at the incumbent probe. In each paid component the certified +minimizer histogram equals the old one. The total saving upper is +therefore exactly zero there. This assertion establishes an +attained minimum cost, allowing different label assignments or +tied histograms when the prices agree. + +## Complete invoice + +All native productive fields are fixed because the public boundaries +stay fixed. The verified original 17-copy invoice has 110,536 paid +jobs, 22,461 productive positions and rank surplus 1,424. We keep all +caller costs and productive fields. The probe is the exact upper +endpoint of #7277's independently certified crossing enclosure, + +```text +91141748217473298207420876011401/25000000000000000000000000000000000. +``` + +The directed complete net upper remains + +```text +−2004494395516543389/1000000000000000000000000000000000000000000000000. +``` + +The negative sign excludes a strict step clearing this probe by this +mechanism. The result leaves changes inside the old crossing enclosure, +changed scalar chronology or role incidences, coupled public/owned +labels and new caller or provider contracts as separate questions. diff --git a/research/p104-owned-contact-tree-bound/PROVENANCE.json b/research/p104-owned-contact-tree-bound/PROVENANCE.json new file mode 100644 index 0000000000..c714903e9c --- /dev/null +++ b/research/p104-owned-contact-tree-bound/PROVENANCE.json @@ -0,0 +1,30 @@ +{ + "bundled": { + "inputs/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" + }, + "inputs/EARLY-RESULT.json.gz": { + "commit": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "git_blob": "ef86c8ec8ed0a2042017a6f42515e70dd15cfffd", + "path": "research/p104-terminal-cut-rechart/EARLY-RESULT.json", + "sha256": "691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/EARLY-RESULT.json" + }, + "inputs/OWNED-STOCK.json.gz": { + "git_blob": "d6c263509d4336ca3712c235b8961b4d58f37289", + "sha256": "df55c81afc652c1d04b3f445efd19aa1d8b151dbb5c6bc369bfa7f1bd3eaa30a", + "source": "Projection regenerated by reconstruct.py from the three exact public sources" + } + }, + "word_reference": { + "commit": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "git_blob": "077bf48c35db0ddafae81f1bfa0ffacc30894b2b", + "path": "research/p104-terminal-cut-rechart/WORD.json.gz", + "sha256": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/WORD.json.gz" + } +} diff --git a/research/p104-owned-contact-tree-bound/README.md b/research/p104-owned-contact-tree-bound/README.md new file mode 100644 index 0000000000..7199e5fd5f --- /dev/null +++ b/research/p104-owned-contact-tree-bound/README.md @@ -0,0 +1,85 @@ +# Owned-contact tree floor on the retained P104 word + +All 197 exclusively owned scalar contacts of the exact #7277 word +form 138 components. Twenty have original paid incidences. Their +tree minima allow arbitrary individual chart labels, including +nonnested labels and dimensions beyond the original catalogue. +Independent directed comparisons certify exact zero paid saving at +the incumbent crossing upper. **NO VERIFIED GAIN.** Conditional κ +change is 0%. + +The proof keeps the original scalar sequence, role incidences, mixed +and public contact charts, public endpoints, productive positions and +complete signed 17-copy caller fixed. It grants free incremental +scalar work, setup, routing, phases, ownership, restoration, precision +and tape. All components and all 6,100 directed histogram comparisons +resolve. No new physical site or supplier was built. [Proof](PROOF.md) +[Exact receipt](AUDIT.json) + +## Replay + +From a clean checkout with CPython 3.12 and assertions: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-owned-contact-tree-bound +``` + +The registered replay authenticates a compact owned-contact +projection, the exact signed caller and frozen #7277 invoice. It +computes the directed floor in two ways, checks the signed complete +margin, and tests parallel-edge multiplicity against exhaustive +enumeration and rejection of a simple cycle. A verified Git-free +export runs without network access: + +```sh +python3.12 -I -B research/p104-owned-contact-tree-bound/verify.py +``` + +For full literal source reconstruction, run this from the checkout +or export root: + +```sh +( +set -e +word=$(mktemp) +trap 'rm -f "$word"' EXIT +curl -fsSL https://raw.githubusercontent.com/CrocSwap/integer-mult-bounds/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/WORD.json.gz -o "$word" +python3.12 -I -B research/p104-owned-contact-tree-bound/verify.py --word "$word" +) +``` + +The extra check authenticates the original word by Git blob and SHA-256, +rebuilds all 137,891 role edges and the complete invoice from the +literal word and caller, and compares the derived projection with the +bundled one. This keeps the 382 KB word as an exact public reference +while preserving the offline certificate replay. The source and +projection checks produce the same audit. [Source manifest](PROVENANCE.json) + +## Open next questions + +Can changing scalar chronology or jointly changing public and owned +contacts lower the full paid bill? Price a bounded changed contact +family before choosing a site. Any surviving family needs exact +signed forward and adjoint action, returned ownership, restoration, +precision, tape and the complete invoice. This proof addresses +a different contract from arbitrary changes in the caller or provider. + +## Credit + +#7277 supplies the exact native word and complete invoice. #7113 +supplies the retained signed caller. #5590 supplies the fixed-contact +subspace price and triangle argument on #5580. #5140 supplies the +relative Clifford rank lower bound on a different owned wire. +#5144 changes shared maps on an older nonmonotone wire. #6293 gives +the tensor-width phase guard for canonical MOVEs. Earlier same-label +and common-label screens on #7277 narrowed the current scope. This +proof allows independent chart labels at every exclusively owned +contact in each component. [#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277) +[#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +[#5590](https://github.com/CrocSwap/integer-mult-bounds/pull/5590) +[#5140](https://github.com/CrocSwap/integer-mult-bounds/pull/5140) +[#5144](https://github.com/CrocSwap/integer-mult-bounds/pull/5144) +[#6293](https://github.com/CrocSwap/integer-mult-bounds/pull/6293) + +OpenAI Codex and subagents materially assisted proof, implementation, +independent audit and packaging. Apache-2.0. [Notice](NOTICE) diff --git a/research/p104-owned-contact-tree-bound/SOURCES.json b/research/p104-owned-contact-tree-bound/SOURCES.json new file mode 100644 index 0000000000..5335fa97d9 --- /dev/null +++ b/research/p104-owned-contact-tree-bound/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/p104-owned-contact-tree-bound/TASK.json b/research/p104-owned-contact-tree-bound/TASK.json new file mode 100644 index 0000000000..461c2a11fa --- /dev/null +++ b/research/p104-owned-contact-tree-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "All 138 exclusively owned scalar-contact components of the exact #7277 native word, with arbitrary independent chart labels, fixed scalar chronology and literal public boundaries.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent audit and packaging.", + "author": "Round 34 research campaign", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "The complete complex signed moment binds. All simultaneously changed owned regions must collectively fund a strictly positive crossing margin.", + "budget_minutes": 1, + "evidence": "PROOF.md, AUDIT.json and exact native/caller provenance, with a rebuilt incidence graph, independent tree recursion, directed price and source/structural controls.", + "open_questions": [ + { + "blocked_by": "Any surviving family needs exact signed action, returned ownership, restoration, precision and tape.", + "first_step": "Price a bounded changed contact family against the unchanged full signed invoice before building a site.", + "question": "Can changing scalar chronology or coupling owned and public contacts lower the complete paid cost?", + "why_it_matters": "The bound fixes mixed/public contacts and the original role incidences." + } + ], + "original_card": { + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "existing_checks": [ + { + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4133: literal-slot defect", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "status": "author-checked" + }, + { + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4136: uniform commutation gap", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "status": "author-checked" + }, + { + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4140: uniform encoding gap", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "status": "author-checked" + }, + { + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "status": "author-checked" + }, + { + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4154: fiber-tag seam mismatch", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "status": "author-checked" + }, + { + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "status": "reviewed" + } + ], + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "id": "p104-side-correction", + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ] + }, + "outcome": "negative-result", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Nonnested contacts and higher-dimensional labels are granted an optimistic dimension price to test whether this mechanism can clear the unchanged incumbent crossing.", + "scope_status": "changed", + "stop_rule": "Exhaust 138 components and all 20 paid regions within 60 runner seconds. Stop when the complete optimistic margin is negative. Retain unvisited regions on cap.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-owned-contact-tree-bound/VERIFY.json b/research/p104-owned-contact-tree-bound/VERIFY.json new file mode 100644 index 0000000000..61a54ab201 --- /dev/null +++ b/research/p104-owned-contact-tree-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "checks": "Authenticate pinned projection and invoice, exhaust all 138 owned contact regions, verify the directed whole-invoice floor and run parallel-edge and cycle controls.", + "timeout_seconds": 60 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-owned-contact-tree-bound/histogram.py b/research/p104-owned-contact-tree-bound/histogram.py new file mode 100644 index 0000000000..aa58eb61f2 --- /dev/null +++ b/research/p104-owned-contact-tree-bound/histogram.py @@ -0,0 +1,87 @@ +"""Check exact minimizer histograms with outward signed intervals.""" +from collections import Counter +from fractions import Fraction as Q +from functools import cache + +GRID = 10**48 + + +@cache +def log_interval(x): + z=(x-1)/(x+1) + t=z + partial=Q(0) + for j in range(1,160,2): + partial+=t/j + t*=z*z + return 2*partial,2*(partial+t/(161*(1-z*z))) + + +def exp_negative(x,n): + t=s=Q(1) + for j in range(1,n+1): + t*=-x/j + s+=t + return s + + +def verify_price(r,k,lower,upper): + shift=r.bit_length()-1 + a,b=log_interval(Q(r,2**shift)) + c,d=log_interval(Q(2)) + scale=10**64 + lo=Q((scale*k*(a+shift*c)).__floor__(),scale) + hi=Q((scale*k*(b+shift*d)).__ceil__(),scale) + assert 0<=lo<=hi<1 + assert lower<=GRID*r*exp_negative(hi,49)<=GRID*r*exp_negative(lo,50)<=upper + + +def profile(values): + out=[0]*9 + for rank in values: + if rank: + out[rank-1]+=1 + return tuple(out) + + +def add(a,b): + return tuple(x+y for x,y in zip(a,b,strict=True)) + + +def minimum(group,links,boundary,low,high,dimension_count=10): + adj={u:Counter(links[u]) for u in group} + profiles={u:[profile(abs(d-b) for b in boundary[u]) for d in range(dimension_count)] for u in group} + checked=ambiguous=0 + + @cache + def floor(v): + return sum(n*low[r] for r,n in enumerate(v,1)) + + @cache + def difference_floor(v): + return sum(n*(low[r] if n>0 else high[r]) for r,n in enumerate(v,1)) + + def choose(options): + nonlocal checked,ambiguous + best=min(options,key=floor) + for v in options: + checked+=1 + delta=tuple(a-b for a,b in zip(v,best,strict=True)) + ambiguous+=difference_floor(delta)<0 + return best + + while len(adj)>1: + leaves=[u for u,a in adj.items() if len(a)==1] + if not leaves: + raise ValueError('simple graph has a cycle') + u=max(leaves) + v,m=adj[u].popitem() + assert adj[v].pop(u)==m + for d in range(dimension_count): + merged=choose([add(p,profile([abs(d-q)]*m)) for q,p in enumerate(profiles[u])]) + profiles[v][d]=add(profiles[v][d],merged) + del adj[u] + u=next(iter(adj)) + assert not adj[u] + answer=choose(profiles[u]) + return floor(answer),answer,checked,ambiguous diff --git a/research/p104-owned-contact-tree-bound/inputs/CALLER.json.gz b/research/p104-owned-contact-tree-bound/inputs/CALLER.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..290ef7c9c52553e421350ea76ac73eb98d1f187b GIT binary patch literal 11215 zcmZv=V{j!-{N+8-#L2{VCdtG$Cbn(cww)W>nb_8iZQHo9Z9c#MK3iM+V!OINb-MaZ z*XizWcO4=C%#Z(R;AodQws8le2|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`|LZDAJ$_iWZB7Aj|ZO zHnOeC@=Sw8{`;OQ+mfmABw1``f%?IaNQ%54=iYlRf4!Q`vb&;-*ddi<<8d_&G!8^*P#C4cKTv_`t{>^4Q++!t8)Q~x@f ziJOr8e7Jsgrl0uvxKUXb)w(~>E9FTCtMPYhE+1QN*G*N&Hoq&H{-ZBwx{P%<5m7kr zt@KU=g*RN9*=9rG?!Yw!uoNtTWb2030Y4KA3<+DBwAvw0r@~rapl z!rdS69w?6kqLDqVbDS}ul93$Ns;>kHS44n77!ZmD+`$&mfkWLO(|D!9BJ9(8^F0$z zMiU4rq&(tkfIOnKCIflk52!1gLyAOYf(0xgjcQLwOxh~tUNHB+Ads`U5r$BBl@?N< z1|TPy0RDuO3NvVhx(Em1G(#3PK=HG5t6tC>bCpJpHC7>23e+QDM*%dz3#v4T1A~W? zqjZ0U?Z0cVW`G+^45o{36|0JDuO%YHf=9s30o=%gWmx#fa79+`g@b@AzCauTTd*eT z6No|ZT%?Et5tIxS2jDm4GzY`?t~S}lRJ7f9eSsM=5ZBgU_PY+1wBA1EakYwNPu|=3 z3!dT!qUi%cU@bR-LR95O_uN{1V%Uxi0KMH88GZr@6|Xk6^-Aa>-f&6 zpi3AA91G?Kl9KTe@cr-}SSpp^=6$cr(D8nlS_>I^v=zC@fzn;D9+=|zZZ6mk*>ilS zOP2FzXJ|QH5iVGcQ`$J-E?CadXb3wM%k`ES9qMSJsqaHhC#FPWBTQn=xNf>ndAr>r zPSM0y9a9)FfOFF~`y)0N1^4;QzF+p!DK6pzC=ic;f9Rt~*?p{=*zTt8kv=iKl8K?U zOU$a2PHg5yVjxW^kV2w7sYG`xU7~qitzuWLV=uQjrO?MsT;@$IKJxa*{j#R0mQy{r zaY{5n)lXFMBcVL%LWwSa}LSsH>7!4Pl?P)h<4@b}FMzGeRQY1f8jD zhtnsp$WK>X&n2#Tdcu5SfJCJvj#=Y*>OM6Qp+V)SHh1Ic#d=XO6F*$pAR(UL@WH7o z)EcgB=fwt;6`To#TN9ytgLez3ZpjBO+fJi|b0aC3=$+LS=5~Vn{GiBabf8|}YVT0_ zN%OrAhM0+&w0Lm6D`Qn3gdRkY;4KtT<>YOD-2f3R==6A;RL)5*UII<41dT&WZ}3x- z?c=(rHp|%NZL#@?BE8!k1Ky9driq*7`T5zZjl269UwYlec6QeS=fe$aJu7;`5SO#& z{?o21i+Wbx7i~9N7tQYcO0U{WL2!*rknSwSx<0eV0FM zvD)LT!*#%{Xc{29=pA)+)Glk9A! zt(U_s>fi(NQUyn7_&kUu{^4GQ+M$VW62RoN0TlR>ghxOn9OfKfIDiRCX^gho!iA16 z!i;=5@|iinDgd+EIN%i=1dX3&+*oBLIIu^42ghMDYL)Yrw9~;500q$$Uu>yB+$us^ zPxMl~Kytf|G*MRT!@aP$0c}3#PT6pAeWa8(0c|iQ)a$uBpUmU`5Wlwmxc@k9Rh)rU9#dY!*|``7&4Ki~ZLI{(MpzyGH{CwoL( z=ezqt^^7lD@{OopiN&IzLPfiZD=UMypzxwxELT#mq7UV2VOHKQRx7pCd{t-EDn=no RWU|j!zX7oRttn#~002MZ1rh)N literal 0 HcmV?d00001 diff --git a/research/p104-owned-contact-tree-bound/inputs/OWNED-STOCK.json.gz b/research/p104-owned-contact-tree-bound/inputs/OWNED-STOCK.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..0adb63ddc8ca7886d3b24a1c10fcba5496cf55e7 GIT binary patch literal 1615 zcmV-V2C(@biwFP!000026OEePZrnByh41?qd#wu%|Cv__48ygJ)M#P{jvKTH^6sVh zGvrD~!@V0F@;e+-6iI3K*X8l;`^)o>%O~>7<=ex*_itaH?jQepc>lP6dinPJ`s3y8 z_3|k$m)D1nm!Hq~k8iIZ504-B&re@6rG1FRrQaW3p6YJ;mZFrh-~E z$g#_(s9ueY$2JF9K&@8Ee%VEC(L;1FwiLL+dV&wlHX@f0bA=(MTRF;7txEuTG+FAP zp_Z$$Xq3hZdZ?PC7?nMCW+SQ{b63}i$t3Pfny9s6P;huX=aH)Fq3V`V@E{|fGZ>8X z@CG$rXYwQ?zMqlrVvay=wpI1MRXyN_j0cloV{>g{hr&?z*MYE{O0vZ*8S=?m_O_^DMHd#b{s*7p3gRw(f9`zcH#u~t**5&hov}LyM z(Jl+9SqY&mOQ^0RlOtWD2p*qg7g~k2KGs)|e_lX4~bIy8C~k_ z?Q%_+vevQL8g!CKe)W`-qWbJzLF*Ns&tksi7d`E7S@Fvpv1_5Jdk^Kgg|U3Q&TSC4 zTUx^XqqQYHL_C!3LC+Bw^>jLKRof&!G145F!F+#rvR~$iU5g{J_faUOcUa0O%F=r>tJEo{};8(MX6^o^U3emZlP>AFQ=y0R>qSd7{^ z>J995lSR~FboPP6*) zaGgow7WT=R_Wk=f6w$#aH@f+gyBz``YHvW@q7YhT3H5MCWLda(w1ORRkR_B1M4K$4 zuHNYL2pGG$u~HCKYKmH|kApbKA`14#K^D*$z+rNbMYR0jAVt8~&yAyoXq>$`Za+?- zR=X^s;1k^-3#h9fVM=to6I~Wf6h_qyRof4XVQXI*M`aR^k+17ij+$mpqJ09`d}lN+ zkA*0;iMf3mg#^prR$Viwxi=c-#uc{jv4=cTX(_?&cm+NE^jTE~9l-}#L{;k(jKGNl zRv7!4N=pguXK>hacIe*54xF6^Swam#)X*GFucNBm)f^p7nk<<_IAd5A&~&^;D9h)l z*659NkVQ0LG|W+hwvH~JqiH}8+GP=q`LJ0ck4$DSSgDR9h&r008t%1SK1Z#}Ptn5B z-lWT-Nnn$JO~TwHMu;|9K(zwDw+^y|YVbxn$P$X)P6k;-J#5wZd8<}Iw8;|cG(_F> zG?9+!8Z19u7Ep)&TQJBX3Wteh3B@Dq%q?j7*+Yteahw~YFW7^8j;0_f}h$~2VkVP~s5usI N{s$xg^d`b6004{8CLRC) literal 0 HcmV?d00001 diff --git a/research/p104-owned-contact-tree-bound/pricing.py b/research/p104-owned-contact-tree-bound/pricing.py new file mode 100644 index 0000000000..ae43b50a6a --- /dev/null +++ b/research/p104-owned-contact-tree-bound/pricing.py @@ -0,0 +1,46 @@ +"""Directed arithmetic for the complete signed price.""" +from fractions import Fraction as F +from functools import cache + +TARGET = F(10018846261809, 2500000000000000) +GRID = 10**48 + + +def round_interval(a, b): + a, b = a*GRID, b*GRID + return F(a.numerator//a.denominator, GRID), F(-((-b.numerator)//b.denominator), GRID) + + +@cache +def log_unit(x): + y = (x-1)/(x+1) + p = sum((2*y**j/j for j in range(1, 111, 2)), F(0)) + return round_interval(p, p+2*y**111/(111*(1-y*y))) + + +@cache +def power(rank, k): + e = rank.bit_length()-1 + lo,hi = [q+e*d for q,d in zip(log_unit(F(rank, 2**e)),log_unit(F(2)),strict=True)] + + def exp_negative(x, n): + term = total = F(1) + assert 0 <= x < 1 + for i in range(1,n+1): + term *= -x/i + total += term + return total + + return round_interval(rank*exp_negative(k*hi, 39), rank*exp_negative(k*lo, 40)) + + +def moment(P, T, k): + lower = upper = F(0) + for r in P.keys()|T.keys(): + n = T[r]-P[r] + lo,hi = power(r,k) + if n < 0: + lo,hi = hi,lo + lower += n*lo + upper += n*hi + return lower,upper diff --git a/research/p104-owned-contact-tree-bound/reconstruct.py b/research/p104-owned-contact-tree-bound/reconstruct.py new file mode 100644 index 0000000000..5f4baee253 --- /dev/null +++ b/research/p104-owned-contact-tree-bound/reconstruct.py @@ -0,0 +1,169 @@ +"""Reconstruct the owned-contact projection and signed invoice from literal inputs.""" +from collections import Counter, defaultdict +from functools import cache + + +def gf2_rank(rows): + pivots = {} + for v in rows: + while v: + pivot = v.bit_length() + if pivot not in pivots: + pivots[pivot] = v + break + v ^= pivots[pivot] + return len(pivots) + + +def reconstruct(word, caller, invoice): + public = word["public"] + program = word["program"] + frames = word["frames"] + dims = [len(frame) for frame in frames] + assert all(gf2_rank(frame) == dim for frame, dim in zip(frames, dims, strict=True)) + owned = word["owned_fields"] + + @cache + def rank(a, b, is_owned): + if a == b: + return 0 + gap = dims[b] - dims[a] + relative = 2 * gf2_rank(frames[a] + frames[b]) - dims[a] - dims[b] + assert relative == abs(gap) > 0 + assert is_owned or gap > 0 + return relative + + local = {} + for clock, (op, role, *args) in enumerate(program): + if role >= public and ( + op in ("INIT", "CLEAR", "SCALE") + or op in ("ADD", "COPY") and args[0] >= public + ): + local[clock] = dims[args[-1]] + + current = word["initial"] + [None] * owned + previous = [(-1, f) for f in word["initial"]] + [None] * owned + pending = [None] * (public + owned) + adjacency = {clock: set() for clock in local} + internal = Counter() + boundary = defaultdict(list) + native_paid = Counter() + edge_count = 0 + lifetimes = 0 + + def touch(role, clock, frame): + nonlocal edge_count + assert current[role] == frame + old_clock, old_frame = previous[role] + move = pending[role] + assert (old_frame == frame and move is None) or move == (old_frame, frame) + assert old_clock < clock + edge_count += 1 + previous[role] = clock, frame + pending[role] = None + if old_clock not in local and clock not in local: + return + assert role >= public + if old_clock in local and clock in local: + adjacency[old_clock].add(clock) + adjacency[clock].add(old_clock) + internal[old_clock, clock] += 1 + elif old_clock in local: + boundary[old_clock].append(dims[frame]) + else: + boundary[clock].append(dims[old_frame]) + + for clock, (op, role, *args) in enumerate(program): + if op == "MOVE": + start, end, is_owned = args + assert current[role] == start and is_owned == (role >= public) + assert previous[role] is not None and pending[role] is None + native_paid[rank(start, end, is_owned)] += 1 + current[role] = end + pending[role] = start, end + elif op == "INIT": + (frame,) = args + assert role >= public and current[role] is previous[role] is pending[role] is None + current[role] = frame + previous[role] = clock, frame + else: + assert op in ("ADD", "COPY", "SCALE", "CLEAR") + frame = args[-1] + touch(role, clock, frame) + if op in ("ADD", "COPY") and args[0] != role: + touch(args[0], clock, frame) + if op == "CLEAR": + assert role >= public + current[role] = previous[role] = None + lifetimes += 1 + + assert current == word["final"] + [None] * owned and lifetimes == 70 + assert all(v is None for v in previous[public:]) + for role, frame in enumerate(word["final"]): + touch(role, len(program), frame) + assert all(v is None for v in pending) + assert edge_count == 137891 and sum(native_paid.values()) == 6280 + + # Assign each mutable contact to exactly one connected component. + component = {} + for root in sorted(local): + if root in component: + continue + component[root] = root + queue = [root] + for clock in queue: + for neighbor in sorted(adjacency[clock]): + if neighbor not in component: + component[neighbor] = root + queue.append(neighbor) + regions = { + root: {"contacts": [], "links": [], "boundary": []} + for root in sorted(set(component.values())) + } + for clock, dim in sorted(local.items()): + row = regions[component[clock]] + row["contacts"].append([clock, dim]) + row["boundary"].extend([clock, b] for b in sorted(boundary[clock])) + for (u, v), count in sorted(internal.items()): + assert component[u] == component[v] + regions[component[u]]["links"].append([u, v, count]) + + main = set(word["live"]) | {r + 112 for r in word["live"]} | set( + word["hosted"]["X2"] + word["hosted"]["Y2"] + ) + assert len(main) == 400 + native_targets = Counter( + rank(a, b, False) + for role, (a, b) in enumerate(zip(word["initial"], word["final"], strict=True)) + if role not in main + ) + assert 0 not in native_targets and sum(native_targets.values()) == 1101 + copies = [event[1] for event in caller["events"] if event[0] == "J"] + assert copies == list(range(1, 18)) + paid, targets = ( + Counter({r: len(copies) * q for r, q in hist.items()}) + for hist in (native_paid, native_targets) + ) + for spec in caller["types"].values(): + for sign, offset, *bits in spec["diagonal"]: + assert sign == -1 and offset == 0 and len(bits) == len(copies) + targets[1 + 8 * sum(bits)] += len(spec["ports"]) + for event in caller["events"]: + if event[0] == "J": + continue + ty, op, _, *args = event + n = len(caller["types"][ty]["ports"]) + if op == "QUERY": + paid[1] += n + elif op in ("IDLE_ONE", "IDLE_ODD"): + paid[8 * len(args[0]) + (op == "IDLE_ODD")] += n + assert {str(r): q for r, q in paid.items()} == invoice["P"] + assert {str(r): q for r, q in targets.items()} == invoice["T"] + assert sum(r * (targets[r] - paid[r]) for r in targets.keys() | paid.keys()) == invoice["S"] + return { + "native_contact_edges": edge_count, + "native_paid_moves": sum(native_paid.values()), + "copies": len(copies), + "max_old_chart_dimension": max(dims), + "regions": list(regions.values()), + } diff --git a/research/p104-owned-contact-tree-bound/verify.py b/research/p104-owned-contact-tree-bound/verify.py new file mode 100644 index 0000000000..6a741a0366 --- /dev/null +++ b/research/p104-owned-contact-tree-bound/verify.py @@ -0,0 +1,186 @@ +"""Verify the paid floor for independently relabeled owned contact charts.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as F +import gzip +from hashlib import sha1, sha256 +from itertools import product +import json +from pathlib import Path +import runpy + +PACKAGE = Path(__file__).resolve().parent +CALLER = "inputs/CALLER.json.gz" +INVOICE = "inputs/EARLY-RESULT.json.gz" +STOCK = "inputs/OWNED-STOCK.json.gz" + + +def authenticated(raw, pin, name): + blob = f"blob {len(raw)}\0".encode() + raw + if sha256(raw).hexdigest() != pin["sha256"] or sha1(blob).hexdigest() != pin["git_blob"]: + raise ValueError(f"Changed source: {name}") + return raw + + +def read_inputs(word_path): + manifest = json.loads((PACKAGE / "PROVENANCE.json").read_bytes()) + pins = manifest["bundled"] + assert set(pins) == {CALLER, INVOICE, STOCK} + source = { + name: json.loads(authenticated(gzip.decompress((PACKAGE / name).read_bytes()), pin, name)) + for name, pin in pins.items() + } + if word_path is not None: + word = json.loads(gzip.decompress( + authenticated(word_path.read_bytes(), manifest["word_reference"], "literal #7277 word") + )) + direct = runpy.run_path(str(PACKAGE / "reconstruct.py"))["reconstruct"] + rebuilt = direct(word, source[CALLER], source[INVOICE]["invoice"]) + assert rebuilt == source[STOCK] + return source[STOCK], source[INVOICE], pins + + +def minimize(row, cost, max_dim): + dims = dict(row["contacts"]) + assert dims and len(dims) == len(row["contacts"]) + assert all(0 <= d <= max_dim for d in dims.values()) + links = {u: [] for u in dims} + seen_edges = set() + old = Counter() + for u, v, mult in row["links"]: + assert u < v and (u, v) not in seen_edges and mult > 0 + seen_edges.add((u, v)) + links[u].append((v, mult)) + links[v].append((u, mult)) + old[abs(dims[u] - dims[v])] += mult + assert len(seen_edges) == len(dims) - 1 + boundary = defaultdict(list) + for u, d in row["boundary"]: + assert 0 <= d <= max_dim + boundary[u].append(d) + old[abs(dims[u] - d)] += 1 + labels = range(max_dim + 1) + reached = set() + + def descend(u, parent): + assert u not in reached + reached.add(u) + children = [(descend(v, u), mult) for v, mult in links[u] if v != parent] + return [ + sum(cost[abs(d - b)] for b in boundary[u]) + + sum(min(sub[q] + mult * cost[abs(d - q)] for q in labels) + for sub, mult in children) + for d in labels + ] + + best = min(descend(min(dims), None)) + assert reached == set(dims) + return best, old + + +def toy_control(): + cost = (0, 5, 8, 10) + row = {"contacts": [[10, 0], [20, 1], [30, 2]], + "links": [[10, 20, 2], [20, 30, 1]], + "boundary": [[10, 0], [20, 2], [30, 3]]} + exact = min( + 2 * cost[abs(a-b)] + cost[abs(b-c)] + cost[a] + cost[abs(b-2)] + cost[abs(c-3)] + for a, b, c in product(range(4), repeat=3) + ) + assert minimize(row, cost, 3)[0] == exact + bad = {**row, "links": row["links"] + [[10, 30, 1]]} + try: + minimize(bad, cost, 3) + except AssertionError: + pass + else: + raise AssertionError("simple cycle accepted as a tree") + + +def run(word_path): + toy_control() + stock, receipt, pins = read_inputs(word_path) + regions = stock["regions"] + assert len(regions) == 138 and stock["copies"] == 17 + assert stock["native_paid_moves"] == 6280 and stock["native_contact_edges"] == 137891 + max_dim = stock["max_old_chart_dimension"] + assert max_dim == 9 + k = F(receipt["price"]["independent_raw_bracket"][1]) + paid, target = ( + Counter({int(rank): count for rank, count in receipt["invoice"][key].items()}) + for key in ("P", "T") + ) + assert sum(paid.values()) == 110536 and sum(target.values()) == 22461 + assert sum(rank * (target[rank] - paid[rank]) for rank in paid.keys() | target.keys()) == 1424 + pricing = runpy.run_path(str(PACKAGE / "pricing.py")) + grid = pricing["GRID"] + powers = {r: tuple(int(v * grid) for v in pricing["power"](r, k)) + for r in paid.keys() | target.keys() | set(range(1, max_dim + 1))} + histogram = runpy.run_path(str(PACKAGE / "histogram.py")) + assert histogram["GRID"] == grid + for rank, interval in powers.items(): + histogram["verify_price"](rank, k, *interval) + powers[0] = (0, 0) + low = [powers[r][0] for r in range(max_dim + 1)] + high = [powers[r][1] for r in range(max_dim + 1)] + comparisons = 0 + + contacts = set() + results = {} + for row in regions: + group = tuple(clock for clock, _ in row["contacts"]) + assert not contacts.intersection(group) + contacts.update(group) + best, original = minimize(row, low, max_dim) + old_upper = sum(n * powers[r][1] for r, n in original.items()) + assert best <= old_upper + if any(r > 0 and n for r, n in original.items()): + results[group] = F(old_upper - best, grid) + links, boundary = defaultdict(dict), defaultdict(list) + for u, v, mult in row["links"]: + links[u][v] = links[v][u] = mult + for u, d in row["boundary"]: + boundary[u].append(d) + floor, hist, checked, ambiguous = histogram["minimum"]( + group, links, boundary, low, high, max_dim + 1 + ) + assert floor == best and ambiguous == 0 + assert hist == tuple(original[r] for r in range(1, max_dim + 1)) + comparisons += checked + else: + assert best == 0 + assert len(results) == 20 and comparisons == 6100 + saving = stock["copies"] * sum(results.values()) + _, baseline = pricing["moment"](paid, target, k) + assert baseline + saving < 0 + return { + "status": "PASS_OWNED_CONTACT_TREE_FLOOR", + "benchmark_head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "incumbent_crossing_upper": str(k), + "all_regions": len(regions), + "owned_contacts": len(contacts), + "paid_regions": len(results), + "unvisited_regions": 0, + "dropped_simple_cycle_edges": 0, + "physical_site_tests": 0, + "whole_saving_upper": str(saving), + "exact_paid_saving_upper": "0", + "exact_whole_incumbent_margin_upper": str(baseline), + "resolved_histogram_comparisons": comparisons, + "original_margin_upper": str(baseline), + "whole_incumbent_margin_upper": str(baseline + saving), + "region_upper_by_contacts": [{"contacts": list(group), "per_copy_upper": str(bound)} + for group, bound in sorted(results.items())], + "source_sha256": {name: pin["sha256"] for name, pin in pins.items()}, + "controls": ["PASS_EXHAUSTIVE_PARALLEL_EDGE_TOY", "REJECT_SIMPLE_CYCLE"], + } + + +if __name__ == "__main__": + assert __debug__ + parser = ArgumentParser(description=__doc__) + parser.add_argument("--word", type=Path, + help="Regenerate all contacts and the invoice from the exact public #7277 word") + result = json.dumps(run(parser.parse_args().word), indent=2, sort_keys=True) + "\n" + assert result == (PACKAGE / "AUDIT.json").read_text() + print(result, end="")