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-retimed-chart207-split-bound/LOCAL-PINS.json b/research/p104-retimed-chart207-split-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..7e34b8b85a --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/LOCAL-PINS.json @@ -0,0 +1,19 @@ +{ + "PROVENANCE.json": "0e6dd27511a9a81fdb68a7bfa276246508753dbd3d7e0810900d6a6e5bd8e0f2", + "engines/compare_geometry.py": "a474929311fe9c569e1cab4a00ee96b527e9cecfc9afeee6cf658bd13b2a9b3a", + "engines/continuation.py": "fd948b9e1c4d44c2ca0f268c31511625c2ce31580dab730b6a9528088648ddb4", + "engines/occupancy.py": "551c0634d838327642ca8e12941abaeb637287ff836c272fac468fa80c822851", + "engines/paired_rank.py": "d1b7c34e6f8c8a7b810414762015e6e300a8292422af66ff671ae09741141f09", + "engines/paired_support.py": "38c796cbe1a73f386177faf88cd53294d4b911f6cde7fd47cd9fcef3b558373f", + "engines/reconcile.py": "7287cdcd3d267ec4ebd5ccd8f37d6df9cb9a0dab50415a5aa0099f8f4f92fe73", + "engines/reverse_207.py": "ec134dd0e310483e0a23353428c1132f3fb9bf6caedfc0ccf086d8d08d20b26a", + "inputs/7314-WORD.json.gz": "c404b9b61220e6cf740d85276df2828bbb4a9d68a4d44b5e283f8d96f78c0fd9", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/IDENTITIES.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "price/inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "price/inputs/PR7338-SHA256.json": "25425e3a6fc025666f50faea07e9d41fa1924a44c121c5503b122f082bed2542", + "price/inputs/RANK-STOCK.json": "4a7841699dd17688f6aada5c902a2a91e94558b2b1b4460c46b0e55aa95b3f9f", + "price/inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "price/quote.py": "1d8a697ccc7d44e3b87d2c02252c2bb21789a490cc2cc7fb9ebdc0ed2ee6f747", + "receipts/SHA256.json": "1286dc448a254babfd6f4768ee450e3cce6ca077bef0e6802afc304724304fd1" +} diff --git a/research/p104-retimed-chart207-split-bound/NOTICE b/research/p104-retimed-chart207-split-bound/NOTICE new file mode 100644 index 0000000000..8f32909be5 --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/NOTICE @@ -0,0 +1,6 @@ +Apache-2.0. + +#7334 supplies the retimed source, #7314 its parent and #7113 the signed +caller. #7298 and #7338 supply directed pricing and the admitted rank +stock. #5599, #7121, #7130 and #7332 supply cocharted productive-split +and exact cohort precedents. OpenAI Codex and subagents materially assisted. diff --git a/research/p104-retimed-chart207-split-bound/PROOF.md b/research/p104-retimed-chart207-split-bound/PROOF.md new file mode 100644 index 0000000000..d5fc8939e8 --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/PROOF.md @@ -0,0 +1,83 @@ +# Exact chart-207 support and reconciliation + +The tested edit splits one rank-nine helper with endpoints +chart 3→127 at a literal chart-207 cut. These three charts +have ranks 0, 8 and 9 and strictly nested spans. All original +paid ranks, MOVE owners and chronology stay fixed. The emitted +helper-319 replacement block runs from event 44588 through 44627. +A cut k is the state immediately before event k. + +The forward and reverse occupancy walks agree on all 41 cuts +44588 through 44628, and 47 overlapping cuts of the parent word. +Both check the public bank, owned bank and eligible pivots. +The aligned 18 old/new scalars match after replacing public 319 +by owned 1567 inside the retimed block. The public pivots are +205, 532, 969, 1081, 1250 and 1453. The full public bank supplies +the local rows and columns. Boundary support is restricted to the +615 exact chart-3→127 cohort roles, excluding main, hosted and +protected roles. No owned role is a local basis pivot. + +The canonical cut list uses the block entrance and the cut after +each chart-207 contact. Between successive such cuts, every +operation is disjoint from the chart-207 bank. Its normalized +prefix rows and suffix impulse columns are constant there. +This maps all 166 raw pairs to 146 representatives. A second +convention also emits the post-block cut 44628, giving 151 pairs. +Its five extra pairs equal their cut-44626 representatives. +Events 44626 and 44627 are signed chart-127 ADDs between roles +1467 and 319, both absent from the chart-207 bank. They remain +literal events and do not create a new chart-207 contact or +change the normalized support data. + +## Exact necessary identities + +At a candidate cut, let P be the normalized prefix and S the +normalized suffix. For a local functional a and direction b, a +compatible split requires `aP=c` and `Sb=d` supported on the +retained boundary cohort, with `ab=cd=1`. The two rational walks +reconstruct these literal operators and solve both exterior +constraints over the rationals. A zero pure image on either +side excludes the split. + +For each remaining bank choose complete rational kernel bases. +Let B represent the bilinear form `cd` and D the form `ab−cd` +on those bases. A pair exists precisely when there are weights x,y +with `xDy=0` and `xBy≠0`. Scaling one side would then give a unit +pair. For fixed x this holds precisely if the row xB is outside the +span of xD. A nonzero wedge of xB and xD is detectable on a basis +vector or sum of two basis vectors, since each wedge coordinate is +a homogeneous quadratic. If every wedge vanishes, existence reduces +to some x with `xD=0` and `xB≠0`. One engine solves this exact left +kernel condition. A second computes the rational rank of D and of +the matrix with the columns of B appended. A rank increase is +equivalent to the required nonzero image of a left-kernel vector. + +The initial run exhausts its 128 keys with 3 prefix exclusions, +57 suffix exclusions and 68 failed pairings. The continuation uses +only the 18 remaining canonical keys. Two share an already verified +identical bank and 16 are fresh key replays. The independent rank +check resolves all 18. All fail unit pairing. The reconciliation +matches every raw key to its exact canonical bank and disposition. +No additional support tests are needed for the five duplicate +endpoint keys. The physical basis and full changed supplier gates +have no surviving input. + +## Complete directed price + +The complete signed #7334 invoice has 110,519 paid positions, +22,461 productive targets, rank surplus 1,424 and zero empty +credit. For 17 native copies the fixed-paid split changes +`ΔT={1:+17,8:+17,9:−17}` and leaves P unchanged. The target count +would rise to 22,478 and its rank mass stays fixed. The directed +one-edit gross upper at the exact comparator crossing is + +```text +484071551322335774046628615447889970860813026739/2500000000000000000000000000000000000000000000000 +``` + +This is about 0.193628620529 raw. One extra rank-one paid position +makes the complete directed upper negative. The fixed-price keys +are alternatives to one split, so their credits are counted once. +The exact support exclusion reduces compatible savings to zero. +Different charts, changed paid paths, enlarged cohorts, or changed +ownership remain separate questions. diff --git a/research/p104-retimed-chart207-split-bound/PROVENANCE.json b/research/p104-retimed-chart207-split-bound/PROVENANCE.json new file mode 100644 index 0000000000..0789838642 --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/PROVENANCE.json @@ -0,0 +1,45 @@ +{ + "files": { + "inputs/7314-WORD.json.gz": { + "commit": "9d0119eb12fbd9fa534b48cd37b68e7099757b91", + "git_blob": "3939a3cc4c516cf2f184bd401fbeb0d61f5cdd40", + "path": "research/p104-funded-863-return/WORD.json.gz", + "sha256": "c404b9b61220e6cf740d85276df2828bbb4a9d68a4d44b5e283f8d96f78c0fd9", + "source": "https://github.com/Clear1nsight/integer-mult-bounds/blob/9d0119eb12fbd9fa534b48cd37b68e7099757b91/research/p104-funded-863-return/WORD.json.gz", + "uncompress": false + }, + "inputs/7334-WORD.json.gz": { + "commit": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "git_blob": "73f43007192eb5a38eb5abb591b871df3e52c7cd", + "path": "research/p104-helper-319-fused-return/WORD.json.gz", + "sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "source": "https://github.com/Clear1nsight/integer-mult-bounds/blob/aaeec8c0acf01e99a5f331ef363a698d9c084ace/research/p104-helper-319-fused-return/WORD.json.gz", + "uncompress": false + }, + "price/inputs/ADMITTED.json": { + "commit": "349996445176e934ffb3c76813adcd230ca8f783", + "git_blob": "464c89e45c4eca230c099e8bac784a90200a5069", + "path": "research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "sha256": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/349996445176e934ffb3c76813adcd230ca8f783/research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "uncompress": false + }, + "price/inputs/PR7338-SHA256.json": { + "commit": "349996445176e934ffb3c76813adcd230ca8f783", + "git_blob": "8a4d2a0cf37422891787610ba0ae95b869e29751", + "path": "research/p104-compensated-fusion-readout-bound/receipts/SHA256.json", + "sha256": "25425e3a6fc025666f50faea07e9d41fa1924a44c121c5503b122f082bed2542", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/349996445176e934ffb3c76813adcd230ca8f783/research/p104-compensated-fusion-readout-bound/receipts/SHA256.json", + "uncompress": false + }, + "price/inputs/pricing.py": { + "commit": "c522451caf287bb3c16eaece72be4c263315dca4", + "git_blob": "40ec194017bda1d524bba4f07b188c53281419d0", + "path": "research/adjacent-owned-add-exchange-bound/pricing.py", + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/c522451caf287bb3c16eaece72be4c263315dca4/research/adjacent-owned-add-exchange-bound/pricing.py", + "uncompress": false + } + }, + "schema_version": 1 +} diff --git a/research/p104-retimed-chart207-split-bound/README.md b/research/p104-retimed-chart207-split-bound/README.md new file mode 100644 index 0000000000..930a57d15f --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/README.md @@ -0,0 +1,76 @@ +# Fixed-paid productive split in the retimed chart-207 block + +**NO VERIFIED GAIN. Conditional κ change 0%.** On exact +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334), +all 166 raw chart-207 cut/pivot keys in the helper-319 replacement +block reduce to 146 exact representatives. Independent rational +replays exclude every representative. Three lack a nonzero pure +prefix, 57 lack a nonzero pure suffix, and 86 lack a unit pairing. +Zero keys remain unresolved and the compatible saving upper is zero. + +The candidate would split one affected chart-3→127 productive target +of rank nine at an intermediate rank-eight chart-207 cut. It would +keep the complete paid itinerary and the signed caller. The full +public cut bank is used for the exact support test, with boundary +images in the 615-member endpoint cohort. Six affected public +roles qualify as pivots. The replay includes both old and retimed +chart histories and all 41 raw cuts of the emitted block. The +five extra endpoint entries in the reverse representation duplicate +earlier keys. See [PROOF.md](PROOF.md). + +## Exact inputs and replay + +The comparator is exact #7334 head +`aaeec8c0acf01e99a5f331ef363a698d9c084ace`, certified κ +`0.00364665195644`, with exact +[#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +signed caller at `07a76c5e2738882c0cb322278e56f6cae3c9885d`. +The independently reproduced peer gain over #7314 was +`0.000000430519994`. This exclusion adds no gain. +Native all-columns, owned erasure, compiler, precision/tape and +analytic recovery are inherited. The exact compressed #7314 +parent word, #7334 word, independently verified alignment, +admission and complete pricing inputs are pinned in the package. + +From a clean checkout, use CPython 3.12 with assertions enabled. + +```sh +python3.12 -I -B research/p104-retimed-chart207-split-bound/replay.py +python3.12 -B scripts/research_package.py --package research/p104-retimed-chart207-split-bound +``` + +Use `--out fresh-directory` to retain ten generated exact receipts. +The package requires only the tracked files and Python standard +library. It recomputes the complete price before reading geometry, +replays both occupied-bank walks and both exact pairing proofs, +and checks the per-key reconciliation. The first 128 and the +remaining 18 keys are replayed under their original separate caps. +Stale price and changed rank-stock inputs are rejected. + +## Open next questions + +A different intermediate chart or changed chronology may produce +a nonzero pairing. First pin one different bounded geometry and +price the full routing, basis, ownership and compiler changes. +A surviving exact pair would still need signed arbitrary-input +forward and adjoint action, dirty restoration, precision and tape +checks, and a complete caller and outer replay. One added raw +rank-one paid position already erases the tested split's +price-only gain. + +## Credit + +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) +supplies the retimed comparator and +[#7314](https://github.com/CrocSwap/integer-mult-bounds/pull/7314) +its exact parent. [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +supplies the signed caller, [#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) +the directed tariff and [#7338](https://github.com/CrocSwap/integer-mult-bounds/pull/7338) +the prior independent admission and full rank stock. +[#5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599) +supplies the cocharted split identity, [#7121](https://github.com/CrocSwap/integer-mult-bounds/pull/7121) +and [#7130](https://github.com/CrocSwap/integer-mult-bounds/pull/7130) +productive-split and pivot precedents, and +[#7332](https://github.com/CrocSwap/integer-mult-bounds/pull/7332) +a related fixed-paid cohort test on chart 240. OpenAI Codex and +subagents materially assisted. diff --git a/research/p104-retimed-chart207-split-bound/SOURCES.json b/research/p104-retimed-chart207-split-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-retimed-chart207-split-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-retimed-chart207-split-bound/TASK.json b/research/p104-retimed-chart207-split-bound/TASK.json new file mode 100644 index 0000000000..522c2a8be7 --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "On exact #7334, split one affected public chart-3\u2192127 rank-nine productive target at a chart-207 cut in the emitted helper-319 replacement block. Preserve the complete paid itinerary and use the full cocharted public bank with boundary images in the fixed 615-member cohort.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "Retimed chart-207 productive split research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "The fixed-paid 1+8 productive split would improve the signed complete invoice if both cut maps admit a common unit pairing.", + "budget_minutes": 6, + "evidence": "Both literal occupancy walks agree on 41 new cuts. 166 raw key occurrences reduce to 146 representatives. Independent exact rational proofs agree on every representative, with three no pure prefix, 57 no pure suffix, and 86 no unit pairing.", + "open_questions": [ + { + "blocked_by": "A surviving pair must still implement signed basis changes with dirty restoration and no additional paid call at the claimed margin.", + "first_step": "Pin one new geometry family and preprice all added routing and compiler costs before repeating the exact two-sided test.", + "question": "Can a different occupied chart or changed chronology expose a valid unit pairing?", + "why_it_matters": "Both pure spaces can be nonzero while their pairings cannot simultaneously be one." + } + ], + "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": "Tests productive support around a new literal retiming with all paid operations fixed, separate from the predecessor paid-fusion family.", + "scope_status": "changed", + "stop_rule": "Freeze complete price before decoding. Bound the first support run at 128 keys and the continuation at its exact 18 untouched keys. No build without an exact unit pairing.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-retimed-chart207-split-bound/VERIFY.json b/research/p104-retimed-chart207-split-bound/VERIFY.json new file mode 100644 index 0000000000..adb37ddded --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Rebuild signed split price, compare two literal chart histories, exhaust both exact paired replays across 146 keys, reconcile all 166 raw keys, and reject changed inputs.", + "timeout_seconds": 150 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-retimed-chart207-split-bound/engines/compare_geometry.py b/research/p104-retimed-chart207-split-bound/engines/compare_geometry.py new file mode 100644 index 0000000000..064d4ea999 --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/engines/compare_geometry.py @@ -0,0 +1,88 @@ +"""Compare complete raw chart-207 cut snapshots and both key cap conventions.""" +from argparse import ArgumentParser +from hashlib import sha256 +from gzip import decompress +from json import dumps, loads +from pathlib import Path + +LEAD = '4c349e06b22bfebb431fab1c9ae04f0e798f398acc6fdd99591b49b1c95ef6ca' +REVERSE = '587739d21541e7ffe01af9cb7e51abaa757ee69b580befe8bb768a81b614aa08' +WORD = '4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a' +CHART = 207 +FIELDS = ('public_bank', 'owned_bank', 'pivots') + + +def read(path, digest): + data = path.read_bytes() + assert sha256(data).hexdigest() == digest, path.name + return data + + +def bank(row): + return tuple(tuple(row[key]) for key in FIELDS) + + +def event_charts(event): + return event[2:4] if event[0] == 'MOVE' else [event[-1]] + + +def compare(forward, reverse, word): + f, b = loads(read(forward,LEAD)), loads(read(reverse,REVERSE)) + tape = loads(decompress(read(word,WORD)))['program'] + assert f['head'] == b['comparator_head'] and f['price_sha256'] == b['price_sha256'] + assert f['new_interval'] == [44588,44628] and f['new']['complete'] and f['old']['complete'] + assert not (b['new_unvisited_cuts'] or b['old_unvisited_cuts']) + assert len(b['new_snapshots']) == len(f['new']['rows']) == 41 + old = {r['cut']:r for r in f['old']['rows']} + common = sorted(cut for cut in map(int,b['old_snapshots']) if cut in old) + assert all(bank(old[cut]) == bank(b['old_snapshots'][str(cut)]) for cut in common) + assert len(common) == 47 + extra_old = sorted(set(map(int,b['old_snapshots']))-set(common)) + assert extra_old == [45719,45737,45738,45968,45969,46011,46012,46308,46309] + + lead_reps, raw_keys, coverage = [], [], [] + latest = None + for cut, row in enumerate(f['new']['rows'],44588): + assert row['cut'] == cut and bank(row) == bank(b['new_snapshots'][str(cut)]) + raw_keys.extend([cut,CHART,p] for p in row['pivots']) + expected_rep = cut == 44588 or CHART in event_charts(tape[cut-1]) + assert row['representative'] == expected_rep + if row['representative']: + latest = cut + lead_reps.extend([cut,CHART,p] for p in row['pivots']) + else: + assert bank(row) == bank(b['new_snapshots'][str(latest)]) + assert all(CHART not in event_charts(tape[t]) for t in range(latest,cut)) + coverage.append([cut,latest]) + assert len(raw_keys) == b['raw_key_count'] == 166 + assert len(lead_reps) == 146 and lead_reps[:128] == f['representative_keys'] + assert lead_reps[128:] == f['unvisited_keys'] and len(f['unvisited_keys']) == 18 + independent_reps = b['representative_keys'] + b['unvisited_keys'] + added = [[44628,CHART,p] for p in b['new_snapshots']['44628']['pivots']] + assert independent_reps == lead_reps + added + assert len(added) == 5 and len(independent_reps) == 151 and len(b['unvisited_keys']) == 23 + assert b['representative_keys'] == f['representative_keys'] + assert b['unvisited_keys'] == f['unvisited_keys'] + added + assert coverage[-3:] == [[44626,44626],[44627,44626],[44628,44626]] + omitted = [[44626,tape[44626]],[44627,tape[44627]]] + assert omitted == [[44626,['ADD',1467,319,'1',127]],[44627,['ADD',319,1467,'-1',127]]] + active = set(b['new_snapshots']['44626']['public_bank']+b['new_snapshots']['44626']['owned_bank']) + assert all(not active.intersection(e[1:3]) for _,e in omitted) + return dict(head=f['head'],price_sha256=f['price_sha256'],forward_sha256=LEAD,reverse_sha256=REVERSE, + matched_raw_new_cuts=41,matched_old_overlap_cuts=len(common), + reverse_only_old_lift_cuts=extra_old, + raw_pivot_pairs=166,lead_representative_pairs=146,reverse_representative_pairs=151, + identical_first_keys=128,lead_unvisited=18,reverse_unvisited=23, + equivalent_extra_pairs=added,equivalent_extra_cut=44626, + disjoint_chart_127_events=omitted,cut_coverage=coverage, + no_distinct_chart_207_event_omitted=True) + + +if __name__ == '__main__': + assert __debug__ + p=ArgumentParser(description=__doc__) + p.add_argument('forward',type=Path) + p.add_argument('reverse',type=Path) + p.add_argument('word',type=Path) + a=p.parse_args() + print(dumps(compare(a.forward,a.reverse,a.word),sort_keys=True,indent=2)) diff --git a/research/p104-retimed-chart207-split-bound/engines/continuation.py b/research/p104-retimed-chart207-split-bound/engines/continuation.py new file mode 100644 index 0000000000..04e62bc970 --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/engines/continuation.py @@ -0,0 +1,130 @@ +"""Resume only the 18 untouched chart-207 split keys from Round 72.""" +from argparse import ArgumentParser +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 +from time import monotonic + +HERE=Path(__file__).resolve().parent +PINS={ + 'inputs/paired_support.py':'38c796cbe1a73f386177faf88cd53294d4b911f6cde7fd47cd9fcef3b558373f', + 'inputs/R72-SUPPORT.json':'d90ce338aab69c0c074f72e2e91e2eaa04fd347ea6cded83237d0996af327f98', + 'inputs/R72-OCCUPANCY.json':'4c349e06b22bfebb431fab1c9ae04f0e798f398acc6fdd99591b49b1c95ef6ca', + 'inputs/7334-WORD.json.gz':'4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a', + 'inputs/PRICE.json':'b3c36d5a1d199a1e74f979d660fac295c55659a9d4edb70eaef541095670323b', + 'inputs/ADMITTED.json':'c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13', +} +CAP=18 + + +def need(condition,message): + if not condition: + raise ValueError(message) + + +def unique(items): + row=dict(items) + need(len(row)==len(items),'Duplicate input key') + return row + + +def pinned(path,digest): + raw=(HERE/path).read_bytes() + need(sha256(raw).hexdigest()==digest,f'Changed dependency {path}') + return raw + + +def parsed(name): + return loads(pinned(name,PINS[name]),object_pairs_hook=unique) + + +def encoded(value): + return (dumps(value,indent=2,sort_keys=True)+'\n').encode() + + +def select(): + geom=parsed('inputs/R72-OCCUPANCY.json') + prior=parsed('inputs/R72-SUPPORT.json') + price=parsed('inputs/PRICE.json') + admission=parsed('inputs/ADMITTED.json') + need(geom['head']==prior['head']==price['head']==admission['head'],'Source head mismatch') + need(prior['geometry_sha256']==PINS['inputs/R72-OCCUPANCY.json'] and + geom['price_sha256']==prior['price_sha256']==PINS['inputs/PRICE.json'],'Geometry or price mismatch') + need(prior['word_sha256']==admission['inputs']['WORD.json.gz']==PINS['inputs/7334-WORD.json.gz'] and + prior['admission_sha256']==PINS['inputs/ADMITTED.json'] and admission['exit']==0,'Admission mismatch') + need(price['productive_delta']=={'1':17,'8':17,'9':-17} and not price['paid_delta'],'Wrong frozen price') + earlier=[tuple(row['key']) for row in prior['decisions']] + keys=[tuple(row) for row in geom['unvisited_keys']] + need(earlier==[tuple(row) for row in geom['representative_keys']] and len(set(earlier))==128 and + not prior['support_only'],'Prior scope did not exhaust the 128 authorized keys') + need(keys==[tuple(row) for row in prior['unresolved']] and len(set(keys))==CAP and + set(keys).isdisjoint(earlier),'Continuation is not the exact untouched suffix') + by_cut={} + for row in prior['decisions']: + cut=row['key'][0] + record={k:v for k,v in row.items() if k!='key'} + need(cut not in by_cut or by_cut[cut]==record,'Different results at the same literal bank') + by_cut[cut]=record + reused=[] + fresh=[] + for key in keys: + cut,chart,pivot=key + need(chart==207 and pivot in geom['endpoint_cohort'],'Wrong target bank or pivot cohort') + if cut in by_cut: + row=by_cut[cut] + need(pivot in row['public_bank'],'New pivot is absent at previously checked cut') + reused.append(dict(key=key,**row)) + else: + fresh.append(key) + derived=geom|dict(representative_keys=keys,unvisited_keys=[], + r72_occupancy_sha256=PINS['inputs/R72-OCCUPANCY.json'], + r72_support_sha256=PINS['inputs/R72-SUPPORT.json'], + same_bank_keys=[row['key'] for row in reused],fresh_keys=fresh) + return derived,reused,fresh,price + + +def main(): + p=ArgumentParser(description=__doc__) + commands=p.add_mutually_exclusive_group(required=True) + commands.add_argument('--derive-only',action='store_true') + commands.add_argument('--support',action='store_true') + p.add_argument('--selection-sha') + a=p.parse_args() + assert __debug__ + derived,reused,fresh,price=select() + selection=encoded(derived) + if a.derive_only: + print(selection.decode(),end='');return + need(a.selection_sha and sha256(selection).hexdigest()==a.selection_sha,'Frozen selection pin required') + pinned('inputs/paired_support.py',PINS['inputs/paired_support.py']) + engine=run_path(str(HERE/'inputs/paired_support.py')) + controls=engine['controls']() + def watchdog(*_): + raise TimeoutError('R73 hard 35-second watchdog') + signal(SIGALRM,watchdog) + alarm(35) + try: + deadline=monotonic()+32 + raw=pinned('inputs/7334-WORD.json.gz',PINS['inputs/7334-WORD.json.gz']) + word=loads(decompress(raw),object_pairs_hook=unique) + exact=engine['audit'](word,derived|dict(representative_keys=fresh),deadline) + finally: + alarm(0) + all_rows={tuple(row['key']):row for row in reused+exact['decisions']} + all_keys=derived['representative_keys'] + result=dict(head=derived['head'],selected=CAP,case_cap=CAP,seconds_cap=35, + status='EXHAUSTED' if not exact['unresolved'] else 'CAPPED', + same_bank_reused=len(reused),fresh_replayed=len(exact['decisions']), + decisions=[all_rows[key] for key in all_keys if key in all_rows], + unresolved=exact['unresolved'],support_only=exact['support_only'], + prefix_events=exact['prefix_events'],suffix_events=exact['suffix_events'], + selection_sha256=a.selection_sha,input_sha256=PINS,controls=controls, + unvisited_credit_upper=price['one_edit_optimistic_credit'][1]) + print(encoded(result).decode(),end='') + + +if __name__=='__main__': + main() diff --git a/research/p104-retimed-chart207-split-bound/engines/occupancy.py b/research/p104-retimed-chart207-split-bound/engines/occupancy.py new file mode 100644 index 0000000000..a9b5f188bd --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/engines/occupancy.py @@ -0,0 +1,140 @@ +"""Pinned forward chart-207 census around the exact #7334 retimed block.""" +from argparse import ArgumentParser +from fractions import Fraction +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from time import monotonic + +PINS = { + "price/PRICE.json": "b3c36d5a1d199a1e74f979d660fac295c55659a9d4edb70eaef541095670323b", + "inputs/7314-WORD.json.gz": "c404b9b61220e6cf740d85276df2828bbb4a9d68a4d44b5e283f8d96f78c0fd9", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/IDENTITIES.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", +} +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +FRAME = 207 +PROTECTED = {319, 863, 1355, 1568} +CAP = 128 +SECONDS = 18 + + +def read(root, name): + raw = (root / name).read_bytes() + if sha256(raw).hexdigest() != PINS[name]: + raise ValueError(f"changed input: {name}") + def unique(pairs): + result = dict(pairs) + if len(result) != len(pairs): + raise ValueError("duplicate JSON key") + return result + return json.loads(decompress(raw) if name.endswith(".gz") else raw, object_pairs_hook=unique) + + +def span(basis): + vectors = {0} + for v in basis: + assert v not in vectors + vectors |= {v ^ x for x in vectors} + return vectors + + +def walk(word, interval, members, deadline, frame=FRAME): + n = word["public"] + tape = word["program"] + charts = word["initial"].copy() + [None] * word["owned_fields"] + lo, hi = interval + assert 0 <= lo <= hi <= len(tape) + rows = [] + last = None + for k in range(len(tape)+1): + if k % 256 == 0 and monotonic() >= deadline: + return {"complete": False, "rows": rows, "unvisited_from_clock": k} + if lo <= k <= hi: + bank = [r for r, f in enumerate(charts[:n]) if f == frame] + rows.append(dict(cut=k, public_bank=bank, pivots=sorted(members.intersection(bank)), + owned_bank=[r for r in range(n,len(charts)) if charts[r]==frame], + representative=k==lo or last)) + if k == len(tape): + break + op,d,*a = tape[k] + if op == "MOVE": + x,y,owned = a + assert charts[d]==x and owned==(d>=n) + charts[d]=y + last = frame in (x,y) + elif op in ("INIT","CLEAR"): + f, = a + assert d>=n and charts[d]==(None if op=="INIT" else f) + charts[d]=f if op=="INIT" else None + last = f==frame + else: + assert op in ("ADD","COPY","SCALE") and Fraction(a[-2]) and charts[d]==a[-1] + if op!="SCALE": + assert charts[a[0]]==a[-1] and a[0]!=d + assert op!="COPY" or d>=n + last = a[-1]==frame + assert charts==word["final"]+[None]*word["owned_fields"] + return {"complete": True,"rows": rows,"unvisited_from_clock": None} + + +def controls(): + word = dict(public=2,owned_fields=1,initial=[0,0],final=[2,2],program=[ + ["MOVE",0,0,1,False],["MOVE",1,0,1,False],["INIT",2,1], + ["COPY",2,1,"1",1],["CLEAR",2,1], + ["MOVE",0,1,2,False],["MOVE",1,1,2,False]]) + s=walk(word,(0,7),{0},float("inf"),1) + assert [r["cut"] for r in s["rows"] if r["pivots"]]==[1,2,3,4,5] + assert s["rows"][4]["public_bank"]==[0,1] and s["rows"][4]["owned_bank"]==[2] + assert not s["rows"][7]["public_bank"] + return ["pre-event cuts and both MOVE endpoints", "owned row separated from public bank"] + + +def main(): + p=ArgumentParser() + p.add_argument("root", type=Path) + p.add_argument("--controls-only",action="store_true") + a=p.parse_args() + check=controls() + if a.controls_only: + print(json.dumps(check)) + return + d=a.root + price=read(d,"price/PRICE.json") + assert price["head"]==HEAD and not price["paid_delta"] + assert price["productive_delta"]=={"1":17,"8":17,"9":-17} + meta=read(d,"inputs/IDENTITIES.json") + old,new=(read(d,f"inputs/{name}-WORD.json.gz") for name in (7314,7334)) + n=new["public"] + assert n==old["public"]==1501 and new["initial"]==old["initial"] and new["final"]==old["final"] + assert new["frames"]==old["frames"] and new["live"]==old["live"] and new["hosted"]==old["hosted"] + ranks=[len(new["frames"][f]) for f in (3,207,127)] + assert ranks==[0,8,9] + assert span(new["frames"][3]) xD) lies inside ker(x -> xB). + rows=len(B) + cols=len(B[0]) if B else 0 + def wedge(b,d): + return any(b[i]*d[j]!=b[j]*d[i] for i in range(cols) for j in range(i)) + has_wedge=any(wedge(b,d) for b,d in zip(B,D,strict=True)) + if not has_wedge: + for i in range(rows): + for j in range(i): + if wedge([x+y for x,y in zip(B[i],B[j],strict=True)], + [x+y for x,y in zip(D[i],D[j],strict=True)]): + has_wedge=True + break + if has_wedge: + break + dr=rank([{i:x for i,x in enumerate(r) if x} for r in D]) + sr=rank([{i:x for i,x in enumerate(d+b) if x} for d,b in zip(D,B,strict=True)]) + return has_wedge,dr,sr + + +def side(word,banks,allowed,deadline,reverse): + n=word["public"] + tape=word["program"] + vectors=[{i:Q(1)} for i in range(n)]+[{} for _ in range(word["owned_fields"])] + rows={} + cuts=range(len(tape),min(banks)-1,-1) if reverse else range(0,max(banks)+1) + for t in cuts: + if t%128==0 and monotonic()>=deadline: + break + if t in banks: + rows[t]=null_pure(banks[t],vectors,allowed) + if t==0 and reverse: + break + op,d,*args=tape[t-1 if reverse else t] + if op=="MOVE": + continue + if op in ("INIT","CLEAR"): + vectors[d]={} + else: + q=coefficient(args[-2]) + source=d if op=="SCALE" else args[0] + assert op=="SCALE" or source!=d + if op=="SCALE": + vectors[d]={i:q*x for i,x in vectors[d].items()} + elif reverse: + plus(vectors[source],vectors[d],q) + if op=="COPY": + vectors[d]={} + elif op=="COPY": + vectors[d]={i:q*x for i,x in vectors[source].items()} + else: + assert op=="ADD" + plus(vectors[d],vectors[source],q) + return rows + + +def run(word,geom,keys): + deadline=monotonic()+32 + groups=Counter(k[0] for k in keys) + banks={row["cut"]:row["public_bank"] for row in geom["new"]["rows"] if row["cut"] in groups} + allowed=set(geom["endpoint_cohort"]) + forward=side(word,banks,allowed,deadline,False) + reverse=side(word,banks,allowed,deadline,True) + ans=[] + def dot(a,b): + return sum(x*b.get(i,0) for i,x in a.items()) + for t,n in sorted(groups.items()): + if t not in forward or t not in reverse or monotonic()>=deadline: + continue + F,R=forward[t],reverse[t] + w=dr=sr=None + if not any(c for a,c in F): + status="no nonzero pure prefix" + elif not any(d for b,d in R): + status="no nonzero pure suffix" + else: + B=[[dot(a,b) for b,d in R] for a,c in F] + C=[[dot(c,d) for b,d in R] for a,c in F] + D=[[x-y for x,y in zip(b,c,strict=True)] for b,c in zip(B,C,strict=True)] + w,dr,sr=pairing(B,D) + status="paired support unresolved" if w or dr!=sr else "no unit pairing" + ans.append(dict(cut=t,cases=n,status=status,prefix_dimension=len(F),suffix_dimension=len(R), + nonzero_wedge=w,exterior_rank=dr,stacked_rank=sr)) + missing=set(groups)-{r["cut"] for r in ans} + counts=Counter() + for row in ans: + counts[row["status"]]+=row["cases"] + return dict(cases=len(keys),rows=ans,counts=dict(counts), + unvisited=[key for key in keys if key[0] in missing]) + + +def main(): + root=Path(sys.argv[1]) + which=sys.argv[2] + assert which in ("first","remaining") + geom=json.loads(checked(root/"lead/OCCUPANCY.json",GEOMETRY)) + word=json.loads(decompress(checked(root/"inputs/7334-WORD.json.gz",WORD))) + assert pairing([[Q(1),Q(0)]],[[Q(0),Q(1)]])[0] + assert pairing([[Q(1)]],[[Q(2)]])==(False,1,1) + assert pairing([[Q(1)]],[[Q(0)]])==(False,0,1) + keys=geom["representative_keys" if which=="first" else "unvisited_keys"] + assert len(keys)==(128 if which=="first" else 18) + data=run(word,geom,keys) + print(json.dumps(data|dict(selection=which,word_sha256=WORD,geometry_sha256=GEOMETRY, + controls=["nonzero wedge","proportional equal rank","nonzero pairing on difference kernel"]), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-retimed-chart207-split-bound/engines/paired_support.py b/research/p104-retimed-chart207-split-bound/engines/paired_support.py new file mode 100644 index 0000000000..46180f7b49 --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/engines/paired_support.py @@ -0,0 +1,356 @@ +"""Exact pure prefix/suffix and unit pairing for the #7334 chart-207 split.""" +from argparse import ArgumentParser +from collections import defaultdict +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic + +HEAD = 'aaeec8c0acf01e99a5f331ef363a698d9c084ace' +WORD = '4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a' +ADMISSION = 'c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13' +PROTECTED = {319,863,1355,1568} +CAP = 128 + + +class Capped(Exception): + pass + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def check_time(deadline): + if monotonic() >= deadline: + raise Capped + + +def pinned(path, digest): + raw = path.read_bytes() + need(sha256(raw).hexdigest() == digest, f'Changed input {path.name}') + return raw + + +def unique(pairs): + doc = dict(pairs) + need(len(doc) == len(pairs), 'Duplicate receipt key') + return doc + + +def read(raw): + return loads(raw,object_pairs_hook=unique) + + +@cache +def rational(value): + return Q(value) + + +def axpy(dst, src, factor): + for j,v in src.items(): + value = dst.get(j,0) + factor*v + if value: + dst[j] = value + else: + dst.pop(j,None) + + +def dot(a,b): + return sum(v*b.get(j,0) for j,v in a.items()) + + +def compose(weights, rows): + vector = {} + for role, coefficient in weights.items(): + axpy(vector,rows[role],coefficient) + return vector + + +def pure_kernel(rows, allowed, deadline): + pivots, pure = {}, [] + for role,row in rows.items(): + check_time(deadline) + exterior = {j:v for j,v in row.items() if j not in allowed} + coeff = {role:Q(1)} + while exterior: + j = min(exterior) + if j not in pivots: + lead = exterior[j] + pivots[j] = ({k:v/lead for k,v in exterior.items()}, + {k:v/lead for k,v in coeff.items()}) + break + other, op = pivots[j] + factor = -exterior[j] + axpy(exterior,other,factor) + axpy(coeff,op,factor) + else: + projection = compose(coeff,rows) + assert projection.keys() <= allowed + pure.append((coeff,projection)) + assert len(pivots)+len(pure) == len(rows) + return sorted(pivots), pure + + +def solve_bilinear(B,D,deadline): + """Find x,y with xBy=1 and xDy=0, or prove no such rational pair.""" + n = len(B) + def trial(x): + bx,dx = compose(x,B),compose(x,D) + if not bx: + return None + if not dx: + j = min(bx) + return x,{j:1/bx[j]} + pivot = min(dx) + for j in sorted(bx.keys() | dx.keys()): + value = bx.get(j,0)*dx[pivot]-bx.get(pivot,0)*dx.get(j,0) + if value: + y = {j:dx[pivot]/value} + if dx.get(j,0): + y[pivot] = -dx[j]/value + assert dot(bx,y) == 1 and dot(dx,y) == 0 + return x,y + return None + for i in range(n): + check_time(deadline) + hit = trial({i:Q(1)}) + if hit: + return hit + # Each wedge coordinate is a homogeneous quadratic in x. Basis vectors + # and pair sums determine all coefficients over Q. + for i in range(n): + check_time(deadline) + for j in range(i+1,n): + hit = trial({i:Q(1),j:Q(1)}) + if hit: + return hit + # All wedges vanish. Only xD=0 but xB!=0 can give a pair. + _, kernel = pure_kernel(dict(enumerate(D)),set(),deadline) + for x,_ in kernel: + hit = trial(x) + if hit: + return hit + return None + + +def paired(prefix,suffix,deadline): + B,D = [],[] + for a,c in prefix: + check_time(deadline) + dot_boundary = {j:v for j,(_,d) in enumerate(suffix) if (v:=dot(c,d))} + dot_difference = {j:v for j,(b,_) in enumerate(suffix) if (v:=dot(a,b)-dot_boundary.get(j,0))} + B.append(dot_boundary); D.append(dot_difference) + hit = solve_bilinear(B,D,deadline) + if hit is None: + return None + x,y = hit + a,c = (compose(x,[pair[i] for pair in prefix]) for i in (0,1)) + b,d = (compose(y,[pair[i] for pair in suffix]) for i in (0,1)) + assert dot(a,b)==dot(c,d)==1 + return dict(a=a,b=b,c=c,d=d) + + +def initial_groups(word): + n = word['public'] + main = set(word['live']) | {r+112 for r in word['live']} + main.update(word['hosted']['X2']); main.update(word['hosted']['Y2']) + cohort = {r for r in range(n) if r not in main and (word['initial'][r],word['final'][r])==(3,127)} + return cohort-PROTECTED,cohort-PROTECTED + + +def prefix_rows(word, cuts, deadline): + n = word['public']; rows = [{r:Q(1)} for r in range(n)]+[None]*word['owned_fields'] + charts = word['initial']+[None]*word['owned_fields'] + banks, seen = {}, 0 + try: + for clock,event in enumerate(word['program']): + if clock%64 == 0 or clock in cuts: + check_time(deadline) + if clock in cuts: + banks[clock] = {r:rows[r].copy() for r in range(n) if charts[r]==207} + if clock >= max(cuts): + break + op,dst,*args = event + if op == 'MOVE': + old,new,owned = args + assert charts[dst] == old and owned==(dst>=n) + charts[dst]=new + elif op == 'INIT': + assert dst>=n and rows[dst] is None + rows[dst],charts[dst]={},args[0] + elif op == 'CLEAR': + assert dst>=n and charts[dst]==args[0] + rows[dst]=charts[dst]=None + elif op == 'SCALE': + assert charts[dst]==args[1] + rows[dst]={j:rational(args[0])*v for j,v in rows[dst].items()} + else: + src,q,chart=args + assert charts[dst]==charts[src]==chart and src!=dst and op in {'ADD','COPY'} + if op=='COPY': + assert dst>=n and not rows[dst], 'Dirty COPY' + axpy(rows[dst],rows[src],rational(q)) + seen=clock+1 + except Capped: + pass + return banks,seen + + +def suffix_rows(word,banks,deadline): + n=word['public']; cols=[{r:Q(1)} for r in range(n)]+[{} for _ in range(word['owned_fields'])] + snapshots,seen={},0 + try: + for clock in range(len(word['program']),min(banks)-1,-1): + if clock%64==0 or clock in banks: + check_time(deadline) + if clock in banks: + snapshots[clock]={r:cols[r].copy() for r in banks[clock]} + if clock==min(banks): + break + op,dst,*args=word['program'][clock-1] + if op in {'ADD','COPY'}: + src,q,_=args + axpy(cols[src],cols[dst],rational(q)) + if op=='COPY': + cols[dst]={} + elif op=='SCALE': + cols[dst]={j:rational(args[0])*v for j,v in cols[dst].items()} + elif op in {'INIT','CLEAR'}: + cols[dst]={} + else: + assert op=='MOVE' + seen+=1 + except Capped: + pass + return snapshots,seen + + +def geometry_keys(geometry): + if 'representative_keys' in geometry: + raw=geometry['representative_keys'] + elif 'keys' in geometry: + raw=geometry['keys'] + else: + raw=[(row['cut'],row['chart'],pivot) for row in geometry['segments'] for pivot in row['pivots']] + result=[tuple(row) if not isinstance(row,dict) else (row['cut'],row['chart'],row['pivot']) for row in raw] + need(len(result)==len(set(result)) and all(len(row)==3 and row[1]==207 and 44588<=row[0]<=44628 for row in result),'Wrong geometry key inventory') + return result + + +def audit(word,geometry,deadline): + all_keys=geometry_keys(geometry) + if not all_keys: + return dict(status='empty_geometry',selected=0,decisions=[],unresolved=[]) + keys=all_keys[:CAP] + cohort,pivots=initial_groups(word) + if 'endpoint_cohort' in geometry: + assert sorted(cohort)==geometry['endpoint_cohort'] + overflow=[tuple(key) for key in geometry.get('unvisited_keys',())] + assert len(overflow)==len(set(overflow)) and not set(overflow).intersection(all_keys) + bank_plan=defaultdict(list) + for cut,chart,pivot in keys: + need(pivot in pivots,'Protected or non-helper pivot') + bank_plan[cut].append(pivot) + banks,forward=prefix_rows(word,bank_plan,deadline) + decisions,opens={}, {} + try: + for cut,bank in banks.items(): + need(set(bank_plan[cut])<=bank.keys(),'Pivot absent from literal chart bank') + exterior,pure=pure_kernel(bank,cohort,deadline) + if any(c for _,c in pure): + opens[cut]=(exterior,pure) + else: + decisions[cut]=dict(status='no_nonzero_pure_prefix',public_bank=list(bank), + prefix_exterior_pivots=exterior,prefix_nullity=len(pure)) + except Capped: + pass + backward=0 + if opens: + snapshots,backward=suffix_rows(word,{c:banks[c] for c in opens},deadline) + try: + for cut,bank in snapshots.items(): + exterior,pure=pure_kernel(bank,cohort,deadline) + pre_rank,pre=opens[cut] + row=dict(public_bank=list(bank),prefix_exterior_pivots=pre_rank, + suffix_exterior_pivots=exterior,prefix_nullity=len(pre),suffix_nullity=len(pure)) + if not any(d for _,d in pure): + decisions[cut]=row|dict(status='no_nonzero_pure_suffix') + continue + witness=paired(pre,pure,deadline) + if witness is None: + decisions[cut]=row|dict(status='no_unit_pairing') + continue + assert compose(witness['a'],banks[cut])==witness['c'] + assert compose(witness['b'],bank)==witness['d'] + decisions[cut]=row|dict(status='exact_support_only',witness={k:{j:str(v) for j,v in value.items()} for k,value in witness.items()}) + except Capped: + pass + rows=[dict(key=key,**decisions[key[0]]) for key in keys if key[0] in decisions] + unresolved=[key for key in all_keys if key[0] not in decisions or key not in keys] + overflow + return dict(status='CAPPED' if unresolved else 'EXHAUSTED',selected=len(keys), + eligible_cohort=sorted(cohort),prefix_events=forward,suffix_events=backward, + decisions=rows,unresolved=unresolved,support_only=[row['key'] for row in rows if row['status']=='exact_support_only']) + + +def controls(): + inf=float('inf') + _,a=pure_kernel({4:{0:Q(1),2:Q(1)},5:{2:Q(1)}},{0},inf) + _,b=pure_kernel({4:{0:Q(1)},5:{3:Q(1)}},{0},inf) + hit=paired(a,b,inf) + assert hit and hit['a'][4] == -hit['a'][5] != 0 + assert dot(hit['a'],hit['b']) == dot(hit['c'],hit['d']) == 1 + _,wrong=pure_kernel({4:{0:Q(1),3:Q(1)},5:{3:Q(1)}},{0},inf) + assert paired(a,wrong,inf) is None + assert solve_bilinear([{0:Q(1)},{1:Q(1)}],[{0:Q(1)},{1:Q(2)}],inf)[0]=={0:Q(1),1:Q(1)} + assert solve_bilinear([{0:Q(1)},{0:Q(2)}],[{0:Q(1)},{0:Q(1)}],inf) is not None + return ['signed_unit_pair','unequal_pairing_rejected','quadratic_cross_term','left_kernel_D'] + + +def main(): + p=ArgumentParser(description=__doc__) + p.add_argument('--controls-only',action='store_true') + for key in ('word','price','geometry','admission'): + p.add_argument('--'+key,type=Path) + p.add_argument('--price-sha'); p.add_argument('--geometry-sha') + a=p.parse_args() + assert __debug__ + checks=controls() + if a.controls_only: + print(dumps(dict(controls=checks),indent=2,sort_keys=True)); return + need(all((a.word,a.price,a.geometry,a.admission,a.price_sha,a.geometry_sha)),'Sealed geometry and price are required') + price=read(pinned(a.price,a.price_sha)); geom=read(pinned(a.geometry,a.geometry_sha)) + admission=read(pinned(a.admission,ADMISSION)) + assert price['head']==admission['head']==HEAD and admission['exit']==0 + assert price['productive_delta']=={'1':17,'8':17,'9':-17} and not price['paid_delta'] + assert admission['inputs']['WORD.json.gz']==WORD + if 'price_sha256' in geom: + assert geom['price_sha256']==a.price_sha + if 'word_sha256' in geom: + assert geom['word_sha256']==WORD + keys=geometry_keys(geom) + if keys: + def watchdog(*_): + raise TimeoutError('hard support watchdog') + signal(SIGALRM,watchdog) + alarm(35) + try: + deadline=monotonic()+32 + result=audit(read(decompress(pinned(a.word,WORD))),geom,deadline) + finally: + alarm(0) + else: + result=dict(status='empty_geometry',selected=0,decisions=[],unresolved=[]) + result.update(head=HEAD,word_sha256=WORD,admission_sha256=ADMISSION,price_sha256=a.price_sha, + geometry_sha256=a.geometry_sha,cap=CAP,seconds_cap=35,controls=checks, + unvisited_credit_upper=price['one_edit_optimistic_credit'][1]) + print(dumps(result,indent=2,sort_keys=True)) + + +if __name__=='__main__': + main() diff --git a/research/p104-retimed-chart207-split-bound/engines/reconcile.py b/research/p104-retimed-chart207-split-bound/engines/reconcile.py new file mode 100644 index 0000000000..d4f6606228 --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/engines/reconcile.py @@ -0,0 +1,133 @@ +"""Reconcile frozen chart-207 occupancy and paired support keys.""" +from collections import Counter +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +import sys + +HEAD="aaeec8c0acf01e99a5f331ef363a698d9c084ace" +FRAME=207 +PINS={ + "72/lead/OCCUPANCY.json":"4c349e06b22bfebb431fab1c9ae04f0e798f398acc6fdd99591b49b1c95ef6ca", + "72/independent/RESULT.json":"587739d21541e7ffe01af9cb7e51abaa757ee69b580befe8bb768a81b614aa08", + "72/independent/COMPARE.json":"0217f80d0aafdc9fa8f281bf725ff68ba2952b68b19e6ab5b3fee802000ed97c", + "72/support/RESULT.json":"d90ce338aab69c0c074f72e2e91e2eaa04fd347ea6cded83237d0996af327f98", + "72/lead/PAIRED.json":"5529a4338efed76989d113100eed30a46bc15c572ab55a58020e8eab423f9143", + "72/inputs/7334-WORD.json.gz":"4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "72/price/PRICE.json":"b3c36d5a1d199a1e74f979d660fac295c55659a9d4edb70eaef541095670323b", + "73/support/RESULT.json":"8ef9be1998d67edf665fc9be07b96e00157f17e86f22f87038ec3b84aa3334ba", + "73/support/SELECTION.json":"d68ce20cabfd2262aec3925d6b055dcc9ffa08d125e694401760c1ffab5d899a", + "73/lead/PAIRED.json":"9b06f7b2e17e6d46fa811e05ab7e0fcc45ff5ecd98cacecb8617b662142a6ddc", +} + + +def unpack(path, expected): + data=path.read_bytes() + if sha256(data).hexdigest()!=expected: + raise ValueError(f"changed receipt or source: {path.name}") + def unique(items): + result=dict(items) + if len(result)!=len(items): + raise ValueError("duplicate JSON key") + return result + return json.loads(decompress(data) if path.suffix==".gz" else data, object_pairs_hook=unique) + + +def touched(event): + return event[2:4] if event[0]=="MOVE" else event[-1:] + + +def bank(row): + return (row["public_bank"],row["owned_bank"],row["pivots"]) + + +def reconcile(p): + f,r,c=(p[k] for k in ("72/lead/OCCUPANCY.json","72/independent/RESULT.json","72/independent/COMPARE.json")) + a,b=(p[k] for k in ("72/support/RESULT.json","73/support/RESULT.json")) + selection=p["73/support/SELECTION.json"] + price=p["72/price/PRICE.json"] + assert f["head"]==r["comparator_head"]==a["head"]==b["head"]==price["head"]==HEAD + assert f["price_sha256"]==r["price_sha256"]==a["price_sha256"]==PINS["72/price/PRICE.json"] + assert not price["paid_delta"] and price["productive_delta"]=={"1":17,"8":17,"9":-17} + assert f["new_interval"]==[44588,44628] and f["new"]["complete"] and f["old"]["complete"] + assert c["matched_raw_new_cuts"]==41 and c["matched_old_overlap_cuts"]==47 + first=f["representative_keys"] + remaining=f["unvisited_keys"] + rev_remaining=r["unvisited_keys"] + assert first==r["representative_keys"] and len(first)==128 + assert remaining==rev_remaining[:18]==selection["representative_keys"]==a["unresolved"] + assert len(remaining)==18 and len(rev_remaining)==23 + aliases=rev_remaining[18:] + assert len(aliases)==5 and aliases==c["equivalent_extra_pairs"] + tape=p["72/inputs/7334-WORD.json.gz"]["program"] + snapshots=f["new"]["rows"] + assert len(snapshots)==41 and [row["cut"] for row in snapshots]==list(range(44588,44629)) + assert all(bank(row)==bank(r["new_snapshots"][str(row["cut"])]) for row in snapshots) + banks={} + raw=[] + repr_cut=None + for row in snapshots: + cut=row["cut"] + if cut==44588 or FRAME in touched(tape[cut-1]): + repr_cut=cut + banks[repr_cut]=row + assert row["representative"]==(repr_cut==cut) + assert bank(row)==bank(banks[repr_cut]) + assert all(FRAME not in touched(event) for event in tape[repr_cut:cut]) + for pivot in row["pivots"]: + raw.append(dict(key=[cut,FRAME,pivot],representative=[repr_cut,FRAME,pivot])) + assert len(raw)==166 + keys=first+remaining + assert len({tuple(k) for k in keys})==146 + assert sorted({tuple(x["representative"]) for x in raw})==sorted(map(tuple,keys)) + alias_lookup={tuple(x["key"]):x["representative"] for x in raw} + assert [alias_lookup[tuple(k)] for k in aliases]==[[44626,FRAME,p] for p in (205,532,969,1250,1453)] + assert tape[44626:44628]==[["ADD",1467,319,"1",127],["ADD",319,1467,"-1",127]] + assert all(r not in set(banks[44626]["public_bank"]+banks[44626]["owned_bank"]) for r in (319,1467)) + assert a["status"]=="CAPPED" and a["selected"]==a["cap"]==128 and not a["support_only"] + assert b["status"]=="EXHAUSTED" and b["selected"]==b["case_cap"]==18 and not b["unresolved"] and not b["support_only"] + assert b["same_bank_reused"]==2 and b["fresh_replayed"]==16 + solved=[] + for round_no,data,subset in ((72,a,first),(73,b,remaining)): + independent=p[f"{round_no}/lead/PAIRED.json"] + assert not independent["unvisited"] and independent["cases"]==len(subset) + by_cut={row["cut"]:row["status"].replace(" ","_") for row in independent["rows"]} + assert [row["key"] for row in data["decisions"]]==subset + for item in data["decisions"]: + key=item["key"] + cut,chart,pivot=key + assert item["public_bank"]==banks[cut]["public_bank"] and pivot in banks[cut]["pivots"] + assert item["status"]==by_cut[cut] and item["status"] in ( + "no_nonzero_pure_prefix","no_nonzero_pure_suffix","no_unit_pairing") + assert chart==FRAME + route="new exact bank check" + if key in selection["same_bank_keys"]: + route="exact same cut and bank certificate from initial 128" + solved.append(dict(key=key,round=round_no,bank_cut=cut,disposition=item["status"],route=route)) + status={tuple(row["key"]):row["disposition"] for row in solved} + for row in raw: + row["disposition"]=status[tuple(row["representative"])] + return dict(head=HEAD,price_sha256=PINS["72/price/PRICE.json"],pins=PINS, + cut_convention="cut k immediately precedes literal event k", + budgets=dict(initial_cap=128,initial_resolved=128,initial_capped=True, + continuation_cap=18,continuation_resolved=18,continuation_same_bank_reuse=2, + continuation_fresh_keys=16,seconds_per_support_runner=35,extra_alias_cases_run=0), + first_128=first,forward_pending_at_cap=remaining,reverse_pending_at_cap=rev_remaining, + reverse_post_block_aliases=[dict(key=k,representative=alias_lookup[tuple(k)]) for k in aliases], + post_block_bank=dict(representative=44626,alias_cut=44628, + public_bank=banks[44626]["public_bank"],owned_bank=banks[44626]["owned_bank"], + pivots=banks[44626]["pivots"],events=[[i,tape[i]] for i in (44626,44627)]), + banks=list(banks.values()),raw_keys=raw,canonical_dispositions=solved, + summary=dict(raw_keys=len(raw),canonical_keys=len(solved),reverse_keys=151, + unresolved=0,advanced=0,exclusions=dict(Counter(row["disposition"] for row in solved)))) + + +def main(): + roots=dict(zip(("72","73"),map(Path,sys.argv[1:]),strict=True)) + inputs={key:unpack(roots[key[:2]]/key[3:],digest) for key,digest in PINS.items()} + print(json.dumps(reconcile(inputs),indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-retimed-chart207-split-bound/engines/reverse_207.py b/research/p104-retimed-chart207-split-bound/engines/reverse_207.py new file mode 100644 index 0000000000..3d4174abc3 --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/engines/reverse_207.py @@ -0,0 +1,228 @@ +"""Reverse exact old/new chart-207 occupancy for the #7334 retimed block.""" +from argparse import ArgumentParser +from fractions import Fraction +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic + +HEAD = 'aaeec8c0acf01e99a5f331ef363a698d9c084ace' +ADMISSION = 'c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13' +PRICE = 'b3c36d5a1d199a1e74f979d660fac295c55659a9d4edb70eaef541095670323b' +PINS = { + '7314-WORD.json.gz':'c404b9b61220e6cf740d85276df2828bbb4a9d68a4d44b5e283f8d96f78c0fd9', + '7334-WORD.json.gz':'4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a', + 'IDENTITIES.json':'f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b', +} +CHART, AUX, OLD_HELPER = 207, 1567, 319 +PROTECTED = {319,863,1355,1568} +CAP = 128 + + +def decode(raw): + def unique(items): + obj = dict(items) + assert len(obj) == len(items), 'duplicate JSON key' + return obj + return loads(raw,object_pairs_hook=unique) + + +def pinned(path, expected): + raw = path.read_bytes() + assert sha256(raw).hexdigest() == expected, ('changed input',path.name) + return raw + + +def roles(event): + return event[1:3] if event[0] in ('ADD','COPY') else event[1:2] + + +def event_charts(event): + return event[2:4] if event[0] == 'MOVE' else [event[-1]] + + +def snapshots(word, marks, affected, eligible, frame, deadline): + """Read exact cut states backward, including the post-final cut.""" + public = word['public'] + frames = word['frames'] + tape = word['program'] + state = dict(enumerate(word['final'])) + selected = {} + target = min(marks) + + @cache + def span(chart): + vectors = {0} + for v in frames[chart]: + assert v not in vectors + vectors.update(x ^ v for x in tuple(vectors)) + return frozenset(vectors) + + visited = 0 + for cut in range(len(tape), target-1, -1): + if monotonic() >= deadline: + break + if cut in marks: + public_bank = sorted(r for r,f in state.items() if f == frame and r < public) + selected[cut] = dict(public_bank=public_bank, + owned_bank=sorted(r for r,f in state.items() if f == frame and r >= public), + pivots=sorted(eligible.intersection(public_bank)), + affected_charts={r:state.get(r) for r in sorted(affected)}) + if cut == target: + break + op, dest, *args = tape[cut-1] + visited += 1 + if op == 'MOVE': + old,new,owned = args + assert state[dest] == new and owned == (dest >= public) + assert span(old) < span(new) or owned and span(new) < span(old) + state[dest] = old + elif op == 'INIT': + assert dest >= public and state.pop(dest) == args[0] + elif op == 'CLEAR': + assert dest >= public and dest not in state + state[dest] = args[0] + else: + assert op in ('ADD','COPY','SCALE') and Fraction(args[-2]) + assert state[dest] == args[-1] + if op in ('ADD','COPY'): + assert args[0] != dest and state[args[0]] == args[-1] + assert op != 'COPY' or dest >= public + return selected, sorted(marks - selected.keys()), visited + + +def controls(): + word = dict(public=2, frames=[[],[1],[1,2]], initial=[0,1], final=[2,1], + program=[ + ['MOVE',0,0,1,False],['INIT',2,1],['COPY',2,0,'-1',1], + ['ADD',1,2,'2',1],['CLEAR',2,1],['MOVE',0,1,2,False]]) + found,missing,_=snapshots(word,{0,1,2,4,5,6},{0,1,2},{0},1,float('inf')) + assert not missing + assert found[0]['public_bank'] == [1] and not found[0]['pivots'] + assert found[1]['pivots'] == [0] and not found[1]['owned_bank'] + assert found[2]['owned_bank'] == found[4]['owned_bank'] == [2] + assert not found[5]['owned_bank'] and found[6]['public_bank'] == [1] + return ['literal_pre_post_move_cut','guarded_owned_lifetime','protected_public_pivot_filter'] + + +def audit(old, new, identity, deadline): + assert identity['status'] == 'PASS_INDEPENDENT_319_BLOCK' + lo,hi = identity['literal_candidate_clocks'] + assert (lo,hi) == (44588,44627) + affected = set(identity['roles']) + assert len(affected) == 14 and OLD_HELPER in affected + assert old['initial'] == new['initial'] and old['final'] == new['final'] + assert old['frames'] == new['frames'] and old['public'] == new['public'] + frames = new['frames'] + def span(chart): + vectors = {0} + for v in frames[chart]: + assert v not in vectors + vectors.update(x ^ v for x in tuple(vectors)) + return vectors + assert (len(frames[3]),len(frames[CHART]),len(frames[127])) == (0,8,9) + assert span(3) < span(CHART) < span(127) + + forbidden = PROTECTED | set(new['live']) | {r+112 for r in new['live']} + forbidden.update(new['hosted']['X2']+new['hosted']['Y2']) + cohort = {r for r in affected if r < new['public'] and + (new['initial'][r],new['final'][r]) == (3,127)} + eligible = cohort - forbidden + old_tape, new_tape = old['program'],new['program'] + old_body = identity['body_clocks'] + new_body = [t for t in range(lo,hi+1) + if new_tape[t][0] in ('ADD','SCALE') and new_tape[t][-1] == CHART] + assert len(old_body) == len(new_body) == 18 + assert set(r for t in old_body for r in roles(old_tape[t])) == affected + for before, after in zip(old_body,new_body,strict=True): + event = old_tape[before].copy() + assert event[0] in ('ADD','SCALE') and event[-1] == CHART + for k in (1,2) if event[0]=='ADD' else (1,): + if event[k] == OLD_HELPER: + event[k] = AUX + assert new_tape[after] == event + assert [new_tape[t] for t in range(lo,hi+1) if new_tape[t][0] in ('INIT','CLEAR')]==[ + ['INIT',AUX,CHART],['CLEAR',AUX,CHART]] + + old_move_clocks = [t for t in range(old_body[0],46309) + if old_tape[t][0]=='MOVE' and old_tape[t][1] in affected and + CHART in event_charts(old_tape[t])] + assert {43029,46308} <= set(old_move_clocks) + old_marks = {t+d for t in old_body+old_move_clocks+identity['window'] for d in (0,1)} + new_marks = set(range(lo,hi+2)) + reps = {lo,hi+1} + reps.update(t+1 for t in range(lo,hi+1) if CHART in event_charts(new_tape[t])) + old_views,old_missing,old_events = snapshots(old,old_marks,affected,eligible,CHART,deadline) + new_views,new_missing,new_events = snapshots(new,new_marks,affected|{AUX},eligible,CHART,deadline) + + alignment = [] + for old_clock,new_clock in zip(old_body,new_body,strict=True): + for offset in (0,1): + a,b = old_clock+offset,new_clock+offset + if a not in old_views or b not in new_views: + continue + old_pivots,new_pivots = old_views[a]['pivots'],new_views[b]['pivots'] + alignment.append(dict(old_clock=old_clock,new_clock=new_clock,side='before' if offset==0 else 'after', + old_pivots=old_pivots,new_pivots=new_pivots, + gained_pivots=sorted(set(new_pivots)-set(old_pivots)), + lost_pivots=sorted(set(old_pivots)-set(new_pivots)))) + raw_keys = [[cut,CHART,r] for cut in sorted(new_views) for r in new_views[cut]['pivots']] + rep_keys = [[cut,CHART,r] for cut in sorted(reps & new_views.keys()) for r in new_views[cut]['pivots']] + return dict( + old_literal_events=len(old_tape),new_literal_events=len(new_tape), + old_reverse_events=old_events,new_reverse_events=new_events, + cohort=sorted(cohort),eligible_affected=sorted(eligible),protected_roles=sorted(PROTECTED), + affected=sorted(affected),old_body=old_body,new_body=new_body,old_move_clocks=old_move_clocks, + old_snapshots=old_views,new_snapshots=new_views,alignment=alignment, + representative_cuts=sorted(reps),raw_key_count=len(raw_keys),representative_key_count=len(rep_keys), + representative_keys=rep_keys[:CAP],unvisited_keys=rep_keys[CAP:], + old_unvisited_cuts=old_missing,new_unvisited_cuts=new_missing, + new_pivot_roles=sorted({r for _,_,r in raw_keys}), + old_relevant_pivot_roles=sorted({r for v in old_views.values() for r in v['pivots']}), + aligned_gains=[r for r in alignment if r['gained_pivots']], + complete=not (old_missing or new_missing or len(rep_keys)>CAP)) + + +def main(): + p = ArgumentParser(description=__doc__) + p.add_argument('--inputs',type=Path) + p.add_argument('--price',type=Path) + p.add_argument('--price-sha') + p.add_argument('--controls-only',action='store_true') + args = p.parse_args() + checks=controls() + if args.controls_only: + print(dumps(checks)) + return + if not all((args.inputs,args.price,args.price_sha)): + p.error('exact old/new inputs and saved price required') + + def stop(*_): + raise TimeoutError('hard runner deadline') + + signal(SIGALRM,stop) + alarm(20) + deadline=monotonic()+17 + try: + assert args.price_sha == PRICE + quote = decode(pinned(args.price,PRICE)) + assert quote['head'] == HEAD and quote['inputs']['ADMITTED.json'] == ADMISSION + assert quote['productive_delta'] == {'1':17,'8':17,'9':-17} and not quote['paid_delta'] + assert sum(quote['paid'].values()) == 110519 and sum(quote['new_targets'].values()) == 22478 + assert 0 < Fraction(quote['new_margin'][0]) and Fraction(quote['margin_with_one_added_raw_rank_one_upper']) < 0 + data={name:pinned(args.inputs/name,digest) for name,digest in PINS.items()} + result=audit(decode(decompress(data['7314-WORD.json.gz'])), + decode(decompress(data['7334-WORD.json.gz'])),decode(data['IDENTITIES.json']),deadline) + finally: + alarm(0) + print(dumps(dict(comparator_head=HEAD,price_sha256=PRICE,input_sha256=PINS,controls=checks, + cut_convention='cut k immediately before event k; include post-block cut', + geometry_only=True,runner_cap=20,case_cap=CAP,**result),sort_keys=True,indent=2)) + + +if __name__ == '__main__': + assert __debug__ + main() diff --git a/research/p104-retimed-chart207-split-bound/inputs/7314-WORD.json.gz b/research/p104-retimed-chart207-split-bound/inputs/7314-WORD.json.gz new file mode 100644 index 0000000000..3939a3cc4c Binary files /dev/null and b/research/p104-retimed-chart207-split-bound/inputs/7314-WORD.json.gz differ diff --git a/research/p104-retimed-chart207-split-bound/inputs/7334-WORD.json.gz b/research/p104-retimed-chart207-split-bound/inputs/7334-WORD.json.gz new file mode 100644 index 0000000000..73f4300719 Binary files /dev/null and b/research/p104-retimed-chart207-split-bound/inputs/7334-WORD.json.gz differ diff --git a/research/p104-retimed-chart207-split-bound/inputs/IDENTITIES.json b/research/p104-retimed-chart207-split-bound/inputs/IDENTITIES.json new file mode 100644 index 0000000000..b1644106d9 --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/inputs/IDENTITIES.json @@ -0,0 +1,72 @@ +{ + "body_clocks": [ + 40222, + 40840, + 42609, + 43022, + 43023, + 43024, + 43025, + 43026, + 43028, + 43030, + 43403, + 43491, + 43535, + 43696, + 43698, + 43887, + 45365, + 45396 + ], + "copy_and_chart_local_ownership_checked": true, + "dirty_readout": { + "319": 1 + }, + "exact_basis_columns": 14, + "forward_direction": { + "1081": -1, + "1467": 1 + }, + "literal_candidate_clocks": [ + 44588, + 44627 + ], + "paid_delta_per_word": { + "1": -1, + "5": -1, + "6": 1 + }, + "ranks": [ + 3, + 8, + 9 + ], + "roles": [ + 198, + 205, + 319, + 532, + 652, + 654, + 962, + 969, + 1081, + 1250, + 1303, + 1305, + 1453, + 1467 + ], + "scope": "Local normalized rational block, literal chart availability and nesting. Absolute Gaussian phase and whole caller separate.", + "status": "PASS_INDEPENDENT_319_BLOCK", + "window": [ + 44616, + 45718 + ], + "word_sha256": [ + "0358b9f6e0340fb3e5aa46c747c558b32a5280cbf9cd92c3b9de627dd18a9a4f", + "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + ], + "wrong_sign_and_omitted_readout_rejected": true +} diff --git a/research/p104-retimed-chart207-split-bound/price/inputs/ADMITTED.json b/research/p104-retimed-chart207-split-bound/price/inputs/ADMITTED.json new file mode 100644 index 0000000000..464c89e45c --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/price/inputs/ADMITTED.json @@ -0,0 +1,58 @@ +{ + "assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "base": "e54523517d0f03e58352e647c403a5af3e525a57", + "caller": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "caller_sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "crossing": [ + "0.00364665195644044790699554028334161", + "0.00364665195644044790699554028334162" + ], + "end": "2026-11-11T23:04:43Z", + "exit": 0, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "hosted_at_admission": "plan and historical success; candidate replay in progress", + "inputs": { + "EARLY-RESULT.json": "ad1ca9b2e2febbf80d9bf8b6ceef14ff90fcc29ef9358310e551628eb1706649", + "INPUTS.json": "abedac59097a1c35c27d91cbdb07207bc562a64743bc406d13c94a8bc970592d", + "NATIVE-RESULT.json": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812", + "PROPOSED-CLAIM.json": "6e31241944c123d2bd4aa8bc94d833b44b3d889bd6d9aafc579108f416b45f03", + "RESULT.json": "7f2d587c59f063b01f1e8b320084a7f0943f2f05d65e3e0f5e80448c6c8e8194", + "SOURCES.json": "ac7b4473035af648d6073e78b6c39675e706e8194b346bb55ed62a0adc81d593", + "VERIFY.json": "ede7dd2dd3733b9a73f72af9dd7edfe819b49b859c5c76e227ec82cb9c220513", + "WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" + }, + "kappa": "0.00364665195644", + "ours": "0", + "peer_gain": "0.000000430519994", + "prior_kappa": "0.003646221436446", + "receipt": { + "peer-prep/IDENTITIES.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "peer-prep/STATIC.json": "500cc563b7dac8b1de1faf1dee9b820e73152dfddc15a650cd1191edd39e8c79", + "peer-price/RANK-STOCK.json": "4a7841699dd17688f6aada5c902a2a91e94558b2b1b4460c46b0e55aa95b3f9f", + "peer-price/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "peer/COMMAND.txt": "714bfab024155d8216f3ef99f3ee7627ddc35ab341c486ac6bd53c476b757130", + "peer/COMMIT.stdout": "597470d8132a3812deb3624a859546c0c13d52b094fd6fc61e7416941130bd70", + "peer/END-UTC.txt": "9c46923c616c14da5b8ed503e1652021d7bd409a10ec91a78a03263013fba08a", + "peer/METADATA.stdout": "5873404cb4424dca918a00d503569f3c29a3190fd029a007e1afb2006399f647", + "peer/RUN.exit": "9a271f2a916b0b6ee6cecb2426f0b3206ef074578be55d9bc94f6f3fe3ab86aa", + "peer/RUN.stderr": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "peer/RUN.stdout": "d589626c7581fbb9928bc615364cfee49deb62dfc0a39a903417ca62be89cf8c", + "peer/START-UTC.txt": "5b78fd6d42a2b42206891318c08e6014de57d7ca46b0201cd11a166f452210f7" + }, + "source_history": "exact anchored base and recursive package provenance, sparse shallow stock wrapper not executed", + "stages": { + "caller": "PASS_HELPER_319_FUSED_CALLER 91166298911/25000000000000", + "early": "PASS_HELPER_319_EXACT_NATIVE_AND_SIGNED_PRICE 0.00364665195644", + "frontier": "PASS_HELPER_319_FUSED_FRONTIER_PROPOSAL 91166298911/25000000000000", + "native": "PASS_HELPER_319_FUSED_NATIVE 3646017316711/1000000000000000" + }, + "start": "2026-11-11T22:54:48Z", + "status": "independently_reproduced_comparable", + "tree": "fa98712a459b20c10240450097c87de433f8a750" +} diff --git a/research/p104-retimed-chart207-split-bound/price/inputs/PR7338-SHA256.json b/research/p104-retimed-chart207-split-bound/price/inputs/PR7338-SHA256.json new file mode 100644 index 0000000000..8a4d2a0cf3 --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/price/inputs/PR7338-SHA256.json @@ -0,0 +1,19 @@ +{ + "BANK-INDEPENDENT.json": "16563e927ec1c1ec783f92862fe4b8027e8daab35ba80b1607e10c26c3bc28ee", + "BANK.json": "ac659b807f526dfb79f9bb173c3861bc743f112a7f40bc42a8b5dc57f48a058d", + "GEOMETRY-68.json": "ce9604444161b3532d02eb788cb3a24fbbdaf4c1354d596ac08a2c9edeb72c76", + "GEOMETRY-69.json": "a2dd10737f5bfbd3818e6766df3890e445fd46f661af9521f5d724b7c56c1d45", + "GEOMETRY-CONTROL.json": "df4175b6cee565ba0792a3207dee5ebd1c31868a441a276de68bf75536a089d6", + "RANK-STOCK.json": "4a7841699dd17688f6aada5c902a2a91e94558b2b1b4460c46b0e55aa95b3f9f", + "READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "RELAXED-COMPARE.json": "23b9a5c0e5507db1bdc2cd39fc7422216bf68b0dd0dbc1e78d315ae25dfe4926", + "RELAXED-INDEPENDENT.json": "dc227ae7aca5f470f148db76a32304ed21c6d4143af3a1d0e7cfd6947856edfb", + "RELAXED.json": "34738b6d9031b3170a58f0cb590d81c01ea2c1038810008483d1c24dc7574150", + "RETIME-KNOWN.json": "08402221016a0a7ed0b2716b3ab1c8de4afcf54158c381ca441320b71b8abac4", + "RETIME-SYNTHETIC.json": "fe9e20a455b87fc43843b221ac061652d2fd2af2c11de2e7b3c9323cc0e883fe", + "STRICT-68.json": "471d5c8f1cb87e1c054b6ea376f4f083f9bac76eabc5823811484f0ed30357b3", + "STRICT-69.json": "bd4c2284ec073e8c3e565350e868595d09098f7ab8347eef440343964f6dbac5", + "STRICT-COMPARE-69.json": "f6538af89286b5e3805f6ed4494e2df095ce62d114c814ae7cdfe820a655a08c", + "STRICT-INDEPENDENT-68.json": "3d9ec5a87d71bc1f669ea8d02591b3fa2d4db282bfc47d3af72335cd57e42587", + "STRICT-INDEPENDENT-69.json": "1eddd0476a4caff1ef6423458f88471f1ce07adcd119171714c9261f8d9d7387" +} diff --git a/research/p104-retimed-chart207-split-bound/price/inputs/RANK-STOCK.json b/research/p104-retimed-chart207-split-bound/price/inputs/RANK-STOCK.json new file mode 100644 index 0000000000..7043a8a985 --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/price/inputs/RANK-STOCK.json @@ -0,0 +1,538 @@ +{ + "admission": "scientific admission pending at preflight; price is conditional on exact #7334 passing", + "complete_targets": { + "1": 306, + "2": 357, + "3": 799, + "4": 3825, + "5": 1360, + "6": 731, + "7": 323, + "8": 544, + "9": 10888, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208, + "137": 208 + }, + "crossing_upper": "182332597822022395349777014167081/50000000000000000000000000000000000", + "disjoint_move_pair_count_upper": 3116, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "input_sha256": { + "READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "dependencies/7298/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "dependencies/round41/RESULT.json": "1b993aa8c66ffce5d2d9f13cafae320c62230722d599d251fa61afc6534b1bc7", + "receipts/NATIVE-RESULT.json": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812", + "receipts/construct.py": "ecb39578063d7f09153a85370a3b9bb7cbf8b36ff9891033a1cce7a2fe7f7fda" + }, + "old_complete_paid": { + "1": 68384, + "2": 14501, + "3": 14093, + "4": 3791, + "5": 5865, + "6": 238, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "old_margin": [ + "-29866980917152322049/10000000000000000000000000000000000000000000000000", + "-29866980917152266101/10000000000000000000000000000000000000000000000000" + ], + "one_edit_optimistic_upper": "1903560515893109741953230020081417399578277511361/5000000000000000000000000000000000000000000000000", + "one_per_public_helper_optimistic_upper": "2095820127998313825890506252109640556935683540008461/5000000000000000000000000000000000000000000000000", + "owned_paid_histogram": { + "1": 20, + "2": 9, + "3": 2, + "4": 13, + "5": 2, + "6": 1 + }, + "public_helper_count": 1101, + "public_paid_histogram": { + "1": 3980, + "2": 844, + "3": 827, + "4": 210, + "5": 343, + "6": 13, + "7": 10, + "8": 5 + }, + "public_paid_moves": 6232, + "rank_prices": { + "1+1": { + "complete_margin": [ + "858321385403521186417773068772405712363430437203/10000000000000000000000000000000000000000000000000", + "53645086587720074151110816798275357022714405823/625000000000000000000000000000000000000000000000" + ], + "credit": [ + "214580346350880296604443267200568173320145689813/2500000000000000000000000000000000000000000000000", + "858321385403521186417773068802272693280582759269/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-9141678614596478813582226931227594287636569562797/10000000000000000000000000000000000000000000000000", + "-571354913412279925848889183201724642977285594177/625000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -34, + "2": 17 + }, + "ranks": [ + 1, + 1 + ] + }, + "1+2": { + "complete_margin": [ + "1180782193580878473879905453225185303784278217059/10000000000000000000000000000000000000000000000000", + "1180782193580878473879905453225185303784278273007/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1180782193580878473879905453255052284701430539091/10000000000000000000000000000000000000000000000000", + "9446257548647027791039243626040418277611444313/80000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-8819217806419121526120094546774814696215721782941/10000000000000000000000000000000000000000000000000", + "-8819217806419121526120094546774814696215721726993/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "2": -17, + "3": 17 + }, + "ranks": [ + 1, + 2 + ] + }, + "1+3": { + "complete_margin": [ + "1389848341449443791535950684381027395734536124509/10000000000000000000000000000000000000000000000000", + "1389848341449443791535950684381027395734536180423/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "347462085362360947883987671102723594162922111631/2500000000000000000000000000000000000000000000000", + "694924170724721895767975342205447188325844223279/5000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-8610151658550556208464049315618972604265463875491/10000000000000000000000000000000000000000000000000", + "-8610151658550556208464049315618972604265463819577/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "3": -17, + "4": 17 + }, + "ranks": [ + 1, + 3 + ] + }, + "1+4": { + "complete_margin": [ + "193142263828747485141280111129765972731137687109/1250000000000000000000000000000000000000000000000", + "772569055314989940565120444519063890924550776427/5000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1545138110629979881130240889067994762766253818921/10000000000000000000000000000000000000000000000000", + "309027622125995976226048177813598952553250763791/2000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-1056857736171252514858719888870234027268862312891/1250000000000000000000000000000000000000000000000", + "-4227430944685010059434879555480936109075449223573/5000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "4": -17, + "5": 17 + }, + "ranks": [ + 1, + 4 + ] + }, + "1+5": { + "complete_margin": [ + "834392976237489866662283238867233696199702541757/5000000000000000000000000000000000000000000000000", + "417196488118744933331141619433616848099851284857/2500000000000000000000000000000000000000000000000" + ], + "credit": [ + "1668785952474979733324566477764334373316557405529/10000000000000000000000000000000000000000000000000", + "1668785952474979733324566477764334373316557405563/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-4165607023762510133337716761132766303800297458243/5000000000000000000000000000000000000000000000000", + "-2082803511881255066668858380566383151900148715143/2500000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "5": -17, + "6": 17 + }, + "ranks": [ + 1, + 5 + ] + }, + "1+6": { + "complete_margin": [ + "1771542005129348740048881099908835681263784441249/10000000000000000000000000000000000000000000000000", + "1771542005129348740048881099908835681263784497197/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1771542005129348740048881099938702662180936763281/10000000000000000000000000000000000000000000000000", + "354308401025869748009776219987740532436187352663/2000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-8228457994870651259951118900091164318736215558751/10000000000000000000000000000000000000000000000000", + "-8228457994870651259951118900091164318736215502803/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "6": -17, + "7": 17 + }, + "ranks": [ + 1, + 6 + ] + }, + "1+7": { + "complete_margin": [ + "1859458789326391366180127207106590253932358169757/10000000000000000000000000000000000000000000000000", + "1859458789326391366180127207106590253932358225739/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "929729394663195683090063603568228617424755245903/5000000000000000000000000000000000000000000000000", + "5810808716644973019312897522301428858904720287/31250000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-8140541210673608633819872792893409746067641830243/10000000000000000000000000000000000000000000000000", + "-8140541210673608633819872792893409746067641774261/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "7": -17, + "8": 17 + }, + "ranks": [ + 1, + 7 + ] + }, + "1+8": { + "complete_margin": [ + "1936286205289343096186514461761692902526099784907/10000000000000000000000000000000000000000000000000", + "1936286205289343096186514461761692902526099840821/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "968143102644671548093257230895779941721626053461/5000000000000000000000000000000000000000000000000", + "484071551322335774046628615447889970860813026739/2500000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-8063713794710656903813485538238307097473900215093/10000000000000000000000000000000000000000000000000", + "-8063713794710656903813485538238307097473900159179/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "8": -17, + "9": 17 + }, + "ranks": [ + 1, + 8 + ] + }, + "2+2": { + "complete_margin": [ + "342461829925360215799616613766761397431076780873/2000000000000000000000000000000000000000000000000", + "856154574813400539499041534416903493577691980131/5000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1712309149626801078998083068863673968072536226363/10000000000000000000000000000000000000000000000000", + "856154574813400539499041534431836984036268113207/5000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-1657538170074639784200383386233238602568923219127/2000000000000000000000000000000000000000000000000", + "-4143845425186599460500958465583096506422308019869/5000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -34, + "4": 17 + }, + "ranks": [ + 2, + 2 + ] + }, + "2+3": { + "complete_margin": [ + "1038332533337951243124209252323374732610103592089/5000000000000000000000000000000000000000000000000", + "2076665066675902486248418504646749465220207240109/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "2076665066675902486248418504676616446137359506193/10000000000000000000000000000000000000000000000000", + "519166266668975621562104626169154111534339876561/2500000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-3961667466662048756875790747676625267389896407911/5000000000000000000000000000000000000000000000000", + "-7923334933324097513751581495353250534779792759891/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -17, + "3": -17, + "5": 17 + }, + "ranks": [ + 2, + 3 + ] + }, + "2+4": { + "complete_margin": [ + "2355602677701438428037034298000189461885076143183/10000000000000000000000000000000000000000000000000", + "1177801338850719214018517149000094730942538099557/5000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1177801338850719214018517149015028221401114232599/5000000000000000000000000000000000000000000000000", + "2355602677701438428037034298030056442802228465249/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-7644397322298561571962965701999810538114923856817/10000000000000000000000000000000000000000000000000", + "-3822198661149280785981482850999905269057461900443/5000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -17, + "4": -17, + "6": 17 + }, + "ranks": [ + 2, + 4 + ] + }, + "2+5": { + "complete_margin": [ + "64550164305020182173891862721772434032493977189/250000000000000000000000000000000000000000000000", + "2582006572200807286955674508870897361299759143457/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1291003286100403643477837254450382171108455704779/5000000000000000000000000000000000000000000000000", + "2582006572200807286955674508900764342216911409609/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-185449835694979817826108137278227565967506022811/250000000000000000000000000000000000000000000000", + "-7417993427799192713044325491129102638700240856543/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -17, + "5": -17, + "7": 17 + }, + "ranks": [ + 2, + 5 + ] + }, + "2+6": { + "complete_margin": [ + "2772679409052218919811235238243020222832712173803/10000000000000000000000000000000000000000000000000", + "346584926131527364976404404780377527854089028721/1250000000000000000000000000000000000000000000000" + ], + "credit": [ + "554535881810443783962247047654577440749972899167/2000000000000000000000000000000000000000000000000", + "1386339704526109459905617619136443601874932247943/5000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-7227320590947781080188764761756979777167287826197/10000000000000000000000000000000000000000000000000", + "-903415073868472635023595595219622472145910971279/1250000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -17, + "6": -17, + "8": 17 + }, + "ranks": [ + 2, + 6 + ] + }, + "2+7": { + "complete_margin": [ + "2937423609212213275948868600095877444095027517461/10000000000000000000000000000000000000000000000000", + "183588975575763329746804287505992340255939223337/625000000000000000000000000000000000000000000000" + ], + "credit": [ + "734355902303053318987217150031436106253044959869/2500000000000000000000000000000000000000000000000", + "2937423609212213275948868600125744425012179839527/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-7062576390787786724051131399904122555904972482539/10000000000000000000000000000000000000000000000000", + "-441411024424236670253195712494007659744060776663/625000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -17, + "7": -17, + "9": 17 + }, + "ranks": [ + 2, + 7 + ] + }, + "3+3": { + "complete_margin": [ + "2564668825570003745693079529156031553835334050633/10000000000000000000000000000000000000000000000000", + "256466882557000374569307952915603155383533410653/1000000000000000000000000000000000000000000000000" + ], + "credit": [ + "2564668825570003745693079529185898534752486372631/10000000000000000000000000000000000000000000000000", + "1282334412785001872846539764592949267376243186341/5000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-7435331174429996254306920470843968446164665949367/10000000000000000000000000000000000000000000000000", + "-743533117442999625430692047084396844616466589347/1000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "3": -34, + "6": 17 + }, + "ranks": [ + 3, + 3 + ] + }, + "3+4": { + "complete_margin": [ + "2946362489249908694206009944683839839364582367373/10000000000000000000000000000000000000000000000000", + "368295311156238586775751243085479979920572802913/1250000000000000000000000000000000000000000000000" + ], + "credit": [ + "736590622312477173551502486178426705070433672347/2500000000000000000000000000000000000000000000000", + "2946362489249908694206009944713706820281734689439/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-7053637510750091305793990055316160160635417632627/10000000000000000000000000000000000000000000000000", + "-881704688843761413224248756914520020079427197087/1250000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "3": -17, + "4": -17, + "7": 17 + }, + "ranks": [ + 3, + 4 + ] + }, + "3+5": { + "complete_margin": [ + "1630341583973160089627948131376151155723919520129/5000000000000000000000000000000000000000000000000", + "3260683167946320179255896262752302311447839096189/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "3260683167946320179255896262782169292364991362273/10000000000000000000000000000000000000000000000000", + "815170791986580044813974065695542323091247840581/2500000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-3369658416026839910372051868623848844276080479871/5000000000000000000000000000000000000000000000000", + "-6739316832053679820744103737247697688552160903811/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "3": -17, + "5": -17, + "8": 17 + }, + "ranks": [ + 3, + 5 + ] + }, + "3+6": { + "complete_margin": [ + "3528183420760683542117844246779527821574533741651/10000000000000000000000000000000000000000000000000", + "1764091710380341771058922123389763910787266898791/5000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1764091710380341771058922123404697401245843031833/5000000000000000000000000000000000000000000000000", + "3528183420760683542117844246809394802491686063717/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-6471816579239316457882155753220472178425466258349/10000000000000000000000000000000000000000000000000", + "-3235908289619658228941077876610236089212733101209/5000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "3": -17, + "6": -17, + "9": 17 + }, + "ranks": [ + 3, + 6 + ] + }, + "4+4": { + "complete_margin": [ + "3415972937126856268850186467409402697562404412621/10000000000000000000000000000000000000000000000000", + "170798646856342813442509323370470134878120223431/500000000000000000000000000000000000000000000000" + ], + "credit": [ + "341597293712685626885018646743926967847955673467/1000000000000000000000000000000000000000000000000", + "3415972937126856268850186467439269678479556734721/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-6584027062873143731149813532590597302437595587379/10000000000000000000000000000000000000000000000000", + "-329201353143657186557490676629529865121879776569/500000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "4": -34, + "8": 17 + }, + "ranks": [ + 4, + 4 + ] + }, + "4+5": { + "complete_margin": [ + "237945064486638717744153752508310488639962668791/625000000000000000000000000000000000000000000000", + "3807121031786219483906460040132967818239402756587/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "3807121031786219483906460040162834799156555022671/10000000000000000000000000000000000000000000000000", + "1903560515893109741953230020081417399578277511361/5000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-387054935513361282255846247491689511360037331209/625000000000000000000000000000000000000000000000", + "-6192878968213780516093539959867032181760597243413/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "4": -17, + "5": -17, + "9": 17 + }, + "ranks": [ + 4, + 5 + ] + } + }, + "scope": "Predecode price only. Pair arithmetic grants all ordinary and physical costs free; each original paid MOVE contributes at most once.", + "whole_move_capacity_optimistic_upper": "477927259198812997685714233883646598515886014070727/625000000000000000000000000000000000000000000000", + "word_git_blob": "73f43007192eb5a38eb5abb591b871df3e52c7cd" +} diff --git a/research/p104-retimed-chart207-split-bound/price/inputs/pricing.py b/research/p104-retimed-chart207-split-bound/price/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/price/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-retimed-chart207-split-bound/price/quote.py b/research/p104-retimed-chart207-split-bound/price/quote.py new file mode 100644 index 0000000000..b6551954a4 --- /dev/null +++ b/research/p104-retimed-chart207-split-bound/price/quote.py @@ -0,0 +1,46 @@ +"""Complete fixed-paid rank-nine to rank-eight plus rank-one handoff quote.""" +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +import json +from pathlib import Path +import runpy + +PINS={ + "ADMITTED.json":"c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "RANK-STOCK.json":"4a7841699dd17688f6aada5c902a2a91e94558b2b1b4460c46b0e55aa95b3f9f", + "pricing.py":"f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", +} +ROOT=Path(__file__).resolve().parent/"inputs" +raw={} +for name,digest in PINS.items(): + data=(ROOT/name).read_bytes() + if sha256(data).hexdigest()!=digest: + raise ValueError("changed pinned input: "+name) + raw[name]=data +base=json.loads(raw["RANK-STOCK.json"]) +admit=json.loads(raw["ADMITTED.json"]) +assert base["head"]==admit["head"]=="aaeec8c0acf01e99a5f331ef363a698d9c084ace" +assert admit["exit"]==0 and admit["status"]=="independently_reproduced_comparable" +k=Fraction(base["crossing_upper"]) +assert k==Fraction(admit["crossing"][1]) +paid, targets = (Counter({int(r):v for r,v in base[key].items()}) + for key in ("old_complete_paid","complete_targets")) +new=targets.copy() +delta={1:17,8:17,9:-17} +new.update(delta) +pre,post=targets.copy(),new.copy() +pre.subtract(paid) +post.subtract(paid) +assert sum(paid.values())==110519 and sum(targets.values())==22461 and sum(new.values())==22478 +assert sum(r*v for r,v in pre.items())==sum(r*v for r,v in post.items())==1424 +cost=runpy.run_path(str(ROOT/"pricing.py"))["cost"] +old_margin,new_margin,credit=(cost(x,k) for x in (pre,post,delta)) +assert old_margin[1]<0