diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 63ba3e9aa8..52b62d0481 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,25 @@ # CI verification -## Current selected-family replay: #6030 +## Current selected-family replay: #7000 with #7001 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.00363005817 to the [application review](research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md), +[validation receipts](research/pr-intake-evidence/pr7000-application/VALIDATION.json), +and [explicit source closure](../certificates/frontier7000-source.json). +`make frontier7000-verify` follows that exact-source selected replay. The review +reuses eleven authenticated preceding executions and records seven fresh serial +application, scalar and complete native-catalogue executions. The earlier +monolithic timeout is retained separately and is not completed coverage. +Consult the receipts for exact commands, source heads and limits. + +The five inherited framework assumptions remain. No complete uniform word, +literal multiplier execution, independent human proof or formal-kernel proof +is asserted. Routine research submissions do not need to rerun this +selected-family replay. The sections below preserve historical checkpoints. + +## Historical selected-family replay: #6030 + +The [historical checkpoint](../certificates/checkpoints/frontier6030.json) binds conditional κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md), [validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json), and [explicit source closure](../certificates/frontier6030-source.json). diff --git a/research/historical-selected-replay-gap/README.md b/research/historical-selected-replay-gap/README.md index 55d8cc3b49..36d9a873ca 100644 --- a/research/historical-selected-replay-gap/README.md +++ b/research/historical-selected-replay-gap/README.md @@ -69,7 +69,11 @@ python3 -B scripts/research_package.py --package research/historical-selected-re The direct command prints `PASS_HISTORICAL_SELECTED_REPLAY_GAP`. A registered replay prints `PASS_REGISTERED_RESEARCH_PACKAGE`. Both require Git history -containing the two inspected commits. +containing the two inspected commits and the source and manifest objects at +`2485805a6d47f36ea83ddde6327d453ac82d44dc`. The verifier uses a temporary +sparse checkout of that commit, checks the declared source digests there, and +uses its planner and manifest inventory. The recorded rejections and selection +therefore remain reproducible after later changes to the live Makefile or CI guide. ## Open next questions diff --git a/research/historical-selected-replay-gap/SOURCES.json b/research/historical-selected-replay-gap/SOURCES.json index c1010eec95..62bb8b3950 100644 --- a/research/historical-selected-replay-gap/SOURCES.json +++ b/research/historical-selected-replay-gap/SOURCES.json @@ -4,13 +4,13 @@ "files": [ { "path": "Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "0d683a06b9e7ee162496108ce9a7c5d2ee94fccf", "sha256": "4f2d4f2dcd15139ec82658a975f85ed300897385f85799218539f4c8d60567da" }, { "path": "certificates/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "eccafa830c16170c36faf93045ddf1f638f7bcd4", "sha256": "4c0b9d37e1034b2076e30a70f8e514416298c462d9ee98bc87fe6556b14df786" }, @@ -22,7 +22,7 @@ }, { "path": "docs/ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "63ba3e9aa8bdc5e942b56e34244b92b16f854085", "sha256": "c7d3027e9ad8bcbff68f07aa9576b30fb2f3c76c44d876d40c7fdbf4a3e2228a" }, @@ -34,163 +34,163 @@ }, { "path": "research/clifford-state-performance/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "6f98a0061a5104dfab82c9e806f819b41811f684", "sha256": "396d0f08df24952248140d5c65c51b8c902ef1c580892ff7ea182890530f67ee" }, { "path": "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "5e0f92af463ec12c5e1dcc3effd44081a88af647", "sha256": "07a9daeaf2bda308a92e9a4684f13d5fc766c7772d74801fceb7f4599fdab226" }, { "path": "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "9e13266bf85e627f1b7dc225e9530ea69fd2c7f0", "sha256": "421e1211fb1897c45621dc6801c276e53f2e6f335583c9c9049e535f87c0a3b1" }, { "path": "research/community-batch932-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "cc4d03eb59b9ab3f952735f7e88ff18c2d15d7af", "sha256": "184629cac91a5cfaca50330a88596008b824221433867dcf8117539c913c284a" }, { "path": "research/community-batch970-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8b9f4111badf7de5d97684799560b55110e9da79", "sha256": "23188ed920e38a54006cb883e181585620821c63bf7e8b5e05d32719417cc37e" }, { "path": "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "a5300d4e7a5381a3f443fc54c768ca6f0f236d68", "sha256": "3c820fb30e1b4d9bcfc6a7ab524375e5b2abd66b940af2c509146104f0bcd79c" }, { "path": "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "d7ff6d777b01d69b6ce84caf25d3b7e4a4d2f211", "sha256": "6b185a9902652f893f3ebd8ada92d2f11b6de6533a9a4d11718a8a4496101128" }, { "path": "research/community-hyperplane599-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "546f37d326d10a99910ae8f908e71ef768524d98", "sha256": "65099d764bfcc39bda5e4d9966783611b094c3522dbdd1435cd498d657a8ef8e" }, { "path": "research/community-k492-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "e538481e4cb16ed936d3195f2dfb5b5a9ca0a76b", "sha256": "2c0f4fa5bc150d05658af2e7c54c4d2c337dd52b7efd3d69530ae73bcbdf452a" }, { "path": "research/community-reconciliation92-audit/MANIFEST.json", - "usage": "input", + "usage": "provenance", "git_blob": "2a2e93685173d5f13cbb5abe740f5d90352e0228", "sha256": "5f501f3c118131e7d069f30ad77186eb2ad6961f9680a0ef105f4514ed41808a" }, { "path": "research/partial-swap-digest/baseline.py", - "usage": "input", + "usage": "provenance", "git_blob": "a2f0190704db83bd8ef48e46e723c49b925804fe", "sha256": "81e9af92cdf38243a540cdcff2062778e449467848d444da37a9553c12ca4c34" }, { "path": "research/r420-two-sided-basis/SOURCES.json", - "usage": "input", + "usage": "provenance", "git_blob": "5d718e11e62f4bcadecf1e02d6b61f87dbe190b0", "sha256": "d9810b0d139c5a1211fd2c1f0d142187cc1fca30026e1e7bc4f9ecfacf1596d1" }, { "path": "research/skip-clones/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8d1bb3b9c8189e35e5d8bfdfa632d7473e8be0d5", "sha256": "0b68e63e35a97ce6b0cdb6e291b88ebaa8f2dd4afb70b2498f10ee89428258dc" }, { "path": "research/split-skip/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "2ab610b6ea2edd2865fda793ef2168b0c76afb4f", "sha256": "7c2b4646a3ecfef6f881da5c43e4bd0fa9a4d1b00548b8ab458d897e16735134" }, { "path": "scripts/historical-ci-inputs/Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "aff68409021c9d401a6f8013b9dfd7dbcc30f2a8", "sha256": "ea8830dd79da493e2d75baf753d733ff7efbcf2b4794afe41fae0ac8f3055646" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "65db599ab0b1dea0312c4ca048e0bd0f44c3736f", "sha256": "96ea543e6c707424afe247e77bd86c82152f90fc76a0773c4232145da5cdf8d1" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "34820a8f24678f918f4d0e7a35380d8013fc3495", "sha256": "628391b6abfbc8674ceec1751867a4392f2cc0b5b66886243e139af86cf355ac" }, { "path": "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "c755b76e0d44ba4917aa94440ebe54daefce5b2a", "sha256": "d7fd929726b326aeeaf0a3996475adec88eee9aac09ae0bebeeaa0bc1fc8f199" }, { "path": "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "7f3c012504187917a728b9fe87043f0fc8cd006a", "sha256": "a854022e0e1d5d4db4d60e586be3ea56005013ef14a1fc06d02bc06e8529c4b0" }, { "path": "scripts/historical-ci-inputs/partial-swap-context.json", - "usage": "input", + "usage": "provenance", "git_blob": "ad65114886bf34a4fd27e79f3be502389e689faa", "sha256": "833a9642f33aeab2ffea17ec9c6b82e0a953f90192b2c82e10bef21538dccba9" }, { "path": "scripts/historical-ci-inputs/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "52075f2463f60af5e16571347f24274fce73a1ea", "sha256": "f3c4be597b2f2136da4ae2cc80c7454f63c90aa01f84e5b8131cee4dd55de815" }, { "path": "scripts/partial_swap/shared.py", - "usage": "input", + "usage": "provenance", "git_blob": "44a0e454c70f9c4b98e258b8443612e6a119904b", "sha256": "5a0646a50b9f3e8ea55168620a78e8853b0ab810517cefc8cfb8696aedee278a" }, { "path": "scripts/replay_historical_check.py", - "usage": "input", + "usage": "provenance", "git_blob": "1e92fff2782970ef71378f594f2350d245a4db26", "sha256": "5467619c78183d3adc82b0cb55af28e5c1a01fca2b0588677816244b53e2bafd" }, { "path": "scripts/research_package.py", - "usage": "input", + "usage": "provenance", "git_blob": "091b4c8f58bac9a9580d76025b887dc5c873d05f", "sha256": "e1256016e7f51827d04fa2179255989f639ae1d97afaa9c16265f85a0c6abd70" }, { "path": "scripts/run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "a96ab35b315ce492e7fbbfd6c5ae211aa066b541", "sha256": "49eb56dd0fc0d8d8ffdb209970a7adf2176223580646f575d5c22e59543b381c" }, { "path": "scripts/verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "6882a4700e410dec569b51ae2eaf1a19cc019195", "sha256": "d6b305eac5b9bdb8172c469ad30a1655a60fa0aceac8b1bf610e1b73f51babd8" }, { "path": "tests/test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "343b24abf6719b81805eba5a84c74e57634c8288", "sha256": "3a5470d0b139828b90e19bf9583ddeafcd69f8e34f2824664eb3a2958a52e34d" } diff --git a/research/historical-selected-replay-gap/VERIFY.json b/research/historical-selected-replay-gap/VERIFY.json index 98553e72ed..ab7efa3471 100644 --- a/research/historical-selected-replay-gap/VERIFY.json +++ b/research/historical-selected-replay-gap/VERIFY.json @@ -4,36 +4,7 @@ "python": "3.12", "requirements": [], "inputs": [ - "Makefile", - "certificates/partial-swap-network.json", - "docs/ci-verification.md", - "research/clifford-state-performance/SOURCE.json", - "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "research/community-batch932-audit/CONTENT-COVERAGE.json", - "research/community-batch970-audit/CONTENT-COVERAGE.json", - "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "research/community-hyperplane599-audit/SOURCE.json", - "research/community-k492-audit/SOURCE.json", - "research/community-reconciliation92-audit/MANIFEST.json", - "research/partial-swap-digest/baseline.py", - "research/r420-two-sided-basis/SOURCES.json", - "research/skip-clones/SOURCE.json", - "research/split-skip/SOURCE.json", - "scripts/historical-ci-inputs/Makefile", - "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "scripts/historical-ci-inputs/partial-swap-context.json", - "scripts/historical-ci-inputs/partial-swap-network.json", - "scripts/partial_swap/shared.py", - "scripts/replay_historical_check.py", - "scripts/research_package.py", - "scripts/run_isolated_tests.py", - "scripts/verify_selected_result.py", - "tests/test_isolated_test_runner.py" + "scripts/research_package.py" ], "commands": [ { diff --git a/research/historical-selected-replay-gap/verify.py b/research/historical-selected-replay-gap/verify.py index 83b995941a..9d266c5a4e 100644 --- a/research/historical-selected-replay-gap/verify.py +++ b/research/historical-selected-replay-gap/verify.py @@ -6,8 +6,10 @@ """ import hashlib import importlib.util +import json import subprocess import sys +import tempfile from pathlib import Path ROOT = Path(__file__).resolve().parents[2] @@ -61,31 +63,47 @@ def require(ok, message): raise SystemExit(message) -def load_checker(): - path = ROOT / "scripts/replay_historical_check.py" - spec = importlib.util.spec_from_file_location("historical_selected_replay_gap_checker", path) +def load_module(path): + spec = importlib.util.spec_from_file_location(path.stem, path) module = importlib.util.module_from_spec(spec) spec.loader.exec_module(module) return module +def checkout_snapshot(snapshot, sources, runner, env): + paths = [runner.canonical_relative_path(row["path"]) for row in sources["files"]] + git = ["git", "-c", "maintenance.auto=false", "-c", "gc.auto=0", + "-c", "core.autocrlf=false"] + subprocess.run([*git, "clone", "--quiet", "--shared", "--no-tags", "--no-checkout", + "--", str(ROOT), str(snapshot)], cwd=ROOT, env=env, check=True) + subprocess.run([*git, "update-ref", "--no-deref", "HEAD", INSPECTED], + cwd=snapshot, env=env, check=True) + # The pinned planner reads omitted manifests from the sparse HEAD/index. + patterns = "".join(f"/{path.as_posix()}\n" for path in paths) + subprocess.run([*git, "sparse-checkout", "set", "--no-cone", "--stdin"], + cwd=snapshot, env=env, input=patterns.encode("utf-8"), check=True) + subprocess.run([*git, "read-tree", "-mu", "HEAD"], cwd=snapshot, env=env, check=True) + for path, row in zip(paths, sources["files"], strict=True): + require(hashlib.sha256((snapshot / path).read_bytes()).hexdigest() == row["sha256"], + "historical checkout source digest changed: " + path.as_posix()) + + def entries(checker): for name, config in checker.CONFIG.items(): for entry in [config, *config.get("additional_inputs", [])]: yield name, entry -def reject(checker, entry): +def reject(root, checker, entry): try: - checker.authenticated_input(ROOT, entry) + checker.authenticated_input(root, entry) except ValueError as exc: return str(exc) raise SystemExit("historical input was admitted: " + entry["path"]) -def main(): - require(not sys.flags.optimize, "assertions must stay enabled") - checker = load_checker() +def check_snapshot(root, env): + checker = load_module(root / "scripts/replay_historical_check.py") selected = [entry for name, entry in entries(checker) if name == "tooling-ledger" and entry["path"] == SELECTED_PATH] require(len(selected) == 1, "selected-result checker overlay is not unique") @@ -94,7 +112,7 @@ def main(): require(entry["accepted_live_sha256"] == [SELECTED_ACCEPTED], "accepted selected-checker successors changed") frozen = (checker.INPUTS / entry["input"]).read_bytes() - live = (ROOT / SELECTED_PATH).read_bytes() + live = (root / SELECTED_PATH).read_bytes() require(hashlib.sha256(frozen).hexdigest() == SELECTED_PIN, "frozen selected checker bytes changed") require(hashlib.sha256(live).hexdigest() == SELECTED_LIVE, "live selected checker digest changed") require(SELECTED_LIVE not in (SELECTED_PIN, SELECTED_ACCEPTED), "live checker was already admitted") @@ -102,7 +120,7 @@ def main(): # live successor, not a broken comparison. require(SELECTED_PIN in (SELECTED_PIN, *entry["accepted_live_sha256"]), "pin membership control failed") - require(reject(checker, entry) == REJECTIONS[SELECTED_PATH][1], + require(reject(root, checker, entry) == REJECTIONS[SELECTED_PATH][1], "selected checker rejection text changed") counts = {path: 0 for path in REJECTIONS} @@ -110,7 +128,7 @@ def main(): for _name, item in entries(checker): if item["path"] not in REJECTIONS: continue - message = reject(checker, item) + message = reject(root, checker, item) counts[item["path"]] += 1 messages.setdefault(item["path"], message) for path, (count, message) in REJECTIONS.items(): @@ -118,20 +136,31 @@ def main(): require(messages[path] == message, "rejection text changed for " + path) require(sum(counts.values()) == 19, "rejection total changed") ci = [item for _name, item in entries(checker) if item["path"] == CI_PATH] - require(len(ci) == 1 and hashlib.sha256((ROOT / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, + require(len(ci) == 1 and hashlib.sha256((root / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, "selected CI note digest changed") diff = subprocess.check_output( - ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=ROOT, text=True) + ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=root, env=env, text=True) changed = sorted(name for name in diff.splitlines() if name) require(changed == CHANGED, "inspected commit diff changed") - sys.path.insert(0, str(ROOT / "scripts")) - from research_package import plan_details - details = plan_details(ROOT, set(changed)) + planner = load_module(root / "scripts/research_package.py") + details = planner.plan_details(root, set(changed)) require([row["package"] for row in details] == PLAN_PACKAGES, "helper plan selection changed") matched = {name for row in details for names in row["causes"].values() for name in names} require(sorted(set(changed) - matched) == UNMATCHED, "unmatched plan paths changed") - require(plan_details(ROOT, set()) == [], "empty change set selected a package") + require(planner.plan_details(root, set()) == [], "empty change set selected a package") + + +def main(): + require(not sys.flags.optimize, "assertions must stay enabled") + sources = json.loads(Path(__file__).with_name("SOURCES.json").read_bytes()) + require(sources["base_commit"] == INSPECTED, "historical checkout base changed") + runner = load_module(ROOT / "scripts/research_package.py") + env = runner.git_source_env() + with tempfile.TemporaryDirectory(prefix="historical-selected-replay-") as temporary: + snapshot = Path(temporary) / "snapshot" + checkout_snapshot(snapshot, sources, runner, env) + check_snapshot(snapshot, env) print("PASS_HISTORICAL_SELECTED_REPLAY_GAP") print("selected_checker_live=" + SELECTED_LIVE) print("rejections=19 distinct_paths=7 plan_packages=9") diff --git a/research/p104-endpoint-vector-growth-bound/NOTICE.md b/research/p104-endpoint-vector-growth-bound/NOTICE.md new file mode 100644 index 0000000000..99f7109731 --- /dev/null +++ b/research/p104-endpoint-vector-growth-bound/NOTICE.md @@ -0,0 +1 @@ +Contributed under the repository's Apache-2.0 license. Exact source lineage and predecessor credits are in README.md and PROVENANCE.json. OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging. diff --git a/research/p104-endpoint-vector-growth-bound/PINS.json b/research/p104-endpoint-vector-growth-bound/PINS.json new file mode 100644 index 0000000000..bd02b2f31f --- /dev/null +++ b/research/p104-endpoint-vector-growth-bound/PINS.json @@ -0,0 +1,16 @@ +{ + "PROVENANCE.json": "8e94c73158ee727f2cc4838f0c3423b85f8f170505cf6cef495652abdf55a229", + "cut_flow.py": "a16c67f11d216d0a7d7f4caf0b994cc0a1dcbc01d667ed0924691f72f0959cdb", + "endpoint_replay.py": "24d63caf9e647840f47675fecf775803c509f5fbc7ae6fc6b5d450782ec1d81d", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/closure.py": "64f57a509aac0c7f56c33ce5f84f99c3a4377d4ecc993f7424ad4115542a173f", + "inputs/inventory.py": "347a7d90d34f0d7134d4dc68d95f135ee7cd9e002d6176eb5968f85f00db7d43", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "inputs/target_closure.py": "8ef8fbc45d4f2414944443d2a89147b4b9c2ba225d0faa065dc351f212b709fb", + "receipts/INDEPENDENT-CAP.json": "c91842d00f6df1249c59518200a605e6aa500ea5250314b12419a33bbaf53192", + "receipts/INDEPENDENT-CONTINUATION.json": "a5ff31a1b7e0f795535cd4b61c7976840b1b537baa2267f2b0c5b4c73a117c12", + "receipts/LEAD-ROUNDING.json": "b74f5437faa13e4dcd7c153798f667c390aa72b90c404a80c1b5a7f972347cbc", + "receipts/LEAD-VERTICES.json": "8b5eda4b09ec0fa823c5e9d89363d20eb98f40d74aef2f456224f1904c1ce2bb", + "reverse_inventory.py": "ac01889cd8e917b5c3f93dcefaa19c159efc18bcdd6973b94b481f08185d0127", + "vertices.py": "72954feb814f9bf72c6de107f4614bbd928f48cb0f5ae38e3547c04bb6affaab" +} diff --git a/research/p104-endpoint-vector-growth-bound/PROOF.md b/research/p104-endpoint-vector-growth-bound/PROOF.md new file mode 100644 index 0000000000..cfbddb7bb7 --- /dev/null +++ b/research/p104-endpoint-vector-growth-bound/PROOF.md @@ -0,0 +1,27 @@ +# Common-vector growth with endpoint credits + +Fix the exact #7334 native word and #7113 signed caller. A chart component consists of role segments between literal MOVEs, allocation events or endpoints, joined whenever ADD or COPY requires them to share a chart. All pure public helper components are eligible, including initial and final segments. Fix main, owned and mixed components and keep scalar order and coefficients fixed. + +Choose a common nonzero vector v in F₂⁹. Any subset of eligible components that do not already contain v can adjoin it. Paid edges are literal MOVEs. Each public helper also has a productive edge from its initial to final frame. Keep containment on all edges and positive productive ranks. For an upper bound, paid rank-zero gaps cost zero. The two independent inventories recover 1,517 total groups, 553 eligible groups, 2,573 incident paid edges and 193 incident productive edges. + +## Edge prices + +Write h(r)=r^(1−κ) for r>0 and h(0)=0. Let c_r=h(r)−h(r−1). The old gap of a nested edge L⊂U is d. Use x and y for selection of its low and high frames. + +- If v lies in U, then y=0. Growing L saves c_d on a paid edge and loses c_d on a productive edge. On a productive edge with d=1, forbid x=1. +- If v lies outside U, containment requires x≤y. Growing only U costs c_(d+1) for paid edges and gains c_(d+1) for productive edges. Growing both keeps the gap. +- If neither endpoint can change, there is no changed term. + +The sum is the full changed native price in this model. The unchanged caller multiplies it by 17. The lead converts linear weights and hard nesting implications to maximum closure. The independent solver constructs the finite paid-growth edge U→L, source-to-variable reward and variable-to-sink penalty arcs directly. Under x≤y a productive high-only reward equals c*y−c*x, so it supplies one terminal reward arc and one terminal penalty arc. A fixed zero endpoint is represented by the sink when a hard implication or paid-growth penalty needs it. + +The optimized independent replay cancels common terminal capacity. If a variable has capacity a from the source and b to the sink, each cut crosses exactly one of those arcs. Subtracting min(a,b) from both capacities reduces all cut costs and the offered benefit by the same constant. Hard capacities are assigned afterward to exceed the reduced offered total. The exact upper is unchanged. Positive and forbidden-cut controls exercise both forms. + +## Shared price, exact upper + +Independent per-edge rounding gives lower optimum zero and a tiny positive upper across the interval. Its complete 17-copy upper is 17 × 12669598508059006000 / 10^52 raw. This relaxation lets identical increments take different favorable endpoint values on different edges. + +Instead, use one shared increment vector for all edges. Let integer a_r,b_r be its outward bounds at scale S=10^52 over the exact old crossing bracket. In scale 2S, the box lies inside the L1 ball with center m_r=a_r+b_r and radius R=Σ_r(b_r−a_r). Each coordinate deviates from its center by at most b_r−a_r. The ball is the convex hull of the 18 vertices m±R e_r. + +For each v, the feasible selections depend only on charts and positivity of productive gaps. For each selection its signed price is linear in the nine shared increments. Thus a nonpositive maximum at all 18 vertices bounds it on the entire ball and the exact crossing bracket. Both solvers certify maximum zero on all 511 × 18 cases. The empty selection attains zero. No claimed saving survives within this model. + +The calculation leaves changed scalar operations, distinct added vectors, shrinking, altered MOVE timing and changes to main or owned components outside scope. No new operator or recurrence is claimed. diff --git a/research/p104-endpoint-vector-growth-bound/PROVENANCE.json b/research/p104-endpoint-vector-growth-bound/PROVENANCE.json new file mode 100644 index 0000000000..5a48feb93c --- /dev/null +++ b/research/p104-endpoint-vector-growth-bound/PROVENANCE.json @@ -0,0 +1,57 @@ +{ + "benchmark": { + "compressed_sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "kappa": "0.00364665195644", + "path": "research/p104-helper-319-fused-return/WORD.json.gz", + "pr": 7334, + "uncompressed_sha256": "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + }, + "caller": { + "head": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "pr": 7113 + }, + "predecessors": [ + { + "credit": "Global input rechart", + "head": "6391d64cd0e37e0988e6b9c41fe13f053ed2c81e", + "pr": 7122 + }, + { + "credit": "Global output rechart", + "head": "97dc14132da53562b7939776d7a83d72af72eeb1", + "pr": 7124 + }, + { + "credit": "One-component inherited multi-ADD audit", + "head": "e4fe4766729247f3f7130005d4b386b6a0253219", + "pr": 7361 + }, + { + "credit": "Four-MOVE inherited fixed-outside audit", + "head": "17034c49a21bd751a3b7c35872fd290e11414896", + "pr": 7358 + }, + { + "credit": "Terminal chart-207 retarget audit", + "head": "3f29a5ebd0347b949760af9482a5eb1b4cbf93e8", + "pr": 7386 + }, + { + "credit": "Directed rank arithmetic", + "head": "5eec7ed633dcf9b9bbc95552aa653da296f863fb", + "pr": 7362 + }, + { + "credit": "Fixed-endpoint common-vector ceiling and independent flow inventory", + "head": "deb2f815482fbd6009cc72e219b12c48cdd49946", + "pr": 7454 + }, + { + "credit": "Current one-component interior scope", + "head": "fb1ee62053a0f0d3a64f92c2c871c04d3823f1f0", + "pr": 7453 + } + ], + "schema_version": 1 +} diff --git a/research/p104-endpoint-vector-growth-bound/README.md b/research/p104-endpoint-vector-growth-bound/README.md new file mode 100644 index 0000000000..1ac49baaeb --- /dev/null +++ b/research/p104-endpoint-vector-growth-bound/README.md @@ -0,0 +1,24 @@ +# Common-vector public helper recharts with endpoint credits + +**NO VERIFIED GAIN.** On exact #7334 and signed #7113, even jointly changing pure public helper input and output charts by one common binary vector gives exact directed upper zero. Both engines cover 553 eligible components, 2,573 paid edges, 193 productive edges and 511 × 18 direction/price cases. The independently reproduced complete comparator remains #7334 at κ = 0.00364665195644. + +The fixed interior model in #7454 has no endpoint credits. Here all pure helper components may grow, and productive nesting and positive target ranks are enforced. Independent per-edge rounding leaves a small positive relaxation. A shared nine-increment L1 envelope closes it exactly. See [PROOF.md](PROOF.md). + +## Reproduction + +Use POSIX CPython 3.12 with assertions enabled. + +```sh +python3.12 -I -B research/p104-endpoint-vector-growth-bound/replay.py +python3.12 -B scripts/research_package.py --package research/p104-endpoint-vector-growth-bound +``` + +The direct runner checks both immutable word hashes and solver pins, reconstructs the two inventories and cut models, and compares all exact results. It retains the original 60-second independent partial receipt and the 10-second continuation that checked exactly its 227 uncovered vertices. The fresh independent replay uses exact terminal-capacity cancellation and matches the merged evidence. It rejects an altered tariff pin and checks positive and blocked graph controls. + +## Open next questions + +Can differing added vectors or shrinking one public chart improve a coupled endpoint assignment? Freeze one such changed model and charge each affected productive and paid edge before attempting a physical rewrite. The present result closes the common-vector restriction only. See `TASK.json`. + +## Credit + +[#7122](https://github.com/CrocSwap/integer-mult-bounds/pull/7122) and [#7124](https://github.com/CrocSwap/integer-mult-bounds/pull/7124) supply global input and output rechart precedents on earlier words. [#7454](https://github.com/CrocSwap/integer-mult-bounds/pull/7454) supplies the fixed-endpoint common-vector family and the independent reverse-inventory and edge-flow engines. [#7453](https://github.com/CrocSwap/integer-mult-bounds/pull/7453) covers one common interior component, and [#7386](https://github.com/CrocSwap/integer-mult-bounds/pull/7386) covers terminal chart-207 retargeting. [#7362](https://github.com/CrocSwap/integer-mult-bounds/pull/7362) supplies directed arithmetic, [#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) the word and [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) the caller. OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging. diff --git a/research/p104-endpoint-vector-growth-bound/SOURCES.json b/research/p104-endpoint-vector-growth-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-endpoint-vector-growth-bound/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-endpoint-vector-growth-bound/TASK.json b/research/p104-endpoint-vector-growth-bound/TASK.json new file mode 100644 index 0000000000..8b381f6f9c --- /dev/null +++ b/research/p104-endpoint-vector-growth-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Exact #7334/#7113. Test arbitrary simultaneous subsets of all 553 pure public helper components, including endpoints, after adjoining one common nonzero binary vector. Enforce nesting and positive target ranks over all 2573 paid edges and 193 productive edges. All 511 vectors and 18 vertices of the shared exact price envelope. Preserve fixed main and owned components, literal scalar sequence and caller.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent replay and packaging.", + "author": "P104 endpoint common-vector growth audit", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Positive whole-incident paid plus productive price is required before a physical endpoint rewrite.", + "budget_minutes": 14, + "evidence": "Forward closure and independent reverse-inventory edge flow certify exact upper zero on all 9198 shared-price direction/vertex cases. The local per-edge relaxation has a positive rounding artifact.", + "open_questions": [ + { + "blocked_by": "No candidate has passed the exact literal or complete-price gates in that different model.", + "first_step": "Freeze a distinct-vector or shrinking model, including all affected productive, paid and boundary terms.", + "question": "Can a compatible assignment use distinct added vectors or a shrinking frame?", + "why_it_matters": "One common vector with joint endpoint prices is exactly exhausted." + } + ], + "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": "Fixed-endpoint closure excludes interior common-vector growth. This family lets productive initial and final charts move and couples their credits with all incident paid gaps.", + "scope_status": "changed", + "stop_rule": "All 511 vectors and 18 vertices, 60-second runner caps. One 10-second local continuation completed only the 227 previously uncovered vertices after the original independent cap. The optimized fresh direct-flow replay fits its own 60-second cap.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-endpoint-vector-growth-bound/VERIFY.json b/research/p104-endpoint-vector-growth-bound/VERIFY.json new file mode 100644 index 0000000000..c519d84a0b --- /dev/null +++ b/research/p104-endpoint-vector-growth-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Authenticate exact sources, reproduce both coupled price solvers and compare all 9198 exact maxima.", + "timeout_seconds": 132 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-endpoint-vector-growth-bound/cut_flow.py b/research/p104-endpoint-vector-growth-bound/cut_flow.py new file mode 100644 index 0000000000..c3b02234c0 --- /dev/null +++ b/research/p104-endpoint-vector-growth-bound/cut_flow.py @@ -0,0 +1,208 @@ +"""Independent reverse-word inventory and edge-capacitated flow for R219.""" +from collections import deque +from fractions import Fraction as Q +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal + +ROOT = Path(__file__).resolve().parent +PINS = { + 'reverse_inventory.py': 'ac01889cd8e917b5c3f93dcefaa19c159efc18bcdd6973b94b481f08185d0127', + 'inputs/pricing.py': 'f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182', + 'inputs/7334-WORD.json.gz': '4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a', +} +WORD_PAYLOAD = '9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac' +HEAD = 'aaeec8c0acf01e99a5f331ef363a698d9c084ace' +CALLER = '07a76c5e2738882c0cb322278e56f6cae3c9885d' +SCALE = 10**49 +LOWER = Q('0.00364665195644044790699554028334161') +UPPER = Q('0.00364665195644044790699554028334162') + + +def exact_inventory(word, trace, space): + frames, fixed, adj, _, transport = trace(word) + # Include untouched segments as singleton components, as well as cocharted + # connected components from literal ADD/COPY. Reverse trace dates each + # segment by its ending clock, independently of a forward union-find. + component = {} + charts = [] + allowed = set() + main = set(word['live']) | {r + 112 for r in word['live']} | set(word['hosted']['X2']) | set(word['hosted']['Y2']) + public = word['public'] + assert len(main) == 400 and public == 1501 + for root in sorted(frames): + if root in component: + continue + g = len(charts) + pending = [root] + component[root] = g + pure = True + while pending: + node = pending.pop() + role, _ = node + assert frames[node] == frames[root] + pure = pure and role < public and role not in main and node not in fixed + for peer in sorted(adj.get(node, ())): + if peer not in component: + component[peer] = g + pending.append(peer) + assert component[peer] == g + charts.append(frames[root]) + if pure: + allowed.add(g) + points = [space(basis) for basis in word['frames']] + ranks = list(map(len, word['frames'])) + pairs = {} + for node, entries in transport.items(): + for clock, other_chart, side in entries: + pair = pairs.setdefault(clock, {}) + assert side not in pair + pair[side] = (component[node], frames[node], other_chart) + edges = [] + for clock, pair in sorted(pairs.items()): + lower, lc, a = pair['source'] + upper, uc, b = pair['target'] + assert a == uc and b == lc and lower != upper + if lower not in allowed and upper not in allowed: + continue + assert points[lc] < points[uc] + assert word['program'][clock][0] == 'MOVE' and word['program'][clock][-1] is False + edges.append((lower, upper, ranks[uc]-ranks[lc])) + spaces = [points[c] for c in charts] + return spaces, allowed, edges + + +def arc(graph, u, v, capacity): + assert u != v and capacity > 0 + graph[u][v] = graph[u].get(v, 0) + capacity + graph[v].setdefault(u, 0) + + +def push_until_cut(graph, s, t, offered): + """Shortest augmenting paths, using the explicit bidirectional residual.""" + flow, augmentations = 0, 0 + while flow < offered: + parent = {s: None} + queue = deque([s]) + while queue and t not in parent: + u = queue.popleft() + for v, capacity in graph[u].items(): + if capacity and v not in parent: + parent[v] = u + queue.append(v) + if t not in parent: + return flow, augmentations, set(parent) + v = t + send = offered - flow + while v != s: + u = parent[v] + send = min(send, graph[u][v]) + v = u + v = t + while v != s: + u = parent[v] + graph[u][v] -= send + graph[v][u] += send + v = u + flow += send + augmentations += 1 + return flow, augmentations, {s} + + +def reduce_edges(v, spaces, allowed, edges, increment): + active = [g for g in sorted(allowed) if v not in spaces[g]] + index = {g: i for i, g in enumerate(active)} + source, sink = len(active), len(active) + 1 + graph = [{} for _ in range(len(active) + 2)] + total = 0 + hard = set() + finite_count = 0 + for lower, upper, d in edges: + x, y = index.get(lower), index.get(upper) + if x is None and y is None: + continue + if v in spaces[upper]: + assert x is not None and y is None + reward = increment[d][1] + arc(graph, source, x, reward) + total += reward + finite_count += 1 + continue + # Changed lower frame requires changed upper frame in this case. + if x is not None: + hard.add((x, y if y is not None else sink)) + # A cut pays for changing U alone, including a fixed lower frame. + if y is not None: + penalty = increment[d + 1][0] + arc(graph, y, x if x is not None else sink, penalty) + finite_count += 1 + for x, y in sorted(hard): + arc(graph, x, y, total + 1) + flow, augmentations, cut = push_until_cut(graph, source, sink, total) + assert all(x not in cut or y in cut for x, y in hard) + return {'vector': v, 'variables': len(active), 'implications': len(hard), + 'finite_arc_occurrences': finite_count, 'source_benefit_scaled': total, + 'flow_scaled': flow, 'upper_scaled': total - flow, + 'augmenting_paths': augmentations} + + +def control(): + # Adding the lower frame gives 5, requires adding its upper neighbor, + # and thus incurs 3. A fixed upper frame changes the optimum back to zero. + graph = [{} for _ in range(4)] + for u, v, c in ((2, 0, 5), (0, 1, 6), (1, 3, 3)): + arc(graph, u, v, c) + f, _, cut = push_until_cut(graph, 2, 3, 5) + assert f == 3 and cut == {0, 1, 2} + graph = [{} for _ in range(4)] + for u, v, c in ((2, 0, 5), (0, 1, 6), (1, 3, 6)): + arc(graph, u, v, c) + f, _, cut = push_until_cut(graph, 2, 3, 5) + assert f == 5 and cut == {2} + + +def stop(*_): + raise TimeoutError('60-second binary-vector flow cap') + + +def main(): + assert __debug__ + signal(SIGALRM, stop) + alarm(60) + for path, digest in PINS.items(): + assert sha256((ROOT / path).read_bytes()).hexdigest() == digest + data = decompress((ROOT / 'inputs' / '7334-WORD.json.gz').read_bytes()) + assert sha256(data).hexdigest() == WORD_PAYLOAD + word = loads(data) + assert len(word['program']) == 76466 + inv = run_path(str(ROOT / 'reverse_inventory.py')) + spaces, allowed, edges = exact_inventory(word, inv['reverse_trace'], inv['frame_space']) + assert len(allowed) == 482 and len(edges) == 2292 + tariff = run_path(str(ROOT / 'inputs' / 'pricing.py'))['power_bounds'] + bounds = [(Q(0), Q(0))] + [(tariff(r, UPPER)[0], tariff(r, LOWER)[1]) for r in range(1, 10)] + increment = {} + for r in range(1, 10): + lo, hi = (bounds[r][0] - bounds[r-1][1]) * SCALE, (bounds[r][1] - bounds[r-1][0]) * SCALE + assert lo.denominator == hi.denominator == 1 and 0 < lo <= hi + increment[r] = (int(lo), int(hi)) + control() + outcomes = [] + try: + for v in range(1, 512): + outcomes.append(reduce_edges(v, spaces, allowed, edges, increment)) + except TimeoutError: + print(dumps(dict(capped=True, results=outcomes), sort_keys=True, indent=2)) + raise SystemExit(2) + finally: + alarm(0) + print(dumps(dict(head=HEAD, caller=CALLER, pins=PINS, groups=len(spaces), + eligible_groups=len(allowed), incident_edges=len(edges), scale=SCALE, + runner_cap_seconds=60, vector_cap=511, capped=False, + increments=increment, results=outcomes), sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/p104-endpoint-vector-growth-bound/endpoint_replay.py b/research/p104-endpoint-vector-growth-bound/endpoint_replay.py new file mode 100644 index 0000000000..ede1a2a7e3 --- /dev/null +++ b/research/p104-endpoint-vector-growth-bound/endpoint_replay.py @@ -0,0 +1,231 @@ +"""Reverse inventory and edge-capacity verification for R222/R223.""" +from collections import defaultdict +from fractions import Fraction as Q +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from math import ceil, floor +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from sys import argv + +ROOT = Path(__file__).resolve().parent +HEAD = 'aaeec8c0acf01e99a5f331ef363a698d9c084ace' +CALLER = '07a76c5e2738882c0cb322278e56f6cae3c9885d' +PINS = { + 'inputs/7334-WORD.json.gz': '4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a', + 'inputs/pricing.py': 'f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182', + 'reverse_inventory.py': 'ac01889cd8e917b5c3f93dcefaa19c159efc18bcdd6973b94b481f08185d0127', + 'cut_flow.py': 'a16c67f11d216d0a7d7f4caf0b994cc0a1dcbc01d667ed0924691f72f0959cdb', +} +PAYLOAD = '9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac' +SCALE = 10**52 + + +def inventory(word, rev): + frames, fixed, adjacent, _, transport = rev['reverse_trace'](word) + main = set(word['live']) | {r+112 for r in word['live']} | set(word['hosted']['X2']) | set(word['hosted']['Y2']) + public = word['public'] + assert public == 1501 and len(main) == 400 + helper = set(range(public)) - main + component, charts, allowed = {}, [], [] + for root in sorted(frames): + if root in component: + continue + i = len(charts) + component[root] = i + pending = [root] + pure = True + while pending: + node = pending.pop() + assert frames[node] == frames[root] + pure = pure and node[0] in helper + for peer in sorted(adjacent.get(node, ())): + if peer not in component: + component[peer] = i + pending.append(peer) + assert component[peer] == i + charts.append(frames[root]) + if pure: + allowed.append(i) + chart_points = list(map(rev['frame_space'], word['frames'])) + points = [chart_points[c] for c in charts] + ranks = [len(word['frames'][c]) for c in charts] + allowed_set = set(allowed) + paid_ends = defaultdict(dict) + for node, rows in transport.items(): + for t, other, side in rows: + assert side not in paid_ends[t] + paid_ends[t][side] = (component[node], other) + edges = [] + for t, pair in sorted(paid_ends.items()): + a, upper_chart = pair['source'] + b, lower_chart = pair['target'] + assert charts[a] == lower_chart and charts[b] == upper_chart + if a not in allowed_set and b not in allowed_set: + continue + assert points[a] < points[b] and word['program'][t][-1] is False + edges.append((a, b, ranks[b]-ranks[a], True)) + ends = defaultdict(list) + for node in fixed: + ends[node[0]].append(node) + for r in sorted(helper): + end = (r, len(word['program'])) + start, = set(ends[r]) - {end} + assert end in fixed and frames[start] == word['initial'][r] and frames[end] == word['final'][r] + a, b = component[start], component[end] + if a not in allowed_set and b not in allowed_set: + continue + assert points[a] < points[b] + edges.append((a, b, ranks[b]-ranks[a], False)) + return points, allowed, edges + + +def compile_edges(v, points, allowed, edges): + active = [g for g in allowed if v not in points[g]] + index = {g: i for i, g in enumerate(active)} + s, t = len(active), len(active)+1 + hard, terms = set(), [] + for a, b, d, paid in edges: + x, y = index.get(a), index.get(b) + if x is None and y is None: + continue + if v in points[b]: + assert x is not None and y is None + if paid: + terms.append((s, x, d, True)) + elif d == 1: + hard.add((x, t)) + else: + terms.append((x, t, d, False)) + continue + if x is not None: + hard.add((x, y if y is not None else t)) + if paid: + if y is not None: + terms.append((y, x if x is not None else t, d+1, False)) + else: + # Nesting forces x <= y, so a reward c for (y,x)=(1,0) + # equals c*y - c*x on every allowed cut. + if y is not None: + terms.append((s, y, d+1, True)) + if x is not None: + terms.append((x, t, d+1, True)) + return s, t, sorted(hard), terms + + +def flow_value(frozen, reward, penalty, push, arc, *, cancel=False): + s, t, hard, terms = frozen + graph = [{} for _ in range(t+1)] + offered = 0 + for u, v, rank, good in terms: + cap = reward[rank] if good else penalty[rank] + arc(graph, u, v, cap) + if u == s: + offered += cap + if cancel: + # A source-to-sink cut crosses exactly one terminal arc at each + # variable. Subtract their common minimum from all cuts and offered. + for node in range(s): + common = min(graph[s].get(node, 0), graph[node].get(t, 0)) + if common: + graph[s][node] -= common + graph[node][t] -= common + offered -= common + for u, v in hard: + arc(graph, u, v, offered+1) + flow, _, cut = push(graph, s, t, offered) + assert all(u not in cut or v in cut for u, v in hard) + return offered-flow + + +def control(push, arc): + # A target reward adds +5 only if the upper grows alone. One paid + # charge of 3 for that upper gives +2. Coupling it to an additional + # finite penalty of 4 makes the upper unprofitable. + terms = [(2, 1, 1, True), (0, 3, 1, True), (1, 3, 2, False)] + for cancel in (False, True): + assert flow_value((2, 3, [(0, 1)], terms), + [0, 5, 3], [0, 5, 3], push, arc, cancel=cancel) == 2 + assert flow_value((2, 3, [(0, 1)], terms+[(1, 3, 3, False)]), + [0, 5, 3, 4], [0, 5, 3, 4], push, arc, cancel=cancel) == 0 + + +def stop(*_): + raise TimeoutError('60-second endpoint shared-price cap') + + +def main(): + assert __debug__ + assert len(argv) in (1, 6) + if len(argv) == 1: + first, last, skip, cap, mode = 1, 511, 0, 60, 'cancel' + else: + first, last, skip, cap = map(int, argv[1:5]) + mode = argv[5] + assert 1 <= first <= last <= 511 and 0 <= skip < 18 and 1 <= cap <= 60 + assert mode in ('direct', 'cancel') + cancel = mode == 'cancel' + signal(SIGALRM, stop) + alarm(cap) + for name, pin in PINS.items(): + assert sha256((ROOT / name).read_bytes()).hexdigest() == pin + raw = decompress((ROOT / 'inputs/7334-WORD.json.gz').read_bytes()) + assert sha256(raw).hexdigest() == PAYLOAD + word = loads(raw) + assert len(word['program']) == 76466 + rev = run_path(str(ROOT / 'reverse_inventory.py')) + points, allowed, edges = inventory(word, rev) + targets, paid = sum(not e[-1] for e in edges), sum(e[-1] for e in edges) + assert (len(points), len(allowed), paid, targets) == (1517, 553, 2573, 193) + flow = run_path(str(ROOT / 'cut_flow.py')) + push, arc = flow['push_until_cut'], flow['arc'] + control(push, arc) + tariff = run_path(str(ROOT / 'inputs/pricing.py'))['power_bounds'] + k0 = Q('0.00364665195644044790699554028334161') + k1 = Q('0.00364665195644044790699554028334162') + h = [(Q(0), Q(0))] + [(tariff(r, k1)[0], tariff(r, k0)[1]) for r in range(1, 10)] + lo = [0] + [floor(SCALE*(h[r][0]-h[r-1][1])) for r in range(1, 10)] + hi = [0] + [ceil(SCALE*(h[r][1]-h[r-1][0])) for r in range(1, 10)] + assert all(0 < a <= b for a, b in zip(lo[1:], hi[1:], strict=True)) + midpoint = [a+b for a,b in zip(lo, hi, strict=True)] + radius = sum(b-a for a,b in zip(lo, hi, strict=True)) + assert 0 < radius < min(midpoint[1:]) + vertices = [] + for rank in range(1, 10): + for sign in (-1, 1): + p = midpoint.copy() + p[rank] += sign*radius + vertices.append(p) + rows, rounding, partial = [], [], None + capped = False + try: + for v in range(first, last+1): + frozen = compile_edges(v, points, allowed, edges) + if v != first or not skip: + rounding.append([v, frozen[0], flow_value(frozen, lo, hi, push, arc, cancel=cancel), + flow_value(frozen, hi, lo, push, arc, cancel=cancel)]) + partial = [v, []] + for price in vertices[skip if v == first else 0:]: + partial[1].append(flow_value(frozen, price, price, push, arc, cancel=cancel)) + rows.append(partial) + partial = None + except TimeoutError: + capped = True + finally: + alarm(0) + print(dumps(dict(head=HEAD, caller=CALLER, pins=PINS, groups=len(points), eligible_groups=len(allowed), + paid_edges=paid, target_edges=targets, increment_scale=SCALE, scale=2*SCALE, + box=list(zip(lo[1:],hi[1:],strict=True)), center=midpoint[1:], radius=radius, + vertices=len(vertices), vectors=len(rows), cap_seconds=cap, + first_vector=first, last_vector=last, skip_first_vertices=skip, mode=mode, + rounding=rounding, rows=rows, partial_row=partial, + max=max((max(values) for _,values in rows),default=None),capped=capped), + indent=2,sort_keys=True)) + if capped: + raise SystemExit(2) + + +if __name__ == '__main__': + main() diff --git a/research/p104-endpoint-vector-growth-bound/inputs/7334-WORD.json.gz b/research/p104-endpoint-vector-growth-bound/inputs/7334-WORD.json.gz new file mode 100644 index 0000000000..73f4300719 Binary files /dev/null and b/research/p104-endpoint-vector-growth-bound/inputs/7334-WORD.json.gz differ diff --git a/research/p104-endpoint-vector-growth-bound/inputs/closure.py b/research/p104-endpoint-vector-growth-bound/inputs/closure.py new file mode 100644 index 0000000000..1bd15a2b91 --- /dev/null +++ b/research/p104-endpoint-vector-growth-bound/inputs/closure.py @@ -0,0 +1,192 @@ +"""Exact directed max closure for adding one binary vector to interior helper frames.""" +from collections import Counter, deque +from fractions import Fraction as F +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from math import ceil, floor +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from sys import setrecursionlimit + +HERE = Path(__file__).resolve().parent +SCALE = 10**52 +PINS = { + 'inputs/7334-WORD.json.gz': '4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a', + 'inputs/pricing.py': 'f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182', +} + + +def maxclosure(weights, implications): + count = len(weights) + source, sink = count, count+1 + graph = [[] for _ in range(count+2)] + positive = sum(max(0,w) for w in weights) + inf = positive+1 + + def edge(u,v,c): + graph[u].append([v,c,len(graph[v])]) + graph[v].append([u,0,len(graph[u])-1]) + + for i,w in enumerate(weights): + if w>0: + edge(source,i,w) + elif w<0: + edge(i,sink,-w) + for u,v in implications: + edge(u,sink if v is None else v,inf) + flow = 0 + while True: + level = [-1]*(count+2) + level[source] = 0 + queue = deque([source]) + while queue: + u = queue.popleft() + for v,c,_ in graph[u]: + if c and level[v]<0: + level[v] = level[u]+1 + queue.append(v) + if level[sink]<0: + chosen = {i for i in range(count) if level[i]>=0} + assert all(u not in chosen or v in chosen for u,v in implications) + assert sum(weights[i] for i in chosen)==positive-flow + return positive-flow,chosen + at = [0]*(count+2) + + def push(u,budget): + if u==sink: + return budget + while at[u]0: + lower,selected=maxclosure(wl,implications) + rec['lower_scaled']=lower + if lower>0: + chosen={active[i] for i in selected} + ranks_delta=Counter() + changed=[] + lower_check=upper_check=0 + for t,a,b,ca,cb,d in edges: + x,y=a in chosen,b in chosen + da=spaces[ca]|{u^v for u in spaces[ca]} if x else spaces[ca] + db=spaces[cb]|{u^v for u in spaces[cb]} if y else spaces[cb] + assert da<=db + dn=d+y-x + if dn!=d: + ranks_delta[d]+=1 + if dn: + ranks_delta[dn]-=1 + changed.append([t,d,dn]) + if dnd: + lower_check-=inc[dn][1] + upper_check-=inc[dn][0] + assert lower_check==lower and lower<=upper_check<=upper + witness={'vector':v,'chosen_groups':sorted(chosen),'segments':{g:groups[g] for g in sorted(chosen)}, + 'contacts':{g:uses[g] for g in sorted(chosen)},'changed_rank_edges':changed, + 'incident_paid_edges':sum(a in chosen or b in chosen for _,a,b,*_ in edges), + 'old_minus_new_rank_hist':{r:c for r,c in ranks_delta.items() if c}, + 'raw_directed_bounds':[str(17*F(lower,SCALE)),str(17*F(upper_check,SCALE))]} + results.append(rec) + if witness: + break + except TimeoutError: + capped=True + finally: + alarm(0) + print(dumps({'pins':PINS|{'inputs/inventory.py':sha256((HERE/'inputs/inventory.py').read_bytes()).hexdigest()}, + 'groups':len(groups),'eligible_groups':len(movable),'incident_edges':len(edges), + 'vectors_checked':len(results),'case_cap':511,'seconds_cap':60,'capped':capped, + 'scale':SCALE,'rounding_intervals':inc,'results':results,'witness':witness},sort_keys=True,indent=2)) + if capped: + raise SystemExit(2) + + +if __name__=='__main__': + main() diff --git a/research/p104-endpoint-vector-growth-bound/inputs/inventory.py b/research/p104-endpoint-vector-growth-bound/inputs/inventory.py new file mode 100644 index 0000000000..ce651d88ee --- /dev/null +++ b/research/p104-endpoint-vector-growth-bound/inputs/inventory.py @@ -0,0 +1,164 @@ +"""Exact current-word common-frame screen for closed public helper components.""" +from collections import Counter, defaultdict +from fractions import Fraction as F +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import alarm + +HERE = Path(__file__).resolve().parent +PINS = { + 'inputs/7334-WORD.json.gz': '4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a', + 'inputs/pricing.py': 'f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182', +} + + +def span(vectors): + result = {0} + for v in vectors: + result |= {x ^ v for x in result} + return result + + +def inventory(w): + roles = w['public'] + w['owned_fields'] + main = set(w['live']) | {i + 112 for i in w['live']} | set(w['hosted']['X2']) | set(w['hosted']['Y2']) + assert w['public'] == 1501 and len(main) == 400 + eligible = set(range(w['public'])) - main + assert len(eligible) == 1101 + parent, nodes, contacts, moves = [], [], [], [] + + def node(role, chart, endpoint=False): + n = len(nodes) + nodes.append([role, chart, endpoint]) + parent.append(n) + return n + + def root(i): + while parent[i] != i: + i, parent[i] = parent[i], parent[parent[i]] + return i + + active = [node(i, c, True) for i, c in enumerate(w['initial'])] + [None]*w['owned_fields'] + assert len(active) == roles + for t,(op,r,*a) in enumerate(w['program']): + old = active[r] + if op == 'INIT': + assert old is None + active[r] = node(r,a[0]) + elif op == 'CLEAR': + assert nodes[old][1] == a[0] + active[r] = None + elif op == 'MOVE': + assert nodes[old][1] == a[0] + new = node(r,a[1]) + moves.append((t,old,new)) + active[r] = new + elif op in ('ADD','COPY'): + s,_,c = a + assert nodes[old][1] == nodes[active[s]][1] == c + parent[root(active[s])] = root(old) + contacts.append((t,old,op)) + else: + assert op == 'SCALE' and nodes[old][1] == a[1] + contacts.append((t,old,op)) + assert all(active[i] is None for i in range(w['public'], roles)) + for i,c in enumerate(w['final']): + assert nodes[active[i]][1] == c + nodes[active[i]][2] = True + groups, uses, incident = defaultdict(list),defaultdict(list),defaultdict(list) + for i,n in enumerate(nodes): + groups[root(i)].append(n) + for t,n,op in contacts: + uses[root(n)].append((t,op)) + for t,a,b in moves: + ra,rb = root(a),root(b) + assert ra != rb + incident[ra].append((t,nodes[b][1],'source')) + incident[rb].append((t,nodes[a][1],'target')) + return eligible,groups,uses,incident + + +def main(): + assert __debug__ + alarm(40) + for name,h in PINS.items(): + assert sha256((HERE/name).read_bytes()).hexdigest() == h + raw = decompress((HERE/'inputs/7334-WORD.json.gz').read_bytes()) + assert sha256(raw).hexdigest() == '9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac' + w = loads(raw) + assert len(w['program']) == 76466 + e,groups,uses,incident = inventory(w) + frames = [tuple(v) for v in w['frames']] + spaces = [span(v) for v in frames] + assert all(len(s)==1<0 else lo)[0 if n>0 else 1] for r,n in delta) + right = sum(n*h(r,lo if n>0 else hi)[1 if n>0 else 0] for r,n in delta) + return 17*left,17*right + + counts, cases = Counter(),[] + for g, members in groups.items(): + if sum(op=='ADD' for _,op in uses[g]) < 2: + continue + counts['multi_add'] += 1 + if any(r not in e for r,_,_ in members): + counts['main_or_owned'] += 1 + continue + if any(endpoint for _,_,endpoint in members): + counts['fixed_endpoint'] += 1 + continue + counts['closed_pure'] += 1 + current, = {c for _,c,_ in members} + d = ranks[current] + edges = sorted(incident[g]) + assert edges and all(w['program'][t][0]=='MOVE' for t,_,_ in edges) + lower = [c for _,c,_ in edges if ranks[c] < d] + upper = [c for _,c,_ in edges if ranks[c] > d] + assert len(lower)+len(upper)==len(edges) + assert all(spaces[c] <= spaces[current] for c in lower) + assert all(spaces[current] <= spaces[c] for c in upper) + min_r = max((ranks[c]+1 for c in lower),default=0) + max_r = min((ranks[c]-1 for c in upper),default=9) + low_space = span(x for c in lower for x in frames[c]) + high_space = set.intersection(set(range(512)),*(spaces[c] for c in upper)) + assert low_space <= spaces[current] <= high_space + first = max(min_r,len(low_space).bit_length()-1) + last = min(max_r,len(high_space).bit_length()-1) + assert first <= d <= last + stock = Counter(abs(d-ranks[c]) for _,c,_ in edges) + + def quote(k): + delta = stock.copy() + delta.subtract(abs(k-ranks[c]) for _,c,_ in edges) + return gain(tuple(sorted((r,n) for r,n in delta.items() if n))) + + relaxed = [k for k in sorted({min_r,max_r}) if quote(k)[1]>0] + if not relaxed: + counts['dimension_nonpositive'] += 1 + continue + feasible = [(k,quote(k)) for k in sorted({first,last}) if quote(k)[1]>0] + if feasible: + counts['geometry_survivor'] += 1 + else: + counts['geometry_exclusion'] += 1 + cases.append({'first_contact':uses[g][0][0],'old_chart':current,'old_rank':d, + 'roles':sorted({r for r,_,_ in members}),'contacts':uses[g], 'moves':edges, + 'relaxed_ranks':[min_r,max_r],'feasible_ranks':[first,last], + 'price_positive_relaxed':[(k,quote(k)) for k in relaxed], + 'price_positive_feasible':feasible,'lower_span':sorted(low_space),'upper_span':sorted(high_space)}) + alarm(0) + print(dumps({'pins':PINS,'counts':counts,'cases':sorted(cases,key=lambda x:x['first_contact']), + 'runner_cap_seconds':40,'paid_zero_disallowed':True,'seed':None},sort_keys=True,indent=2,default=str)) + + +if __name__ == '__main__': + main() diff --git a/research/p104-endpoint-vector-growth-bound/inputs/pricing.py b/research/p104-endpoint-vector-growth-bound/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-endpoint-vector-growth-bound/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-endpoint-vector-growth-bound/inputs/target_closure.py b/research/p104-endpoint-vector-growth-bound/inputs/target_closure.py new file mode 100644 index 0000000000..745ae99aea --- /dev/null +++ b/research/p104-endpoint-vector-growth-bound/inputs/target_closure.py @@ -0,0 +1,149 @@ +"""Coupled one-vector productive endpoint and paid interior chart moves.""" +from collections import Counter +from fractions import Fraction as F +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from math import ceil, floor +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal + +H = Path(__file__).resolve().parent +I = H / 'inputs' +S = 10**52 + + +def timed_out(*_): + raise TimeoutError + + +def get_inventory(w, base): + public, groups, uses, incident = base['inventory'](w) + spaces = list(map(base['span'],w['frames'])) + chart = {g: members[0][1] for g,members in groups.items()} + movable = {g for g,members in groups.items() if all(r in public for r,_,_ in members)} + endpoint = {(r,c):g for g,members in groups.items() for r,c,b in members if b and r in public} + assert len(endpoint) == 2202 + ends = {} + for g, rows in incident.items(): + for t,_,side in rows: + ends.setdefault(t,{})[side] = g + edges = [(t, e['source'], e['target'], True) for t,e in sorted(ends.items())] + edges += [(r,endpoint[r,w['initial'][r]],endpoint[r,w['final'][r]],False) for r in sorted(public)] + out = [] + for t,a,b,paid in edges: + if a not in movable and b not in movable: + continue + ca,cb = chart[a],chart[b] + assert spaces[ca] < spaces[cb] + assert not paid or w['program'][t][-1] is False + out.append((t,a,b,ca,cb,len(w['frames'][cb])-len(w['frames'][ca]),paid)) + return groups,uses,spaces,chart,movable,out + + +def bound(v, active, spaces, edges, inc, maxclosure, high): + ids = {g:i for i,g in enumerate(active)} + weights = [0]*len(active) + imp = set() + for _,a,b,ca,cb,d,paid in edges: + x,y = ids.get(a), ids.get(b) + if x is None and y is None: + continue + if v in spaces[cb]: + assert x is not None and y is None + if paid: + weights[x] += inc[d][high] + elif d==1: + imp.add((x,None)) + else: + weights[x] -= inc[d][1-high] + else: + slope = -inc[d+1][1-high] if paid else inc[d+1][high] + if x is not None: + imp.add((x,y)) + weights[x] -= slope + if y is not None: + weights[y] += slope + value,chosen = maxclosure(weights,imp) + return value,{active[i] for i in chosen} + + +def certify(v, chosen, edges, spaces, inc): + price = [0,0] + dp,dt = Counter(),Counter() + p,tg = [],[] + for t,a,b,ca,cb,d,paid in edges: + x,y=a in chosen,b in chosen + a2=spaces[ca]|{u^v for u in spaces[ca]} if x else spaces[ca] + b2=spaces[cb]|{u^v for u in spaces[cb]} if y else spaces[cb] + assert a2<=b2 + dn=d+y-x + assert paid or dn>0 + if dn==d: + continue + hist,delta,records=(dp,-1,p) if paid else (dt,1,tg) + hist[d]-=delta + if dn: + hist[dn]+=delta + records.append([t,d,dn]) + l,h = inc[max(d,dn)] + if paid==(dn= n and r not in cursor + cursor[r] = r, t + frames[cursor[r]] = payload[0] + continue + outgoing = cursor[r] + if op == 'INIT': + assert r >= n and frames[outgoing] == payload[0] + del cursor[r] + elif op == 'MOVE': + lo, hi, owned = payload + assert frames[outgoing] == hi and owned == (r >= n) + incoming = r, t + frames[incoming] = lo + cursor[r] = incoming + transport[incoming].add((t, hi, 'source')) + transport[outgoing].add((t, lo, 'target')) + elif op in ('ADD', 'COPY'): + s, _, chart = payload + other = cursor[s] + assert r != s and frames[other] == frames[outgoing] == chart + adj[outgoing].add(other) + adj[other].add(outgoing) + contacts[outgoing].add((t, op)) + contacts[other].add((t, op)) + else: + assert op == 'SCALE' and frames[outgoing] == payload[1] + contacts[outgoing].add((t, op)) + assert sorted(cursor) == list(range(n)) + assert [frames[cursor[r]] for r in range(n)] == w['initial'] + fixed.update(cursor.values()) + return frames, fixed, adj, contacts, transport + + +def components(adj): + seen = set() + for vertex in sorted(adj): + if vertex in seen: + continue + group, stack = {vertex}, [vertex] + while stack: + node = stack.pop() + new = adj[node] - group + stack.extend(new) + group.update(new) + seen.update(group) + yield group + + +def frame_space(basis): + points = {0} + for size in range(1, len(basis) + 1): + for terms in combinations(basis, size): + v = 0 + for term in terms: + v ^= term + points.add(v) + assert len(points) == 1 << len(basis) + return points + + +def solve(w, inherited): + n = w['public'] + main = set(w['live']) | {i + 112 for i in w['live']} | set(w['hosted']['X2']) | set(w['hosted']['Y2']) + assert len(main) == 400 and n == 1501 and len(w['program']) == 76466 + frames, fixed, adj, contacts, transport = reverse_trace(w) + spaces = [frame_space(f) for f in w['frames']] + ranks = [len(f) for f in w['frames']] + tariff = run_path(str(ROOT / 'inputs' / 'pricing.py'))['power_bounds'] + k0 = Fraction('0.00364665195644044790699554028334161') + k1 = Fraction('0.00364665195644044790699554028334162') + lower = [Fraction(0)] + [tariff(r, k1)[0] for r in range(1, 10)] + upper = [Fraction(0)] + [tariff(r, k0)[1] for r in range(1, 10)] + + @cache + def priced(deltas): + lo = sum((lower[r] if c > 0 else upper[r]) * c for r, c in deltas) + hi = sum((upper[r] if c > 0 else lower[r]) * c for r, c in deltas) + return str(17 * lo), str(17 * hi) + + counts, rows = Counter(), [] + for group in components(adj): + events = sorted(set().union(*(contacts[s] for s in group))) + if sum(tag == 'ADD' for _, tag in events) < 2: + continue + counts['multi_add'] += 1 + if any(r in main or r >= n for r, _ in group): + counts['main_or_owned'] += 1 + continue + if group & fixed: + counts['fixed_endpoint'] += 1 + continue + counts['closed_pure'] += 1 + chart, = {frames[s] for s in group} + edges = sorted(set().union(*(transport[s] for s in group))) + assert edges and len(edges) == len({t for t, _, _ in edges}) + incoming = [c for _, c, side in edges if side == 'target'] + outgoing = [c for _, c, side in edges if side == 'source'] + assert len(incoming) == len(outgoing) == len(group) + lo = max(ranks[c] + 1 for c in incoming) + hi = min(ranks[c] - 1 for c in outgoing) + low_space, high_space = {0}, set(range(512)) + for c in incoming: + low_space = {a ^ b for a in low_space for b in spaces[c]} + for c in outgoing: + high_space &= spaces[c] + d = ranks[chart] + assert low_space <= spaces[chart] <= high_space and lo <= d <= hi + first = max(lo, len(low_space).bit_length() - 1) + last = min(hi, len(high_space).bit_length() - 1) + assert first <= d <= last + old = Counter([d - ranks[c] for c in incoming] + [ranks[c] - d for c in outgoing]) + + def endpoints(a, b): + out = [] + for rank in sorted({a, b}): + terms = old.copy() + terms.subtract([rank - ranks[c] for c in incoming]) + terms.subtract([ranks[c] - rank for c in outgoing]) + quote = priced(tuple(sorted((r, c) for r, c in terms.items() if c))) + if Fraction(quote[1]) > 0: + out.append((rank, quote)) + return out + + relaxed = endpoints(lo, hi) + if not relaxed: + counts['dimension_nonpositive'] += 1 + continue + possible = endpoints(first, last) + counts['geometry_survivor' if possible else 'geometry_exclusion'] += 1 + rows.append({'first_contact': events[0][0], 'old_chart': chart, 'old_rank': d, + 'roles': sorted({r for r, _ in group}), 'contacts': events, 'moves': edges, + 'relaxed_ranks': [lo, hi], 'feasible_ranks': [first, last], + 'price_positive_relaxed': relaxed, 'price_positive_feasible': possible, + 'lower_span': sorted(low_space), 'upper_span': sorted(high_space)}) + rows.sort(key=lambda r: r['first_contact']) + rebind = {(r['key'][0], min(r['clock_map'][x] for x in r['signed_ancestor_ADDs'])) for r in inherited['outcomes']} + actual = {(r['old_chart'], min(t for t, tag in r['contacts'] if tag == 'ADD')) for r in rows} + assert len(rebind) == 13 and actual - rebind == {(746, 40834)} and rebind <= actual + changed, = (r for r in rows if r['old_chart'] == 746) + assert [t for t, tag in changed['contacts'] if tag == 'ADD'] == [40834, 41179] + assert changed['relaxed_ranks'] == [4, 6] and changed['feasible_ranks'] == [5, 6] + assert not changed['price_positive_feasible'] + return {'counts': counts, 'cases': rows, 'exact_prior_7361_keys': sorted(rebind), + 'exact_prior_7369_key': [746, 40834], 'new_price_positive_keys': [], 'runner_cap_seconds': 40} + + +def main(): + assert __debug__ + alarm(40) + result = solve(*verify_inputs()) + alarm(0) + print(dumps(result, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/p104-endpoint-vector-growth-bound/vertices.py b/research/p104-endpoint-vector-growth-bound/vertices.py new file mode 100644 index 0000000000..7a30c34052 --- /dev/null +++ b/research/p104-endpoint-vector-growth-bound/vertices.py @@ -0,0 +1,65 @@ +"""Certify a shared price vector by an enclosing exact L1 polytope.""" +from fractions import Fraction as F +from gzip import decompress +from hashlib import sha256 +from json import dumps,loads +from math import ceil,floor +from pathlib import Path +from runpy import run_path +from signal import SIGALRM,alarm,signal + +I=Path(__file__).resolve().parent/'inputs' +S=10**52 + + +def stop(*_): + raise TimeoutError('60-second shared price cap') + + +def main(): + assert __debug__ + signal(SIGALRM,stop) + alarm(60) + raw=decompress((I/'7334-WORD.json.gz').read_bytes()) + assert sha256(raw).hexdigest()=='9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac' + w=loads(raw) + common=run_path(str(I/'target_closure.py')) + inv=run_path(str(I/'inventory.py')) + groups,uses,spaces,chart,movable,edges=common['get_inventory'](w,inv) + solver=run_path(str(I/'closure.py'))['maxclosure'] + h=run_path(str(I/'pricing.py'))['power_bounds'] + lo,hi=map(F,('0.00364665195644044790699554028334161','0.00364665195644044790699554028334162')) + h0={0:(F(0),F(0))}|{r:(h(r,hi)[0],h(r,lo)[1]) for r in range(1,10)} + box={r:(floor(S*(h0[r][0]-h0[r-1][1])),ceil(S*(h0[r][1]-h0[r-1][0]))) for r in range(1,10)} + mid={r:l+u for r,(l,u) in box.items()} + radius=sum(u-l for l,u in box.values()) + assert radius>0 and min(mid.values())>radius + # Quantities here use scale 2*S. The nine price intervals lie inside this L1 ball. + vertices=[{r:(m+sign*radius*(r==j),)*2 for r,m in mid.items()} for j in range(1,10) for sign in (-1,1)] + rows=[] + capped=False + running=None + try: + for v in range(1,512): + active=sorted(g for g in movable if v not in spaces[chart[g]]) + running=[v,[]] + for vals in vertices: + value,_=common['bound'](v,active,spaces,edges,vals,solver,1) + running[1].append(value) + rows.append(running) + running=None + except TimeoutError: + capped=True + finally: + alarm(0) + print(dumps({'pins':{p.name:sha256(p.read_bytes()).hexdigest() for p in sorted(I.iterdir())}, + 'scale':2*S,'directed_increment_box':box,'radius':radius,'center':mid, + 'vectors_checked':len(rows),'vertex_count':len(vertices),'runner_cap_seconds':60, + 'rows':rows,'partial_row':running,'capped':capped,'eligible_groups':len(movable), + 'max':max((max(a) for _,a in rows),default=None)},sort_keys=True,indent=2)) + if capped: + raise SystemExit(2) + + +if __name__=='__main__': + main()