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-outer-temporal-aggregate-bound/LOCAL-PINS.json b/research/p104-owned-outer-temporal-aggregate-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..450a0c9ca8 --- /dev/null +++ b/research/p104-owned-outer-temporal-aggregate-bound/LOCAL-PINS.json @@ -0,0 +1,14 @@ +{ + "PROVENANCE.json": "574e5269d96ac9dfb317fa517298a38208171b13685e067a632f0bf9d6716ec9", + "engines/reverse.py": "f665e9dc6d716a054c41778af59734e25382dd2af090e60ad06a8f72531eae15", + "engines/temporal_outer.py": "09f4046fc283eec3a776260d4c6df68459604cae171568dc40e7bdb85823119d", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "inputs/PLAN.md": "33ae20a2ff97879168287fe72badb5f921944012fa2d1d7026b5f08dedcbb001", + "inputs/PR7378-SHA256.json": "7741eb200e8f23be52d55f6f520bcfcb86eaf2c7da0bdedf704528ba23749de5", + "inputs/R122-PRICE.json": "08a403b6c8d5a3332212042ec69624ab5cf343fb7b6aa6e94f42583653f77912", + "inputs/R122-RESULT.json": "6d040aae3e99a8261152c17965b692b964d18ed7139c7a003da50934ec8d2098", + "receipts/ALIASES.json": "d70e526d2c97515a7ed78753549755e11552cf41af0981a6e465a58afe0b3e26", + "receipts/SHA256.json": "d2041d8e94d940df351d5baac9198a82d5cbe7cbcdac0c0c75708a8736aa6f33", + "replay.py": "2ba7706e5bcb2a0f4a478b4796ba12276c0851d89f535a8098db437c2b0bb05e" +} diff --git a/research/p104-owned-outer-temporal-aggregate-bound/NOTICE b/research/p104-owned-outer-temporal-aggregate-bound/NOTICE new file mode 100644 index 0000000000..dd14bd474d --- /dev/null +++ b/research/p104-owned-outer-temporal-aggregate-bound/NOTICE @@ -0,0 +1,8 @@ +Apache-2.0. + +#7334 and #7113 supply the exact native word and signed caller. +#7378 supplies the exact fixed-bank proof, signed aggregate and +directed quote. #7354 and #7355 supply earlier owned chronology +and sole-write evidence. #7362 and #7298 supply the inherited +invoice and directed tariff. OpenAI Codex and subagents materially +assisted proof, implementation, independent replay and packaging. diff --git a/research/p104-owned-outer-temporal-aggregate-bound/PROOF.md b/research/p104-owned-outer-temporal-aggregate-bound/PROOF.md new file mode 100644 index 0000000000..1bb570dd5e --- /dev/null +++ b/research/p104-owned-outer-temporal-aggregate-bound/PROOF.md @@ -0,0 +1,82 @@ +# Temporal obstruction for owner 1531 + +The owned role has original lifetime 32607–44247. Its paid MOVEs +are at u=41996 and v=44242, in strict chart chain 594⊊117⊊534 of +dimensions 1, 5 and 6. The only intervening owner contacts are +the incoming ADDs at 41997 and 44241. They read role 1291 with +coefficient −2 and role 732 with coefficient −1. Neither changes +any source trajectory. The required aggregate a on normalized +arbitrary inputs is + +```text +a = −2 R1291(41997) − R732(44241). +``` + +Replace the two paid MOVEs by a direct rank-five chart 594→534 +MOVE at either u or v. Let d be the unchanged owner row at +pre-event u. The two original writes are removed, so the old +late owner row is never available as a donor. The target +at the corridor exit is d+a. + +For the early switch, chart 594 is available immediately before +the replacement at u. Chart 534 is available immediately after +it at u and throughout the later cuts. For the late switch, +chart 594 is available throughout the corridor and immediately +before the replacement at v. Chart 534 is available immediately +after it at v. The within-clock cuts share the same untouched +donor rows because the replacement moves only the owner. +Every old donor row remains read-only, with its own trajectory +and lifetime. The test grants all live cocharted rows, including +owned donors, and arbitrary rational coefficients. Combining +donors and scaling the owner at different legal times can +therefore only generate a row in the span of d and the legal +union for that switch. The proof permits the union across both +switches as an additional relaxation. + +## Exact input-coordinate witness + +On input e244, the old pre-u owner diagonal is zero. The exact +old source values are R1291(41997)=0 and R732(44241)=1/2. +The required aggregate has response −1/2. The chronological +sweep visits both literal outer banks at every pre-event cut +in [41996,44242], inclusive. Each pre-event key denotes the +unchanged donor bank on either side of a replacement MOVE at +that same clock when the corresponding schedule allows it. + +The following table records all nine exact aliases. An alias +is contiguous and ends at an incident donor event, ingress, +lifetime change or a switch boundary. The receipt includes +schedule tags and the birth clock for the only owned donor. + +| Chart | Inclusive cuts | Live donors | +|---:|---|---| +| 594 | 41996 | 575, 1231, 1502 | +| 594 | 41997–42014 | 575, 1231, 1502 | +| 594 | 42015–43333 | 1231, 1502 | +| 594 | 43334–44241 | 1231 | +| 594 | 44242 | 1231 | +| 534 | 41996 | 995, 1489 | +| 534 | 41997–43307 | 995, 1489 | +| 534 | 43308–44241 | 995 | +| 534 | 44242 | 995 | + +All 7,163 donor incidences are zero on e244. The old diagonal +is also zero, so no sequence of legal unchanged donor writes +can supply the aggregate under either schedule. There is no +unvisited cut. This covers temporal donor selection within +both specified fixed-switch schedules, including any number +of such unchanged donor reads. Changed donor trajectories, +switch clocks and producer or recovery contracts remain open. + +## Directed price + +Both schedules spend the same two old paid anchors. The complete +17-copy delta is P1 −17, P4 −17 and P5 +17. Paid count is +110,502, productive count 22,461 and signed rank surplus 1,424. +The optimistic complete one-edit gross is at most +0.154513811062998 raw at the old crossing. The complete +fixed-target margin upper is below −139.59718548090816 at +κ = 0.0040075385047236. One additional paid rank-one position +would defeat the positive probe. The exact scope realizes zero +saving before any new physical proof, signed compiler, ordinary +work, ownership, precision or tape checks. diff --git a/research/p104-owned-outer-temporal-aggregate-bound/PROVENANCE.json b/research/p104-owned-outer-temporal-aggregate-bound/PROVENANCE.json new file mode 100644 index 0000000000..c44884fd07 --- /dev/null +++ b/research/p104-owned-outer-temporal-aggregate-bound/PROVENANCE.json @@ -0,0 +1,51 @@ +{ + "caller": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "scope": "Exact retained signed caller. No caller replay is required for this scoped exclusion.", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/7113" + }, + "derived_inputs": { + "inputs/PLAN.md": { + "relationship": "Frozen two-switch temporal scope, exact old quote and bounded gates.", + "sha256": "33ae20a2ff97879168287fe72badb5f921944012fa2d1d7026b5f08dedcbb001" + }, + "inputs/R122-PRICE.json": { + "key": "PRICE.json", + "receipt": "inputs/PR7378-SHA256.json", + "relationship": "Exact #7378 PRICE.json receipt, signed price inherited without changing the invoice.", + "sha256": "08a403b6c8d5a3332212042ec69624ab5cf343fb7b6aa6e94f42583653f77912" + }, + "inputs/R122-RESULT.json": { + "key": "LEAD.json", + "receipt": "inputs/PR7378-SHA256.json", + "relationship": "Exact #7378 LEAD.json receipt, original write clocks and signed aggregate.", + "sha256": "6d040aae3e99a8261152c17965b692b964d18ed7139c7a003da50934ec8d2098" + } + }, + "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/PR7378-SHA256.json": { + "commit": "fb5e20890e74159f7c432f4d78cc1ebcfea9a420", + "git_blob": "7ab025bde96e35af8cb251269fa5f6b2df232e64", + "path": "research/p104-owned-two-write-aggregate-bound/receipts/SHA256.json", + "sha256": "7741eb200e8f23be52d55f6f520bcfcb86eaf2c7da0bdedf704528ba23749de5", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/fb5e20890e74159f7c432f4d78cc1ebcfea9a420/research/p104-owned-two-write-aggregate-bound/receipts/SHA256.json" + } + }, + "schema_version": 1 +} diff --git a/research/p104-owned-outer-temporal-aggregate-bound/README.md b/research/p104-owned-outer-temporal-aggregate-bound/README.md new file mode 100644 index 0000000000..67873439aa --- /dev/null +++ b/research/p104-owned-outer-temporal-aggregate-bound/README.md @@ -0,0 +1,62 @@ +# Temporal outer donor banks for an owned write aggregate + +**NO VERIFIED GAIN.** The independently reproduced comparator +remains [#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) +`aaeec8c0acf01e99a5f331ef363a698d9c084ace`, conditional +κ = `0.00364665195644`, with signed +[#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +`07a76c5e2738882c0cb322278e56f6cae3c9885d`. + +[#7378](https://github.com/CrocSwap/integer-mult-bounds/pull/7378) +excludes the two original fixed outer banks for the owner-1531 +two-write aggregate. This test allows the aggregate to be +assembled at multiple clocks from the unchanged live donor banks +in either old-clock switch schedule. The input-244 impulse is +zero on every donor at all 4,494 chart/cut pairs and on the +initial owner diagonal. The required signed aggregate has +response −1/2. Both switch schedules are excluded. +[Proof and price](PROOF.md) · [Exact alias inventory](receipts/ALIASES.json). + +## Replay + +Use POSIX CPython 3.12 with assertions from a clean checkout. + +```sh +python3.12 -I -B research/p104-owned-outer-temporal-aggregate-bound/replay.py +``` + +The standard-library command authenticates the exact native word, +the #7378 directed quote and aggregate receipt, and the frozen +two-switch scope. Forward and reverse engines reproduce three +receipts and reject three altered dependencies. Use +`--out fresh-directory` to retain the receipts. Git metadata, +network access, external source roots and prior temporary state +are unnecessary. [Source provenance](PROVENANCE.json) · +[Verification](VERIFICATION.md). + +## Open next questions + +Can a separately priced changed donor path carry input coordinate +244 into an eligible outer coframe while preserving all original +observations? First pin one concrete trajectory and charge any +new paid call, ownership, restoration and source access. This +changes the fixed donor contract tested here. + +## Credit + +[#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) +and [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +supply the exact word and signed caller. +[#7378](https://github.com/CrocSwap/integer-mult-bounds/pull/7378) +at `fb5e20890e74159f7c432f4d78cc1ebcfea9a420` supplies the two +fixed-bank exclusions, signed aggregate and exact quote. +[#7354](https://github.com/CrocSwap/integer-mult-bounds/pull/7354) +and [#7355](https://github.com/CrocSwap/integer-mult-bounds/pull/7355) +supply prior owned chronology and adjacent sole-write evidence. +[#7362](https://github.com/CrocSwap/integer-mult-bounds/pull/7362) +and [#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) +supply the inherited signed stock and directed tariff. +The earlier [released producer and recovery scope](https://github.com/CrocSwap/integer-mult-bounds/discussions/7111#discussioncomment-19554307) +includes the same paid pair with a different contract. +OpenAI Codex and subagents materially assisted proof, implementation, +independent replay and packaging. diff --git a/research/p104-owned-outer-temporal-aggregate-bound/SOURCES.json b/research/p104-owned-outer-temporal-aggregate-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-owned-outer-temporal-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-outer-temporal-aggregate-bound/TASK.json b/research/p104-owned-outer-temporal-aggregate-bound/TASK.json new file mode 100644 index 0000000000..f11cd0c10d --- /dev/null +++ b/research/p104-owned-outer-temporal-aggregate-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "One exact #7334 owner1531 lifetime and paid pair 41996/44242. Replace both paid legs by a rank-five ascent at either original MOVE clock, allowing arbitrary unchanged cocharted donors at any pre-event cut in the closed corridor with within-switch placement.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "P104 owned outer-bank timing research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "The same one-edit signed rank-five paid credit needs the complete old aggregate from the union of the existing live donor banks in at least one fixed switch schedule.", + "budget_minutes": 10, + "evidence": "Input coordinate 244 annihilates the old owner diagonal and every donor at 4,494 chart/cut pairs, but evaluates to \u22121/2 on the required aggregate. Independent reverse chart lifetimes and signed sparse covectors agree on all nine exact bank aliases and every affected coordinate.", + "open_questions": [ + { + "blocked_by": "All unchanged temporal outer donors lose the same required coordinate.", + "first_step": "Price one exact donor-path or producer change that creates input coordinate 244 in an eligible outer coframe while preserving its original observations.", + "question": "Can a changed donor trajectory carry the missing coordinate into a legal outer bank?", + "why_it_matters": "A legal one-edit fusion would improve the binding signed paid moment if the complete added work is charged." + } + ], + "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": "The #7378 two-endpoint proof does not cover changing banks. This test grants the full temporal bank union for both old-clock switch schedules.", + "scope_status": "changed", + "stop_rule": "One 76,466-event word, two old-clock switches and 4,494 bank cuts under 20 runner seconds. The exact coordinate exclusion closes the whole scoped donor union.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-owned-outer-temporal-aggregate-bound/VERIFICATION.md b/research/p104-owned-outer-temporal-aggregate-bound/VERIFICATION.md new file mode 100644 index 0000000000..938dc86929 --- /dev/null +++ b/research/p104-owned-outer-temporal-aggregate-bound/VERIFICATION.md @@ -0,0 +1,25 @@ +# Verification + +Direct CPython 3.12.14 replay exited 0 in 0.47 seconds. +A relocated Git-free copy with a cleared environment exited 0 +in 0.53 seconds and reproduced all three receipts byte for byte. + +The forward exact impulse and independent reverse occupancy +and sparse covectors agree on all nine alias bounds, every +donor and live owned birth, and both old signed source values. +They cover 4,494 chart/cut pairs and 7,163 donor incidences. +The reverse engine also checks the clean destination of the +sole original COPY at event 33805. + +The replay rejects alterations to the pinned #7378 quote, the +#7378 aggregate receipt and the forward alias receipt used by +the reverse checker. Each altered dependency is rejected +before the absent native word is opened. Synthetic controls +exercise the within-clock switch boundaries, nonzero donor +values, signed source weights, transpose COPY and SCALE, +and clean initialization and erasure. + +No new signed physical construction or caller replay was needed +for the scoped negative result. + +[Replay](README.md) · [Exact receipt hashes](receipts/SHA256.json). diff --git a/research/p104-owned-outer-temporal-aggregate-bound/VERIFY.json b/research/p104-owned-outer-temporal-aggregate-bound/VERIFY.json new file mode 100644 index 0000000000..9082424f25 --- /dev/null +++ b/research/p104-owned-outer-temporal-aggregate-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Regenerate the signed quote and both exact chronology/covector receipts, reconcile all nine banks, and reject altered dependencies.", + "timeout_seconds": 150 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-owned-outer-temporal-aggregate-bound/engines/reverse.py b/research/p104-owned-outer-temporal-aggregate-bound/engines/reverse.py new file mode 100644 index 0000000000..14b724ee6c --- /dev/null +++ b/research/p104-owned-outer-temporal-aggregate-bound/engines/reverse.py @@ -0,0 +1,225 @@ +"""R147 independent reverse ownership chronology and sparse signed covectors.""" +from argparse import ArgumentParser +from collections import defaultdict +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from signal import SIGALRM, alarm, signal + +HERE = Path(__file__).resolve().parent +PINS = { + "inputs/PRICE.json": "144140e01329901d6563014a532c7711c3515972c9b6863979d8bb62d43f4d07", + "inputs/FORWARD.json": "d70e526d2c97515a7ed78753549755e11552cf41af0981a6e465a58afe0b3e26", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", +} +PAYLOAD = "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +U, V, H, AXIS = 41996, 44242, 1531, 244 +A, B, C = 594, 117, 534 +NATIVE_EVENTS = 76466 + + +def unique(items): + out = dict(items) + if len(out) != len(items): + raise ValueError("duplicate JSON key") + return out + + +def checked(root, name): + raw = (root / name).read_bytes() + if sha256(raw).hexdigest() != PINS[name]: + raise ValueError("changed dependency " + name) + return raw + + +@cache +def scalar(x): + return Q(x) + + +def update(vec, key, delta): + value = vec.get(key, 0) + delta + if value: + vec[key] = value + else: + vec.pop(key, None) + + +def reverse_axis(events, cut, role, axis): + covector = {role: Q(1)} + for t in range(cut - 1, -1, -1): + event = events[t] + op, dst = event[:2] + if dst not in covector: + continue + if op == "ADD": + update(covector, event[2], covector[dst] * scalar(event[3])) + elif op == "COPY": + update(covector, event[2], covector.pop(dst) * scalar(event[3])) + elif op == "SCALE": + covector[dst] *= scalar(event[2]) + elif op in ("INIT", "CLEAR"): + covector.pop(dst) + else: + assert op == "MOVE" + if not covector: + return Q(0) + return covector.get(axis, Q(0)) + + +def operands(e): + return e[1:3] if e[0] in ("ADD", "COPY") else e[1:2] + + +def potentially_changes_bank(event, chart): + op = event[0] + if all(r == H for r in operands(event)): + return False + return chart in event[2:4] if op == "MOVE" else chart == event[-1] + + +def reverse_inventory(word): + n, m, events = word["public"], word["owned_fields"], word["program"] + assert (n, m, len(events)) == (1501, 68, NATIVE_EVENTS) + charts = list(word["final"]) + [None] * m + bank = defaultdict(set) + for r, c in enumerate(charts): + if c is not None: + bank[c].add(r) + active_clear = {} + birth = {} + snapshots = {A: {}, C: {}} + boundaries = {A: {U, U + 1, V}, C: {U, U + 1, V}} + owner_contacts = [] + + def reverse_change(r, after, before): + assert charts[r] == after + if after is not None: + bank[after].remove(r) + if before is not None: + bank[before].add(r) + charts[r] = before + + for t in range(len(events) - 1, -1, -1): + event = events[t] + op, dst = event[:2] + if op == "MOVE": + old, new, owned = event[2:] + assert owned == (dst >= n) + reverse_change(dst, new, old) + elif op == "CLEAR": + assert dst >= n and dst not in active_clear + active_clear[dst] = t + reverse_change(dst, None, event[2]) + elif op == "INIT": + assert dst >= n and dst in active_clear + birth[active_clear.pop(dst)] = t + reverse_change(dst, event[2], None) + elif op in ("ADD", "COPY", "SCALE"): + assert all(charts[r] == event[-1] for r in operands(event)) + else: + raise ValueError(op) + if U < t < V and H in operands(event): + owner_contacts.append([t,event]) + if U <= t <= V: + for c in (A,C): + labels = sorted(bank[c] - {H}) + snapshots[c][t] = labels, [(r,active_clear[r]) for r in labels if r >= n] + if t < V and potentially_changes_bank(event,c): + boundaries[c].add(t+1) + assert charts == word["initial"] + [None]*m and not active_clear + assert owner_contacts[::-1] == [[41997,["ADD",H,1291,"-2",B]], + [44241,["ADD",H,732,"-1",B]]] + assert events[U] == ["MOVE",H,A,B,True] and events[V] == ["MOVE",H,B,C,True] + assert birth[44247] == 32607 and events[32607][:2] == ["INIT",H] and events[44247][:2] == ["CLEAR",H] + return snapshots, boundaries, birth + + +def controls(): + word = [ + ["ADD",1,0,"-3",0], + ["SCALE",1,"2",0], + ["INIT",3,0], + ["COPY",3,1,"1/2",0], + ["CLEAR",3,0], + ] + assert reverse_axis(word,4,3,0) == -3 + assert reverse_axis(word,3,3,0) == 0 and reverse_axis(word,5,3,0) == 0 + assert potentially_changes_bank(["MOVE",1,2,3,False],2) + assert potentially_changes_bank(["MOVE",1,2,3,False],3) + assert not potentially_changes_bank(["MOVE",H,2,3,True],2) + return ["signed transpose COPY and SCALE", "clean initialization and erasure", + "two-sided chart membership boundaries", "omitted changed owner excluded"] + + +def run(root): + price = json.loads(checked(root,"inputs/PRICE.json"),object_pairs_hook=unique) + lead = json.loads(checked(root,"inputs/FORWARD.json"),object_pairs_hook=unique) + assert price["caps"] == {"events":NATIVE_EVENTS,"schedules":2,"bank_cuts":4494,"seconds":20} + assert price["switches"] == {"early":U,"late":V} and price["owner"] == H and price["input_axis"] == AXIS + assert (lead["head"],lead["caller"]) == (price["head"],price["caller"]) + assert lead["price_sha256"] == PINS["inputs/PRICE.json"] + raw = decompress(checked(root,"inputs/7334-WORD.json.gz")) + assert sha256(raw).hexdigest() == PAYLOAD + word = json.loads(raw,object_pairs_hook=unique) + events = word["program"] + snapshots,boundaries,birth = reverse_inventory(word) + cases, cuts, incidences = [], 0, 0 + for chart in (A,C): + starts = sorted(boundaries[chart]) + prior = lead["aliases"][str(chart)] + assert [r["first"] for r in prior] == starts + for first,after,expected in zip(starts,starts[1:]+[V+1],prior): + assert (first,after-1) == (expected["first"],expected["last"]) + roles,life = snapshots[chart][first] + assert all(snapshots[chart][t] == (roles,life) for t in range(first,after)) + assert roles == expected["roles"] and [[r,birth[c]] for r,c in life] == expected["owned_births"] + values = [[r,str(reverse_axis(events,first,r,AXIS))] for r in roles] + assert all(value == "0" for _,value in values) and not expected["nonzero"] + cuts += after-first + incidences += (after-first)*len(roles) + cases.append(dict(chart=chart,first=first,last=after-1,roles=roles, + owned_births=expected["owned_births"],coordinate_244=values)) + old = [] + for t in (41997,44241): + op,dst,src,signed,chart = events[t] + assert (op,dst,chart) == ("ADD",H,B) + coefficient = reverse_axis(events,t,src,AXIS) + old.append([t,src,signed,str(coefficient),str(coefficient*scalar(signed))]) + assert old == lead["old_source_responses"] + aggregate = sum(scalar(row[-1]) for row in old) + diagonal = [U,str(reverse_axis(events,U,H,AXIS))] + assert diagonal == lead["owner_diagonal"] == [U,"0"] + copies = [[t,e[1],str(reverse_axis(events,t,e[1],AXIS))] + for t,e in enumerate(events) if e[0] == "COPY"] + assert len(copies) == 1 and copies[0][-1] == "0" + assert len(cases) == 9 and cuts == lead["bank_cuts"] == 4494 + assert incidences == lead["donor_incidences"] == 7163 and aggregate == Q(-1,2) + return dict(pins=PINS,head=price["head"],caller=price["caller"],events=len(events),bank_cuts=cuts, + donor_incidences=incidences,aliases=cases,old_source_responses=old, + aggregate_response=str(aggregate),owner_diagonal=diagonal,copy_prewrite=copies, + controls=controls(),unresolved=[]) + + +def stop(_signal,_frame): + raise TimeoutError("20 second reverse audit cap") + + +def main(): + assert __debug__ + parser = ArgumentParser(description=__doc__) + parser.add_argument("--root",type=Path,default=HERE) + args = parser.parse_args() + signal(SIGALRM,stop) + alarm(20) + try: + print(json.dumps(run(args.root),sort_keys=True,indent=2)) + finally: + alarm(0) + + +if __name__ == "__main__": + main() diff --git a/research/p104-owned-outer-temporal-aggregate-bound/engines/temporal_outer.py b/research/p104-owned-outer-temporal-aggregate-bound/engines/temporal_outer.py new file mode 100644 index 0000000000..00658cb47f --- /dev/null +++ b/research/p104-owned-outer-temporal-aggregate-bound/engines/temporal_outer.py @@ -0,0 +1,262 @@ +"""Exact input-244 impulse over both outer banks of the owned two-write pair.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps,loads +from pathlib import Path +from signal import SIGALRM,alarm,signal +from time import monotonic + +ROOT=Path(__file__).resolve().parent +HEAD="aaeec8c0acf01e99a5f331ef363a698d9c084ace" +CALLER="07a76c5e2738882c0cb322278e56f6cae3c9885d" +PINS={ + "inputs/PLAN.md":"33ae20a2ff97879168287fe72badb5f921944012fa2d1d7026b5f08dedcbb001", + "inputs/R122-PRICE.json":"08a403b6c8d5a3332212042ec69624ab5cf343fb7b6aa6e94f42583653f77912", + "inputs/R122-RESULT.json":"6d040aae3e99a8261152c17965b692b964d18ed7139c7a003da50934ec8d2098", + "inputs/7334-WORD.json.gz":"4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", +} +PAYLOAD="9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" +U,V,H=41996,44242,1531 +A,B,C=594,117,534 +LIFETIME=[32607,44247] +WRITES=[[41997,["ADD",H,1291,"-2",B]],[44241,["ADD",H,732,"-1",B]]] +EVENTS, BANK_CUTS, SECONDS=76466,4494,20 +AXIS=244 +ZERO=Q(0) + + +def unique(items): + out=dict(items) + if len(out)!=len(items): + raise ValueError("duplicate JSON key") + return out + + +def checked(root,name): + raw=(root/name).read_bytes() + if sha256(raw).hexdigest()!=PINS[name]: + raise ValueError("changed dependency "+name) + return raw + + +def quote(root): + checked(root,"inputs/PLAN.md") + p,w=[loads(checked(root,f"inputs/R122-{key}.json"),object_pairs_hook=unique) + for key in ("PRICE","RESULT")] + assert (p["head"],p["caller"])==(w["head"],w["caller"])==(HEAD,CALLER) + assert p["word_sha256"]==PINS["inputs/7334-WORD.json.gz"] + assert p["row"]["key"]==[U,V,H] and p["row"]["charts"]==[A,B,C] + assert p["row"]["lifetime"]==LIFETIME and p["row"]["paid_ranks"]==[4,1] + assert p["paid_delta"]=={"1":-17,"4":-17,"5":17} + assert (p["paid"],p["productive"],p["surplus"],p["compatible_edits"])==(110502,22461,1424,1) + assert p["bank_cuts"]==[[U,A],[V,C]] and w["old_adds"]==WRITES and not w["unvisited"] + assert all(r["witness"]==[AXIS,"-1/2"] for r in w["results"]) + assert w["aggregate"][str(AXIS)]=="-1/2" + assert Q(p["complete_probe_margin"][0])>0>Q(p["complete_fixed_target_upper"]) + assert Q(p["extra_rank_one_upper"])<0 + keys=("paid_delta","paid","productive","surplus","gain_at_old_crossing","complete_probe_margin", + "complete_fixed_target_upper","extra_rank_one_upper","compatible_edits") + return {"head":HEAD,"caller":CALLER,"pins":PINS,**{k:p[k] for k in keys}, + "switches":{"early":U,"late":V},"inclusive_cuts":[U,V], + "bank_charts":[A,C],"owner":H,"input_axis":AXIS, + "caps":{"events":EVENTS,"schedules":2,"bank_cuts":BANK_CUTS,"seconds":SECONDS}} + + +@cache +def q(s): + return Q(s) + + +def legality(t,chart): + if chart==A: + return ["early pre-switch","late"] if t==U else ( + ["late pre-switch"] if t==V else ["late"]) + assert chart==C + return ["early post-switch"] if t==U else ( + ["early","late post-switch"] if t==V else ["early"]) + + +def contacts(event): + return event[1:3] if event[0] in ("ADD","COPY") else event[1:2] + + +def coverage(t,chart,stock,values,born,n): + live=sorted(stock[chart]-{H}) + return dict(legality=legality(t,chart),roles=live, + owned_births=[[r,born[r]] for r in live if r>=n], + nonzero=[[r,str(values[r])] for r in live if values[r]]) + + +def controls(): + assert legality(U,A)==["early pre-switch","late"] + assert legality(U,C)==["early post-switch"] + assert legality(V,A)==["late pre-switch"] + assert legality(V,C)==["early","late post-switch"] + data=coverage(U,A,{A:{1,4,H}},[ZERO,Q(-1,2),ZERO,ZERO,ZERO],{4:0},3) + assert data["roles"]==[1,4] and data["nonzero"]==[[1,"-1/2"]] + assert data["owned_births"]==[[4,0]] + assert -2*Q(1,2)-Q(-1,2)==Q(-1,2) + return ["within-clock schedule boundary","read-only owner exclusion","signed nonzero donor retained", + "old signed source sum"] + + +def validate_window(tape,frames,n): + assert H>=n and tape[U]==["MOVE",H,A,B,True] and tape[V]==["MOVE",H,B,C,True] + assert tape[LIFETIME[0]][:2]==["INIT",H] and tape[LIFETIME[1]][:2]==["CLEAR",H] + assert [[t,tape[t]] for t in range(U+1,V) if H in contacts(tape[t])]==WRITES + assert not [t for t in range(LIFETIME[0]+1,LIFETIME[1]) if tape[t][:2] in (["INIT",H],["CLEAR",H])] + sets=[] + for chart in (A,B,C): + stock={0} + for v in frames[chart]: + assert v not in stock + stock|={u^v for u in stock} + sets.append(stock) + assert sets[0]=deadline: + raise TimeoutError("forward impulse") + if U<=t<=V: + if t==U: + diag=values[H] + for chart in (A,C): + data=coverage(t,chart,stock,values,born,n) + entries=banks[chart] + if entries and entries[-1]["epoch"]==changes[chart] and entries[-1]["legality"]==data["legality"]: + entry=entries[-1] + assert entry["last"]==t-1 and all(entry[k]==v for k,v in data.items()) + entry["last"]=t + else: + entries.append(dict(first=t,last=t,epoch=changes[chart],**data)) + out["bank_cuts"]+=1 + out["donor_incidences"]+=len(data["roles"]) + if t in watched: + assert event==watched[t] + src,coefficient=event[2:4] + old_sources.append([t,src,coefficient,str(values[src]),str(q(coefficient)*values[src])]) + op,d,*a=event + touch=[r for r in contacts(event) if r!=H] + before={state[r] for r in touch} + if op=="MOVE": + old,new,owned=a + assert owned==(d>=n) + change(d,old,new) + fresh.discard(d) + elif op=="INIT": + assert d>=n and d not in born + change(d,None,a[0]) + values[d]=ZERO + born[d]=t + fresh.add(d) + elif op=="CLEAR": + assert d>=n + change(d,a[0],None) + values[d]=ZERO + del born[d] + fresh.discard(d) + elif op=="SCALE": + assert state[d]==a[-1] + values[d]*=q(a[0]) + fresh.discard(d) + else: + s,coefficient,chart=a + assert op in ("ADD","COPY") and d!=s and state[d]==state[s]==chart + assert op!="COPY" or d>=n and d in fresh and values[d]==0 + values[d]=(values[d] if op=="ADD" else ZERO)+q(coefficient)*values[s] + fresh.discard(d) + if U<=t