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-owned-add-source-span-bound/LOCAL-PINS.json b/research/p104-owned-add-source-span-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..cfd03973cb --- /dev/null +++ b/research/p104-owned-add-source-span-bound/LOCAL-PINS.json @@ -0,0 +1,17 @@ +{ + "engines/forward.py": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "engines/quote.py": "dfe84971057c11b3d9e2d9e2b10405e325453264ff83a5ab32c3c31b8f02a6fb", + "engines/reverse.py": "f8b48f2ed99d003e20f5b3fb2270603c4edbc3ce9a01484102816aa2710ce9ff", + "inputs/7113-CALLER.json.gz": "7e8038559cd158f6e32ef6d1a3bf15ab6a8ecc2239af32ab1699511ac28e26d9", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/R82-CONTACTS.json": "664c3824078877c6b9e6ace20d8b03202a250e67e0f09b66a7304ce1ab8a5d00", + "inputs/R82-PRICE.json": "82baf8740dfc695d304602d92bd3888961c965f76a5bcb4784cbd4f9726e7ee6", + "inputs/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "receipts/COMPARE.json": "86a49fe8ea6a5049621dcb2c90df3b55a2f48d82681ceefae6eda51c66665092", + "receipts/FORWARD.json.gz": "b4ecc7135594958bc22a3a01aa9d083f5091831b82f383b8bca538a2c8a94184", + "receipts/PRICE.json": "c9166ff18194a7e69f91a06f76329a2ff838bb65b08c4ed7a5a06038fdfa966d", + "receipts/REVERSE.json.gz": "eafded39baff4bf2aea555c7e72ee77d5f930c95ccc666c60478b18aac2de259", + "receipts/SHA256.json": "7ba1d4854aa6ab8bfd97973e591a16bfea4174cdc72e07541778de089efa6693" +} diff --git a/research/p104-owned-add-source-span-bound/NOTICE b/research/p104-owned-add-source-span-bound/NOTICE new file mode 100644 index 0000000000..9ba6144a0c --- /dev/null +++ b/research/p104-owned-add-source-span-bound/NOTICE @@ -0,0 +1,7 @@ +Apache-2.0. + +#7334 supplies the native word and complete comparator. #7113 supplies +the signed caller and frame contract. #7298 supplies directed arithmetic. +#7354 supplies the three windows and exact +price inputs. #7308 and #7312 supply adjacent donor and retiming scopes. +OpenAI Codex and subagents materially assisted. diff --git a/research/p104-owned-add-source-span-bound/PROOF.md b/research/p104-owned-add-source-span-bound/PROOF.md new file mode 100644 index 0000000000..b24f083730 --- /dev/null +++ b/research/p104-owned-add-source-span-bound/PROOF.md @@ -0,0 +1,13 @@ +# Exact source-span obstruction + +For each chart U let `T_U` denote the retained exact frame operator on the full factor, including spectators. A field in chart U has normalized value `T_U⁻¹x`. A signed MOVE applies the exact frame quotient, so its normalized row is unchanged. Cocharted ADD and SCALE act by their literal scalar coefficients on normalized rows. INIT creates a zero owned row, fresh COPY writes the source multiple, and CLEAR ends the owned lifetime. Starting from all 1,501 independently arbitrary full public inputs, the normalized rows are linear forms in those 1,501 independent inputs. The coefficients identify equality on arbitrary inputs. This uses the exact signed frame premise, including absolute phase. It does not approximate or sample the physical field. + +For an owned destination r, fix the two consecutive MOVEs A→B→C and the sole interior contact r←r+γs in B. In the proposed monotone fusion r uses one MOVE A→C and stays in the chosen outer chart at the new ADD cut. The old source s and all other owners retain their itineraries and updates. Since r has no other interior incidence, removing or relocating its own write leaves the other live rows at the chosen cut unchanged. Use these original rows as the donor bank, excluding r and retaining each actual owned lifetime. Any same-chart donor combination realizing the original ADD must have normalized row equal to the original pre-ADD row of s. The nonzero scalar γ cancels from this necessary identity. Chart validity, full physical restoration and grid legality would be additional obligations after a support pass. + +The two exact replays derive the banks independently. The forward engine propagates sparse rational normalized rows and reduces from increasing pivots. The reverse engine first walks structure and live ownership without computing values, then propagates all requested linear forms backwards from their pre-event cuts. The backward rule for ADD carries the destination's coefficient to the source while retaining the destination coefficient, COPY additionally clears the destination coefficient, SCALE multiplies it, and INIT or CLEAR ends its propagation. The backward engine transposes the result into 69 distinct normalized rows and uses fraction-free reverse-pivot elimination. Its receipt records each row, the ordered bank and exact donor and augmented ranks. Both engines agree on every nonzero donor bank, source-row size, chart and rank. + +Twenty-four cuts have an exact donor column zero over the rationals with a nonzero target entry. The independent engine also verifies that the target entry has a nonzero residue modulo 65521, and all literal denominators are units modulo that prime. A modular span failure alone does not certify a rational exclusion. For the other nine cuts, the exact integer rank gap is one and an explicit rational covector separates the target. All nine are chart 529 exit cuts of owner 1532. The reverse pivot is coordinate 1307, and the covector evaluates to −2 on the target and zero on every donor. Seven cases have donor rank 13 and augmented rank 14. Two have ranks 12 and 13. The package evaluates every covector directly against all exact stored donor rows. + +The price fixes the entire 17-copy paid and productive histograms. One edit for each of the three nonoverlapping windows gives combined changes `P1−51, P4−17, P5−17, P6+34`. The paid position total would fall from 110,519 to 110,468, while 22,461 productive fields and rank surplus 1,424 stay fixed. The exact gross moment is `17(3H1 + H4 + H5 − 2H6)`, with `H_r = r^(1−κ)`. At the exact comparator raw crossing upper the directed bound is approximately 0.488271001558. Granting those edits independent compatibility makes this a price relaxation. The complete bound with one additional paid rank-one position is already negative. The three original ADD coefficients are 4, 1/4 and −4. The rational support gate is more permissive than the comparator's fixed 1125/F25 common native grid, which therefore does not create additional witnesses. Any successful physical edit would still have to prove the caller, signed arbitrary-input forward and adjoint actions, owned erasure, exact grid and physical tape costs. + +This exclusion covers one destination-owned window at a time, its 33 pinned typed cuts in total, the retained paid itineraries and the required original source row. It permits every live cocharted row except the moved owner, including live owned donors. Changed donor itineraries, a different chronology, compensation between interacting edits, multiple-ADD response maps or newly paid helpers are outside this scope. diff --git a/research/p104-owned-add-source-span-bound/PROVENANCE.json b/research/p104-owned-add-source-span-bound/PROVENANCE.json new file mode 100644 index 0000000000..d9590e4f21 --- /dev/null +++ b/research/p104-owned-add-source-span-bound/PROVENANCE.json @@ -0,0 +1,65 @@ +{ + "files": { + "inputs/7113-CALLER.json.gz": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "git_blob": "9451ceaf6e8e037894680b549f3ef41c21b260d7", + "path": "research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json", + "sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json", + "uncompress": true + }, + "inputs/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/CrocSwap/integer-mult-bounds/blob/aaeec8c0acf01e99a5f331ef363a698d9c084ace/research/p104-helper-319-fused-return/WORD.json.gz", + "uncompress": false + }, + "inputs/ADMITTED.json": { + "commit": "f92b4c999204e0437dc89359f87fc7be3ecdd12e", + "git_blob": "464c89e45c4eca230c099e8bac784a90200a5069", + "path": "research/p104-owned-move-chronology-bound/inputs/ADMITTED.json", + "scope": "Independent exact #7334 complete four-stage replay admission.", + "sha256": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/f92b4c999204e0437dc89359f87fc7be3ecdd12e/research/p104-owned-move-chronology-bound/inputs/ADMITTED.json", + "uncompress": false + }, + "inputs/R82-CONTACTS.json": { + "commit": "f92b4c999204e0437dc89359f87fc7be3ecdd12e", + "git_blob": "ca75bfa82d1d66965bba3f7bde30609329c4db8a", + "path": "research/p104-owned-move-chronology-bound/receipts/R82-FORWARD.json", + "scope": "Frozen R82 fixed-counterpart forward geometry receipt.", + "sha256": "664c3824078877c6b9e6ace20d8b03202a250e67e0f09b66a7304ce1ab8a5d00", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/f92b4c999204e0437dc89359f87fc7be3ecdd12e/research/p104-owned-move-chronology-bound/receipts/R82-FORWARD.json", + "uncompress": false + }, + "inputs/R82-PRICE.json": { + "commit": "f92b4c999204e0437dc89359f87fc7be3ecdd12e", + "git_blob": "ab817d4377e10dd96a31ba332222b20cd5532873", + "path": "research/p104-owned-move-chronology-bound/receipts/R82-PRICE.json", + "scope": "Frozen R82 directed complete price and contact-window receipt.", + "sha256": "82baf8740dfc695d304602d92bd3888961c965f76a5bcb4784cbd4f9726e7ee6", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/f92b4c999204e0437dc89359f87fc7be3ecdd12e/research/p104-owned-move-chronology-bound/receipts/R82-PRICE.json", + "uncompress": false + }, + "inputs/READBACK.json": { + "commit": "f92b4c999204e0437dc89359f87fc7be3ecdd12e", + "git_blob": "625b508eead24b4428253bd257620b7e775800c1", + "path": "research/p104-owned-move-chronology-bound/inputs/READBACK.json", + "scope": "Independent exact #7334 directed paid/productive price readback.", + "sha256": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/f92b4c999204e0437dc89359f87fc7be3ecdd12e/research/p104-owned-move-chronology-bound/inputs/READBACK.json", + "uncompress": false + }, + "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-owned-add-source-span-bound/README.md b/research/p104-owned-add-source-span-bound/README.md new file mode 100644 index 0000000000..377ae72e9d --- /dev/null +++ b/research/p104-owned-add-source-span-bound/README.md @@ -0,0 +1,27 @@ +# Same-chart donor spans for three owned ADDs + +**NO VERIFIED GAIN. Conditional κ change 0%.** All 33 proposed cuts for three destination-owned, single-ADD windows on exact #7334 fail the arbitrary-input source-span test. Twenty-four cuts have an absent donor coordinate. The other nine have an exact rational covector that annihilates every eligible donor and evaluates to −2 on the required source row. Both exact engines agree on every bank and rank. The 33-cut scope is exhausted with zero survivors and zero unresolved cases. + +## Comparator and complete price + +The independently reproduced comparator is [#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) at `aaeec8c0acf01e99a5f331ef363a698d9c084ace`, κ = 0.00364665195644, using the exact [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) signed 17-copy caller. In a proposed edit the moved owner stays live and fuses its two monotone MOVEs, with the ADD source replaced by a linear combination of other live roles in the chosen outer chart. The literal source's value and itinerary stay intact. + +The directed compatible gross relaxation is 0.488271001558 raw at the old crossing across the three distinct windows. It grants extra ordinary ADDs, setup, routing, ownership, restoration, tape and precision costs for free. One extra paid rank-one position defeats even that combined relaxation. The complete productive histogram stays fixed. No cut supports the local source identity, so the verified saving is zero. See [the exact price](receipts/PRICE.json) and [proof](PROOF.md). + +## Replay + +Use CPython 3.12 with assertions and the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-owned-add-source-span-bound +``` + +From the package directory or a Git-free export, use `python3.12 -I -B replay.py --out fresh-receipts`. The replay authenticates the exact signed caller and native word, reconstructs the complete price before native decoding, regenerates both exact support receipts, rechecks each separating witness against its ordered donor bank, and rejects changed input bytes. Paths, source references and verification coverage are in [PROVENANCE.json](PROVENANCE.json) and [VERIFICATION.md](VERIFICATION.md). The selected record stays unchanged. + +## Credit + +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) supplies the exact word and complete comparator, [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) the signed caller, and [#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) the directed tariff. [#7354](https://github.com/CrocSwap/integer-mult-bounds/pull/7354) at f92b4c999204e0437dc89359f87fc7be3ecdd12e supplies the three frozen windows and their price. [#7308](https://github.com/CrocSwap/integer-mult-bounds/pull/7308) at 2c777389ec0476e97ab141c645af01ff28a46aa6 tests the moved owner's row in its original destination bank at the original paid MOVE clock. This package tests the original ADD's read-only source row against a new cut and chart while retaining the moved owner. [#7312](https://github.com/CrocSwap/integer-mult-bounds/pull/7312) provides a related public counterpart retiming scope. OpenAI Codex and subagents materially assisted. + +## Open next questions + +Four same-lifetime monotone pairs have multiple intervening ADDs. Choose one exact ordered window, extract its joint external response, and price the necessary changed contract before attempting support. Interacting edits, moving a donor, changing the original counterpart's itinerary, and new paid helpers remain open. diff --git a/research/p104-owned-add-source-span-bound/SOURCES.json b/research/p104-owned-add-source-span-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-owned-add-source-span-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-owned-add-source-span-bound/TASK.json b/research/p104-owned-add-source-span-bound/TASK.json new file mode 100644 index 0000000000..877ea4fcc4 --- /dev/null +++ b/research/p104-owned-add-source-span-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Exact #7334 signed native word. At each of 33 frozen outer-chart cuts of three monotone destination-owned one-ADD windows, test the literal source row against all other live same-chart donor rows.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "Owned ADD source-span research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "A valid replacement source could remove one paid MOVE per native copy while keeping productive stock and the exact signed caller fixed.", + "budget_minutes": 5, + "evidence": "Forward exact rational and independent backward integer-covector replays agree on all 33 cuts and exact ranks. Twenty-four exterior-coordinate and nine exact dual exclusions. No unresolved key.", + "open_questions": [ + { + "blocked_by": "The tested three single-ADD owner windows have no exact same-chart replacement source under the retained routes.", + "first_step": "Pin one of the four ordered windows and price a changed response before testing exact source and destination rows.", + "question": "Can a multiple-ADD window preserve its complete response using existing paid routes?", + "why_it_matters": "Four original monotone owned pairs have more than one intervening ADD." + } + ], + "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": "Extends the fixed-counterpart owned MOVE chronology to arbitrary combinations of retained same-chart donors on three exact windows.", + "scope_status": "changed", + "stop_rule": "Exactly 33 pinned pre-event cut keys per engine or its bounded 20-second runner. Build at most one exact survivor after a positive complete bill.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-owned-add-source-span-bound/VERIFICATION.md b/research/p104-owned-add-source-span-bound/VERIFICATION.md new file mode 100644 index 0000000000..186d482373 --- /dev/null +++ b/research/p104-owned-add-source-span-bound/VERIFICATION.md @@ -0,0 +1,9 @@ +# Verification receipts + +Both original scoped runs completed locally under CPython 3.12 with assertions. The forward rational replay visited all 33 cuts. The independent final backward replay took 0.29 seconds and produced all 69 exact rows, ranks and covectors. Its relocated rerun took 0.19 seconds and matched the final receipt byte for byte. An initial independent invocation failed before support because it omitted the result accumulator; the corrected invocation exhausted the exact same frozen keys. No candidate build, changed-native replay, or selected historical replay was triggered. + +The package freezes the complete quote and both exact support receipts by SHA-256 over their JSON payloads. The runner regenerates them and recomputes all separation evaluations. It also checks planted multi-source and signed owned COPY fixtures, changed donor and exact dependent-bank cases, and rejects both a changed price byte and a changed compressed native word before their respective use. The comparator's separate four-stage complete local admission and exact hosted checks passed. [Exact #7334 workflow](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/43114736518) + +The package is a clean replay of the 33-cut necessary support screen. The official committed export, publication commit transport and hosted checks for this contribution are separate. + +The original lead replay took 3.39 seconds. The package direct replay passed in 3.99 seconds. The local registered replay passed in 7.65 seconds and the staged Git-free replay in 7.07 seconds when those two checks ran concurrently. Their output includes the exact comparison over all 33 keys, donor banks and ranks. The archived Git-free copy emitted all four receipt files byte for byte. The frozen predecessor geometry, price, independent admission and price readback match the four published Git blobs on exact #7354. diff --git a/research/p104-owned-add-source-span-bound/VERIFY.json b/research/p104-owned-add-source-span-bound/VERIFY.json new file mode 100644 index 0000000000..64ba0fb30a --- /dev/null +++ b/research/p104-owned-add-source-span-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Regenerate complete predecode price, both 33-cut engines and every exact row and witness; verify all donor/augmented ranks and rejecting corrupted inputs.", + "timeout_seconds": 75 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-owned-add-source-span-bound/engines/forward.py b/research/p104-owned-add-source-span-bound/engines/forward.py new file mode 100644 index 0000000000..46e4621b69 --- /dev/null +++ b/research/p104-owned-add-source-span-bound/engines/forward.py @@ -0,0 +1,169 @@ +"""Match the literal ADD source using other live rows in the retimed chart.""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +import sys +from time import monotonic + +HEAD="aaeec8c0acf01e99a5f331ef363a698d9c084ace" +WORD="4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PRICE="c9166ff18194a7e69f91a06f76329a2ff838bb65b08c4ed7a5a06038fdfa966d" + + +def checked(path,want,compressed=False): + raw=path.read_bytes() + if sha256(raw).hexdigest()!=want: + raise ValueError(f"changed dependency: {path.name}") + return json.loads(decompress(raw) if compressed else raw) + + +@cache +def scalar(x): + return Q(x) + + +def axpy(dst,src,c): + for k,a in src.items(): + value=dst.get(k,0)+c*a + if value: + dst[k]=value + else: + dst.pop(k,None) + + +def reduce_row(row,basis,weights,multiplier): + for k,(v,w) in sorted(basis.items()): + a=row.get(k,0) + if a: + axpy(row,v,-a) + axpy(weights,w,multiplier*a) + + +def solve(target,bank,deadline): + basis={} + for role,vector in sorted(bank.items()): + if monotonic()>=deadline: + return None + r=vector.copy() + w={role:Q(1)} + reduce_row(r,basis,w,-1) + if r: + k=min(r) + d=r[k] + basis[k]=({i:a/d for i,a in r.items()},{i:a/d for i,a in w.items()}) + residual=target.copy() + weights={} + reduce_row(residual,basis,weights,1) + rebuilt={} + for role,a in weights.items(): + axpy(rebuilt,bank[role],a) + axpy(rebuilt,residual,Q(1)) + assert rebuilt==target + return dict(rank=len(basis), residual={i:str(v) for i,v in residual.items()}, + matching_coefficients={i:str(v) for i,v in weights.items()} if not residual else None) + + +def snapshot(word,requested,targets,deadline): + public=word["public"] + active=word["initial"]+[None]*word["owned_fields"] + rows=[{i:Q(1)} for i in range(public)]+[None]*word["owned_fields"] + banks,values={},{} + stop=max(requested.keys()|targets.keys()) + for t,e in enumerate(word["program"]): + if t%64==0 and monotonic()>=deadline: + break + for chart,r in requested.get(t,()): + banks[t,chart,r]={i:rows[i].copy() for i in range(len(active)) if i!=r and active[i]==chart and rows[i]} + for s in targets.get(t,()): + assert active[s] is not None + values[t,s]=rows[s].copy() + if t==stop: + break + op,r,*args=e + if op=="MOVE": + assert active[r]==args[0] and args[2]==(r>=public) + active[r]=args[1] + elif op=="INIT": + assert active[r] is None and rows[r] is None and r>=public + active[r]=args[0] + rows[r]={} + elif op=="CLEAR": + assert active[r]==args[0] and rows[r] is not None and r>=public + active[r]=rows[r]=None + elif op=="SCALE": + assert active[r]==args[1] and scalar(args[0]) + rows[r]={i:v*scalar(args[0]) for i,v in rows[r].items()} + else: + s,k,chart=args + assert active[r]==active[s]==chart and r!=s and op in ("ADD","COPY") + if op=="COPY": + assert r>=public and not rows[r] + axpy(rows[r],rows[s],scalar(k)) + return banks,values + + +def controls(): + d=monotonic()+1 + a,b={0:Q(1),1:Q(1)},{1:Q(2)} + assert solve({0:Q(3)}, {7:a,8:b},d)["matching_coefficients"]=={7:"3",8:"-3/2"} + assert solve({2:Q(1)}, {7:a,8:b},d)["residual"]=={2:"1"} + assert solve({0:Q(3)}, {7:{0:Q(1),2:Q(1)},8:b},d)["residual"]=={2:"-3"} + assert solve({}, {7:a},d)["matching_coefficients"]=={} + return ["two-donor span","separating coordinate","changed donor row","zero source"] + + +def main(): + root=Path(sys.argv[1]) + price=checked(root/"price/PRICE.json",PRICE) + word=checked(root/"inputs/7334-WORD.json.gz",WORD,True) + assert price["head"]==HEAD and price["word_sha256"]==WORD + moves=word["program"] + req,targets=defaultdict(set),defaultdict(set) + bykey={} + for p in price["candidates"]: + r,s=p["owner"],p["peer"] + f,g=p["move_clocks"] + a,b,c=p["chart_path"] + t,add=p["literal_ADD"] + assert add[:2]==[r,s] and moves[t]==["ADD",*add] and f=deadline or (t,s) not in values or (cut,chart,r) not in banks: + pending.append(key) + continue + bank=banks[cut,chart,r] + source=values[t,s] + result=solve(source,bank,deadline) + if result is None: + pending.append(key) + continue + output.append(dict(key=key,source=[t,s],target_chart=chart,bank_roles=sorted(bank), + source_nnz=len(source),**result, + decision="exact span survivor" if result["matching_coefficients"] is not None else "outside donor span")) + print(json.dumps(dict(head=HEAD,price_sha256=PRICE,word_sha256=WORD,status="CAPPED" if pending else "EXHAUSTED", + case_cap=33,seconds_cap=18,controls=checks,counts=Counter(x["decision"] for x in output), + decisions=output,unvisited=pending,survivors=[x["key"] for x in output if x["matching_coefficients"] is not None]), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-owned-add-source-span-bound/engines/quote.py b/research/p104-owned-add-source-span-bound/engines/quote.py new file mode 100644 index 0000000000..fa9bd6969d --- /dev/null +++ b/research/p104-owned-add-source-span-bound/engines/quote.py @@ -0,0 +1,68 @@ +"""Full predecode price for replacing the source of one owned destination ADD.""" +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path + +ROOT=Path(__file__).resolve().parent +PINS={"inputs/R82-PRICE.json":"82baf8740dfc695d304602d92bd3888961c965f76a5bcb4784cbd4f9726e7ee6", + "inputs/R82-CONTACTS.json":"664c3824078877c6b9e6ace20d8b03202a250e67e0f09b66a7304ce1ab8a5d00", + "inputs/READBACK.json":"337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/pricing.py":"f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182"} + + +def integer_histogram(values): + return Counter({int(r):c for r,c in values.items()}) + + +def main(): + inputs={} + for key,want in PINS.items(): + payload=(ROOT/key).read_bytes() + if sha256(payload).hexdigest()!=want: + raise ValueError(f"changed dependency: {key}") + if key.endswith(".json"): + inputs[key]=loads(payload) + prev=inputs["inputs/R82-PRICE.json"] + contacts=inputs["inputs/R82-CONTACTS.json"] + old=inputs["inputs/READBACK.json"] + assert old["head"]==prev["head"]==contacts["head"] + assert contacts["status"]=="EXHAUSTED" and not contacts["survivors"] + group=[p for p in prev["candidates"] if p["owner_access"]=="destination"] + assert {p["owner"] for p in group}=={1501,1531,1532} + assert all(a["move_clocks"][1]0 + with_extra=signed.copy() + with_extra[1]-=1 + assert f(with_extra,upper)[1]<0 + interval=lambda x:[str(i) for i in x] + print(dumps(dict(head=old["head"],word_sha256=prev["word_sha256"],input_sha256=PINS, + case_cap=33,time_cap_seconds=20,build_cap=1,candidates=group,keys=keys, + gross_upper_all_three=interval(gross),complete_probe_margin=interval(changed), + extra_rank_one_upper=interval(f(with_extra,upper)),paid_all_three=dict(modified), + scope="Keep all fixed paid itineraries except fuse one destination-owned pair. Match its literal source value by exact existing same-chart donor rows. Optimistically free added ordinary work, no new paid operation. No word decoded."),indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-owned-add-source-span-bound/engines/reverse.py b/research/p104-owned-add-source-span-bound/engines/reverse.py new file mode 100644 index 0000000000..5efbeac87e --- /dev/null +++ b/research/p104-owned-add-source-span-bound/engines/reverse.py @@ -0,0 +1,393 @@ +"""Independent normalized reverse-contact and fraction-free donor-span gate.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from math import gcd, isqrt, lcm +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic + +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +WORD = "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PRICE = "c9166ff18194a7e69f91a06f76329a2ff838bb65b08c4ed7a5a06038fdfa966d" +PRIME = 65521 + + +def unique(pairs): + values = dict(pairs) + assert len(values) == len(pairs), "duplicate JSON key" + return values + + +def checked(path, pin, compressed=False): + raw = path.read_bytes() + if sha256(raw).hexdigest() != pin: + raise ValueError(f"changed input {path.name}") + return loads(decompress(raw) if compressed else raw, object_pairs_hook=unique) + + +@cache +def coefficient(raw): + q = Fraction(raw) + assert q and q.denominator % PRIME, "nonunit native denominator" + return q.numerator, q.denominator + + +def normalized(values, denominator): + if not values: + return {}, 1 + divisor = gcd(denominator, *values.values()) + if divisor != 1: + return {j: a // divisor for j, a in values.items()}, denominator // divisor + return values, denominator + + +def sum_scaled(first, second, factor): + a, da = first + b, db = second + numerator, denom = factor + if not b: + return first + common = lcm(da, db * denom) + out = {j: v * (common // da) for j, v in a.items()} + weight = numerator * (common // (db * denom)) + for j, v in b.items(): + val = out.get(j, 0) + weight * v + if val: + out[j] = val + else: + out.pop(j, None) + return normalized(out, common) + + +def incidence(e): + return e[1:3] if e[0] in ("ADD", "COPY") else e[1:2] + + +def candidates(word, quote): + n = word["public"] + tape = word["program"] + stock = {} + for case in quote["candidates"]: + owner = case["owner"] + left, right = case["move_clocks"] + a, middle, c = case["chart_path"] + original, entry = case["literal_ADD"] + assert case["owner_access"] == "destination" and entry[0] == owner + assert entry[1] == case["peer"] and entry[-1] == middle + assert tape[left] == ["MOVE", owner, a, middle, True] + assert tape[right] == ["MOVE", owner, middle, c, True] + assert tape[original] == ["ADD", *entry] + assert n <= owner and left < original < right + assert [i for i in range(left + 1, right) if owner in incidence(tape[i])] == [original] + assert case["cut_windows_pre_event"] == {"entrance": [left, right], "exit": [left + 1, right]} + stock[owner, left, right] = case + assert len(stock) == 3 and len({tuple(k) for k in quote["keys"]}) == quote["case_cap"] == 33 + return stock + + +def collect(word, cuts, observations, cap): + """Forward structural pass only. Assign one ID to each requested live value.""" + n = word["public"] + chart = list(word["initial"]) + [None] * word["owned_fields"] + revisions = [0] * len(chart) + fresh = set() + starts = {} + lifetimes = {} + requests = defaultdict(list) + observation_ids = {} + bank_ids = {} + value_id = {} + paid = Counter() + + @cache + def span(f): + vectors = {0} + for v in word["frames"][f]: + assert v not in vectors + vectors.update(v ^ t for t in tuple(vectors)) + return vectors + + def request(t, role): + assert chart[role] is not None + key = role, revisions[role] + if key not in value_id: + value_id[key] = len(value_id) + requests[t].append((role, value_id[key])) + return value_id[key] + + tape = word["program"] + for t in range(len(tape) + 1): + if t % 128 == 0 and monotonic() >= cap: + raise TimeoutError("literal structural scan") + for role in observations.get(t, ()): + observation_ids[t, role] = request(t, role) + for key, chart_id, exclude in cuts.get(t, ()): + bank_ids[key] = [(r, request(t, r)) for r, c in enumerate(chart) if c == chart_id and r != exclude] + if t == len(tape): + break + op, d, *args = tape[t] + assert 0 <= d < len(chart) + if op == "INIT": + assert d >= n and chart[d] is None + chart[d], starts[d] = args[0], t + fresh.add(d) + elif op == "CLEAR": + assert d >= n and chart[d] == args[0] and d in starts + lifetimes[d, starts.pop(d)] = t + chart[d] = None + fresh.discard(d) + elif op == "MOVE": + a, b, owned = args + assert chart[d] == a and owned == (d >= n) + assert span(a) < span(b) or owned and span(b) < span(a) + paid[abs(len(word["frames"][b]) - len(word["frames"][a]))] += 1 + chart[d] = b + fresh.discard(d) + continue + elif op == "SCALE": + assert chart[d] == args[-1] + coefficient(args[-2]) + fresh.discard(d) + else: + assert op in ("ADD", "COPY") + src, coeff, f = args + assert d != src and chart[d] == chart[src] == f + coefficient(coeff) + if op == "COPY": + assert d >= n and d in fresh + fresh.discard(d) + revisions[d] += 1 + assert not starts and chart == word["final"] + [None] * word["owned_fields"] + return requests, observation_ids, bank_ids, lifetimes, dict(paid), len(value_id) + + +def transpose_prefix(word, requests, count, cap): + """Propagate all requested output covectors backward, then transpose to input rows.""" + n = word["public"] + empty = ({}, 1) + adjoint = [empty] * (n + word["owned_fields"]) + tape = word["program"] + for t in range(max(requests), -1, -1): + if t % 128 == 0 and monotonic() >= cap: + raise TimeoutError("reverse normalized prefix") + op, d, *args = tape[t] + if op in ("INIT", "CLEAR"): + adjoint[d] = empty + elif op == "SCALE": + adjoint[d] = sum_scaled(empty, adjoint[d], coefficient(args[-2])) + elif op in ("ADD", "COPY"): + src = args[0] + adjoint[src] = sum_scaled(adjoint[src], adjoint[d], coefficient(args[-2])) + if op == "COPY": + adjoint[d] = empty + else: + assert op == "MOVE" + for r, output in requests.get(t, ()): + adjoint[r] = sum_scaled(adjoint[r], ({output: 1}, 1), (1, 1)) + assert not any(d for d, _ in adjoint[n:]) + by_output = [[] for _ in range(count)] + for coord, (coeffs, d) in enumerate(adjoint[:n]): + assert d % PRIME + for i, v in coeffs.items(): + by_output[i].append((coord, v, d)) + rows = [] + for entries in by_output: + common = lcm(*(d for _, _, d in entries)) + rows.append(normalized({i: v * (common // d) for i, v, d in entries}, common)) + return rows + + +def eliminate(v, basis, record=False): + """Reverse-pivot integer elimination. All leading pivots are exact.""" + v = v.copy() + reductions = [] + multiplier = 1 + while v: + k = max(v) + if k not in basis: + break + w = basis[k] + a, b = w[k], v[k] + d = gcd(a, b) + a, b = a // d, b // d + next_v = {j: a * x for j, x in v.items()} + for j, x in w.items(): + z = next_v.get(j, 0) - b * x + if z: + next_v[j] = z + else: + next_v.pop(j, None) + assert k not in next_v + g = gcd(*next_v.values()) or 1 + v = {j: x // g for j, x in next_v.items()} + if record: + reductions.append((k, Fraction(b, a) * multiplier)) + multiplier *= Fraction(g, a) + return v, reductions, multiplier + + +def dot(row, covector): + numerator, denominator = row + return sum((numerator.get(j, 0) * v for j, v in covector.items()), Fraction(0)) / denominator + + +def exact_span(bank, target): + t, dt = target + if not t: + return dict(status="exact_span", coefficients={}) + exterior = next((j for j in sorted(t) if all(j not in row for _, (row, _) in bank)), None) + basis = {} + histories = {} + for role, (v, d) in bank: + reduced, steps, scale = eliminate(v, basis, record=True) + if reduced: + pivot = max(reduced) + basis[pivot] = reduced + histories[pivot] = (role, d, steps, scale) + if exterior is not None: + residue = t[exterior] * pow(dt, -1, PRIME) % PRIME + return dict(status="absent_exterior_coordinate", donor_rank=len(basis), augmented_rank=len(basis)+1, + coordinate=exterior, target_coefficient=str(Fraction(t[exterior], dt)), + target_residue_mod_prime=residue) + residual, steps, scale = eliminate(t, basis, record=True) + if residual: + k = max(residual) + dual = {k: Fraction(1)} + for p, v in sorted(basis.items()): + coefficient = -sum((v.get(j, 0) * c for j, c in dual.items()), Fraction(0)) / v[p] + if coefficient: + dual[p] = coefficient + target_value = dot(target, dual) + assert target_value and all(dot(v, dual) == 0 for _, v in bank) + return dict(status="exact_rank_exclusion", donor_rank=len(basis), augmented_rank=len(basis) + 1, + missing_reverse_pivot=k, residual_integer_row=residual, + separating_covector={j: str(v) for j, v in dual.items()}, separated_target=str(target_value)) + pending = dict(steps) + solution = defaultdict(Fraction) + for pivot in sorted(basis): + if pivot not in pending: + continue + weight = pending.pop(pivot) + if not weight: + continue + role, denom, reductions, factor = histories[pivot] + weight /= factor + solution[role] += weight * denom / dt + for j, scalar in reductions: + pending[j] = pending.get(j, Fraction(0)) - weight * scalar + assert not pending + check = ({}, 1) + rows = dict(bank) + for r, x in solution.items(): + check = sum_scaled(check, rows[r], (x.numerator, x.denominator)) + assert check == target, (check, target) + return dict(status="exact_span", donor_rank=len(basis), + coefficients={r: str(x) for r, x in sorted(solution.items()) if x}) + + +def controls(): + toy = {"public": 4, "owned_fields": 1, "frames": [[]], "initial": [0] * 4, "final": [0] * 4, + "program": [["INIT", 4, 0], ["COPY", 4, 0, "1/2", 0], ["ADD", 4, 1, "-3", 0], + ["ADD", 0, 2, "2", 0], ["CLEAR", 4, 0]]} + req, ids, banks, _, _, count = collect(toy, {3:[((3,), 0, 4)], 4:[((4,), 0, 4)]}, {3:[4]}, float("inf")) + rows = transpose_prefix(toy, req, count, float("inf")) + target = rows[ids[3, 4]] + before = [(r, rows[i]) for r, i in banks[3,] if r in (0, 1)] + after = [(r, rows[i]) for r, i in banks[4,] if r in (0, 1)] + assert exact_span(before, target)["coefficients"] == {0:"1/2", 1:"-3"} + assert exact_span(after, target)["status"] == "exact_rank_exclusion" + assert exact_span(before[1:], target)["status"] == "absent_exterior_coordinate" + # Nontrivial exact dependency and reconstruction after a shared pivot. + multi = [(5, ({0: 3, 1: -1}, 2)), (6, ({0: 1, 1: 4}, 3)), (7, ({0: 11, 1: 2}, 1))] + hit = exact_span(multi, ({0: 11, 1: 2}, 1)) + assert hit["status"] == "exact_span" and len(hit["coefficients"]) == 2 + return ["signed_multi_source_and_owned_COPY", "intervening_write_blocks_span", "absent_exterior_coordinate", + "dependent_donor_bank_exact_reconstruction"] + + +def audit(word, quote, cap, decisions): + assert (word["public"], word["owned_fields"], len(word["program"])) == (1501, 68, 76466) + stock = candidates(word, quote) + observed = defaultdict(set) + cuts = defaultdict(list) + for row in quote["keys"]: + key = tuple(row) + owner, left, right, side, t = key + item = stock[owner, left, right] + chart = item["chart_path"][0 if side == "entrance" else 2] + assert item["cut_windows_pre_event"][side][0] <= t <= item["cut_windows_pre_event"][side][1] + cuts[t].append((key, chart, owner)) + observed[item["literal_ADD"][0]].add(item["peer"]) + requests, refs, banks, lifetimes, paid, count = collect(word, cuts, observed, cap) + assert paid == {1:4000, 2:853, 3:829, 4:223, 5:345, 6:14, 7:10, 8:5} + for item in stock.values(): + left, right = item["owner_lifetime"] + assert lifetimes[item["owner"], left] == right + rows = transpose_prefix(word, requests, count, cap) + for entry in quote["keys"]: + if monotonic() >= cap: + raise TimeoutError("exact donor bank gate") + owner, left, right, side, t = entry + item = stock[owner, left, right] + source = item["peer"] + target_id = refs[item["literal_ADD"][0], source] + target = rows[target_id] + bank = [(r, rows[i]) for r, i in banks[tuple(entry)]] + chart = item["chart_path"][0 if side == "entrance" else 2] + decision = exact_span(bank, target) + decisions.append(dict(key=entry, proposed_chart=chart, literal_read_peer=source, + literal_read_clock=item["literal_ADD"][0], donors=len(bank), owned_donors=sum(r>=word["public"] for r,_ in bank), + target_row_id=target_id, donor_role_row_ids=banks[tuple(entry)], + donor_rowset_sha256=sha256(dumps(bank, sort_keys=True).encode()).hexdigest(), **decision)) + return rows + + +def main(): + parser = ArgumentParser(description=__doc__) + parser.add_argument("--word", type=Path) + parser.add_argument("--price", type=Path) + parser.add_argument("--controls-only", action="store_true") + args = parser.parse_args() + if args.controls_only: + print(dumps(controls())) + return + assert args.word is not None and args.price is not None and __debug__ + start = monotonic() + def stop(*_): + raise TimeoutError("hard 20-second runner cap") + signal(SIGALRM, stop) + alarm(20) + decisions = [] + keys = [] + rows = None + tests = [] + timed_out = None + try: + tests = controls() + assert all(PRIME % d for d in range(2, isqrt(PRIME)+1)) + quote = checked(args.price, PRICE) + assert quote["head"] == HEAD and quote["word_sha256"] == WORD + keys = quote["keys"] + rows = audit(checked(args.word, WORD, compressed=True), quote, start+18, decisions) + except TimeoutError as error: + timed_out = str(error) + finally: + alarm(0) + result = dict(head=HEAD, word_sha256=WORD, price_sha256=PRICE, prime=PRIME, + case_cap=33, runner_cap_seconds=20, controls=tests, distinct_requested_rows=len(rows) if rows is not None else None, + requested_integer_rows=rows, + cases=decisions, disposition_counts=dict(Counter(r["status"] for r in decisions)), + unresolved=keys[len(decisions):], timeout=timed_out, + survivors=[r for r in decisions if r["status"] == "exact_span"]) + print(dumps(result, sort_keys=True, indent=2)) + if timed_out: + raise SystemExit(2) + + +if __name__ == "__main__": + main() diff --git a/research/p104-owned-add-source-span-bound/inputs/7113-CALLER.json.gz b/research/p104-owned-add-source-span-bound/inputs/7113-CALLER.json.gz new file mode 100644 index 0000000000..2479c3a615 Binary files /dev/null and b/research/p104-owned-add-source-span-bound/inputs/7113-CALLER.json.gz differ diff --git a/research/p104-owned-add-source-span-bound/inputs/7334-WORD.json.gz b/research/p104-owned-add-source-span-bound/inputs/7334-WORD.json.gz new file mode 100644 index 0000000000..73f4300719 Binary files /dev/null and b/research/p104-owned-add-source-span-bound/inputs/7334-WORD.json.gz differ diff --git a/research/p104-owned-add-source-span-bound/inputs/ADMITTED.json b/research/p104-owned-add-source-span-bound/inputs/ADMITTED.json new file mode 100644 index 0000000000..464c89e45c --- /dev/null +++ b/research/p104-owned-add-source-span-bound/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-owned-add-source-span-bound/inputs/R82-CONTACTS.json b/research/p104-owned-add-source-span-bound/inputs/R82-CONTACTS.json new file mode 100644 index 0000000000..ca75bfa82d --- /dev/null +++ b/research/p104-owned-add-source-span-bound/inputs/R82-CONTACTS.json @@ -0,0 +1,1578 @@ +{ + "case_cap": 51, + "controls": [ + "peer read must follow update", + "read-only peer commutation", + "peer write barrier", + "guarded COPY barrier", + "owned lifetime barrier", + "coframe MOVE transports only" + ], + "counts": { + "excluded": 51 + }, + "decisions": [ + { + "actual_peer_chart": 534, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1502, + 33140, + 33142, + "entrance", + 33140 + ], + "original_add": [ + 33141, + [ + 1489, + 1502, + "4", + 534 + ] + ], + "owner_lifetime": 33136, + "peer": 1489, + "peer_lifetime": -1, + "required_chart": 541 + }, + { + "actual_peer_chart": 534, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1502, + 33140, + 33142, + "entrance", + 33141 + ], + "original_add": [ + 33141, + [ + 1489, + 1502, + "4", + 534 + ] + ], + "owner_lifetime": 33136, + "peer": 1489, + "peer_lifetime": -1, + "required_chart": 541 + }, + { + "actual_peer_chart": 534, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1502, + 33140, + 33142, + "entrance", + 33142 + ], + "original_add": [ + 33141, + [ + 1489, + 1502, + "4", + 534 + ] + ], + "owner_lifetime": 33136, + "peer": 1489, + "peer_lifetime": -1, + "required_chart": 541 + }, + { + "actual_peer_chart": 534, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1502, + 33140, + 33142, + "exit", + 33141 + ], + "original_add": [ + 33141, + [ + 1489, + 1502, + "4", + 534 + ] + ], + "owner_lifetime": 33136, + "peer": 1489, + "peer_lifetime": -1, + "required_chart": 117 + }, + { + "actual_peer_chart": 534, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1502, + 33140, + 33142, + "exit", + 33142 + ], + "original_add": [ + 33141, + [ + 1489, + 1502, + "4", + 534 + ] + ], + "owner_lifetime": 33136, + "peer": 1489, + "peer_lifetime": -1, + "required_chart": 117 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1503, + 39805, + 39811, + "entrance", + 39805 + ], + "original_add": [ + 39806, + [ + 497, + 1503, + "-4", + 520 + ] + ], + "owner_lifetime": 39802, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1503, + 39805, + 39811, + "entrance", + 39806 + ], + "original_add": [ + 39806, + [ + 497, + 1503, + "-4", + 520 + ] + ], + "owner_lifetime": 39802, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1503, + 39805, + 39811, + "entrance", + 39807 + ], + "original_add": [ + 39806, + [ + 497, + 1503, + "-4", + 520 + ] + ], + "owner_lifetime": 39802, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1503, + 39805, + 39811, + "entrance", + 39808 + ], + "original_add": [ + 39806, + [ + 497, + 1503, + "-4", + 520 + ] + ], + "owner_lifetime": 39802, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [ + [ + 39808, + [ + "ADD", + 992, + 497, + "-1", + 520 + ], + "counterpart chronology" + ] + ], + "decision": "excluded", + "failures": [ + "counterpart chart", + "crossed incident barrier" + ], + "key": [ + 1503, + 39805, + 39811, + "entrance", + 39809 + ], + "original_add": [ + 39806, + [ + 497, + 1503, + "-4", + 520 + ] + ], + "owner_lifetime": 39802, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [ + [ + 39808, + [ + "ADD", + 992, + 497, + "-1", + 520 + ], + "counterpart chronology" + ] + ], + "decision": "excluded", + "failures": [ + "counterpart chart", + "crossed incident barrier" + ], + "key": [ + 1503, + 39805, + 39811, + "entrance", + 39810 + ], + "original_add": [ + 39806, + [ + 497, + 1503, + "-4", + 520 + ] + ], + "owner_lifetime": 39802, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [ + [ + 39808, + [ + "ADD", + 992, + 497, + "-1", + 520 + ], + "counterpart chronology" + ] + ], + "decision": "excluded", + "failures": [ + "counterpart chart", + "crossed incident barrier" + ], + "key": [ + 1503, + 39805, + 39811, + "entrance", + 39811 + ], + "original_add": [ + 39806, + [ + 497, + 1503, + "-4", + 520 + ] + ], + "owner_lifetime": 39802, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1503, + 39805, + 39811, + "exit", + 39806 + ], + "original_add": [ + 39806, + [ + 497, + 1503, + "-4", + 520 + ] + ], + "owner_lifetime": 39802, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1503, + 39805, + 39811, + "exit", + 39807 + ], + "original_add": [ + 39806, + [ + 497, + 1503, + "-4", + 520 + ] + ], + "owner_lifetime": 39802, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1503, + 39805, + 39811, + "exit", + 39808 + ], + "original_add": [ + 39806, + [ + 497, + 1503, + "-4", + 520 + ] + ], + "owner_lifetime": 39802, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [ + [ + 39808, + [ + "ADD", + 992, + 497, + "-1", + 520 + ], + "counterpart chronology" + ] + ], + "decision": "excluded", + "failures": [ + "counterpart chart", + "crossed incident barrier" + ], + "key": [ + 1503, + 39805, + 39811, + "exit", + 39809 + ], + "original_add": [ + 39806, + [ + 497, + 1503, + "-4", + 520 + ] + ], + "owner_lifetime": 39802, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [ + [ + 39808, + [ + "ADD", + 992, + 497, + "-1", + 520 + ], + "counterpart chronology" + ] + ], + "decision": "excluded", + "failures": [ + "counterpart chart", + "crossed incident barrier" + ], + "key": [ + 1503, + 39805, + 39811, + "exit", + 39810 + ], + "original_add": [ + 39806, + [ + 497, + 1503, + "-4", + 520 + ] + ], + "owner_lifetime": 39802, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [ + [ + 39808, + [ + "ADD", + 992, + 497, + "-1", + 520 + ], + "counterpart chronology" + ] + ], + "decision": "excluded", + "failures": [ + "counterpart chart", + "crossed incident barrier" + ], + "key": [ + 1503, + 39805, + 39811, + "exit", + 39811 + ], + "original_add": [ + 39806, + [ + 497, + 1503, + "-4", + 520 + ] + ], + "owner_lifetime": 39802, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "entrance", + 39866 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "entrance", + 39867 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "entrance", + 39868 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "entrance", + 39869 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "entrance", + 39870 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "entrance", + 39871 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "entrance", + 39872 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "entrance", + 39873 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "entrance", + 39874 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "entrance", + 39875 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 595 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "exit", + 39867 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "exit", + 39868 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "exit", + 39869 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "exit", + 39870 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "exit", + 39871 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "exit", + 39872 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "exit", + 39873 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "exit", + 39874 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 520, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1532, + 39866, + 39875, + "exit", + 39875 + ], + "original_add": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "owner_lifetime": 38119, + "peer": 497, + "peer_lifetime": -1, + "required_chart": 529 + }, + { + "actual_peer_chart": 115, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1501, + 40554, + 40558, + "entrance", + 40554 + ], + "original_add": [ + 40555, + [ + 1501, + 1525, + "1/4", + 115 + ] + ], + "owner_lifetime": 39975, + "peer": 1525, + "peer_lifetime": 33804, + "required_chart": 549 + }, + { + "actual_peer_chart": 115, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1501, + 40554, + 40558, + "entrance", + 40555 + ], + "original_add": [ + 40555, + [ + 1501, + 1525, + "1/4", + 115 + ] + ], + "owner_lifetime": 39975, + "peer": 1525, + "peer_lifetime": 33804, + "required_chart": 549 + }, + { + "actual_peer_chart": 115, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1501, + 40554, + 40558, + "entrance", + 40556 + ], + "original_add": [ + 40555, + [ + 1501, + 1525, + "1/4", + 115 + ] + ], + "owner_lifetime": 39975, + "peer": 1525, + "peer_lifetime": 33804, + "required_chart": 549 + }, + { + "actual_peer_chart": null, + "crossed_incident_barriers": [ + [ + 40556, + [ + "CLEAR", + 1525, + 115 + ], + "counterpart chronology" + ] + ], + "decision": "excluded", + "failures": [ + "counterpart chart", + "changed lifetime", + "crossed incident barrier" + ], + "key": [ + 1501, + 40554, + 40558, + "entrance", + 40557 + ], + "original_add": [ + 40555, + [ + 1501, + 1525, + "1/4", + 115 + ] + ], + "owner_lifetime": 39975, + "peer": 1525, + "peer_lifetime": null, + "required_chart": 549 + }, + { + "actual_peer_chart": null, + "crossed_incident_barriers": [ + [ + 40556, + [ + "CLEAR", + 1525, + 115 + ], + "counterpart chronology" + ] + ], + "decision": "excluded", + "failures": [ + "counterpart chart", + "changed lifetime", + "crossed incident barrier" + ], + "key": [ + 1501, + 40554, + 40558, + "entrance", + 40558 + ], + "original_add": [ + 40555, + [ + 1501, + 1525, + "1/4", + 115 + ] + ], + "owner_lifetime": 39975, + "peer": 1525, + "peer_lifetime": null, + "required_chart": 549 + }, + { + "actual_peer_chart": 115, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1501, + 40554, + 40558, + "exit", + 40555 + ], + "original_add": [ + 40555, + [ + 1501, + 1525, + "1/4", + 115 + ] + ], + "owner_lifetime": 39975, + "peer": 1525, + "peer_lifetime": 33804, + "required_chart": 593 + }, + { + "actual_peer_chart": 115, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1501, + 40554, + 40558, + "exit", + 40556 + ], + "original_add": [ + 40555, + [ + 1501, + 1525, + "1/4", + 115 + ] + ], + "owner_lifetime": 39975, + "peer": 1525, + "peer_lifetime": 33804, + "required_chart": 593 + }, + { + "actual_peer_chart": null, + "crossed_incident_barriers": [ + [ + 40556, + [ + "CLEAR", + 1525, + 115 + ], + "counterpart chronology" + ] + ], + "decision": "excluded", + "failures": [ + "counterpart chart", + "changed lifetime", + "crossed incident barrier" + ], + "key": [ + 1501, + 40554, + 40558, + "exit", + 40557 + ], + "original_add": [ + 40555, + [ + 1501, + 1525, + "1/4", + 115 + ] + ], + "owner_lifetime": 39975, + "peer": 1525, + "peer_lifetime": null, + "required_chart": 593 + }, + { + "actual_peer_chart": null, + "crossed_incident_barriers": [ + [ + 40556, + [ + "CLEAR", + 1525, + 115 + ], + "counterpart chronology" + ] + ], + "decision": "excluded", + "failures": [ + "counterpart chart", + "changed lifetime", + "crossed incident barrier" + ], + "key": [ + 1501, + 40554, + 40558, + "exit", + 40558 + ], + "original_add": [ + 40555, + [ + 1501, + 1525, + "1/4", + 115 + ] + ], + "owner_lifetime": 39975, + "peer": 1525, + "peer_lifetime": null, + "required_chart": 593 + }, + { + "actual_peer_chart": 534, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1531, + 44242, + 44244, + "entrance", + 44242 + ], + "original_add": [ + 44243, + [ + 1531, + 995, + "-4", + 534 + ] + ], + "owner_lifetime": 32607, + "peer": 995, + "peer_lifetime": -1, + "required_chart": 117 + }, + { + "actual_peer_chart": 534, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1531, + 44242, + 44244, + "entrance", + 44243 + ], + "original_add": [ + 44243, + [ + 1531, + 995, + "-4", + 534 + ] + ], + "owner_lifetime": 32607, + "peer": 995, + "peer_lifetime": -1, + "required_chart": 117 + }, + { + "actual_peer_chart": 534, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1531, + 44242, + 44244, + "entrance", + 44244 + ], + "original_add": [ + 44243, + [ + 1531, + 995, + "-4", + 534 + ] + ], + "owner_lifetime": 32607, + "peer": 995, + "peer_lifetime": -1, + "required_chart": 117 + }, + { + "actual_peer_chart": 534, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1531, + 44242, + 44244, + "exit", + 44243 + ], + "original_add": [ + 44243, + [ + 1531, + 995, + "-4", + 534 + ] + ], + "owner_lifetime": 32607, + "peer": 995, + "peer_lifetime": -1, + "required_chart": 541 + }, + { + "actual_peer_chart": 534, + "crossed_incident_barriers": [], + "decision": "excluded", + "failures": [ + "counterpart chart" + ], + "key": [ + 1531, + 44242, + 44244, + "exit", + 44244 + ], + "original_add": [ + 44243, + [ + 1531, + 995, + "-4", + 534 + ] + ], + "owner_lifetime": 32607, + "peer": 995, + "peer_lifetime": -1, + "required_chart": 541 + } + ], + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "placement_cap": 10, + "price_sha256": "82baf8740dfc695d304602d92bd3888961c965f76a5bcb4784cbd4f9726e7ee6", + "seconds_cap": 18, + "status": "EXHAUSTED", + "survivors": [], + "unvisited": [], + "word_sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +} diff --git a/research/p104-owned-add-source-span-bound/inputs/R82-PRICE.json b/research/p104-owned-add-source-span-bound/inputs/R82-PRICE.json new file mode 100644 index 0000000000..ab817d4377 --- /dev/null +++ b/research/p104-owned-add-source-span-bound/inputs/R82-PRICE.json @@ -0,0 +1,588 @@ +{ + "build_cap": 1, + "caller_head": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "candidate_count": 5, + "candidates": [ + { + "chart_path": [ + 541, + 534, + 117 + ], + "cut_windows_pre_event": { + "entrance": [ + 33140, + 33142 + ], + "exit": [ + 33141, + 33142 + ] + }, + "literal_ADD": [ + 33141, + [ + 1489, + 1502, + "4", + 534 + ] + ], + "move_clocks": [ + 33140, + 33142 + ], + "owner": 1502, + "owner_access": "source", + "owner_lifetime": [ + 33136, + 43333 + ], + "paid_delta": { + "1": -34, + "2": 17 + }, + "paid_new": 2, + "paid_old": [ + 1, + 1 + ], + "peer": 1489, + "quote": { + "complete_margin_at_crossing": [ + "858321385403521186417773068772405712363430437203/10000000000000000000000000000000000000000000000000", + "53645086587720074151110816798275357022714405823/625000000000000000000000000000000000000000000000" + ], + "complete_margin_at_moonshot": [ + "-1396726115492226473042776929224878016991402235844139/10000000000000000000000000000000000000000000000000", + "-279345223098445294608555385844975603398280447157429/2000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "427222934743114711483975651429956291031490795297/5000000000000000000000000000000000000000000000000", + "854445869486229422967951302859912582062981646559/10000000000000000000000000000000000000000000000000" + ], + "complete_margin_with_one_extra_rank_one_at_crossing": [ + "-9141678614596478813582226931227594287636569562797/10000000000000000000000000000000000000000000000000", + "-571354913412279925848889183201724642977285594177/625000000000000000000000000000000000000000000000" + ], + "empty_root_credits": 0, + "gross_at_crossing": [ + "214580346350880296604443267200568173320145689813/2500000000000000000000000000000000000000000000000", + "858321385403521186417773068802272693280582759269/10000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "47157310821488302895668077648480860052905945727/500000000000000000000000000000000000000000000000", + "943146216429766057913361552969617201058118914557/10000000000000000000000000000000000000000000000000" + ], + "paid": { + "1": 68350, + "2": 14518, + "3": 14093, + "4": 3791, + "5": 5865, + "6": 238, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "paid_delta": { + "1": -34, + "2": 17 + }, + "paid_positions": 110502, + "productive_positions": 22461, + "rank_surplus": 1424 + }, + "target_delta": {} + }, + { + "chart_path": [ + 529, + 520, + 595 + ], + "cut_windows_pre_event": { + "entrance": [ + 39805, + 39811 + ], + "exit": [ + 39806, + 39811 + ] + }, + "literal_ADD": [ + 39806, + [ + 497, + 1503, + "-4", + 520 + ] + ], + "move_clocks": [ + 39805, + 39811 + ], + "owner": 1503, + "owner_access": "source", + "owner_lifetime": [ + 39802, + 39887 + ], + "paid_delta": { + "1": -17, + "5": -17, + "6": 17 + }, + "paid_new": 6, + "paid_old": [ + 1, + 5 + ], + "peer": 497, + "quote": { + "complete_margin_at_crossing": [ + "834392976237489866662283238867233696199702541757/5000000000000000000000000000000000000000000000000", + "417196488118744933331141619433616848099851284857/2500000000000000000000000000000000000000000000000" + ], + "complete_margin_at_moonshot": [ + "-5452484757419563846706261254714879070036744426969/39062500000000000000000000000000000000000000000", + "-1395836097899408344756802881207009041929406573247121/10000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "1664910657158075350132431761866333578213961927363/10000000000000000000000000000000000000000000000000", + "1664910657158075350132431761866333578213961983277/10000000000000000000000000000000000000000000000000" + ], + "complete_margin_with_one_extra_rank_one_at_crossing": [ + "-4165607023762510133337716761132766303800297458243/5000000000000000000000000000000000000000000000000", + "-2082803511881255066668858380566383151900148715143/2500000000000000000000000000000000000000000000000" + ], + "empty_root_credits": 0, + "gross_at_crossing": [ + "1668785952474979733324566477764334373316557405529/10000000000000000000000000000000000000000000000000", + "1668785952474979733324566477764334373316557405563/10000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "1833163809247894343887409570838592263053781454581/10000000000000000000000000000000000000000000000000", + "366632761849578868777481914167718452610756290923/2000000000000000000000000000000000000000000000000" + ], + "paid": { + "1": 68367, + "2": 14501, + "3": 14093, + "4": 3791, + "5": 5848, + "6": 255, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "paid_delta": { + "1": -17, + "5": -17, + "6": 17 + }, + "paid_positions": 110502, + "productive_positions": 22461, + "rank_surplus": 1424 + }, + "target_delta": {} + }, + { + "chart_path": [ + 595, + 520, + 529 + ], + "cut_windows_pre_event": { + "entrance": [ + 39866, + 39875 + ], + "exit": [ + 39867, + 39875 + ] + }, + "literal_ADD": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "move_clocks": [ + 39866, + 39875 + ], + "owner": 1532, + "owner_access": "destination", + "owner_lifetime": [ + 38119, + 39878 + ], + "paid_delta": { + "1": -17, + "5": -17, + "6": 17 + }, + "paid_new": 6, + "paid_old": [ + 5, + 1 + ], + "peer": 497, + "quote": { + "complete_margin_at_crossing": [ + "834392976237489866662283238867233696199702541757/5000000000000000000000000000000000000000000000000", + "417196488118744933331141619433616848099851284857/2500000000000000000000000000000000000000000000000" + ], + "complete_margin_at_moonshot": [ + "-5452484757419563846706261254714879070036744426969/39062500000000000000000000000000000000000000000", + "-1395836097899408344756802881207009041929406573247121/10000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "1664910657158075350132431761866333578213961927363/10000000000000000000000000000000000000000000000000", + "1664910657158075350132431761866333578213961983277/10000000000000000000000000000000000000000000000000" + ], + "complete_margin_with_one_extra_rank_one_at_crossing": [ + "-4165607023762510133337716761132766303800297458243/5000000000000000000000000000000000000000000000000", + "-2082803511881255066668858380566383151900148715143/2500000000000000000000000000000000000000000000000" + ], + "empty_root_credits": 0, + "gross_at_crossing": [ + "1668785952474979733324566477764334373316557405529/10000000000000000000000000000000000000000000000000", + "1668785952474979733324566477764334373316557405563/10000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "1833163809247894343887409570838592263053781454581/10000000000000000000000000000000000000000000000000", + "366632761849578868777481914167718452610756290923/2000000000000000000000000000000000000000000000000" + ], + "paid": { + "1": 68367, + "2": 14501, + "3": 14093, + "4": 3791, + "5": 5848, + "6": 255, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "paid_delta": { + "1": -17, + "5": -17, + "6": 17 + }, + "paid_positions": 110502, + "productive_positions": 22461, + "rank_surplus": 1424 + }, + "target_delta": {} + }, + { + "chart_path": [ + 549, + 115, + 593 + ], + "cut_windows_pre_event": { + "entrance": [ + 40554, + 40558 + ], + "exit": [ + 40555, + 40558 + ] + }, + "literal_ADD": [ + 40555, + [ + 1501, + 1525, + "1/4", + 115 + ] + ], + "move_clocks": [ + 40554, + 40558 + ], + "owner": 1501, + "owner_access": "destination", + "owner_lifetime": [ + 39975, + 43332 + ], + "paid_delta": { + "2": -17, + "4": -17, + "6": 17 + }, + "paid_new": 6, + "paid_old": [ + 2, + 4 + ], + "peer": 1525, + "quote": { + "complete_margin_at_crossing": [ + "2355602677701438428037034298000189461885076143183/10000000000000000000000000000000000000000000000000", + "1177801338850719214018517149000094730942538099557/5000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_moonshot": [ + "-139508183721626357659843394481649159660999076897079/1000000000000000000000000000000000000000000000000", + "-139508183721626357659843394481649159660999076891383/1000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "2351727569399542983384747415154394827772957238617/10000000000000000000000000000000000000000000000000", + "587931892349885745846186853788598706943239323637/2500000000000000000000000000000000000000000000000" + ], + "complete_margin_with_one_extra_rank_one_at_crossing": [ + "-7644397322298561571962965701999810538114923856817/10000000000000000000000000000000000000000000000000", + "-3822198661149280785981482850999905269057461900443/5000000000000000000000000000000000000000000000000" + ], + "empty_root_credits": 0, + "gross_at_crossing": [ + "1177801338850719214018517149015028221401114232599/5000000000000000000000000000000000000000000000000", + "2355602677701438428037034298030056442802228465249/10000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "517484898478532500451269192271207516493917157571/2000000000000000000000000000000000000000000000000", + "1293712246196331251128172980678018791234792893953/5000000000000000000000000000000000000000000000000" + ], + "paid": { + "1": 68384, + "2": 14484, + "3": 14093, + "4": 3774, + "5": 5865, + "6": 255, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "paid_delta": { + "2": -17, + "4": -17, + "6": 17 + }, + "paid_positions": 110502, + "productive_positions": 22461, + "rank_surplus": 1424 + }, + "target_delta": {} + }, + { + "chart_path": [ + 117, + 534, + 541 + ], + "cut_windows_pre_event": { + "entrance": [ + 44242, + 44244 + ], + "exit": [ + 44243, + 44244 + ] + }, + "literal_ADD": [ + 44243, + [ + 1531, + 995, + "-4", + 534 + ] + ], + "move_clocks": [ + 44242, + 44244 + ], + "owner": 1531, + "owner_access": "destination", + "owner_lifetime": [ + 32607, + 44247 + ], + "paid_delta": { + "1": -34, + "2": 17 + }, + "paid_new": 2, + "paid_old": [ + 1, + 1 + ], + "peer": 995, + "quote": { + "complete_margin_at_crossing": [ + "858321385403521186417773068772405712363430437203/10000000000000000000000000000000000000000000000000", + "53645086587720074151110816798275357022714405823/625000000000000000000000000000000000000000000000" + ], + "complete_margin_at_moonshot": [ + "-1396726115492226473042776929224878016991402235844139/10000000000000000000000000000000000000000000000000", + "-279345223098445294608555385844975603398280447157429/2000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "427222934743114711483975651429956291031490795297/5000000000000000000000000000000000000000000000000", + "854445869486229422967951302859912582062981646559/10000000000000000000000000000000000000000000000000" + ], + "complete_margin_with_one_extra_rank_one_at_crossing": [ + "-9141678614596478813582226931227594287636569562797/10000000000000000000000000000000000000000000000000", + "-571354913412279925848889183201724642977285594177/625000000000000000000000000000000000000000000000" + ], + "empty_root_credits": 0, + "gross_at_crossing": [ + "214580346350880296604443267200568173320145689813/2500000000000000000000000000000000000000000000000", + "858321385403521186417773068802272693280582759269/10000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "47157310821488302895668077648480860052905945727/500000000000000000000000000000000000000000000000", + "943146216429766057913361552969617201058118914557/10000000000000000000000000000000000000000000000000" + ], + "paid": { + "1": 68350, + "2": 14518, + "3": 14093, + "4": 3791, + "5": 5865, + "6": 238, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "paid_delta": { + "1": -34, + "2": 17 + }, + "paid_positions": 110502, + "productive_positions": 22461, + "rank_surplus": 1424 + }, + "target_delta": {} + } + ], + "first_runner_seconds": 20, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "input_sha256": { + "inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/R80-COMPARE.json": "f06d6c49823f06421928ff3b9d73d34332c0040f148926dc25df609a7e3220a8", + "inputs/R80-FORWARD.json": "db293c67c896f54788681b7a8a9fec5f13da0e31fe5b3dd65fbe30e370ff1d2e", + "inputs/R80-REVERSE.json": "12c31ae16b9a364fd84c16d2f76cee873ab279984eb88e1cf1568be905c8f010", + "inputs/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182" + }, + "nonempty_disjoint_matchings": 31, + "old_complete_margin_at_crossing": [ + "-29866980917152322049/10000000000000000000000000000000000000000000000000", + "-29866980917152266101/10000000000000000000000000000000000000000000000000" + ], + "old_complete_margin_at_moonshot": [ + "-1397669261708656239100690290777847634192460354758679/10000000000000000000000000000000000000000000000000", + "-698834630854328119550345145388923817096230177350851/5000000000000000000000000000000000000000000000000" + ], + "old_crossing_upper": "182332597822022395349777014167081/50000000000000000000000000000000000", + "one_edit_gross_upper_at_crossing": "2355602677701438428037034298030056442802228465249/10000000000000000000000000000000000000000000000000", + "price_probe": "182332647822022395349777014167081/50000000000000000000000000000000000", + "scope": "Uses sealed nine-pair R80 receipts only. Prices one alternative per pair, grants any support and added ordinary cost free, no new word decode or support search.", + "typed_end_placements": 10, + "whole_compatible_relaxation": { + "complete_margin_at_crossing": [ + "7409817353458440267521713391133403595079356472813/10000000000000000000000000000000000000000000000000", + "740981735345844026752171339113340359507935652871/1000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_moonshot": [ + "-8684557607280676598717702516055469860511043551453/62500000000000000000000000000000000000000000000", + "-694764608582454127897416201284437588840883484087777/5000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "7405943626657712625800110595125463237618005068539/10000000000000000000000000000000000000000000000000", + "1851485906664428156450027648781365809404501281109/2500000000000000000000000000000000000000000000000" + ], + "complete_margin_with_one_extra_rank_one_at_crossing": [ + "-2590182646541559732478286608866596404920643527187/10000000000000000000000000000000000000000000000000", + "-259018264654155973247828660886659640492064347129/1000000000000000000000000000000000000000000000000" + ], + "empty_root_credits": 0, + "gross_at_crossing": [ + "7409817353458440267521713391163270575996508794777/10000000000000000000000000000000000000000000000000", + "463113584591152516720107086947704410999781799681/625000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "4070022271873991652928944104486228255346693263057/5000000000000000000000000000000000000000000000000", + "8140044543747983305857888208972456510693386526233/10000000000000000000000000000000000000000000000000" + ], + "paid": { + "1": 68282, + "2": 14518, + "3": 14093, + "4": 3774, + "5": 5831, + "6": 289, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "paid_delta": { + "1": -102, + "2": 17, + "4": -17, + "5": -34, + "6": 51 + }, + "paid_positions": 110434, + "productive_positions": 22461, + "rank_surplus": 1424 + }, + "word_sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +} diff --git a/research/p104-owned-add-source-span-bound/inputs/READBACK.json b/research/p104-owned-add-source-span-bound/inputs/READBACK.json new file mode 100644 index 0000000000..625b508eea --- /dev/null +++ b/research/p104-owned-add-source-span-bound/inputs/READBACK.json @@ -0,0 +1,188 @@ +{ + "assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "bit_admitted": "12039/3125000", + "bit_claim_headroom": "3000951089/25000000000000", + "bit_premise": "376669/100000000", + "caller_head": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "claim": "91166298911/25000000000000", + "context_c": 2430, + "context_headroom": 1666, + "copies": 17, + "directed_bounds": { + "new_at_claim": [ + "347195197206460540909548691538238227127/2000000000000000000000000000000000000000000000000", + "1735975986032302704547743457691191192207/10000000000000000000000000000000000000000000000000" + ], + "new_at_old_crossing_upper": [ + "333717954993733063339209580360321337006028706669/2000000000000000000000000000000000000000000000000", + "1668589774968665316696047901801606685030143589709/10000000000000000000000000000000000000000000000000" + ], + "new_at_raw_lower": [ + "8890529086421014119/10000000000000000000000000000000000000000000000000", + "8890529086421080299/10000000000000000000000000000000000000000000000000" + ], + "new_at_raw_upper": [ + "-29866980917152322049/10000000000000000000000000000000000000000000000000", + "-29866980917152266101/10000000000000000000000000000000000000000000000000" + ], + "new_at_tested": [ + "1464673416007288863003441470091977383033/10000000000000000000000000000000000000000000000000", + "1464673416007288863003441470091977438357/10000000000000000000000000000000000000000000000000" + ], + "old_at_claim": [ + "-1668785950738799647054310634446839861363893886031/10000000000000000000000000000000000000000000000000", + "-66751438029551985882172425377873594454555753177/400000000000000000000000000000000000000000000000" + ], + "old_at_old_crossing_upper": [ + "-357270001119021587349/10000000000000000000000000000000000000000000000000", + "-357270001119021530951/10000000000000000000000000000000000000000000000000" + ] + }, + "empty_root_credits": 0, + "exact_gain": "215259997/500000000000000", + "exact_relative_percent": "21525999700/1823110718223", + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "incumbent": "1823110718223/500000000000000", + "main_boundaries": 104, + "native_grid": [ + 1125, + 25 + ], + "native_ingredient_claim": "3646017316711/1000000000000000", + "new_raw_interval": [ + "364665195644044790699554028334161/100000000000000000000000000000000000", + "182332597822022395349777014167081/50000000000000000000000000000000000" + ], + "old_raw_upper": "36462214364462343366888845568981/10000000000000000000000000000000000", + "ordinary": 782715464, + "ordinary_delta": 52088, + "ordinary_headroom": 217284536, + "outer_functional": 4, + "outer_strict": 54, + "outer_strict_slack": "299635334804355997/10000000000000000000000000000000000", + "owned_lifetimes": 73, + "owned_peak": 50, + "paid": { + "1": 68384, + "2": 14501, + "3": 14093, + "4": 3791, + "5": 5865, + "6": 238, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "paid_delta": { + "1": -17, + "5": -17, + "6": 17 + }, + "paid_positions": 110519, + "parent": "9d0119eb12fbd9fa534b48cd37b68e7099757b91", + "path_pins": { + "dependencies/7298/pricing.py": { + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182" + }, + "dependencies/7314/NATIVE-RESULT.json": { + "sha256": "336f463da5afe5b60bfd3b9f0ce8aeea5a5feb1f854613bf4218ba0b28b3371b" + }, + "dependencies/7314/PROPOSED-CLAIM.json": { + "sha256": "41a08c4b7d0b2de4af22bc778948a143027eb3065fff47b0400b6ded1cc52778" + }, + "dependencies/7314/RESULT.json": { + "sha256": "432191ca572c9221935787ebe392699e3a1ef4512b0bf4fbc704657321cc87ca" + }, + "dependencies/round65/price.json": { + "sha256": "25205ad2cf4230bd2b2b704eec9f96ec4a5486fd575b5599861b28ffdd15b00b" + }, + "receipts/EARLY-RESULT.json": { + "git_blob": "675d6cf2374f3384019dfd53b2bdffd845005f13", + "sha256": "ad1ca9b2e2febbf80d9bf8b6ceef14ff90fcc29ef9358310e551628eb1706649" + }, + "receipts/INPUTS.json": { + "git_blob": "95c53f4594287a72d9b586f10ee136d0a1686984", + "sha256": "abedac59097a1c35c27d91cbdb07207bc562a64743bc406d13c94a8bc970592d" + }, + "receipts/NATIVE-RESULT.json": { + "git_blob": "eb101307d4d0399efed96d88cf6d4c01ec9c7369", + "sha256": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812" + }, + "receipts/PROOF.md": { + "git_blob": "7644e5571d583183ee93b686612b5ec4555f6911", + "sha256": "560de573bfd4563c16ca3c7308fa729b4188fabe802d8830f343c3873f75b59d" + }, + "receipts/PROPOSED-CLAIM.json": { + "git_blob": "6b491894580741e3e2c11a453722a0302db7b5d6", + "sha256": "6e31241944c123d2bd4aa8bc94d833b44b3d889bd6d9aafc579108f416b45f03" + }, + "receipts/README.md": { + "git_blob": "b3a055f4e0d334ce2e7df3310caaa0849eb3eba1", + "sha256": "b4db0eb83ab6a2f7151bed2da955a487f4816ec9d1976eccc21e54c2725490b0" + }, + "receipts/REFERENCE.json": { + "git_blob": "8859e243cc39546bcb1e257d95c19a658c455dc7", + "sha256": "3e66e054b803551f18b8670da0b2990a7d0eeb689dfc45b56dbcba295551da70" + }, + "receipts/REPLAY.txt": { + "git_blob": "0b8d8048c18740060f4b7f6d380a5f3a0f30ee53", + "sha256": "230984f4b8206ae4d0c0f18fbba86ff43a1a9623f8ed337cf1285360f9a67c0c" + }, + "receipts/RESULT.json": { + "git_blob": "3034a490f5b0656ae71495c99493c4ab1ac1f5c6", + "sha256": "7f2d587c59f063b01f1e8b320084a7f0943f2f05d65e3e0f5e80448c6c8e8194" + }, + "receipts/SOURCES.json": { + "git_blob": "6b97e903a6df8de437068a0e2907823885928053", + "sha256": "ac7b4473035af648d6073e78b6c39675e706e8194b346bb55ed62a0adc81d593" + }, + "receipts/VERIFY.json": { + "git_blob": "cc98ee2a5c5a79e670094a6f55c7cacda8fd330c", + "sha256": "ede7dd2dd3733b9a73f72af9dd7edfe819b49b859c5c76e227ec82cb9c220513" + }, + "receipts/construct.py": { + "git_blob": "89e923bd738dfc404ca76b7ae36f13844ac4bfbb", + "sha256": "ecb39578063d7f09153a85370a3b9bb7cbf8b36ff9891033a1cce7a2fe7f7fda" + } + }, + "physical_maps": 3037, + "productive_fields": 22461, + "rank_surplus": 1424, + "raw_strict_separation": "43051999421357030665572644351/100000000000000000000000000000000000", + "scope": "Exact receipt and directed-price readback. No native or caller execution in this audit.", + "source_archive_sha256": "0589953b3886d96eacf3bda3d38d8d574bb739fba1056af7f32f56047b6061e2", + "targets": { + "1": 306, + "2": 357, + "3": 799, + "4": 3825, + "5": 1360, + "6": 731, + "7": 323, + "8": 544, + "9": 10888, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208, + "137": 208 + }, + "tested": "364665195644007/100000000000000000" +} diff --git a/research/p104-owned-add-source-span-bound/inputs/pricing.py b/research/p104-owned-add-source-span-bound/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-owned-add-source-span-bound/inputs/pricing.py @@ -0,0 +1,82 @@ +"""Directed interval arithmetic and the retained signed BIT invoice.""" +from collections import Counter +from fractions import Fraction +from functools import cache + +TARGET = "10018846261809/2500000000000000" +SCALE = 10**49 + + +def rounded(x, upper): + scaled = SCALE*x + if upper: + return Fraction(-((-scaled.numerator) // scaled.denominator), SCALE) + return Fraction(scaled.numerator // scaled.denominator, SCALE) + + +@cache +def log_bounds(x): + z = (x-1)/(x+1) + terms = 60 + exact_partial = 2*sum(z**(2*i+1)/(2*i+1) for i in range(terms)) + tail = 2*z**(2*terms+1)/((2*terms+1)*(1-z*z)) + return rounded(exact_partial, False), rounded(exact_partial+tail, True) + + +@cache +def power_bounds(rank, k): + binary = 2**(rank.bit_length()-1) + shift = binary.bit_length()-1 + l2, u2 = log_bounds(Fraction(2)) + lo, hi = log_bounds(Fraction(rank, binary)) + lo, hi = k*(lo+shift*l2), k*(hi+shift*u2) + assert 0 <= lo <= hi < 1 + + def exponential(z, terms): + total = term = Fraction(1) + for i in range(1, terms+1): + term *= -z/i + total += term + return total + + return rounded(rank*exponential(hi, 35), False), rounded(rank*exponential(lo, 34), True) + + +def cost(hist, k): + lower = upper = Fraction(0) + for r, n in hist.items(): + a, b = (n*x for x in power_bounds(r, k)) + lower += min(a, b) + upper += max(a, b) + return lower, upper + + +def profile(invoice, native, word, ranks): + copies = invoice["native_calls"] + assert copies == len(invoice["native_instances"]) == 36 + assert {tuple((r["stage"], r["copy"])) for r in invoice["native_instances"]} == { + (stage, which) for stage in range(1, 19) for which in (0, 1) + } + assert all(r["ports"] == 111 for r in invoice["native_instances"]) + assert native == Counter({int(r): n for r, n in invoice["native_paid"].items()}) + assert sum(native.values()) == 2871 + caller_paid = {1: 444, **{r: 444 for r in range(7, 57, 7)}} + assert invoice["event_counts"]["QUERY"]*111 == caller_paid[1] + assert invoice["event_counts"]["IDLE_ONE"]*111 == 8*444 + full_paid = Counter({r: copies*n for r, n in native.items()}) + full_paid.update(caller_paid) + + helpers = Counter(ranks[word["final"][j]]-ranks[word["start"][j]] + for j in range(222, word["public"])) + assert helpers == Counter({int(r): n for r, n in invoice["native_helpers"].items()}) + caller_targets = {**{r: 444 for r in range(8, 65, 7)}, 127: 222} + full_targets = Counter({r: copies*n for r, n in helpers.items()}) + full_targets.update(caller_targets) + assert full_paid == Counter({int(r): n for r, n in invoice["paid"].items()}) + assert full_targets == Counter({int(r): n for r, n in invoice["targets"].items()}) + assert sum(full_paid.values()) == invoice["paid_jobs"] + assert sum(full_targets.values()) == invoice["productive_fields"] + signed = full_targets.copy() + signed.subtract(full_paid) + assert sum(r*n for r, n in signed.items()) == invoice["rank_surplus"] + return signed, copies diff --git a/research/p104-owned-add-source-span-bound/receipts/COMPARE.json b/research/p104-owned-add-source-span-bound/receipts/COMPARE.json new file mode 100644 index 0000000000..211be60919 --- /dev/null +++ b/research/p104-owned-add-source-span-bound/receipts/COMPARE.json @@ -0,0 +1,20 @@ +{ + "cases": 33, + "exact_donor_rank_agreements": 33, + "gross_optimistic_stock": [ + "1220677503894984836944843461149165877349842157499/2500000000000000000000000000000000000000000000000", + "305169375973746209236210865287291469337460539379/625000000000000000000000000000000000000000000000" + ], + "mutations_rejected": [ + "price bytes", + "compressed native word bytes" + ], + "rows": 69, + "supported_credit": 0, + "survivors": 0, + "unresolved": 0, + "witness_counts": { + "absent_exterior_coordinate": 24, + "exact_rank_exclusion": 9 + } +} diff --git a/research/p104-owned-add-source-span-bound/receipts/FORWARD.json.gz b/research/p104-owned-add-source-span-bound/receipts/FORWARD.json.gz new file mode 100644 index 0000000000..aa9b89ed4c Binary files /dev/null and b/research/p104-owned-add-source-span-bound/receipts/FORWARD.json.gz differ diff --git a/research/p104-owned-add-source-span-bound/receipts/PRICE.json b/research/p104-owned-add-source-span-bound/receipts/PRICE.json new file mode 100644 index 0000000000..8289421872 --- /dev/null +++ b/research/p104-owned-add-source-span-bound/receipts/PRICE.json @@ -0,0 +1,580 @@ +{ + "build_cap": 1, + "candidates": [ + { + "chart_path": [ + 595, + 520, + 529 + ], + "cut_windows_pre_event": { + "entrance": [ + 39866, + 39875 + ], + "exit": [ + 39867, + 39875 + ] + }, + "literal_ADD": [ + 39867, + [ + 1532, + 497, + "4", + 520 + ] + ], + "move_clocks": [ + 39866, + 39875 + ], + "owner": 1532, + "owner_access": "destination", + "owner_lifetime": [ + 38119, + 39878 + ], + "paid_delta": { + "1": -17, + "5": -17, + "6": 17 + }, + "paid_new": 6, + "paid_old": [ + 5, + 1 + ], + "peer": 497, + "quote": { + "complete_margin_at_crossing": [ + "834392976237489866662283238867233696199702541757/5000000000000000000000000000000000000000000000000", + "417196488118744933331141619433616848099851284857/2500000000000000000000000000000000000000000000000" + ], + "complete_margin_at_moonshot": [ + "-5452484757419563846706261254714879070036744426969/39062500000000000000000000000000000000000000000", + "-1395836097899408344756802881207009041929406573247121/10000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "1664910657158075350132431761866333578213961927363/10000000000000000000000000000000000000000000000000", + "1664910657158075350132431761866333578213961983277/10000000000000000000000000000000000000000000000000" + ], + "complete_margin_with_one_extra_rank_one_at_crossing": [ + "-4165607023762510133337716761132766303800297458243/5000000000000000000000000000000000000000000000000", + "-2082803511881255066668858380566383151900148715143/2500000000000000000000000000000000000000000000000" + ], + "empty_root_credits": 0, + "gross_at_crossing": [ + "1668785952474979733324566477764334373316557405529/10000000000000000000000000000000000000000000000000", + "1668785952474979733324566477764334373316557405563/10000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "1833163809247894343887409570838592263053781454581/10000000000000000000000000000000000000000000000000", + "366632761849578868777481914167718452610756290923/2000000000000000000000000000000000000000000000000" + ], + "paid": { + "1": 68367, + "16": 416, + "2": 14501, + "24": 416, + "3": 14093, + "32": 416, + "4": 3791, + "40": 416, + "48": 416, + "5": 5848, + "56": 416, + "6": 255, + "64": 208, + "7": 170, + "8": 741, + "9": 32 + }, + "paid_delta": { + "1": -17, + "5": -17, + "6": 17 + }, + "paid_positions": 110502, + "productive_positions": 22461, + "rank_surplus": 1424 + }, + "target_delta": {} + }, + { + "chart_path": [ + 549, + 115, + 593 + ], + "cut_windows_pre_event": { + "entrance": [ + 40554, + 40558 + ], + "exit": [ + 40555, + 40558 + ] + }, + "literal_ADD": [ + 40555, + [ + 1501, + 1525, + "1/4", + 115 + ] + ], + "move_clocks": [ + 40554, + 40558 + ], + "owner": 1501, + "owner_access": "destination", + "owner_lifetime": [ + 39975, + 43332 + ], + "paid_delta": { + "2": -17, + "4": -17, + "6": 17 + }, + "paid_new": 6, + "paid_old": [ + 2, + 4 + ], + "peer": 1525, + "quote": { + "complete_margin_at_crossing": [ + "2355602677701438428037034298000189461885076143183/10000000000000000000000000000000000000000000000000", + "1177801338850719214018517149000094730942538099557/5000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_moonshot": [ + "-139508183721626357659843394481649159660999076897079/1000000000000000000000000000000000000000000000000", + "-139508183721626357659843394481649159660999076891383/1000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "2351727569399542983384747415154394827772957238617/10000000000000000000000000000000000000000000000000", + "587931892349885745846186853788598706943239323637/2500000000000000000000000000000000000000000000000" + ], + "complete_margin_with_one_extra_rank_one_at_crossing": [ + "-7644397322298561571962965701999810538114923856817/10000000000000000000000000000000000000000000000000", + "-3822198661149280785981482850999905269057461900443/5000000000000000000000000000000000000000000000000" + ], + "empty_root_credits": 0, + "gross_at_crossing": [ + "1177801338850719214018517149015028221401114232599/5000000000000000000000000000000000000000000000000", + "2355602677701438428037034298030056442802228465249/10000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "517484898478532500451269192271207516493917157571/2000000000000000000000000000000000000000000000000", + "1293712246196331251128172980678018791234792893953/5000000000000000000000000000000000000000000000000" + ], + "paid": { + "1": 68384, + "16": 416, + "2": 14484, + "24": 416, + "3": 14093, + "32": 416, + "4": 3774, + "40": 416, + "48": 416, + "5": 5865, + "56": 416, + "6": 255, + "64": 208, + "7": 170, + "8": 741, + "9": 32 + }, + "paid_delta": { + "2": -17, + "4": -17, + "6": 17 + }, + "paid_positions": 110502, + "productive_positions": 22461, + "rank_surplus": 1424 + }, + "target_delta": {} + }, + { + "chart_path": [ + 117, + 534, + 541 + ], + "cut_windows_pre_event": { + "entrance": [ + 44242, + 44244 + ], + "exit": [ + 44243, + 44244 + ] + }, + "literal_ADD": [ + 44243, + [ + 1531, + 995, + "-4", + 534 + ] + ], + "move_clocks": [ + 44242, + 44244 + ], + "owner": 1531, + "owner_access": "destination", + "owner_lifetime": [ + 32607, + 44247 + ], + "paid_delta": { + "1": -34, + "2": 17 + }, + "paid_new": 2, + "paid_old": [ + 1, + 1 + ], + "peer": 995, + "quote": { + "complete_margin_at_crossing": [ + "858321385403521186417773068772405712363430437203/10000000000000000000000000000000000000000000000000", + "53645086587720074151110816798275357022714405823/625000000000000000000000000000000000000000000000" + ], + "complete_margin_at_moonshot": [ + "-1396726115492226473042776929224878016991402235844139/10000000000000000000000000000000000000000000000000", + "-279345223098445294608555385844975603398280447157429/2000000000000000000000000000000000000000000000000" + ], + "complete_margin_at_probe": [ + "427222934743114711483975651429956291031490795297/5000000000000000000000000000000000000000000000000", + "854445869486229422967951302859912582062981646559/10000000000000000000000000000000000000000000000000" + ], + "complete_margin_with_one_extra_rank_one_at_crossing": [ + "-9141678614596478813582226931227594287636569562797/10000000000000000000000000000000000000000000000000", + "-571354913412279925848889183201724642977285594177/625000000000000000000000000000000000000000000000" + ], + "empty_root_credits": 0, + "gross_at_crossing": [ + "214580346350880296604443267200568173320145689813/2500000000000000000000000000000000000000000000000", + "858321385403521186417773068802272693280582759269/10000000000000000000000000000000000000000000000000" + ], + "gross_at_moonshot": [ + "47157310821488302895668077648480860052905945727/500000000000000000000000000000000000000000000000", + "943146216429766057913361552969617201058118914557/10000000000000000000000000000000000000000000000000" + ], + "paid": { + "1": 68350, + "16": 416, + "2": 14518, + "24": 416, + "3": 14093, + "32": 416, + "4": 3791, + "40": 416, + "48": 416, + "5": 5865, + "56": 416, + "6": 238, + "64": 208, + "7": 170, + "8": 741, + "9": 32 + }, + "paid_delta": { + "1": -34, + "2": 17 + }, + "paid_positions": 110502, + "productive_positions": 22461, + "rank_surplus": 1424 + }, + "target_delta": {} + } + ], + "case_cap": 33, + "complete_probe_margin": [ + "2439417799014313902296214502569964516347740576789/5000000000000000000000000000000000000000000000000", + "1219708899507156951148107251284982258173870302373/2500000000000000000000000000000000000000000000000" + ], + "extra_rank_one_upper": [ + "-2558644992210030326110313077716601735758891846001/5000000000000000000000000000000000000000000000000", + "-639661248052507581527578269429150433939722954511/1250000000000000000000000000000000000000000000000" + ], + "gross_upper_all_three": [ + "1220677503894984836944843461149165877349842157499/2500000000000000000000000000000000000000000000000", + "305169375973746209236210865287291469337460539379/625000000000000000000000000000000000000000000000" + ], + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "input_sha256": { + "inputs/R82-CONTACTS.json": "664c3824078877c6b9e6ace20d8b03202a250e67e0f09b66a7304ce1ab8a5d00", + "inputs/R82-PRICE.json": "82baf8740dfc695d304602d92bd3888961c965f76a5bcb4784cbd4f9726e7ee6", + "inputs/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182" + }, + "keys": [ + [ + 1532, + 39866, + 39875, + "entrance", + 39866 + ], + [ + 1532, + 39866, + 39875, + "entrance", + 39867 + ], + [ + 1532, + 39866, + 39875, + "entrance", + 39868 + ], + [ + 1532, + 39866, + 39875, + "entrance", + 39869 + ], + [ + 1532, + 39866, + 39875, + "entrance", + 39870 + ], + [ + 1532, + 39866, + 39875, + "entrance", + 39871 + ], + [ + 1532, + 39866, + 39875, + "entrance", + 39872 + ], + [ + 1532, + 39866, + 39875, + "entrance", + 39873 + ], + [ + 1532, + 39866, + 39875, + "entrance", + 39874 + ], + [ + 1532, + 39866, + 39875, + "entrance", + 39875 + ], + [ + 1532, + 39866, + 39875, + "exit", + 39867 + ], + [ + 1532, + 39866, + 39875, + "exit", + 39868 + ], + [ + 1532, + 39866, + 39875, + "exit", + 39869 + ], + [ + 1532, + 39866, + 39875, + "exit", + 39870 + ], + [ + 1532, + 39866, + 39875, + "exit", + 39871 + ], + [ + 1532, + 39866, + 39875, + "exit", + 39872 + ], + [ + 1532, + 39866, + 39875, + "exit", + 39873 + ], + [ + 1532, + 39866, + 39875, + "exit", + 39874 + ], + [ + 1532, + 39866, + 39875, + "exit", + 39875 + ], + [ + 1501, + 40554, + 40558, + "entrance", + 40554 + ], + [ + 1501, + 40554, + 40558, + "entrance", + 40555 + ], + [ + 1501, + 40554, + 40558, + "entrance", + 40556 + ], + [ + 1501, + 40554, + 40558, + "entrance", + 40557 + ], + [ + 1501, + 40554, + 40558, + "entrance", + 40558 + ], + [ + 1501, + 40554, + 40558, + "exit", + 40555 + ], + [ + 1501, + 40554, + 40558, + "exit", + 40556 + ], + [ + 1501, + 40554, + 40558, + "exit", + 40557 + ], + [ + 1501, + 40554, + 40558, + "exit", + 40558 + ], + [ + 1531, + 44242, + 44244, + "entrance", + 44242 + ], + [ + 1531, + 44242, + 44244, + "entrance", + 44243 + ], + [ + 1531, + 44242, + 44244, + "entrance", + 44244 + ], + [ + 1531, + 44242, + 44244, + "exit", + 44243 + ], + [ + 1531, + 44242, + 44244, + "exit", + 44244 + ] + ], + "paid_all_three": { + "1": 68333, + "2": 14501, + "3": 14093, + "4": 3774, + "5": 5848, + "6": 272, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "scope": "Keep all fixed paid itineraries except fuse one destination-owned pair. Match its literal source value by exact existing same-chart donor rows. Optimistically free added ordinary work, no new paid operation. No word decoded.", + "time_cap_seconds": 20, + "word_sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +} diff --git a/research/p104-owned-add-source-span-bound/receipts/REVERSE.json.gz b/research/p104-owned-add-source-span-bound/receipts/REVERSE.json.gz new file mode 100644 index 0000000000..8430db4f04 Binary files /dev/null and b/research/p104-owned-add-source-span-bound/receipts/REVERSE.json.gz differ diff --git a/research/p104-owned-add-source-span-bound/receipts/SHA256.json b/research/p104-owned-add-source-span-bound/receipts/SHA256.json new file mode 100644 index 0000000000..6534bc020d --- /dev/null +++ b/research/p104-owned-add-source-span-bound/receipts/SHA256.json @@ -0,0 +1,6 @@ +{ + "COMPARE.json": "86a49fe8ea6a5049621dcb2c90df3b55a2f48d82681ceefae6eda51c66665092", + "FORWARD.json": "b29e92b11e0354f920d9dbaca31c18e6d72e772e21c818b91db471db2bc86895", + "PRICE.json": "c9166ff18194a7e69f91a06f76329a2ff838bb65b08c4ed7a5a06038fdfa966d", + "REVERSE.json": "f9696533a81d85c450430eef46fa0e622a63c8d694e95f47a21b81f670868ca7" +} diff --git a/research/p104-owned-add-source-span-bound/replay.py b/research/p104-owned-add-source-span-bound/replay.py new file mode 100644 index 0000000000..878cf0eb98 --- /dev/null +++ b/research/p104-owned-add-source-span-bound/replay.py @@ -0,0 +1,184 @@ +"""Reprice and independently reconstruct every signed donor-span exclusion.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction +from gzip import decompress +from hashlib import sha1, sha256 +from json import dumps, loads +from pathlib import Path +from shutil import copyfile +from subprocess import run +from sys import executable +from tempfile import TemporaryDirectory + +HERE = Path(__file__).resolve().parent +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER = "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc" +WORD = "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +ADMISSION = "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13" +PRIME = 65521 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def unique(pairs): + values = dict(pairs) + require(len(values) == len(pairs), "Duplicate JSON key") + return values + + +def read(raw): + return loads(raw, object_pairs_hook=unique) + + +def digest(raw): + return sha256(raw).hexdigest() + + +def verify_pins(): + for name, want in read((HERE / "LOCAL-PINS.json").read_bytes()).items(): + path = (HERE / name).resolve() + require(path.is_relative_to(HERE) and digest(path.read_bytes()) == want, f"Changed local input {name}") + for name, proof in read((HERE / "PROVENANCE.json").read_bytes())["files"].items(): + path = (HERE / name).resolve() + require(path.is_relative_to(HERE), f"Unsafe source path {name}") + raw = path.read_bytes() + if proof.get("uncompress"): + raw = decompress(raw) + blob = sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + require(digest(raw) == proof["sha256"] and blob == proof["git_blob"], f"Changed public source {name}") + admission = (HERE / "inputs/ADMITTED.json").read_bytes() + require(digest(admission) == ADMISSION, "Changed comparator admission") + verified = read(admission) + require(verified["head"] == HEAD and verified["caller_sha256"] == CALLER + and len(verified["stages"]) == 4 and verified["exit"] == 0, "Incomplete comparator admission") + base = read((HERE / "inputs/READBACK.json").read_bytes()) + require(base["head"] == HEAD and base["native_grid"] == [1125, 25] + and set(base["assumptions"]) == set(verified["assumptions"]) == { + "native_all_columns", "owned_erasure", "compiler", "precision_tape", "analytic_recovery"}, + "Changed comparator contract") + + +def certify(quote, lead, independent): + require(quote["head"] == lead["head"] == independent["head"] == HEAD + and quote["word_sha256"] == lead["word_sha256"] == independent["word_sha256"] == WORD, + "Changed science comparator") + price_hash = digest((HERE / "receipts/PRICE.json").read_bytes()) + require(lead["price_sha256"] == independent["price_sha256"] == price_hash, "Changed predecode quote") + require(lead["status"] == "EXHAUSTED" and not lead["unvisited"] and not lead["survivors"] + and not independent["unresolved"] and not independent["survivors"] + and independent["timeout"] is None and independent["prime"] == PRIME, "Incomplete exact sweep") + require(len(quote["keys"]) == len(lead["decisions"]) == len(independent["cases"]) == 33, + "Changed key census") + gross = list(map(Fraction, quote["gross_upper_all_three"])) + require(0 < gross[0] <= gross[1] < 1 + and Fraction(quote["extra_rank_one_upper"][1]) < 0 + and sum(quote["paid_all_three"].values()) == 110468, "Changed complete stock upper") + rows = independent["requested_integer_rows"] + require(len(rows) == independent["distinct_requested_rows"] == 69, "Changed exact row count") + bins = Counter() + + for key, forward, reverse in zip(quote["keys"], lead["decisions"], independent["cases"], strict=True): + require(forward["key"] == reverse["key"] == key and forward["target_chart"] == reverse["proposed_chart"] + and forward["source"] == [reverse["literal_read_clock"], reverse["literal_read_peer"]], + "Changed cut or source") + target = rows[reverse["target_row_id"]] + bank = [(role, rows[idx]) for role, idx in reverse["donor_role_row_ids"]] + require(forward["decision"] == "outside donor span" and forward["matching_coefficients"] is None + and forward["residual"] and forward["rank"] == reverse["donor_rank"] + and reverse["augmented_rank"] == reverse["donor_rank"] + 1 + and forward["bank_roles"] == [role for role, row in bank if row[0]] + and forward["source_nnz"] == len(target[0]) and len(bank) == reverse["donors"] + and all(role != key[0] for role, _ in bank), "Bank or rank mismatch") + require(all(row[1] > 0 and row[1] % PRIME for _, row in bank) and target[1] > 0 and target[1] % PRIME, + "Nonunit denominator") + + if reverse["status"] == "absent_exterior_coordinate": + j = str(reverse["coordinate"]) + residue = target[0][j] * pow(target[1], -1, PRIME) % PRIME + require(all(j not in row[0] for _, row in bank) + and Fraction(target[0][j], target[1]) == Fraction(reverse["target_coefficient"]) + and residue == reverse["target_residue_mod_prime"] != 0, "Invalid exterior certificate") + else: + require(reverse["status"] == "exact_rank_exclusion", "Unexpected witness kind") + dual = {j: Fraction(x) for j, x in reverse["separating_covector"].items()} + + def dot(row): + return sum((row[0].get(j, 0) * value for j, value in dual.items()), Fraction(0)) / row[1] + + require(all(dot(row) == 0 for _, row in bank) + and dot(target) == Fraction(reverse["separated_target"]) == -2, "Invalid rational dual") + bins[reverse["status"]] += 1 + require(bins == {"absent_exterior_coordinate": 24, "exact_rank_exclusion": 9}, + "Unexpected certificate census") + return dict(cases=33, rows=69, witness_counts=dict(bins), exact_donor_rank_agreements=33, + survivors=0, unresolved=0, supported_credit=0, gross_optimistic_stock=quote["gross_upper_all_three"]) + + +def replay(out): + require(__debug__, "Run with assertions") + verify_pins() + wanted = read((HERE / "receipts/SHA256.json").read_bytes()) + out.mkdir(parents=True, exist_ok=False) + with TemporaryDirectory(prefix="owned-add-span-") as tmp: + root = Path(tmp) + (root / "inputs").mkdir() + price_inputs = root / "price/inputs" + price_inputs.mkdir(parents=True) + for name in ("R82-CONTACTS.json", "R82-PRICE.json", "READBACK.json", "pricing.py"): + copyfile(HERE / "inputs" / name, price_inputs / name) + quote_runner = root / "price/quote.py" + copyfile(HERE / "engines/quote.py", quote_runner) + + def stage(name, script, *args): + cmd = [executable, "-I", "-B", str(script), *map(str, args)] + result = run(cmd, cwd=root, capture_output=True, check=True, timeout=22) + exact = HERE / "receipts" / (name if name == "PRICE.json" else name + ".gz") + raw = exact.read_bytes() + expected = raw if name == "PRICE.json" else decompress(raw) + require(result.stdout == expected and digest(result.stdout) == wanted[name], f"Changed receipt {name}") + (out / name).write_bytes(result.stdout) + return result.stdout + + raw_quote = stage("PRICE.json", quote_runner) + price = root / "price/PRICE.json" + price.write_bytes(raw_quote) + word = root / "inputs/7334-WORD.json.gz" + copyfile(HERE / "inputs" / word.name, word) + require(digest(decompress(word.read_bytes())) == PAYLOAD, "Changed canonical native payload") + lead = read(stage("FORWARD.json", HERE / "engines/forward.py", root)) + independent = read(stage("REVERSE.json", HERE / "engines/reverse.py", "--word", word, "--price", price)) + result = certify(read(raw_quote), lead, independent) + for target in (price, word): + raw = target.read_bytes() + target.write_bytes(raw + b"\n") + mutation = run([executable, "-I", "-B", str(HERE / "engines/reverse.py"), "--word", str(word), + "--price", str(price)], cwd=root, capture_output=True, timeout=22) + require(mutation.returncode != 0 and not mutation.stdout + and f"changed input {target.name}".encode() in mutation.stderr, "Changed pinned input passed") + target.write_bytes(raw) + result["mutations_rejected"] = ["price bytes", "compressed native word bytes"] + raw = (dumps(result, sort_keys=True, indent=2) + "\n").encode() + require(raw == (HERE / "receipts/COMPARE.json").read_bytes() + and digest(raw) == wanted["COMPARE.json"], "Changed comparison receipt") + (out / "COMPARE.json").write_bytes(raw) + print("PASS_OWNED_ADD_SOURCE_SPAN_BOUND cases=33 excluded=33 unresolved=0 kappa_change=0") + + +def main(): + p = ArgumentParser(description=__doc__) + p.add_argument("--out", type=Path) + args = p.parse_args() + if args.out: + replay(args.out.resolve()) + else: + with TemporaryDirectory(prefix="owned-add-span-receipts-") as tmp: + replay(Path(tmp) / "out") + + +if __name__ == "__main__": + main()