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-two-write-aggregate-bound/LOCAL-PINS.json b/research/p104-owned-two-write-aggregate-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..ec4d6a5df3 --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/LOCAL-PINS.json @@ -0,0 +1,19 @@ +{ + "PROVENANCE.json": "2c1b11fbd21107c9e61a899e66f3e85a537316df4b0d3ec77f6c226a6632867f", + "engines/aggregate.py": "5c5f9753cea43e59b78a7474c3b5c7987de682fc0a519602298602b368b96e04", + "engines/aggregate_covectors.py": "a2bcf9f1e90a5f365dba24854d843cfb33aa082c32e8d7a2c36e0e171dfd2f18", + "engines/compare.py": "cc71ced23ac058acbd8ef01ff3d22d7ad4e51e71c58af7f18c292c0691c89dbb", + "engines/quote.py": "7526fb6fffc8862b09bfe40d573bb25fd0dea63bf679c7802aa36c7ead90035e", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/BENCHMARK.json": "004331cff6ca8644489d7b7084e5c67439d74a2d283e4d64a9fdb9f88679253d", + "inputs/PR7362-SHA256.json": "2c90ca39b0f075cc4b3ec9e90c66fde473465e7bb50cf1db9a820d3a29556c0b", + "inputs/R80-REVERSE.json": "12c31ae16b9a364fd84c16d2f76cee873ab279984eb88e1cf1568be905c8f010", + "inputs/R92-PRICE.json.gz": "2274f514fb12f9ced0c24abe0c02a76c16cfee4c61f909e37a5ad89b07852371", + "inputs/donor_span.py": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "inputs/reverse_span.py": "f8b48f2ed99d003e20f5b3fb2270603c4edbc3ce9a01484102816aa2710ce9ff", + "receipts/AGREEMENT.json": "a3ad2b5e2e8cfa0814ed9745a97c79a944f425a920bb7a089f726ba1bc105d43", + "receipts/SHA256.json": "7741eb200e8f23be52d55f6f520bcfcb86eaf2c7da0bdedf704528ba23749de5", + "replay.py": "a2cd61a5b0bfea89f231ca8c337fc507b9ac4fcd322b03302b28adb6f3bb7d90" +} diff --git a/research/p104-owned-two-write-aggregate-bound/NOTICE b/research/p104-owned-two-write-aggregate-bound/NOTICE new file mode 100644 index 0000000000..4feae6b5af --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/NOTICE @@ -0,0 +1,3 @@ +Apache-2.0. + +#7334 and #7113 supply the exact word and signed caller. #7354 supplies the owned chronology inventory, #7355 the exact forward and reverse span engines, #7307 the owned chronology predecessor, #7362 the complete rank stock, and #7298 the directed tariff. The released role-1531 result in #7111 and Round 112 supply related fixed-producer and public aggregate evidence. OpenAI Codex and subagents materially assisted. diff --git a/research/p104-owned-two-write-aggregate-bound/PROOF.md b/research/p104-owned-two-write-aggregate-bound/PROOF.md new file mode 100644 index 0000000000..3147bdf2df --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/PROOF.md @@ -0,0 +1,18 @@ +# Owned role 1531 two-write aggregate + +The exact owned lifetime begins at 32607 and ends with CLEAR at 44247. Its frozen paid pair is 41996/44242, on charts 594→117→534 of ranks 1, 5 and 6. Between the paid positions the only incidents of owner 1531 are the incoming ADDs at 41997 and 44241. These read role 1291 with signed coefficient −2 and role 732 with coefficient −1, respectively. Neither old write changes any other row. The complete signed aggregate is therefore the sum of the two signed original source rows on the same normalized public input coordinates. Both independent engines calculate all its 219 nonzero coordinates exactly. + +The proposed rewrite keeps the old owner state at the interval boundary, fuses both paid MOVEs and replaces the two original writes at one frozen pre-event cut. If d is the old owner row at 41996, and a the signed aggregate, the required row is d+a. At either endpoint grant every other live cocharted donor row u, including existing owned roles, and arbitrary rational scaling of d. Reproducing d+a then requires a to lie in the span of d and the u rows. The late cut still uses d from 41996 because both old writes are removed. Using the literal late owner row would give the aggregate to itself and would not implement the rewrite. + +| Pre-event cut | Chart | Granted read-only donors | Rational rank with diagonal | Rank after adding aggregate | +|---:|---:|---|---:|---:| +| 41996 | 594 | Public 575 and 1231, owned 1502 | 4 | 5 | +| 44242 | 534 | Public 995 | 2 | 3 | + +The covector supported at input coordinate 244 annihilates all rows in both banks, including d. It evaluates to −1/2 on a. This excludes arbitrary rational combinations for the entire two-cut scope and therefore also excludes legal sparse dyadic implementations there. The proof uses no assumption about the initial public values. It grants more than the proposed two donor ADDs and one diagonal SCALE, so no coefficient or physical prototype gate is needed. + +## Complete price + +The endpoints spend the same old paid pair, so at most one edit can be priced. The complete 17-copy paid delta is `{1:−17,4:−17,5:+17}`, taking 110,519 paid positions to 110,502. The 22,461 productive positions, rank surplus 1,424 and the exact signed caller stay fixed. At the old crossing the directed gross upper is 0.154513811062998 raw. The complete positive probe lower before support is approximately 0.1541262781727697. The complete fixed-target upper at κ = 0.0040075385047236 is approximately −139.59718548090817. One extra paid rank-one charge exceeds the one-edit allowance. The support exclusion gives zero realized savings. + +The retained premises are native all-column action, owned erasure, compiler, precision/tape and analytic recovery. The scope fixes the owner, its exterior state and both old endpoint cuts. Other insertion clocks, new donor routing, or changed producer and recovery maps require separate evidence. diff --git a/research/p104-owned-two-write-aggregate-bound/PROVENANCE.json b/research/p104-owned-two-write-aggregate-bound/PROVENANCE.json new file mode 100644 index 0000000000..ab604e113b --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/PROVENANCE.json @@ -0,0 +1,68 @@ +{ + "derived_inputs": { + "inputs/BENCHMARK.json": { + "receipt": "inputs/ADMITTED.json", + "relationship": "Exact admission SHA, head, and crossing checked at replay" + }, + "inputs/R92-PRICE.json.gz": { + "compression": "gzip", + "key": "R92-PRICE.json", + "receipt": "inputs/PR7362-SHA256.json" + } + }, + "files": { + "inputs/7334-WORD.json.gz": { + "commit": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "git_blob": "73f43007192eb5a38eb5abb591b871df3e52c7cd", + "path": "research/p104-helper-319-fused-return/WORD.json.gz", + "sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "source": "https://github.com/Clear1nsight/integer-mult-bounds/blob/aaeec8c0acf01e99a5f331ef363a698d9c084ace/research/p104-helper-319-fused-return/WORD.json.gz", + "uncompress": false + }, + "inputs/ADMITTED.json": { + "commit": "349996445176e934ffb3c76813adcd230ca8f783", + "git_blob": "464c89e45c4eca230c099e8bac784a90200a5069", + "path": "research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "sha256": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/349996445176e934ffb3c76813adcd230ca8f783/research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "uncompress": false + }, + "inputs/PR7362-SHA256.json": { + "commit": "5eec7ed633dcf9b9bbc95552aa653da296f863fb", + "git_blob": "b1486e0b5cfe4535f381ed26f7bce4aee21d8a43", + "path": "research/p104-rank-two-virtual-cut-bound/receipts/SHA256.json", + "sha256": "2c90ca39b0f075cc4b3ec9e90c66fde473465e7bb50cf1db9a820d3a29556c0b", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/5eec7ed633dcf9b9bbc95552aa653da296f863fb/research/p104-rank-two-virtual-cut-bound/receipts/SHA256.json" + }, + "inputs/R80-REVERSE.json": { + "commit": "f92b4c999204e0437dc89359f87fc7be3ecdd12e", + "git_blob": "8e23bd56fa820905337d68d3dc6c20229337a55a", + "path": "research/p104-owned-move-chronology-bound/receipts/R80-REVERSE.json", + "sha256": "12c31ae16b9a364fd84c16d2f76cee873ab279984eb88e1cf1568be905c8f010", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/f92b4c999204e0437dc89359f87fc7be3ecdd12e/research/p104-owned-move-chronology-bound/receipts/R80-REVERSE.json" + }, + "inputs/donor_span.py": { + "commit": "403e0d388c35e83b15eab5bba67be563b33d5a8a", + "git_blob": "46e4621b69bba513f327de53153298e7f4ca0645", + "path": "research/p104-owned-add-source-span-bound/engines/forward.py", + "sha256": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/403e0d388c35e83b15eab5bba67be563b33d5a8a/research/p104-owned-add-source-span-bound/engines/forward.py" + }, + "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 + }, + "inputs/reverse_span.py": { + "commit": "403e0d388c35e83b15eab5bba67be563b33d5a8a", + "git_blob": "5efbeac87e3963085149244304614844307c8034", + "path": "research/p104-owned-add-source-span-bound/engines/reverse.py", + "sha256": "f8b48f2ed99d003e20f5b3fb2270603c4edbc3ce9a01484102816aa2710ce9ff", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/403e0d388c35e83b15eab5bba67be563b33d5a8a/research/p104-owned-add-source-span-bound/engines/reverse.py" + } + }, + "schema_version": 1 +} diff --git a/research/p104-owned-two-write-aggregate-bound/README.md b/research/p104-owned-two-write-aggregate-bound/README.md new file mode 100644 index 0000000000..ab0f03e81a --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/README.md @@ -0,0 +1,29 @@ +# Fixed endpoint span bound for one owned two-write aggregate + +**NO VERIFIED GAIN.** Exact Δκ = 0 relative to independently reproduced conditional κ = `0.00364665195644` on #7334 `aaeec8c0acf01e99a5f331ef363a698d9c084ace` with signed #7113 `07a76c5e2738882c0cb322278e56f6cae3c9885d`. [Comparator #7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) · [Signed caller #7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) + +Owner 1531 receives exactly two unobserved signed writes between its paid moves at 41996 and 44242. Moving their sum to either old endpoint would allow a direct rank-five route if that endpoint supplied the same arbitrary-input row. Both exact engines exclude both banks even after granting every other live cocharted row, including owned donors, and the old dirty destination diagonal. Coordinate 244 is zero on all granted rows and −1/2 on the aggregate. [Proof](PROOF.md) · [Exact agreement](receipts/AGREEMENT.json) + +The two placements share one paid debit. The directed saving upper is 0.154513811062998 raw for one compatible edit across 17 caller copies. The realized saving is zero. Two fixed banks exhausted, with no unresolved key in this scope. [Complete price](PROOF.md) + +## Replay + +Use CPython 3.12 with assertions from a clean checkout. + +```sh +python3.12 -I -B research/p104-owned-two-write-aggregate-bound/replay.py +``` + +The standard-library replay authenticates the exact #7354 inventory, #7362 rank-stock manifest, #7334 word and both #7355 proof engines. It regenerates the price, both signed bank receipts and their agreement. Add `--out fresh-directory` to retain the four receipts. Altered inventory, price and word controls reject. [Verification](VERIFICATION.md) · [Provenance](PROVENANCE.json) · [Path-keyed pins](LOCAL-PINS.json) + +## Open next questions + +Could a changed donor path or an explicitly different producer supply coordinate 244 while preserving the remaining lifetime? Start by pinning the changed source and pricing every added paid leg against the one-edit upper. This result fixes both old endpoint cuts, the original owner, the donor paths and the original post-window state. A later-response cancellation or changed-contract construction requires a separate proof and complete invoice. + +## Credit + +#7354 at `f92b4c999204e0437dc89359f87fc7be3ecdd12e` supplies the exact owned-lifetime stock. #7355 at `403e0d388c35e83b15eab5bba67be563b33d5a8a` supplies both span engines and covers a separate later sole-ADD pair on the same owner. #7307 supplies the earlier owned terminal chronology method. [#7354](https://github.com/CrocSwap/integer-mult-bounds/pull/7354) · [#7355](https://github.com/CrocSwap/integer-mult-bounds/pull/7355) · [#7307](https://github.com/CrocSwap/integer-mult-bounds/pull/7307) + +The released role-1531 result includes these paid anchors inside a longer changed-producer route with terminal recovery. The fixed two-endpoint aggregate is a separate target. Campaign Round 112 supplies the analogous two-write check on a public role. #7362 supplies the full paid and productive stock, #7338 the admitted witness receipt and #7298 the directed tariff. [Exact released role-1531 finding](https://github.com/CrocSwap/integer-mult-bounds/discussions/7111#discussioncomment-19554307) · [Campaign discussion](https://github.com/CrocSwap/integer-mult-bounds/discussions/7111) · [#7362](https://github.com/CrocSwap/integer-mult-bounds/pull/7362) · [#7338](https://github.com/CrocSwap/integer-mult-bounds/pull/7338) · [#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) + +OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging. diff --git a/research/p104-owned-two-write-aggregate-bound/SOURCES.json b/research/p104-owned-two-write-aggregate-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-owned-two-write-aggregate-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-two-write-aggregate-bound/TASK.json b/research/p104-owned-two-write-aggregate-bound/TASK.json new file mode 100644 index 0000000000..0bc81f9762 --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "One exact #7334 owned lifetime, role1531, paid pair 41996/44242 and the two exact signed incoming ADDs. Test the old aggregate at the two fixed endpoint banks.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "P104 owned two-write aggregate research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "The paid rank-five fusion has a positive price only if an old endpoint can supply the original signed aggregate and preserve the owned state.", + "budget_minutes": 10, + "evidence": "Both exact engines agree on the 219-coordinate signed aggregate and the same absent coordinate 244 in both fixed endpoint banks, granting the old destination diagonal and all live cocharted donors.", + "open_questions": [ + { + "blocked_by": "Coordinate 244 is absent from every granted row in both old endpoint banks.", + "first_step": "Pin one concrete changed donor path or producer and charge the full new route before trying signed support.", + "question": "Can a separately priced producer or donor-route change supply the missing owned aggregate?", + "why_it_matters": "A lawful fixed-owner fusion would reduce the binding complex paid moment." + } + ], + "original_card": { + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "existing_checks": [ + { + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4133: literal-slot defect", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "status": "author-checked" + }, + { + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4136: uniform commutation gap", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "status": "author-checked" + }, + { + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4140: uniform encoding gap", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "status": "author-checked" + }, + { + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "status": "author-checked" + }, + { + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4154: fiber-tag seam mismatch", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "status": "author-checked" + }, + { + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "status": "reviewed" + } + ], + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "id": "p104-side-correction", + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ] + }, + "outcome": "negative-result", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Tests an owned two-write aggregate at fixed endpoints, distinct from prior terminal-zero/sole-ADD scopes and the longer changed-producer role-1531 work.", + "scope_status": "changed", + "stop_rule": "At most one owner, two banks, 76,466 events and 20 seconds. Stop after an exact exclusion at both banks.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-owned-two-write-aggregate-bound/VERIFICATION.md b/research/p104-owned-two-write-aggregate-bound/VERIFICATION.md new file mode 100644 index 0000000000..44110316cf --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/VERIFICATION.md @@ -0,0 +1,7 @@ +# Verification + +The direct CPython 3.12 package replay exited zero in 4.01 seconds. A relocated Git-free copy with an empty inherited environment exited zero in 4.04 seconds. All four receipts matched byte for byte. Four controls reject changes to the inherited inventory, price input to either bank engine, or native word. + +The independent reverse pass visits all 76,466 events under the two-bank 20-second cap. Both engines agree on the two original signed ADDs, all 219 nonzero aggregate coordinates, both endpoint bank inventories and the common separator. No unresolved bank, suffix, physical candidate or κ gain. + +[Provenance](PROVENANCE.json) · [Replay command](README.md) · [Receipt digests](receipts/SHA256.json) diff --git a/research/p104-owned-two-write-aggregate-bound/VERIFY.json b/research/p104-owned-two-write-aggregate-bound/VERIFY.json new file mode 100644 index 0000000000..f7e57582cd --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Authenticate the exact inventory and word, regenerate directed price, independently reconstruct all signed aggregate coordinates, compare both exclusions and reject altered dependencies.", + "timeout_seconds": 100 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-owned-two-write-aggregate-bound/engines/aggregate.py b/research/p104-owned-two-write-aggregate-bound/engines/aggregate.py new file mode 100644 index 0000000000..d6084feb06 --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/engines/aggregate.py @@ -0,0 +1,143 @@ +"""Test the two frozen cocharted banks for one owned two-write aggregate.""" +from collections import defaultdict +from fractions import Fraction +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from sys import argv +from time import monotonic + +ROOT = Path(__file__).resolve().parents[1] +PINS = { + "plan/PRICE.json": "08a403b6c8d5a3332212042ec69624ab5cf343fb7b6aa6e94f42583653f77912", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/donor_span.py": "4d5306e2c0b7e91c79d22c82e8e760aed2c311979298c558e631975d4d1ae5b1", +} +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + + +def unique(items): + result = dict(items) + if len(result) != len(items): + raise ValueError("duplicate JSON key") + return result + + +def checked(rel): + data = (ROOT / rel).read_bytes() + if sha256(data).hexdigest() != PINS[rel]: + raise ValueError(f"changed dependency {rel}") + return data + + +def touches(event, owner): + return owner in event[1:3] if event[0] in ("ADD", "COPY") else event[1] == owner + + +def legal(value): + return (value != 0 and value.denominator.bit_count() == 1 and value.denominator <= 2**25 + and abs(value.numerator).bit_length() <= 24 and abs(value) + 1 < 2**16) + + +def stop(*_): + raise TimeoutError("20-second hard cap") + + +def test_bank(bank, owner, owner_row, aggregate, engine, deadline): + assert owner not in bank + bank = bank | {owner: owner_row} + axes = set().union(*(row.keys() for row in bank.values())) + absent = next((i for i in sorted(aggregate) if i not in axes), None) + if absent is not None: + return {"status": "coordinate exclusion", "witness": [absent, str(aggregate[absent])]} + exact = engine["solve"](aggregate, bank, deadline) + if exact is None: + raise TimeoutError("exact rational fallback cap") + match = exact["matching_coefficients"] + if match is None: + return {"status": "rational exclusion", "exact": exact} + donor = {int(r): Fraction(v) for r, v in match.items()} + scale = 1 + donor.pop(owner, Fraction(0)) + eligible = len(donor) <= 2 and all(legal(v) for v in donor.values()) and (scale == 1 or legal(scale)) + return {"status": "exact coefficient survivor" if eligible else "coefficient gate unresolved", + "exact": exact, "destination_scale": str(scale)} + + +def main(): + assert __debug__ + price = loads(checked("plan/PRICE.json"), object_pairs_hook=unique) + checked("inputs/donor_span.py") + engine = run_path(str(ROOT / "inputs/donor_span.py")) + controls = engine["controls"]() + cancellation = {4: Fraction(1, 2)} + engine["axpy"](cancellation, {4: Fraction(1)}, Fraction(-1, 2)) + assert not cancellation and legal(Fraction(1, 4)) and not legal(Fraction(1, 3)) + controls.append("signed two-write cancellation and coefficient gate") + if argv[1:] == ["--controls-only"]: + print(dumps({"controls": controls, "frozen_bank_cuts": price["bank_cuts"]}, sort_keys=True)) + return 0 + assert not argv[1:] + signal(SIGALRM, stop) + alarm(20) + deadline = monotonic() + 18 + results, aggregate, old_adds = [], {}, [] + timeout = None + try: + payload = decompress(checked("inputs/7334-WORD.json.gz")) + assert sha256(payload).hexdigest() == PAYLOAD + word = loads(payload, object_pairs_hook=unique) + tape = word["program"] + assert len(tape) == price["caps"]["events"] + row = price["row"] + f, g, owner = row["key"] + a, b, c = row["charts"] + birth, clear = row["lifetime"] + assert owner >= word["public"] and birth < f < g < clear + assert tape[birth][:2] == ["INIT", owner] and tape[clear][:2] == ["CLEAR", owner] + assert tape[f] == ["MOVE", owner, a, b, True] and tape[g] == ["MOVE", owner, b, c, True] + assert [t for t in range(birth + 1, clear) if tape[t][:2] == ["INIT", owner] + or tape[t][:2] == ["CLEAR", owner]] == [] + times = [t for t in range(f + 1, g) if touches(tape[t], owner)] + assert times == [41997, 44241] + requirements, targets = defaultdict(set), defaultdict(set) + targets[f].add(owner) + for cut, chart in price["bank_cuts"]: + requirements[cut].add((chart, owner)) + for t in times: + op, dest, source, coefficient, chart = tape[t] + assert op == "ADD" and dest == owner and source != owner and chart == b + old_adds.append([t, tape[t]]) + requirements[t].add((b, -1)) + targets[t].add(source) + banks, values = engine["snapshot"](word, requirements, targets, deadline) + for t, (_, _, source, coefficient, _) in old_adds: + if (t, source) not in values: + raise TimeoutError("old signed source snapshot cap") + assert banks[t, b, -1][source] == values[t, source] + engine["axpy"](aggregate, values[t, source], Fraction(coefficient)) + for cut, chart in price["bank_cuts"]: + if (cut, chart, owner) not in banks or (f, owner) not in values or monotonic() >= deadline: + raise TimeoutError("endpoint snapshot or exact span cap") + bank = banks[cut, chart, owner] + proof = test_bank(bank, owner, values[f, owner], aggregate, engine, deadline) + results.append({"key": [cut, chart], "read_only_donors": sorted(bank), + "old_owner_diagonal_clock": f, **proof}) + except TimeoutError as error: + timeout = str(error) + finally: + alarm(0) + completed = [r["key"] for r in results] + print(dumps({ + "pins": PINS, "controls": controls, "head": price["head"], "caller": price["caller"], + "old_adds": old_adds, "aggregate": {i: str(v) for i, v in aggregate.items()}, + "results": results, "unvisited": [k for k in price["bank_cuts"] if k not in completed], + "timeout": timeout, + }, sort_keys=True, indent=2)) + return 124 if timeout else 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/p104-owned-two-write-aggregate-bound/engines/aggregate_covectors.py b/research/p104-owned-two-write-aggregate-bound/engines/aggregate_covectors.py new file mode 100644 index 0000000000..3024ce1460 --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/engines/aggregate_covectors.py @@ -0,0 +1,220 @@ +"""Reverse normalized covectors for two endpoint banks of the frozen owned aggregate.""" +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 lcm +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from time import monotonic + +ROOT=Path(__file__).resolve().parents[1] +PINS={ + "plan/PRICE.json":"08a403b6c8d5a3332212042ec69624ab5cf343fb7b6aa6e94f42583653f77912", + "inputs/7334-WORD.json.gz":"4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "independent/reused/reverse_span.py":"f8b48f2ed99d003e20f5b3fb2270603c4edbc3ce9a01484102816aa2710ce9ff", +} +OWNER,FIRST,LAST,BIRTH,CLEAR=1531,41996,44242,32607,44247 +ADDS=(41997,44241) +BANKS=((41996,594),(44242,534)) +EVENTS,SECONDS=76466,20 + + +def checked(root,name): + raw=(root/name).read_bytes() + if sha256(raw).hexdigest()!=PINS[name]: + raise ValueError("changed dependency "+name) + return raw + + +def freeze(price): + assert price["head"]=="aaeec8c0acf01e99a5f331ef363a698d9c084ace" + assert price["caller"]=="07a76c5e2738882c0cb322278e56f6cae3c9885d" + assert price["word_sha256"]==PINS["inputs/7334-WORD.json.gz"] + assert price["caps"]=={"banks":2,"events":EVENTS,"prototype_seconds":120,"seconds":SECONDS,"windows":1} + assert price["bank_cuts"]==[list(key) for key in BANKS] + assert price["row"]["key"]==[FIRST,LAST,OWNER] and price["row"]["lifetime"]==[BIRTH,CLEAR] + assert price["row"]["charts"]==[594,117,534] + assert price["row"]["paid_ranks"]==[4,1] + assert price["row"]["intervening"]==[[t,"ADD","destination"] for t in ADDS] + + +def backward(word,engine,deadline,progress): + tape,n,m,frames=(word[k] for k in ("program","public","owned_fields","frames")) + assert (len(tape),n,m)==(EVENTS,1501,68) + assert tape[BIRTH][:2]==["INIT",OWNER] and tape[CLEAR][:2]==["CLEAR",OWNER] + assert tape[FIRST]==["MOVE",OWNER,594,117,True] and tape[LAST]==["MOVE",OWNER,117,534,True] + assert all(tape[t][:2]==["ADD",OWNER] and tape[t][-1]==117 for t in ADDS) + assert tuple(len(frames[c]) for c in (594,117,534))==(1,5,6) + + @cache + def space(chart): + result={0} + for axis in frames[chart]: + assert axis not in result + result|={axis^u for u in result} + return result + + chart=word["final"]+[None]*m + fresh_copy=set() + empty=({},1) + adj=[empty]*(n+m) + captures={} + sources={} + banks={} + owned_incidence=[] + births=[] + scale,coefficient=engine["sum_scaled"],engine["coefficient"] + + def observe(clock,role): + key=(clock,role) + assert chart[role] is not None and key not in captures + i=len(captures) + captures[key]=i + adj[role]=scale(adj[role],({i:1},1),(1,1)) + return i + + for t in range(EVENTS-1,-1,-1): + progress["last_unvisited"]=t + if t%128==0 and monotonic()>=deadline: + raise TimeoutError("reverse event cap") + op,d,*args=tape[t] + assert 0<=d=n) + assert space(a)=n and chart[d]==args[0] + chart[d]=None + fresh_copy.discard(d) + adj[d]=empty + elif op=="CLEAR": + assert d>=n and chart[d] is None + chart[d]=args[0] + adj[d]=empty + else: + assert op in ("ADD","COPY","SCALE") and chart[d]==args[-1] + q=coefficient(args[-2]) + if op=="SCALE": + adj[d]=scale(empty,adj[d],q) + else: + s=args[0] + assert s!=d and chart[s]==chart[d] + adj[s]=scale(adj[s],adj[d],q) + if op=="COPY": + assert d>=n + fresh_copy.add(d) + adj[d]=empty + if t in ADDS: + sources[t]=observe(t,tape[t][2]) + if t==FIRST: + observe(t,OWNER) + for cut,coframe in BANKS: + if t==cut: + banks[(cut,coframe)]={r:observe(t,r) for r,c in enumerate(chart) if c==coframe and r!=OWNER} + progress["events"]+=1 + + assert chart==word["initial"]+[None]*m and not fresh_copy + assert not any(v for v,_ in adj[n:]) + assert tuple(reversed(owned_incidence))==ADDS and births==[CLEAR,BIRTH] + progress["last_unvisited"]=None + by_row=[[] for _ in captures] + for coord,(entries,den) in enumerate(adj[:n]): + for i,a in entries.items(): + by_row[i].append((coord,a,den)) + rows=[] + for entries in by_row: + den=lcm(*(d for _,_,d in entries)) + rows.append(engine["normalized"]({j:a*(den//d) for j,a,d in entries},den)) + return sources,banks,rows,captures[FIRST,OWNER] + + +def certify(word,sources,banks,rows,owner_index,engine,deadline,out): + tape=word["program"] + n=word["public"] + aggregate=({},1) + for t in ADDS: + q=engine["coefficient"](tape[t][3]) + aggregate=engine["sum_scaled"](aggregate,rows[sources[t]],q) + for key in BANKS: + if monotonic()>=deadline: + raise TimeoutError("two-bank span cap") + donors=banks[key] + public=[r for r in donors if r=n] + bank=[(r,rows[i]) for r,i in donors.items()]+[(OWNER,rows[owner_index])] + proof=engine["exact_span"](bank,aggregate) + if proof["status"]=="absent_exterior_coordinate": + proof["separating_covector"]={proof["coordinate"]:"1"} + elif proof["status"]=="exact_span": + coeffs={r:Fraction(v) for r,v in proof["coefficients"].items()} + scale=1+coeffs.pop(OWNER,Fraction(0)) + legal=lambda v: bool(v and v.denominator.bit_count()==1 and v.denominator<=2**25 and + abs(v.numerator).bit_length()<=24 and abs(v)+1<2**16) + proof["destination_scale"]=str(scale) + proof["legal_sparse_representation"]=len(coeffs)<=2 and legal(scale) and all(map(legal,coeffs.values())) + out.append(dict(key=key,read_only_public=public,read_only_owned=owned,old_owner_diagonal_clock=FIRST, + proof=proof)) + return aggregate + + +def main(): + parser=ArgumentParser() + parser.add_argument("--root",type=Path,default=ROOT) + parser.add_argument("--controls-only",action="store_true") + args=parser.parse_args() + assert __debug__ + name="independent/reused/reverse_span.py" + checked(args.root,name) + engine=run_path(str(args.root/name)) + price=loads(checked(args.root,"plan/PRICE.json"),object_pairs_hook=engine["unique"]) + freeze(price) + tests=engine["controls"]() + assert engine["sum_scaled"](({2:1},2),({2:1},1),(-1,2))==({},1) + assert engine["sum_scaled"](({2:1},2),({2:1},1),(1,2))==({2:1},1) + tests+=["signed zero aggregate","sign mutation produces nonzero aggregate"] + if args.controls_only: + print(dumps({"controls":tests,"banks":BANKS},sort_keys=True)) + return 0 + + def stop(*_): + raise TimeoutError("hard 20-second cap") + + signal(SIGALRM,stop) + alarm(SECONDS) + deadline=monotonic()+18 + out,old_adds,aggregate,timeout=[],[],None,None + progress={"events":0,"last_unvisited":EVENTS-1} + try: + payload=decompress(checked(args.root,"inputs/7334-WORD.json.gz")) + assert sha256(payload).hexdigest()=="9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + word=loads(payload,object_pairs_hook=engine["unique"]) + old_adds=[[t,word["program"][t]] for t in ADDS] + sources,banks,rows,owner_index=backward(word,engine,deadline,progress) + aggregate=certify(word,sources,banks,rows,owner_index,engine,deadline,out) + except TimeoutError as exc: + timeout=str(exc) + finally: + alarm(0) + projected=None if aggregate is None else {i:str(Fraction(v,aggregate[1])) for i,v in aggregate[0].items()} + completed={r["key"] for r in out} + print(dumps(dict(head=price["head"],caller=price["caller"],pins=PINS,controls=tests,caps=price["caps"], + progress=progress,old_adds=old_adds,aggregate=projected,results=out, + counts=Counter(r["proof"]["status"] for r in out), + unvisited=[k for k in BANKS if k not in completed],timeout=timeout),indent=2,sort_keys=True)) + return 2 if timeout else 0 + + +if __name__=="__main__": + raise SystemExit(main()) diff --git a/research/p104-owned-two-write-aggregate-bound/engines/compare.py b/research/p104-owned-two-write-aggregate-bound/engines/compare.py new file mode 100644 index 0000000000..fbcddb2620 --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/engines/compare.py @@ -0,0 +1,46 @@ +"""Compare the two exact R122 aggregate and endpoint bank receipts.""" +from hashlib import sha256 +from json import dumps,loads +from pathlib import Path + +ROOT=Path(__file__).resolve().parents[1] +PINS={ + "lead/RESULT.json":"6d040aae3e99a8261152c17965b692b964d18ed7139c7a003da50934ec8d2098", + "independent/RESULT.json":"12d42fc77b2de5d955744259741e63d0e4fbe0735ca290103c6a024557ec6996", +} + + +def checked(name): + raw=(ROOT/name).read_bytes() + if sha256(raw).hexdigest()!=PINS[name]: + raise ValueError("changed dependency "+name) + return loads(raw) + + +def main(): + assert __debug__ + primary,reverse=map(checked,PINS) + assert (primary["head"],primary["caller"])==(reverse["head"],reverse["caller"]) + for key in ("plan/PRICE.json","inputs/7334-WORD.json.gz"): + assert primary["pins"][key]==reverse["pins"][key] + assert primary["old_adds"]==reverse["old_adds"] + assert primary["aggregate"]==reverse["aggregate"] and len(reverse["aggregate"])==219 + assert not primary["unvisited"] and not reverse["unvisited"] + assert primary["timeout"] is reverse["timeout"] is None + assert reverse["progress"]=={"events":76466,"last_unvisited":None} + banks=[] + for a,b in zip(primary["results"],reverse["results"],strict=True): + assert a["key"]==b["key"] and a["old_owner_diagonal_clock"]==b["old_owner_diagonal_clock"]==41996 + assert a["read_only_donors"]==sorted(b["read_only_public"]+b["read_only_owned"]) + assert a["status"]=="coordinate exclusion" and b["proof"]["status"]=="absent_exterior_coordinate" + assert a["witness"]==[b["proof"]["coordinate"],b["proof"]["target_coefficient"]]==[244,"-1/2"] + banks.append(dict(key=a["key"],read_only_donors=a["read_only_donors"], + donor_rank=b["proof"]["donor_rank"],augmented_rank=b["proof"]["augmented_rank"])) + assert len(banks)==2 + print(dumps(dict(pins=PINS,bank_agreement=banks,old_adds=reverse["old_adds"], + aggregate_nonzero_coordinates=219,common_separator={"244":"1"},separator_value="-1/2",unresolved=0), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-owned-two-write-aggregate-bound/engines/quote.py b/research/p104-owned-two-write-aggregate-bound/engines/quote.py new file mode 100644 index 0000000000..e009de608d --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/engines/quote.py @@ -0,0 +1,79 @@ +"""Preprice one owned lifetime with two unobserved intermediate writes.""" +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().parents[1] +PINS = { + "inputs/R80-REVERSE.json": "12c31ae16b9a364fd84c16d2f76cee873ab279984eb88e1cf1568be905c8f010", + "inputs/BENCHMARK.json": "004331cff6ca8644489d7b7084e5c67439d74a2d283e4d64a9fdb9f88679253d", + "inputs/R92-PRICE.json": "05d7a5ebdd2eeedd6c8f534e8e2eeac22484daf9f387f4a6b88cc9eed22a6b8f", + "inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", +} + + +def unique(items): + doc = dict(items) + if len(doc) != len(items): + raise ValueError("duplicate JSON key") + return doc + + +def hist(data): + return Counter({int(rank): count for rank, count in data.items()}) + + +def main(): + assert __debug__ + docs = [] + for rel, expected in PINS.items(): + raw = (ROOT / rel).read_bytes() + if sha256(raw).hexdigest() != expected: + raise ValueError(f"changed dependency {rel}") + if rel.endswith(".json"): + docs.append(loads(raw, object_pairs_hook=unique)) + inventory, bench, prior = docs + assert inventory["complete"] and inventory["neighbor_pairs"] == len(inventory["pairs"]) == 9 + assert inventory["head"] == bench["head"] == prior["head"] + assert inventory["word_sha256"] == prior["word_sha256"] + row, = [x for x in inventory["pairs"] if not x["opposite_direction"] + and len(x["intervening"]) == 2 + and all(op == "ADD" and access == "destination" for _, op, access in x["intervening"])] + assert row["key"] == [41996, 44242, 1531] and row["lifetime"] == [32607, 44247] + assert row["charts"] == [594, 117, 534] and row["paid_ranks"] == [4, 1] + assert [x[0] for x in row["intervening"]] == [41997, 44241] + paid, target = hist(prior["old_paid"]), hist(prior["old_targets"]) + old = target.copy() + old.subtract(paid) + delta = {1: -17, 4: -17, 5: 17} + paid.update(delta) + new = target.copy() + new.subtract(paid) + assert sum(paid.values()) == 110502 and sum(target.values()) == 22461 + assert sum(k * v for k, v in old.items()) == sum(k * v for k, v in new.items()) == 1424 + at, probe, fixed = map(Fraction, (prior["old_crossing_upper"], prior["probe"], prior["moonshot"])) + assert at == Fraction(bench["crossing"][1]) and at < probe < Fraction(prior["retained_bit_premise"]) + cost = run_path(str(ROOT / "inputs/pricing.py"))["cost"] + net = cost({k: -v for k, v in delta.items()}, at) + probe_margin = cost(new, probe) + assert probe_margin[0] > 0 and cost(new, at)[1] - 1 < 0 + print(dumps({ + "head": bench["head"], "caller": prior["caller_head"], "word_sha256": prior["word_sha256"], + "pins": PINS, "old_crossing_upper": str(at), "probe": str(probe), + "row": row, "bank_cuts": [[41996, 594], [44242, 534]], "compatible_edits": 1, + "paid_delta": delta, "paid": sum(paid.values()), "productive": sum(target.values()), + "surplus": 1424, "gain_at_old_crossing": list(map(str, net)), + "complete_probe_margin": list(map(str, probe_margin)), + "complete_fixed_target_upper": str(cost(new, fixed)[1]), + "extra_rank_one_upper": str(cost(new, at)[1] - 1), + "caps": {"windows": 1, "banks": 2, "events": 76466, "seconds": 20, + "prototype_seconds": 120}, + "scope": "One owned lifetime with two unobserved writes, fixed aggregate at one old endpoint.", + }, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-owned-two-write-aggregate-bound/inputs/7334-WORD.json.gz b/research/p104-owned-two-write-aggregate-bound/inputs/7334-WORD.json.gz new file mode 100644 index 0000000000..73f4300719 Binary files /dev/null and b/research/p104-owned-two-write-aggregate-bound/inputs/7334-WORD.json.gz differ diff --git a/research/p104-owned-two-write-aggregate-bound/inputs/ADMITTED.json b/research/p104-owned-two-write-aggregate-bound/inputs/ADMITTED.json new file mode 100644 index 0000000000..464c89e45c --- /dev/null +++ b/research/p104-owned-two-write-aggregate-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-two-write-aggregate-bound/inputs/BENCHMARK.json b/research/p104-owned-two-write-aggregate-bound/inputs/BENCHMARK.json new file mode 100644 index 0000000000..3cadb16667 --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/inputs/BENCHMARK.json @@ -0,0 +1,67 @@ +{ + "admission_sha256": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "checks": { + "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" + }, + "crossing": [ + "0.00364665195644044790699554028334161", + "0.00364665195644044790699554028334162" + ], + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "kappa": "0.00364665195644", + "main": "e54523517d0f03e58352e647c403a5af3e525a57", + "package_sha256": { + "research/p104-helper-319-fused-return/EARLY-RESULT.json": "ad1ca9b2e2febbf80d9bf8b6ceef14ff90fcc29ef9358310e551628eb1706649", + "research/p104-helper-319-fused-return/ENVIRONMENT.json": "1a4a755aa63e3c25c09a493550a0d13a58e23f8b50083d3f81ce3716581d8ad3", + "research/p104-helper-319-fused-return/INPUTS.json": "abedac59097a1c35c27d91cbdb07207bc562a64743bc406d13c94a8bc970592d", + "research/p104-helper-319-fused-return/NATIVE-RESULT.json": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812", + "research/p104-helper-319-fused-return/NOTICE": "fd84c06a1c3343a1802808741c0863ffcec031f5c98eb78ddc350a747d3e2ddc", + "research/p104-helper-319-fused-return/PROOF.md": "560de573bfd4563c16ca3c7308fa729b4188fabe802d8830f343c3873f75b59d", + "research/p104-helper-319-fused-return/PROPOSED-CLAIM.json": "6e31241944c123d2bd4aa8bc94d833b44b3d889bd6d9aafc579108f416b45f03", + "research/p104-helper-319-fused-return/README.md": "b4db0eb83ab6a2f7151bed2da955a487f4816ec9d1976eccc21e54c2725490b0", + "research/p104-helper-319-fused-return/REFERENCE.json": "3e66e054b803551f18b8670da0b2990a7d0eeb689dfc45b56dbcba295551da70", + "research/p104-helper-319-fused-return/REPLAY.txt": "230984f4b8206ae4d0c0f18fbba86ff43a1a9623f8ed337cf1285360f9a67c0c", + "research/p104-helper-319-fused-return/RESULT.json": "7f2d587c59f063b01f1e8b320084a7f0943f2f05d65e3e0f5e80448c6c8e8194", + "research/p104-helper-319-fused-return/SOURCES.json": "ac7b4473035af648d6073e78b6c39675e706e8194b346bb55ed62a0adc81d593", + "research/p104-helper-319-fused-return/TASK.json": "cceea066802e1175b1a78f65e8bff4677ce09e87fd7686265d63ee7236b32b1a", + "research/p104-helper-319-fused-return/VERIFY.json": "ede7dd2dd3733b9a73f72af9dd7edfe819b49b859c5c76e227ec82cb9c220513", + "research/p104-helper-319-fused-return/WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "research/p104-helper-319-fused-return/adapt.py": "a9237d6dff55ce13c1e1d10159f592f35a0a79eb0a3c054063ba39665ba96296", + "research/p104-helper-319-fused-return/construct.py": "ecb39578063d7f09153a85370a3b9bb7cbf8b36ff9891033a1cce7a2fe7f7fda", + "research/p104-helper-319-fused-return/derive_grid.py": "ceb7a44ef19d72a16db7b43c65c85910d965499d1715436011de32af5d39dbb0", + "research/p104-helper-319-fused-return/frontier.py": "c5f5e4e1f1f2d189f4816291764f1966c8165a7090d8624f72828199400333c2", + "research/p104-helper-319-fused-return/inputs/pr7314.tar.gz": "0589953b3886d96eacf3bda3d38d8d574bb739fba1056af7f32f56047b6061e2", + "research/p104-helper-319-fused-return/packing_reference.py": "c977cf46a9498d013145f74186081ec67674d11473295df399bca61f8a4e7382", + "research/p104-helper-319-fused-return/price.py": "6ec0f568b3491f3713ffabb2a8cc7b467339da175c8dcaa76369fbc3a9881029", + "research/p104-helper-319-fused-return/source.py": "a2be5bb28c7a9c9d528b8bae0d9ef99636bb8fabf80d66b7f8d3084de68358aa", + "research/p104-helper-319-fused-return/verify_caller.py": "6ef60923041d97f77f8291f568f2e81492af09021f4e1065054cf5376cbff861", + "research/p104-helper-319-fused-return/verify_early.py": "94e0e8bac205eed91f9f1f0ada110479a067ee7a3cd73d38d231947a0d46c0f9", + "research/p104-helper-319-fused-return/verify_native.py": "592729b40642957a4d2766c386d73925a1044d2b4eedce5176d988b8cef3b134" + }, + "receipt_sha256": { + "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_tree": "fa98712a459b20c10240450097c87de433f8a750", + "status": "exact-complete-receipt-reused" +} diff --git a/research/p104-owned-two-write-aggregate-bound/inputs/PR7362-SHA256.json b/research/p104-owned-two-write-aggregate-bound/inputs/PR7362-SHA256.json new file mode 100644 index 0000000000..b1486e0b5c --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/inputs/PR7362-SHA256.json @@ -0,0 +1,11 @@ +{ + "R92-COMPARE.json": "92bd567e3203a2cbc2e0c508bf921966c59ead267c1f373f7534a4a50cb208ac", + "R92-GEOMETRY.json": "e9f93f3271855012b2de705c70f186f78c31a369d28110e92c5f2ffadae209b3", + "R92-GUARDS.json": "c23e9c74b3479e4af6c452eeb73e000878148ec385560a0642433a1c5bac4a07", + "R92-PRICE.json": "05d7a5ebdd2eeedd6c8f534e8e2eeac22484daf9f387f4a6b88cc9eed22a6b8f", + "R92-REVERSE.json": "f8e56b109352e07dfb8203bdbe42a10cb94374246b4cd419421e4f52e2730c4a", + "R93-COMPARE.json": "8a1f52179e5d457aa729714b0b79577894c1e22ab74a8b2f700838f471ffceb1", + "R93-MODULAR.json": "01ad2a656e69699b80b56d63cdf82448e424cd1c6e67636d53c079a6f03f55a5", + "R93-PRICE.json": "c108a061c6c03306a99a6fbafe919208954a7479ae28fb8a8fbf45d9832e6144", + "R93-RATIONAL.json": "2800af56efe23f7420a12f0713a659cd4fa4a3fb7c58449749ef697097ccccbf" +} diff --git a/research/p104-owned-two-write-aggregate-bound/inputs/R80-REVERSE.json b/research/p104-owned-two-write-aggregate-bound/inputs/R80-REVERSE.json new file mode 100644 index 0000000000..8e23bd56fa --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/inputs/R80-REVERSE.json @@ -0,0 +1,1240 @@ +{ + "case_cap": 4, + "complete": true, + "contact_free_diagnostic_keys": [], + "controls": [ + "nonzero_signed_scale", + "exact_return_diagnostic", + "incomparable_outer_charts", + "source_add_barrier", + "destination_copy_barrier", + "owner_reuse_barrier" + ], + "geometry_tested": 0, + "hard_seconds": 20, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "input_sha256": { + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "price/PRICE.json": "76926ec9ff997159d281e0363326edb2e1aff8c530b041f361565030588e02cf" + }, + "lifetimes": 73, + "literal_events": 76466, + "moves": [ + { + "birth": 30522, + "charts": [ + 477, + 1090 + ], + "clear": 45376, + "clock": 30529, + "next_contact": [ + 30530, + "ADD", + "destination" + ], + "owner": 1510, + "rank": 4 + }, + { + "birth": 30532, + "charts": [ + 1090, + 470 + ], + "clear": 45348, + "clock": 30537, + "next_contact": [ + 30538, + "ADD", + "source" + ], + "owner": 1520, + "rank": 1 + }, + { + "birth": 30545, + "charts": [ + 470, + 601 + ], + "clear": 39889, + "clock": 30551, + "next_contact": [ + 30552, + "ADD", + "source" + ], + "owner": 1521, + "rank": 2 + }, + { + "birth": 30461, + "charts": [ + 601, + 470 + ], + "clear": 39888, + "clock": 30581, + "next_contact": [ + 30582, + "ADD", + "source" + ], + "owner": 1547, + "rank": 2 + }, + { + "birth": 30577, + "charts": [ + 470, + 1090 + ], + "clear": 41485, + "clock": 30593, + "next_contact": [ + 30594, + "ADD", + "source" + ], + "owner": 1546, + "rank": 1 + }, + { + "birth": 32923, + "charts": [ + 267, + 1091 + ], + "clear": 38909, + "clock": 32939, + "next_contact": [ + 32940, + "ADD", + "source" + ], + "owner": 1529, + "rank": 4 + }, + { + "birth": 33112, + "charts": [ + 543, + 541 + ], + "clear": 39499, + "clock": 33125, + "next_contact": [ + 33126, + "ADD", + "source" + ], + "owner": 1528, + "rank": 1 + }, + { + "birth": 33130, + "charts": [ + 1091, + 260 + ], + "clear": 45353, + "clock": 33133, + "next_contact": [ + 33134, + "ADD", + "source" + ], + "owner": 1514, + "rank": 1 + }, + { + "birth": 33136, + "charts": [ + 541, + 534 + ], + "clear": 43333, + "clock": 33140, + "next_contact": [ + 33141, + "ADD", + "source" + ], + "owner": 1502, + "rank": 1 + }, + { + "birth": 33136, + "charts": [ + 534, + 117 + ], + "clear": 43333, + "clock": 33142, + "next_contact": [ + 33143, + "ADD", + "source" + ], + "owner": 1502, + "rank": 1 + }, + { + "birth": 33136, + "charts": [ + 117, + 594 + ], + "clear": 43333, + "clock": 33149, + "next_contact": [ + 33150, + "ADD", + "source" + ], + "owner": 1502, + "rank": 4 + }, + { + "birth": 34511, + "charts": [ + 517, + 243 + ], + "clear": 45387, + "clock": 34515, + "next_contact": [ + 34516, + "ADD", + "destination" + ], + "owner": 1513, + "rank": 4 + }, + { + "birth": 34517, + "charts": [ + 243, + 431 + ], + "clear": 45359, + "clock": 34519, + "next_contact": [ + 34520, + "ADD", + "source" + ], + "owner": 1518, + "rank": 1 + }, + { + "birth": 35134, + "charts": [ + 599, + 260 + ], + "clear": 38143, + "clock": 35143, + "next_contact": [ + 35144, + "ADD", + "source" + ], + "owner": 1541, + "rank": 2 + }, + { + "birth": 34522, + "charts": [ + 431, + 600 + ], + "clear": 39858, + "clock": 35434, + "next_contact": [ + 35435, + "ADD", + "source" + ], + "owner": 1519, + "rank": 2 + }, + { + "birth": 35406, + "charts": [ + 600, + 431 + ], + "clear": 39854, + "clock": 35439, + "next_contact": [ + 35440, + "ADD", + "source" + ], + "owner": 1545, + "rank": 2 + }, + { + "birth": 35413, + "charts": [ + 431, + 243 + ], + "clear": 39856, + "clock": 35443, + "next_contact": [ + 35444, + "ADD", + "source" + ], + "owner": 1544, + "rank": 1 + }, + { + "birth": 36313, + "charts": [ + 518, + 240 + ], + "clear": 45373, + "clock": 36315, + "next_contact": [ + 36316, + "ADD", + "destination" + ], + "owner": 1512, + "rank": 4 + }, + { + "birth": 36317, + "charts": [ + 240, + 394 + ], + "clear": 45372, + "clock": 36319, + "next_contact": [ + 36320, + "ADD", + "source" + ], + "owner": 1516, + "rank": 1 + }, + { + "birth": 36322, + "charts": [ + 394, + 598 + ], + "clear": 39836, + "clock": 36327, + "next_contact": [ + 36328, + "ADD", + "source" + ], + "owner": 1517, + "rank": 2 + }, + { + "birth": 36166, + "charts": [ + 598, + 394 + ], + "clear": 39835, + "clock": 36337, + "next_contact": [ + 36338, + "ADD", + "source" + ], + "owner": 1543, + "rank": 2 + }, + { + "birth": 36171, + "charts": [ + 394, + 240 + ], + "clear": 39984, + "clock": 36349, + "next_contact": [ + 36350, + "ADD", + "source" + ], + "owner": 1542, + "rank": 1 + }, + { + "birth": 35414, + "charts": [ + 243, + 517 + ], + "clear": 39857, + "clock": 39544, + "next_contact": [ + 39545, + "ADD", + "source" + ], + "owner": 1539, + "rank": 4 + }, + { + "birth": 36172, + "charts": [ + 240, + 518 + ], + "clear": 39985, + "clock": 39572, + "next_contact": [ + 39573, + "ADD", + "source" + ], + "owner": 1538, + "rank": 4 + }, + { + "birth": 39093, + "charts": [ + 531, + 529 + ], + "clear": 39721, + "clock": 39718, + "next_contact": [ + 39719, + "ADD", + "source" + ], + "owner": 1526, + "rank": 1 + }, + { + "birth": 37951, + "charts": [ + 529, + 531 + ], + "clear": 39779, + "clock": 39776, + "next_contact": [ + 39777, + "ADD", + "source" + ], + "owner": 1548, + "rank": 1 + }, + { + "birth": 39802, + "charts": [ + 529, + 520 + ], + "clear": 39887, + "clock": 39805, + "next_contact": [ + 39806, + "ADD", + "source" + ], + "owner": 1503, + "rank": 1 + }, + { + "birth": 39802, + "charts": [ + 520, + 595 + ], + "clear": 39887, + "clock": 39811, + "next_contact": [ + 39812, + "ADD", + "source" + ], + "owner": 1503, + "rank": 5 + }, + { + "birth": 39841, + "charts": [ + 260, + 599 + ], + "clear": 39852, + "clock": 39844, + "next_contact": [ + 39845, + "ADD", + "source" + ], + "owner": 1515, + "rank": 2 + }, + { + "birth": 38119, + "charts": [ + 595, + 520 + ], + "clear": 39878, + "clock": 39866, + "next_contact": [ + 39867, + "ADD", + "destination" + ], + "owner": 1532, + "rank": 5 + }, + { + "birth": 38119, + "charts": [ + 520, + 529 + ], + "clear": 39878, + "clock": 39875, + "next_contact": [ + 39876, + "SCALE", + "SCALE" + ], + "owner": 1532, + "rank": 1 + }, + { + "birth": 38021, + "charts": [ + 549, + 559 + ], + "clear": 40544, + "clock": 40529, + "next_contact": [ + 40530, + "ADD", + "source" + ], + "owner": 1549, + "rank": 1 + }, + { + "birth": 39564, + "charts": [ + 559, + 549 + ], + "clear": 40549, + "clock": 40547, + "next_contact": [ + 40548, + "ADD", + "source" + ], + "owner": 1527, + "rank": 1 + }, + { + "birth": 39975, + "charts": [ + 549, + 115 + ], + "clear": 43332, + "clock": 40554, + "next_contact": [ + 40555, + "ADD", + "destination" + ], + "owner": 1501, + "rank": 2 + }, + { + "birth": 39975, + "charts": [ + 115, + 593 + ], + "clear": 43332, + "clock": 40558, + "next_contact": [ + 40559, + "ADD", + "source" + ], + "owner": 1501, + "rank": 4 + }, + { + "birth": 30579, + "charts": [ + 1090, + 477 + ], + "clear": 41486, + "clock": 41482, + "next_contact": [ + 41483, + "ADD", + "source" + ], + "owner": 1537, + "rank": 4 + }, + { + "birth": 33298, + "charts": [ + 593, + 549 + ], + "clear": 41640, + "clock": 41637, + "next_contact": [ + 41638, + "SCALE", + "SCALE" + ], + "owner": 1530, + "rank": 6 + }, + { + "birth": 32607, + "charts": [ + 594, + 117 + ], + "clear": 44247, + "clock": 41996, + "next_contact": [ + 41997, + "ADD", + "destination" + ], + "owner": 1531, + "rank": 4 + }, + { + "birth": 39828, + "charts": [ + 591, + 1031 + ], + "clear": 42527, + "clock": 42468, + "next_contact": [ + 42469, + "ADD", + "source" + ], + "owner": 1504, + "rank": 3 + }, + { + "birth": 39828, + "charts": [ + 1031, + 597 + ], + "clear": 42527, + "clock": 42473, + "next_contact": [ + 42474, + "ADD", + "source" + ], + "owner": 1504, + "rank": 4 + }, + { + "birth": 38130, + "charts": [ + 597, + 1031 + ], + "clear": 42494, + "clock": 42478, + "next_contact": [ + 42479, + "ADD", + "source" + ], + "owner": 1533, + "rank": 4 + }, + { + "birth": 38130, + "charts": [ + 1031, + 591 + ], + "clear": 42494, + "clock": 42491, + "next_contact": [ + 42492, + "SCALE", + "SCALE" + ], + "owner": 1533, + "rank": 3 + }, + { + "birth": 37991, + "charts": [ + 541, + 543 + ], + "clear": 44239, + "clock": 44235, + "next_contact": [ + 44236, + "ADD", + "source" + ], + "owner": 1550, + "rank": 1 + }, + { + "birth": 32607, + "charts": [ + 117, + 534 + ], + "clear": 44247, + "clock": 44242, + "next_contact": [ + 44243, + "ADD", + "destination" + ], + "owner": 1531, + "rank": 1 + }, + { + "birth": 32607, + "charts": [ + 534, + 541 + ], + "clear": 44247, + "clock": 44244, + "next_contact": [ + 44245, + "SCALE", + "SCALE" + ], + "owner": 1531, + "rank": 1 + }, + { + "birth": 37892, + "charts": [ + 1091, + 267 + ], + "clear": 45643, + "clock": 45629, + "next_contact": [ + 45630, + "ADD", + "source" + ], + "owner": 1551, + "rank": 4 + }, + { + "birth": 32219, + "charts": [ + 260, + 1091 + ], + "clear": 45649, + "clock": 45647, + "next_contact": [ + 45648, + "ADD", + "source" + ], + "owner": 1540, + "rank": 1 + } + ], + "neighbor_pairs": 9, + "next_owned_contact_counts": { + "ADD": 43, + "SCALE": 4 + }, + "owned_paid": 47, + "owned_paid_by_rank": { + "1": 20, + "2": 9, + "3": 2, + "4": 13, + "5": 2, + "6": 1 + }, + "pairs": [ + { + "barriers": [ + [ + 33141, + "ADD", + "source" + ] + ], + "charts": [ + 541, + 534, + 117 + ], + "intervening": [ + [ + 33141, + "ADD", + "source" + ] + ], + "key": [ + 33140, + 33142, + 1502 + ], + "lifetime": [ + 33136, + 43333 + ], + "opposite_direction": false, + "paid_ranks": [ + 1, + 1 + ], + "ranks": [ + 7, + 6, + 5 + ], + "scales": [], + "status": "same_direction" + }, + { + "barriers": [ + [ + 33143, + "ADD", + "source" + ], + [ + 33145, + "ADD", + "source" + ] + ], + "charts": [ + 534, + 117, + 594 + ], + "intervening": [ + [ + 33143, + "ADD", + "source" + ], + [ + 33145, + "ADD", + "source" + ] + ], + "key": [ + 33142, + 33149, + 1502 + ], + "lifetime": [ + 33136, + 43333 + ], + "opposite_direction": false, + "paid_ranks": [ + 1, + 4 + ], + "ranks": [ + 6, + 5, + 1 + ], + "scales": [], + "status": "same_direction" + }, + { + "barriers": [ + [ + 39806, + "ADD", + "source" + ] + ], + "charts": [ + 529, + 520, + 595 + ], + "intervening": [ + [ + 39806, + "ADD", + "source" + ] + ], + "key": [ + 39805, + 39811, + 1503 + ], + "lifetime": [ + 39802, + 39887 + ], + "opposite_direction": false, + "paid_ranks": [ + 1, + 5 + ], + "ranks": [ + 7, + 6, + 1 + ], + "scales": [], + "status": "same_direction" + }, + { + "barriers": [ + [ + 39867, + "ADD", + "destination" + ] + ], + "charts": [ + 595, + 520, + 529 + ], + "intervening": [ + [ + 39867, + "ADD", + "destination" + ] + ], + "key": [ + 39866, + 39875, + 1532 + ], + "lifetime": [ + 38119, + 39878 + ], + "opposite_direction": false, + "paid_ranks": [ + 5, + 1 + ], + "ranks": [ + 1, + 6, + 7 + ], + "scales": [], + "status": "same_direction" + }, + { + "barriers": [ + [ + 40555, + "ADD", + "destination" + ] + ], + "charts": [ + 549, + 115, + 593 + ], + "intervening": [ + [ + 40555, + "ADD", + "destination" + ] + ], + "key": [ + 40554, + 40558, + 1501 + ], + "lifetime": [ + 39975, + 43332 + ], + "opposite_direction": false, + "paid_ranks": [ + 2, + 4 + ], + "ranks": [ + 7, + 5, + 1 + ], + "scales": [], + "status": "same_direction" + }, + { + "barriers": [ + [ + 42469, + "ADD", + "source" + ], + [ + 42470, + "ADD", + "source" + ], + [ + 42471, + "ADD", + "destination" + ] + ], + "charts": [ + 591, + 1031, + 597 + ], + "intervening": [ + [ + 42469, + "ADD", + "source" + ], + [ + 42470, + "ADD", + "source" + ], + [ + 42471, + "ADD", + "destination" + ] + ], + "key": [ + 42468, + 42473, + 1504 + ], + "lifetime": [ + 39828, + 42527 + ], + "opposite_direction": false, + "paid_ranks": [ + 3, + 4 + ], + "ranks": [ + 8, + 5, + 1 + ], + "scales": [], + "status": "same_direction" + }, + { + "barriers": [ + [ + 42479, + "ADD", + "source" + ], + [ + 42489, + "ADD", + "destination" + ], + [ + 42490, + "ADD", + "destination" + ] + ], + "charts": [ + 597, + 1031, + 591 + ], + "intervening": [ + [ + 42479, + "ADD", + "source" + ], + [ + 42489, + "ADD", + "destination" + ], + [ + 42490, + "ADD", + "destination" + ] + ], + "key": [ + 42478, + 42491, + 1533 + ], + "lifetime": [ + 38130, + 42494 + ], + "opposite_direction": false, + "paid_ranks": [ + 4, + 3 + ], + "ranks": [ + 1, + 5, + 8 + ], + "scales": [], + "status": "same_direction" + }, + { + "barriers": [ + [ + 41997, + "ADD", + "destination" + ], + [ + 44241, + "ADD", + "destination" + ] + ], + "charts": [ + 594, + 117, + 534 + ], + "intervening": [ + [ + 41997, + "ADD", + "destination" + ], + [ + 44241, + "ADD", + "destination" + ] + ], + "key": [ + 41996, + 44242, + 1531 + ], + "lifetime": [ + 32607, + 44247 + ], + "opposite_direction": false, + "paid_ranks": [ + 4, + 1 + ], + "ranks": [ + 1, + 5, + 6 + ], + "scales": [], + "status": "same_direction" + }, + { + "barriers": [ + [ + 44243, + "ADD", + "destination" + ] + ], + "charts": [ + 117, + 534, + 541 + ], + "intervening": [ + [ + 44243, + "ADD", + "destination" + ] + ], + "key": [ + 44242, + 44244, + 1531 + ], + "lifetime": [ + 32607, + 44247 + ], + "opposite_direction": false, + "paid_ranks": [ + 1, + 1 + ], + "ranks": [ + 5, + 6, + 7 + ], + "scales": [], + "status": "same_direction" + } + ], + "price_sha256": "76926ec9ff997159d281e0363326edb2e1aff8c530b041f361565030588e02cf", + "scope": "Reverse per-owner owned MOVE neighbor census. Same lifetime. Strict opposite directions. SCALE-only or contact-free diagnostic. Exact chart-span containment. No build.", + "status_counts": { + "same_direction": 9 + }, + "strict_opposite": 0, + "survivor_keys": [], + "unvisited_geometry": [], + "unvisited_literal_interval": null, + "word_sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +} diff --git a/research/p104-owned-two-write-aggregate-bound/inputs/R92-PRICE.json.gz b/research/p104-owned-two-write-aggregate-bound/inputs/R92-PRICE.json.gz new file mode 100644 index 0000000000..0307eb95e2 Binary files /dev/null and b/research/p104-owned-two-write-aggregate-bound/inputs/R92-PRICE.json.gz differ diff --git a/research/p104-owned-two-write-aggregate-bound/inputs/donor_span.py b/research/p104-owned-two-write-aggregate-bound/inputs/donor_span.py new file mode 100644 index 0000000000..46e4621b69 --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/inputs/donor_span.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-two-write-aggregate-bound/inputs/pricing.py b/research/p104-owned-two-write-aggregate-bound/inputs/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-owned-two-write-aggregate-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-two-write-aggregate-bound/inputs/reverse_span.py b/research/p104-owned-two-write-aggregate-bound/inputs/reverse_span.py new file mode 100644 index 0000000000..5efbeac87e --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/inputs/reverse_span.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-two-write-aggregate-bound/receipts/AGREEMENT.json b/research/p104-owned-two-write-aggregate-bound/receipts/AGREEMENT.json new file mode 100644 index 0000000000..0693abcc6a --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/receipts/AGREEMENT.json @@ -0,0 +1,60 @@ +{ + "aggregate_nonzero_coordinates": 219, + "bank_agreement": [ + { + "augmented_rank": 5, + "donor_rank": 4, + "key": [ + 41996, + 594 + ], + "read_only_donors": [ + 575, + 1231, + 1502 + ] + }, + { + "augmented_rank": 3, + "donor_rank": 2, + "key": [ + 44242, + 534 + ], + "read_only_donors": [ + 995 + ] + } + ], + "common_separator": { + "244": "1" + }, + "old_adds": [ + [ + 41997, + [ + "ADD", + 1531, + 1291, + "-2", + 117 + ] + ], + [ + 44241, + [ + "ADD", + 1531, + 732, + "-1", + 117 + ] + ] + ], + "pins": { + "independent/RESULT.json": "12d42fc77b2de5d955744259741e63d0e4fbe0735ca290103c6a024557ec6996", + "lead/RESULT.json": "6d040aae3e99a8261152c17965b692b964d18ed7139c7a003da50934ec8d2098" + }, + "separator_value": "-1/2", + "unresolved": 0 +} diff --git a/research/p104-owned-two-write-aggregate-bound/receipts/SHA256.json b/research/p104-owned-two-write-aggregate-bound/receipts/SHA256.json new file mode 100644 index 0000000000..7ab025bde9 --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/receipts/SHA256.json @@ -0,0 +1,6 @@ +{ + "AGREEMENT.json": "a3ad2b5e2e8cfa0814ed9745a97c79a944f425a920bb7a089f726ba1bc105d43", + "INDEPENDENT.json": "12d42fc77b2de5d955744259741e63d0e4fbe0735ca290103c6a024557ec6996", + "LEAD.json": "6d040aae3e99a8261152c17965b692b964d18ed7139c7a003da50934ec8d2098", + "PRICE.json": "08a403b6c8d5a3332212042ec69624ab5cf343fb7b6aa6e94f42583653f77912" +} diff --git a/research/p104-owned-two-write-aggregate-bound/replay.py b/research/p104-owned-two-write-aggregate-bound/replay.py new file mode 100644 index 0000000000..669ad72933 --- /dev/null +++ b/research/p104-owned-two-write-aggregate-bound/replay.py @@ -0,0 +1,141 @@ +"""Git-free replay of the two fixed endpoint owned-aggregate exclusions.""" +from argparse import ArgumentParser +from gzip import decompress +from hashlib import sha1,sha256 +from json import loads +from pathlib import Path,PurePosixPath +from shutil import copyfile +from subprocess import run +import sys +from tempfile import TemporaryDirectory + +ROOT=Path(__file__).resolve().parent + + +def unique(items): + doc=dict(items) + if len(doc)!=len(items): + raise ValueError("duplicate JSON key") + return doc + + +def decode(raw): + return loads(raw,object_pairs_hook=unique) + + +def digest(raw): + return sha256(raw).hexdigest() + + +def relative(name): + path=PurePosixPath(name) + if path.is_absolute() or path.as_posix()!=name or ".." in path.parts: + raise ValueError("invalid relative path "+name) + return path + + +def source(name): + return (ROOT/relative(name)).read_bytes() + + +def inputs(): + pins=decode(source("LOCAL-PINS.json")) + for name,expected in pins.items(): + if digest(source(name))!=expected: + raise ValueError("changed package dependency "+name) + provenance=decode(source("PROVENANCE.json")) + for name,record in provenance["files"].items(): + raw=source(name) + assert digest(raw)==record["sha256"]==pins[name] + assert sha1(f"blob {len(raw)}\0".encode()+raw).hexdigest()==record["git_blob"] + raw={} + for name,record in provenance["derived_inputs"].items(): + predecessor=decode(source(record["receipt"])) + if name.endswith(".gz"): + content=decompress(source(name)) + assert digest(content)==predecessor[record["key"]] + raw[PurePosixPath(name).name.removesuffix(".gz")]=content + else: + content=source(name) + bench=decode(content) + assert bench["admission_sha256"]==digest(source(record["receipt"])) + assert all(bench[k]==predecessor[k] for k in ("head","crossing","kappa","assumptions")) + raw[PurePosixPath(name).name]=content + return raw + + +def command(script,check=True): + call=run([sys.executable,"-I","-B",str(script)],capture_output=True,timeout=25) + if check and call.returncode: + sys.stderr.write(call.stderr.decode(errors="replace")) + call.check_returncode() + return call + + +def replay(root,out): + raw_inputs=inputs() + expected=decode(source("receipts/SHA256.json")) + for folder in ("inputs","plan","lead","independent/reused"): + (root/folder).mkdir(parents=True) + for name,content in raw_inputs.items(): + (root/"inputs"/name).write_bytes(content) + for name in ("pricing.py","R80-REVERSE.json","donor_span.py"): + copyfile(ROOT/"inputs"/name,root/"inputs"/name) + copyfile(ROOT/"inputs/reverse_span.py",root/"independent/reused/reverse_span.py") + copyfile(ROOT/"inputs/7334-WORD.json.gz",root/"inputs/7334-WORD.json.gz") + for path in ("plan/quote.py","lead/aggregate.py","independent/aggregate_covectors.py","independent/compare.py"): + copyfile(ROOT/"engines"/Path(path).name,root/path) + + outputs={} + def record(name,script,target=None): + raw=command(root/script).stdout + assert digest(raw)==expected[name],("changed receipt",name) + outputs[name]=raw + if target: + (root/target).write_bytes(raw) + return decode(raw) + + price=record("PRICE.json","plan/quote.py","plan/PRICE.json") + assert price["surplus"]==1424 and price["productive"]==22461 and price["paid"]==110502 + assert price["paid_delta"]=={"1":-17,"4":-17,"5":17} + assert price["bank_cuts"]==[[41996,594],[44242,534]] and price["compatible_edits"]==1 + lead=record("LEAD.json","lead/aggregate.py","lead/RESULT.json") + independent=record("INDEPENDENT.json","independent/aggregate_covectors.py","independent/RESULT.json") + agreement=record("AGREEMENT.json","independent/compare.py") + assert all(r["status"]=="coordinate exclusion" for r in lead["results"]) + assert independent["counts"]=={"absent_exterior_coordinate":2} + assert agreement["aggregate_nonzero_coordinates"]==219 + assert agreement["common_separator"]=={"244":"1"} and agreement["separator_value"]=="-1/2" + assert agreement["unresolved"]==0 + assert outputs["AGREEMENT.json"]==source("receipts/AGREEMENT.json") + + for name,script in (("inputs/R80-REVERSE.json","plan/quote.py"), + ("plan/PRICE.json","lead/aggregate.py"),("plan/PRICE.json","independent/aggregate_covectors.py"), + ("inputs/7334-WORD.json.gz","independent/aggregate_covectors.py")): + file=root/name + original=file.read_bytes() + file.write_bytes(original+b"\n") + rejected=command(root/script,check=False) + assert rejected.returncode==1 and not rejected.stdout + assert b"changed dependency" in rejected.stderr and file.name.encode() in rejected.stderr + file.write_bytes(original) + + assert set(outputs)==set(expected) + if out is not None: + out.mkdir(parents=True) + for name,raw in outputs.items(): + (out/relative(name)).write_bytes(raw) + print("PASS_P104_OWNED_TWO_WRITE_AGGREGATE_BOUND windows=1 endpoint_banks=2 separator=244 unresolved=0") + + +def main(): + assert __debug__ and sys.version_info[:2]==(3,12) + parser=ArgumentParser(description=__doc__) + parser.add_argument("--out",type=Path) + args=parser.parse_args() + with TemporaryDirectory() as tmp: + replay(Path(tmp),args.out) + + +if __name__=="__main__": + main()