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-even-idle-projector-bound/LOCAL-PINS.json b/research/p104-even-idle-projector-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..1e5b79efad --- /dev/null +++ b/research/p104-even-idle-projector-bound/LOCAL-PINS.json @@ -0,0 +1,15 @@ +{ + "dependencies/7113/research/signed-caller-8x9/replay/supplier7112/short-caller/check_odd_physical_binding.py": "5c80c3b0415a7f91d216395248dd6f13297eed637732098e1ca8fb0548951b98", + "dependencies/7298/RESULT.json": "aaf594b981f37e7dbddb12fd052d9286cf5c8c95c8d5265ab6426408f6e58cc5", + "dependencies/7298/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "dependencies/7298/verify.py": "4a4291c9019ef23c664ae9646b076dc57054b49f5c5ffd21908aa9f0edf19902", + "dependencies/round30/complex/source/inputs/CALLER.json.gz": "58beaf24e01c0589ecd5d1676d6d27e75b779f089d0674eda11725465ffc04e1", + "dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz": "9851ebaa4b4404be1f5670b8a8dfc6ee96a8e19e85731edd4a71d52bbfa9c793", + "dependencies/round30/complex/source/inputs/WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "engines/disjoint.py": "a560df5e252e283a3d962a0258000c76e3befb80a632aa44f78a9ea331c3a096", + "engines/independent_disjoint.py": "79b053724e1a03c00b3d8c449afbca763792fc0b7b4b3efd96b86768b9cb9505", + "engines/independent_singleton.py": "acc29bb66913fd7ba0baef848805f5ab64bea5428f5225397aac5d84a1f9fadd", + "engines/singleton.py": "cdf54b266ac31fd0efe544badbb9840598d4c63c4d3cd363f60ae9a74cc4b256", + "receipts/SHA256.json": "6ea4cfdb5ba09a673c528c0fe412fe69921c21329140fff50b1f726c289891ec", + "receipts/SUMMARY.json": "1aae263d683f754ce8ac4c88457d64f1ed6cf8d6ec83856222395135d969857c" +} diff --git a/research/p104-even-idle-projector-bound/NOTICE b/research/p104-even-idle-projector-bound/NOTICE new file mode 100644 index 0000000000..fa429b0626 --- /dev/null +++ b/research/p104-even-idle-projector-bound/NOTICE @@ -0,0 +1,7 @@ +Apache-2.0. +#7113 supplies the exact signed caller and idle interface. #7277 supplies +the native word and comparable invoice. #7298 supplies directed pricing. +Discussion #7111 and the older #7108, #7003 and #7002 callers supply the +earlier conjugacy and derivative lineage. #7144, #7295, #7296 and #7305 +supply related scoped precedents. OpenAI Codex and subagents materially +assisted. diff --git a/research/p104-even-idle-projector-bound/PROOF.md b/research/p104-even-idle-projector-bound/PROOF.md new file mode 100644 index 0000000000..ae1c6c9fe4 --- /dev/null +++ b/research/p104-even-idle-projector-bound/PROOF.md @@ -0,0 +1,44 @@ +# One-slot disjoint-mask fusion forces a common projector + +Fix either signed specialization q = +1 or q = −1 and set all 17 +independent body variables to one. An even IDLE_ONE with mask S and +role r is a factor of the form + +$$ +I+\left(\prod_{j\in S} z_j-1\right)E_{rr}, +\qquad E_{rr}=e_r e_r^{\mathsf T}. +$$ + +At this specialization the factor is identity. Let F be the complete +specialized operator and let P be the invertible prefix immediately +before this factor. Its contribution to the left-normalized derivative +$F^{-1}\partial F/\partial z_j$ is $P^{-1}E_{rr}P$ when j is in S, +and zero otherwise. + +Delete two retained even idles with nonempty disjoint masks and +insert one even idle with their union at an arbitrary clock and role. +All deleted and inserted factors evaluate to identity. Every unchanged +factor has the same specialized prefix and suffix, so its derivative +contribution cancels when comparing the two formal caller words. +Choose one body variable from each original mask. Equality of the +formal operators forces the single normalized projector of the new +idle to equal both old normalized projectors. Thus the two old +normalized projectors must agree, irrespective of the insertion +clock or role. + +For earlier and later old coordinate projectors $E_{ss}$ and $E_{tt}$ +with intervening product M, this condition is equivalent to +$E_{tt}M=ME_{ss}$. The primary gate checks the off-axis components +of $Me_s$ and $e_t^{\mathsf T}M$ after reduction modulo 65521. +It verifies that the modulus is prime and that the used rational +denominators and gates are units. A nonzero outside component +certifies an exact failure. The independent gate uses exact rational +prefixes and their inverses to compare the original conjugated +projectors directly. A coordinate swap is a positive transport +control. A shear changes the conjugate and is rejected. + +The condition allows non-diagonal intermediate conjugates. It keeps +the other caller events fixed and assumes a single one-role idle +whose stage derivatives use the same projector. Repeated stages, +odd-idle replacements, multi-role children and other changed +operators require different arguments. diff --git a/research/p104-even-idle-projector-bound/PROVENANCE.json b/research/p104-even-idle-projector-bound/PROVENANCE.json new file mode 100644 index 0000000000..c6c0c35b51 --- /dev/null +++ b/research/p104-even-idle-projector-bound/PROVENANCE.json @@ -0,0 +1,61 @@ +{ + "files": { + "dependencies/7113/research/signed-caller-8x9/replay/supplier7112/short-caller/check_odd_physical_binding.py": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "git_blob": "def1e6a18439bd40d1b12af04c6347bbf6b74c55", + "path": "research/signed-caller-8x9/replay/supplier7112/short-caller/check_odd_physical_binding.py", + "sha256": "5c80c3b0415a7f91d216395248dd6f13297eed637732098e1ca8fb0548951b98", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/replay/supplier7112/short-caller/check_odd_physical_binding.py", + "uncompress": false + }, + "dependencies/7298/RESULT.json": { + "commit": "c522451caf287bb3c16eaece72be4c263315dca4", + "git_blob": "c66ad2ed50e6f70c2c60cbb5b8b222dcd1b64a6f", + "path": "research/adjacent-owned-add-exchange-bound/RESULT.json", + "sha256": "aaf594b981f37e7dbddb12fd052d9286cf5c8c95c8d5265ab6426408f6e58cc5", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/c522451caf287bb3c16eaece72be4c263315dca4/research/adjacent-owned-add-exchange-bound/RESULT.json", + "uncompress": false + }, + "dependencies/7298/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 + }, + "dependencies/7298/verify.py": { + "commit": "c522451caf287bb3c16eaece72be4c263315dca4", + "git_blob": "a45510da2548ec701c7719e6205f079318bbd930", + "path": "research/adjacent-owned-add-exchange-bound/verify.py", + "sha256": "4a4291c9019ef23c664ae9646b076dc57054b49f5c5ffd21908aa9f0edf19902", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/c522451caf287bb3c16eaece72be4c263315dca4/research/adjacent-owned-add-exchange-bound/verify.py", + "uncompress": false + }, + "dependencies/round30/complex/source/inputs/CALLER.json.gz": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "git_blob": "9451ceaf6e8e037894680b549f3ef41c21b260d7", + "path": "research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json", + "sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json", + "uncompress": true + }, + "dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz": { + "commit": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "git_blob": "ef86c8ec8ed0a2042017a6f42515e70dd15cfffd", + "path": "research/p104-terminal-cut-rechart/EARLY-RESULT.json", + "sha256": "691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/EARLY-RESULT.json", + "uncompress": true + }, + "dependencies/round30/complex/source/inputs/WORD.json.gz": { + "commit": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "git_blob": "077bf48c35db0ddafae81f1bfa0ffacc30894b2b", + "path": "research/p104-terminal-cut-rechart/WORD.json.gz", + "sha256": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/WORD.json.gz", + "uncompress": false + } + }, + "schema_version": 1 +} diff --git a/research/p104-even-idle-projector-bound/README.md b/research/p104-even-idle-projector-bound/README.md new file mode 100644 index 0000000000..bdeaa6b17e --- /dev/null +++ b/research/p104-even-idle-projector-bound/README.md @@ -0,0 +1,125 @@ +# Type B even-idle projector bound on the signed P104 caller + +**NO VERIFIED GAIN. Exact conditional κ change 0%.** On the exact +[#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +17-stage caller reused by [#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277), +no two Type B even IDLE_ONE jobs with disjoint masks can be replaced +by one grouped one-role idle with their union. The exclusion covers +insertion at any clock and role. Every other caller event and the +native word stay fixed. + +The singleton gate checks all 544 distinct-stage pairs among +34 singleton-mask jobs. The complete gate checks all 1,348 +disjoint-mask pairs among 60 even IDLE_ONE jobs, including the +same 544 singleton pairs. The independent exact rational replay +finds different prefix-conjugated projectors at both signed +unit-body probes for every pair. Zero cases survive or remain +unresolved. + +## Exact price and support + +The primary replay reconstructs the complete signed #7277 invoice +with 17 native copies, 110,536 paid positions and 22,461 productive +fields. It saves every directed price before testing support. The +retained grouped idle interface charges rank 8 times the mask +size. At equal field volume, a pair of old ranks r and s has +optimistic signed credit `8(Hᵣ + Hₛ − Hᵣ₊ₛ)` across the eight +Type B ports. Hᵣ is the retained tariff at the exact old crossing +upper. The price-only credit for a singleton pair is about +0.3206061111022773 raw units. There are at most 17 disjoint +singleton replacements, giving a whole-stock upper of about +5.450303888738714. + +For all masks, the replay prices 35 rank signatures. Each event +is assigned its largest incident upper credit. Half the sum of +these event weights bounds any disjoint selection, because each +selected pair uses two distinct events. The complete optimistic +upper is about 35.71990804514672 raw units. These upper bounds +grant original field volume and free additional work. The exact +rational prices and paid histograms are in the emitted receipts. +Both bounds fall to zero after support. + +At body one, the removed and inserted even idles are identity. +The [derivative proof](PROOF.md) compares the two normalized +derivatives for one variable from each disjoint mask. A one-role +replacement has the same projector for both derivatives, which +forces equality of the two original projectors at either q sign. +The primary replay certifies off-axis nonzero components modulo +65521. The independent replay recomputes full rational prefixes, +their inverses and the original endpoint at q = ±1. It confirms +every primary exclusion at the indicated sign. Controls cover +a role-changing coordinate swap, a separating shear, overlapping +masks and the event-weight upper bound. + +The scope covers one replacement, with no simultaneous change +to the retained J blocks, QUERYs, odd idles or other scalar events. +Repeated stages, a changed carrier volume, a multi-role replacement +and changes to the surrounding caller require separate evidence. +The complete comparable witness remains κ = 0.003645669928698. + +## Replay + +From a clean checkout with CPython 3.12 and assertions enabled: + +~~~sh +python3.12 -B scripts/research_package.py --package research/p104-even-idle-projector-bound +python3.12 -B scripts/check_research_commit.py --package research/p104-even-idle-projector-bound --check-modes --check-source-history +~~~ + +From a Git-free export, this also emits all six complete receipts +into a fresh directory: + +~~~sh +python3.12 -I -B research/p104-even-idle-projector-bound/replay.py --out fresh-receipts +~~~ + +[PROVENANCE.json](PROVENANCE.json) pins seven public inputs by +commit, path, Git blob and SHA-256. [LOCAL-PINS.json](LOCAL-PINS.json) +pins the bundled replay closure by package-relative path. The +replay verifies all six deterministic plaintext receipts against +[SHA256.json](receipts/SHA256.json). [SUMMARY.json](receipts/SUMMARY.json) +contains the exact pre-support uppers and closed counts. +Only the standard library is required. + +## Credit and relation to earlier screens + +[#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) at +`07a76c5e2738882c0cb322278e56f6cae3c9885d` supplies the signed caller +and grouped-idle physical interface. [#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277) +at `ed090b57ed88f8859e5ff4643645099e6ba856ea` supplies the native +word and complete comparable invoice. [#7298](https://github.com/CrocSwap/integer-mult-bounds/pull/7298) +supplies the retained directed tariff and known-good invoice control. + +[Discussion #7111](https://github.com/CrocSwap/integer-mult-bounds/discussions/7111) +reports an earlier fixed-caller conjugacy screen of 1,984 pairs and +the common-cut projector criterion. Its local proof pins the older +signed caller with SHA-256 +`9557f713ab4ffb91ede05e8a6d5668c694b9940fc16f2f2d657e2f2b2cac2d3f`. +The matching [#7108 caller retained by #7113](https://github.com/CrocSwap/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/replay/supplier7108/CALLER.json) +has 256 Type A disjoint pairs, 1,536 Type B even-even pairs and +192 Type B odd-even pairs when its four odd-odd pairs are excluded. +This count and digest identify the earlier 18-stage stock. +Earlier local analysis of [#7003](https://github.com/CrocSwap/integer-mult-bounds/pull/7003) +and [#7002](https://github.com/CrocSwap/integer-mult-bounds/pull/7002) +used unit-body derivative projectors for other fixed-HOST bounds. +The present certificate replays the exact 17-stage Type B stock +with complete signed pricing and independent rational checks. + +[#7144](https://github.com/CrocSwap/integer-mult-bounds/pull/7144) +supplies the related diagonal-gauge rigidity result, +[#7295](https://github.com/CrocSwap/integer-mult-bounds/pull/7295) +the fixed-contact idle-capacity bound, +[#7296](https://github.com/CrocSwap/integer-mult-bounds/pull/7296) +the one-child displaced-volume bound for an odd/even pair, and +[#7305](https://github.com/CrocSwap/integer-mult-bounds/pull/7305) +the BIT arbitrary-slot analogue. OpenAI Codex and subagents +materially assisted. + +## Open next questions + +Can a multi-role grouped operator preserve both distinct normalized +projectors at a favorable complete price? Pin one changed child +action and its field-volume tariff. Bound compatible savings across +the full signed invoice before attempting a literal construction. +A surviving proposal still needs exact signed arbitrary-input +action, ownership, restoration, precision and tape checks. diff --git a/research/p104-even-idle-projector-bound/SOURCES.json b/research/p104-even-idle-projector-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-even-idle-projector-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-even-idle-projector-bound/TASK.json b/research/p104-even-idle-projector-bound/TASK.json new file mode 100644 index 0000000000..1cc56f15ed --- /dev/null +++ b/research/p104-even-idle-projector-bound/TASK.json @@ -0,0 +1,84 @@ +{ + "actual_scope": "One grouped Type B even IDLE_ONE at an arbitrary clock and role replacing two retained nonempty disjoint-mask even idles in the exact #7113 caller, under the complete #7277 bill.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent audit and packaging.", + "author": "Even idle projector research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Find whether two literal even idles can share one grouped child before spending effort on a physical build.", + "budget_minutes": 4, + "evidence": "Complete 17-copy signed invoice, paired derivative necessary condition, independent exact rational prefix conjugacy, known-good singleton subset and swap/shear controls.", + "open_questions": [ + { + "blocked_by": "A candidate still needs exact signed arbitrary-input action, ownership and restoration, and fully charged routing, precision and tape.", + "first_step": "Pin the changed child action and field-volume tariff, then price the full compatible stock before building.", + "question": "Can a multi-role grouped operator preserve both old normalized derivative projectors at a favorable complete price?", + "why_it_matters": "One coordinate projector cannot equal the two distinct original projectors in any tested pair." + } + ], + "original_card": { + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "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": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "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": "joint-query-controller", + "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": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "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" + ] + }, + "outcome": "negative-result", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "This tests a disjoint-mask single-role replacement at arbitrary insertion, rather than fixed-J odd-idle demotion or a fixed-contact stock grant.", + "scope_status": "changed", + "stop_rule": "Save both complete optimistic prices before checking signed unit-body projectors. Exhaust the 544 singleton and all 1,348 disjoint pairs within their runner caps or report unresolved keys.", + "task_id": "joint-query-controller" +} diff --git a/research/p104-even-idle-projector-bound/VERIFY.json b/research/p104-even-idle-projector-bound/VERIFY.json new file mode 100644 index 0000000000..1b5aadc313 --- /dev/null +++ b/research/p104-even-idle-projector-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Rebuild the complete signed prices and exact 544/1,348 disjoint-mask projector exclusions, independently verify both rational phase probes, and check all six deterministic receipts.", + "timeout_seconds": 110 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-even-idle-projector-bound/dependencies/7113/research/signed-caller-8x9/replay/supplier7112/short-caller/check_odd_physical_binding.py b/research/p104-even-idle-projector-bound/dependencies/7113/research/signed-caller-8x9/replay/supplier7112/short-caller/check_odd_physical_binding.py new file mode 100644 index 0000000000..def1e6a184 --- /dev/null +++ b/research/p104-even-idle-projector-bound/dependencies/7113/research/signed-caller-8x9/replay/supplier7112/short-caller/check_odd_physical_binding.py @@ -0,0 +1,82 @@ +"""Check physical phase-polynomial substitution and exact paid occurrence binding.""" +from pathlib import Path +from hashlib import sha256 +from collections import Counter +import gzip +import json + +root=Path(__file__).resolve().parent +source=root/"upstream_application.py" +phase=root/"DATA-PHASES.json" +assert sha256(source.read_bytes()).hexdigest()=="d98987db98553dc55bfc80e3ca47abfcd51c57af6f8cda61101391d8eae94184" +assert sha256(phase.read_bytes()).hexdigest()=="c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" +cpath=root/"ODD-TYPE-AB-CALLER.json" +caller=json.loads(cpath.read_bytes()) +rec=json.loads((root/"ODD-TYPE-AB-REPLAY.json").read_text()) +assert sha256(cpath.read_bytes()).hexdigest()==rec["caller_sha256"] +word=json.loads(gzip.decompress((root.parent/"WORD.json.gz").read_bytes())) +sha=sha256(json.dumps(word,sort_keys=True,separators=(",",":")).encode()).hexdigest() +assert sha==rec["source_word_sha256"] +r=json.loads((root.parent/"RESULT.json").read_text()) +stages=caller["stages"] +ambient=9+8*stages +helper_count=sum(r["native"]["helpers"].values()) +main_count=sum(d["roles"]*len(d["ports"]) for d in caller["types"].values()) +a=source.read_text() +a=a[:a.index("def inverse(matrix):")] +def patch(old,new,count=1): + global a + assert a.count(old)==count,(old,a.count(old)) + a=a.replace(old,new) +patch("range(153)","range(expected_ambient)",2) +patch("caller['ambient_rank'] == 153 and caller['stages'] == 18","caller['ambient_rank'] == expected_ambient and caller['stages'] == expected_stages") +patch("list(range(1,19))","list(range(1,expected_stages+1))",2) +patch("len(helpers) == 1080","len(helpers) == expected_helpers") +patch("len(owners) == 3952","len(owners) == expected_mains") +patch("all(0 <= r < 38 for r in plane_a)","all(r in type_owners(caller, 'A') for r in plane_a)") +patch("all(38 <= r < 76 for r in plane_b[:2])","all(r in type_owners(caller, 'B') for r in plane_b[:2])") +patch("word['public']+51","word['public']+word['owned_fields']") +patch("op in ('QUERY','IDLE_ONE')","op in ('QUERY','IDLE_ONE','IDLE_ODD')") +patch("all(1 <= s <= 18 for s in selected)","all(1 <= s <= expected_stages for s in selected)") +patch("rank = 8*len(selected); idle_uses += len(kind['ports'])","""rank = 8*len(selected); idle_uses += len(kind['ports']) + if op == 'IDLE_ODD': + need(len(selected)==1 and a[1:]==[-1], 'one complete signed child') + rank += 1 + stage=selected[0] + for pi in kind['ports']: + q=word['ports'][pi] + axes=[q]+[1 << (9+8*(stage-1)+j) for j in range(8)] + need(all(dot(x,y)==(i==j) for i,x in enumerate(axes) for j,y in enumerate(axes)), + 'signed rank-nine axes are independent and orthonormal') + pos=terms((x,1) for x in axes) + signed=sub(pos,terms([(q,2)])) + need(translation(sub(pos,signed))==q,'exact negative central phase correction')""") +patch("len(selection)==18","len(selection)==expected_stages") +patch("ambient=153, native_calls=18, native_public=1480, fresh_helpers=19440", + "ambient=expected_ambient, native_calls=expected_stages, native_public=word['public'], fresh_helpers=expected_helpers*expected_stages") +patch("reserved_native_banks=18*51","reserved_native_banks=expected_stages*word['owned_fields']") +def type_owners(C,t): + x=C["types"][t] + return range(x["offset"],x["offset"]+x["roles"]) +env=dict(globals(),__file__=str(source),expected_ambient=ambient,expected_stages=stages, + expected_helpers=helper_count,expected_mains=main_count) +exec(compile(a,str(source),"exec"),env) +invoice={"P":rec["paid"],"T":rec["target"]} +f=env["complex_application"] +phases=json.loads(phase.read_bytes()) +result=f(word,caller,{"invoice":invoice},phases) +bad=next(i for i,e in enumerate(caller["events"]) if e[0]=="J") +caller["events"][bad][2][0]=caller["events"][bad][2][1] +try: + f(word,caller,{"invoice":invoice},phases) +except ValueError as e: + assert str(e)=="A owners" +else: + raise AssertionError("alias control") +record={"native_sha256":sha,"caller_sha256":rec["caller_sha256"], + "source_reviewer_sha256":sha256(source.read_bytes()).hexdigest(), + "patched_application_sha256":sha256(a.encode()).hexdigest(), + "occurrence_and_geometry":result,"aliased_main_rejected":True, + "scope":"Current caller port and ownership substitution, full phase-polynomial native contact identities on disjoint stage axes, whole signed idle/output geometry, and ordered paid positions. Retains the standard nested chart and local operator premises and requires separate full native replay and complete fixed-tape tariff application."} +with (root/"ODD-PHYSICAL-BINDING.json").open("x") as out:json.dump(record,out,indent=2) +print("PASS exact physical binding",result["paid_positions"],result["native_contact_boundaries"],result["productive_fields"],flush=True) diff --git a/research/p104-even-idle-projector-bound/dependencies/7298/RESULT.json b/research/p104-even-idle-projector-bound/dependencies/7298/RESULT.json new file mode 100644 index 0000000000..c66ad2ed50 --- /dev/null +++ b/research/p104-even-idle-projector-bound/dependencies/7298/RESULT.json @@ -0,0 +1,97 @@ +{ + "bit": { + "add_pairs": 30551, + "checked_edges": 62474, + "copies": 36, + "eligible": 0, + "normalized_neighbors": 31265, + "saving_upper": "0", + "shared_owned": 246, + "target": "10018846261809/2500000000000000", + "target_margin_upper": "-150259748047868384659982093203238820648182213480307/2500000000000000000000000000000000000000000000000", + "unresolved": 0 + }, + "complex": { + "cases": [ + { + "complete_upper": "-270628787660064862669178534471473339574581160716573/2000000000000000000000000000000000000000000000000", + "events": [ + [ + 34511, + 34513 + ], + [ + 36306, + 36308 + ], + [ + 41987, + 41989 + ] + ], + "new_ranks": [ + 4, + 4 + ], + "old_ranks": [ + 0, + 0 + ] + }, + { + "complete_upper": "-5299092335389733735192584095979599221603492103289/156250000000000000000000000000000000000000000000", + "events": [ + [ + 33139, + 33141 + ], + [ + 44255, + 44257 + ] + ], + "new_ranks": [ + 1, + 2 + ], + "old_ranks": [ + 0, + 1 + ] + }, + { + "complete_upper": "-844193076311159197372651950923578810446691810127887/5000000000000000000000000000000000000000000000000", + "events": [ + [ + 39852, + 39854 + ] + ], + "new_ranks": [ + 5, + 6 + ], + "old_ranks": [ + 0, + 1 + ] + } + ], + "copies": 17, + "counts": { + "all": 65118, + "different_charts": 4625, + "excluded": 14, + "shared_owned": 20 + }, + "probe": "91141748217473298207420876011401/25000000000000000000000000000000000", + "unresolved": 0 + }, + "controls": { + "cross_operands_rejected": true, + "nonnested_rank_not_dimension_gap": true, + "same_source_and_destination_commute": true, + "self_add_rejected": true + }, + "status": "PASS_ADJACENT_OWNED_ADD_EXCHANGE_BOUND" +} diff --git a/research/p104-even-idle-projector-bound/dependencies/7298/pricing.py b/research/p104-even-idle-projector-bound/dependencies/7298/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/p104-even-idle-projector-bound/dependencies/7298/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-even-idle-projector-bound/dependencies/7298/verify.py b/research/p104-even-idle-projector-bound/dependencies/7298/verify.py new file mode 100644 index 0000000000..a45510da25 --- /dev/null +++ b/research/p104-even-idle-projector-bound/dependencies/7298/verify.py @@ -0,0 +1,253 @@ +"""Replay the exact adjacent shared-owned ADD census on both native words.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import cache +from hashlib import sha1, sha256 +from itertools import pairwise +from pathlib import Path +import gzip +import json +import runpy + +HERE=Path(__file__).resolve().parent +BIT='research/paired-query-only-bit/' +PRICING=runpy.run_path(str(HERE/'pricing.py')) + + +def read(path,pin): + raw=path.read_bytes() + if raw.startswith(b'\x1f\x8b') and pin.get('uncompress',False): + raw=gzip.decompress(raw) + blob=sha1(f'blob {len(raw)}\0'.encode()+raw).hexdigest() + if sha256(raw).hexdigest()!=pin['sha256'] or blob!=pin['git_blob']: + raise ValueError('Changed input: '+path.name) + return raw + + +def rank(rows): + pivots={} + for x in rows: + while x and x.bit_length() in pivots: + x^=pivots[x.bit_length()] + if x: + pivots[x.bit_length()]=x + return len(pivots) + + +def commutes(a,b,c,d): + return a!=b and c!=d and a!=d and c!=b + + +def complex_scan(word,caller,early): + frames=word['frames'] + n=word['public'] + dims=list(map(len,frames)) + program=word['program'] + assert all(rank(f)==r for f,r in zip(frames,dims,strict=True)) + + @cache + def distance(a,b): + return 2*rank(frames[a]+frames[b])-dims[a]-dims[b] + + chains={} + at={} + scalar=[] + native=Counter() + for t,(tag,d,*args) in enumerate(program): + if tag=='MOVE': + a,b,owned=args + r=distance(a,b) + assert owned==(d>=n) and r==abs(dims[a]-dims[b])>0 + native[r]+=1 + continue + scalar.append(t) + if tag=='INIT': + assert d not in chains + chains[d]=[] + for role in {d,args[0]} if tag in ('ADD','COPY') else {d}: + if role>=n: + seq=chains[role] + at[t,role]=seq,len(seq) + seq.append(t) + if tag=='CLEAR': + del chains[d] + assert not chains and sum(native.values())==6280 + stages=[e[1] for e in caller['events'] if e[0]=='J'] + assert stages==list(range(1,18)) + copies=len(stages) + paid=Counter({r:copies*v for r,v in native.items()}) + main=set(word['live'])|{x+112 for x in word['live']}|set(word['hosted']['X2']+word['hosted']['Y2']) + helper=Counter(dims[b]-dims[a] for r,(a,b) in enumerate(zip(word['initial'],word['final'],strict=True)) if r not in main) + targets=Counter({r:copies*v for r,v in helper.items()}) + for info in caller['types'].values(): + for sign,offset,*bits in info['diagonal']: + assert (sign,offset,len(bits))==(-1,0,copies) + targets[1+8*sum(bits)]+=len(info['ports']) + for e in caller['events']: + if e[0]=='J': + continue + kind,tag,_,*args=e + if tag=='QUERY': + paid[1]+=len(caller['types'][kind]['ports']) + if tag in ('IDLE_ONE','IDLE_ODD'): + paid[8*len(args[0])+int(tag=='IDLE_ODD')]+=len(caller['types'][kind]['ports']) + assert dict(paid)=={int(r):v for r,v in early['invoice']['P'].items()} + assert dict(targets)=={int(r):v for r,v in early['invoice']['T'].items()} + assert sum(paid.values())==110536 and sum(targets.values())==22461 + net=targets.copy() + net.subtract(paid) + assert sum(r*v for r,v in net.items())==1424 + k=Q(early['price']['independent_raw_bracket'][1]) + base=PRICING['cost'](net,k) + assert base[1]<0 + counts=Counter() + rows=defaultdict(list) + for t,u in pairwise(scalar): + p,q=program[t],program[u] + if p[0]!=q[0] or p[0]!='ADD': + continue + counts['all']+=1 + a,b,f=p[1],p[2],p[-1] + c,d,g=q[1],q[2],q[-1] + if f==g: + continue + counts['different_charts']+=1 + shared={a,b}&{c,d} + if not any(role>=n for role in shared): + continue + counts['shared_owned']+=1 + if min(shared)0 and j+1=n for r in set(a[1:3])&set(b[1:3]))] + eligible=[(a,b) for a,b in owned if a[-1]!=b[-1]] + assert len(scalar)-1==31265 and len(all_pairs)==30551 and len(owned)==246 and not eligible + margin=PRICING['cost'](signed,Q(PRICING['TARGET']))[1] + assert margin<0 + return {'normalized_neighbors':len(scalar)-1,'add_pairs':len(all_pairs),'shared_owned':len(owned), + 'checked_edges':edges,'eligible':len(eligible),'unresolved':0,'copies':copies, + 'target':PRICING['TARGET'],'target_margin_upper':str(margin),'saving_upper':'0'} + + +def controls(): + assert commutes(0,2,1,2) and commutes(0,1,0,2) + assert not commutes(0,1,1,2) and not commutes(0,1,1,0) + assert not commutes(0,0,1,2) + assert 2*rank([1,2,1,4])-4==2 + return {'same_source_and_destination_commute':True,'cross_operands_rejected':True, + 'self_add_rejected':True,'nonnested_rank_not_dimension_gap':True} + + +def unique_keys(entries): + out={} + for k,v in entries: + if k in out: + raise ValueError('Duplicate manifest key: '+k) + out[k]=v + return out + + +def run(root): + p=json.loads((HERE/'PROVENANCE.json').read_bytes(),object_pairs_hook=unique_keys) + c={} + for k,pin in p['bundled'].items(): + raw=read(HERE/k,pin) + c[k]=json.loads(gzip.decompress(raw) if raw.startswith(b'\x1f\x8b') else raw) + rows=json.loads((HERE/'SOURCES.json').read_bytes(),object_pairs_hook=unique_keys)['files'] + pins=unique_keys((row['path'],row) for row in rows) + bitword=BIT+'retained/inputs/BIT-NATIVE-WORD.json.gz' + invoice=BIT+'EFREE-RESULT.json' + return {'status':'PASS_ADJACENT_OWNED_ADD_EXCHANGE_BOUND','controls':controls(), + 'complex':complex_scan(c['inputs/WORD.json.gz'],c['inputs/CALLER.json.gz'],c['inputs/EARLY-RESULT.json.gz']), + 'bit':bit_scan(json.loads(gzip.decompress(read(root/bitword,pins[bitword]))), + json.loads(read(root/invoice,pins[invoice])))} + + +if __name__=='__main__': + assert __debug__ + parser=ArgumentParser(description=__doc__) + parser.add_argument('--root',type=Path,default=Path.cwd()) + args=parser.parse_args() + result=json.dumps(run(args.root),sort_keys=True,indent=2)+'\n' + frozen=HERE/'RESULT.json' + if frozen.is_file(): + assert result==frozen.read_text() + print(result,end='') diff --git a/research/p104-even-idle-projector-bound/dependencies/round30/complex/source/inputs/CALLER.json.gz b/research/p104-even-idle-projector-bound/dependencies/round30/complex/source/inputs/CALLER.json.gz new file mode 100644 index 0000000000..290ef7c9c5 Binary files /dev/null and b/research/p104-even-idle-projector-bound/dependencies/round30/complex/source/inputs/CALLER.json.gz differ diff --git a/research/p104-even-idle-projector-bound/dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz b/research/p104-even-idle-projector-bound/dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz new file mode 100644 index 0000000000..8f4096badd Binary files /dev/null and b/research/p104-even-idle-projector-bound/dependencies/round30/complex/source/inputs/EARLY-RESULT.json.gz differ diff --git a/research/p104-even-idle-projector-bound/dependencies/round30/complex/source/inputs/WORD.json.gz b/research/p104-even-idle-projector-bound/dependencies/round30/complex/source/inputs/WORD.json.gz new file mode 100644 index 0000000000..077bf48c35 Binary files /dev/null and b/research/p104-even-idle-projector-bound/dependencies/round30/complex/source/inputs/WORD.json.gz differ diff --git a/research/p104-even-idle-projector-bound/engines/disjoint.py b/research/p104-even-idle-projector-bound/engines/disjoint.py new file mode 100644 index 0000000000..a0e6da4093 --- /dev/null +++ b/research/p104-even-idle-projector-bound/engines/disjoint.py @@ -0,0 +1,252 @@ +"""Disjoint-mask Type B idle pairing with an arbitrary insertion slot.""" + +from argparse import ArgumentParser +from bisect import bisect_left, bisect_right +from collections import Counter +from fractions import Fraction as Q +from functools import cache +from hashlib import sha256 +from itertools import combinations +import json +from math import isqrt +from pathlib import Path +import runpy +from time import monotonic + +R52 = "cdf54b266ac31fd0efe544badbb9840598d4c63c4d3cd363f60ae9a74cc4b256" +R52_PRICE = "95b4d2ca88d7716fcd86cbe07811703b9fadbad24dad15a3753b4bab49036e59" +R52_BODY = "487d2788192b1e9845a6b047c105050987dba7ba6f72aef413ce6261b1b9a3e5" +CAP = {"body1":22,"nonunit":22,"structural":42} + + +def checked(path,pin): + raw = path.read_bytes() + if sha256(raw).hexdigest() != pin: + raise ValueError(f"Changed input {path.name}") + return raw + + +def distinct_mask_pairs(jobs): + return [(a,b) for a,b in combinations(jobs,2) if jobs[a][1].isdisjoint(jobs[b][1])] + + +def compatible_upper(pairs,weights): + per_event = {} + for a,b in pairs: + w = weights[a,b] + assert w >= 0 + per_event[a] = max(w,per_event.get(a,0)) + per_event[b] = max(w,per_event.get(b,0)) + return sum(per_event.values(),Q(0))/2,per_event + + +def price(roots, old, known): + files = old["authenticate"](roots) + unpack = old["unpack"] + input_path = "round30/complex/source/inputs/" + word,caller,early = (unpack(files[input_path+x]) for x in ("WORD.json.gz","CALLER.json","EARLY-RESULT.json")) + predecessor = runpy.run_path(str(roots["7298"]/"verify.py")) + replay = predecessor["complex_scan"](word,caller,early) + assert json.loads(json.dumps(replay)) == unpack(files["7298/RESULT.json"])["complex"] + binding = next(raw for key,raw in files.items() if key.startswith("7113/")) + assert b"rank = 8*len(selected)" in binding + block = caller["types"]["B"] + ports = len(block["ports"]) + assert (block["roles"],block["offset"],ports,caller["stages"],replay["copies"]) == (36,36,8,17,17) + jobs = {} + for i,e in enumerate(caller["events"]): + if e[:2] == ["B","IDLE_ONE"]: + mask = frozenset(e[3]) + assert mask and len(mask) == len(e[3]) and all(1 <= x <= 17 for x in mask) + assert 36 <= e[2] < 72 + jobs[i] = (e[2]-36,mask) + assert len(jobs) == 60 + cases = distinct_mask_pairs(jobs) + assert len(cases) <= 1770 + singleton_pairs = [p for p in cases if all(len(jobs[i][1]) == 1 for i in p)] + assert len(singleton_pairs) == 544 and list(map(list,singleton_pairs)) == known["pair_keys"] + kappa = Q(replay["probe"]) + paid = Counter({int(k):v for k,v in early["invoice"]["P"].items()}) + targets = Counter({int(k):v for k,v in early["invoice"]["T"].items()}) + assert sum(paid.values()) == 110536 and sum(targets.values()) == 22461 + net = targets.copy() + net.subtract(paid) + assert sum(r*v for r,v in net.items()) == 1424 + cost = predecessor["PRICING"]["cost"] + power = predecessor["PRICING"]["power_bounds"] + old_margin = cost(net,kappa) + assert old_margin[1] < 0 + + @cache + def quote(r,s): + delta = Counter() + delta[r] += ports + delta[s] += ports + delta[r+s] -= ports + next_net = net.copy() + next_net.update(delta) + credit = cost(delta,kappa) + margin = cost(next_net,kappa) + assert credit[0] > 0 and margin[0] > 0 + a,b,c = power(r,kappa),power(s,kappa),power(r+s,kappa) + volume = ((a[0]+b[0])/c[1],(a[1]+b[1])/c[0]) + return {"old_ranks":[r,s],"new_rank":r+s,"paid_old_minus_new":dict(delta), + "credit":list(map(str,credit)), "complete_margin":list(map(str,margin)), + "break_even_volume_factor_before_other_charges":list(map(str,volume))} + + prices,weights,key_signatures = {},{},{} + for a,b in cases: + r,s = sorted(8*len(jobs[i][1]) for i in (a,b)) + signature = f"{r}+{s}" + prices[signature] = quote(r,s) + key_signatures[a,b] = signature + weights[a,b] = Q(prices[signature]["credit"][1]) + upper,event_bounds = compatible_upper(cases,weights) + pre = { + "head":old["HEAD"], "caller_head":old["CALLER_HEAD"], + "inputs":{**old["PINS"],"r52/lead/screen.py":R52,"r52/run/PRICE.json":R52_PRICE, + "r52/run/BODY1.json":R52_BODY}, + "crossing_upper":str(kappa),"native_copies":17,"type_b_ports":ports, + "old_complete_paid":paid,"old_complete_targets":targets,"old_complete_margin":list(map(str,old_margin)), + "job_masks":[[i,r,sorted(mask)] for i,(r,mask) in jobs.items()], + "mask_size_counts":dict(Counter(len(m) for r,m in jobs.values())), + "price_by_rank_signature":prices, + "pair_keys":[[a,b,key_signatures[a,b]] for a,b in cases], + "singleton_control_pairs":len(singleton_pairs),"scope_pairs":len(cases),"pair_cap":1770, + "per_event_upper":{i:str(x) for i,x in event_bounds.items()}, + "whole_compatible_optimistic_upper":str(upper), + "whole_upper_rule":"half sum of per-event maximum incident upper credit", + "one_new_grouped_idle_clock_and_role":"arbitrary", + "equal_original_volume_and_free_extra_work_granted":True, + "followup":{"nonunit_body_vectors":old["BODIES"],"pin_union_coordinates_to_one":True, + "nonunit_hard_seconds":25, + "structural_max_cases":3,"structural_hard_seconds":45}, + } + return pre,caller,jobs,cases,weights + + +def controls(old): + jobs = {10:(0,frozenset({1,2})),20:(1,frozenset({2,3})),30:(0,frozenset({4}))} + assert distinct_mask_pairs(jobs) == [(10,30),(20,30)] + assert compatible_upper([(10,30),(20,30)],{(10,30):Q(1),(20,30):Q(2)})[0] == Q(5,2) + vector,_ = old["transport"]([],0,False,old["MOD"],2) + assert old["outside"](vector,1) == [0,1] + swap = [(0,"SWAP",0,1,0)] + vector,_ = old["transport"](swap,0,False,old["MOD"],2) + dual,_ = old["transport"](swap,1,True,old["MOD"],2) + assert old["outside"](vector,1) is None and old["outside"](dual,0) is None + return [*old["controls"](),"multistage_intersection_rejected","per_event_weight_bound", + "different_projectors_fail_common_derivative","transported_projectors_pass"] + + +def nonunit_stage(old,caller,jobs,cases,bodies,deadline): + # Different pairs require different identity loci for their removed idles. + # Reuse transports only when that mask union is identical. + compiled = {} + rows = [] + for a,b in cases: + if monotonic() >= deadline: + break + source,first_mask = jobs[a] + target,second_mask = jobs[b] + union = first_mask | second_mask + if union not in compiled: + values = [tuple(1 if j in union else v for j,v in enumerate(body,1)) for body in bodies] + compiled[union] = [(n,q,*old["compile_gates"](caller,q,body)) + for n,body in enumerate(values) for q in (1,old["MOD"]-1)] + if monotonic() >= deadline: + break + witness = None + for i,q,clocks,gates in compiled[union]: + interval = gates[bisect_right(clocks,a):bisect_left(clocks,b)] + write,_ = old["transport"](interval,source,False,old["MOD"]) + read,_ = old["transport"](interval,target,True,old["MOD"]) + outside_write = old["outside"](write,target) + outside_read = old["outside"](read,source) + if outside_write or outside_read: + witness = {"vector_index":i,"q":1 if q == 1 else -1, + "outside_write":outside_write,"outside_read":outside_read} + break + rows.append({"key":[a,b],"unit_body_mask":sorted(union),"witness":witness}) + return rows + + +def main(args,start): + checked(args.r52,R52) + old = runpy.run_path(str(args.r52)) + known = json.loads(checked(args.r52_run/"PRICE.json",R52_PRICE)) + known_body = json.loads(checked(args.r52_run/"BODY1.json",R52_BODY)) + assert known_body["exclusions"] == known_body["visited"] == 544 and not known_body["unvisited"] + known_by_key = {tuple(r["key"]):r["witness"] for r in known_body["records"]} + roots = {"round30":args.round30,"7298":args.predecessor,"7113":args.caller_root} + pre,caller,jobs,cases,weights = price(roots,old,known) + out = args.out + if args.stage in ("price","body1"): + pin = old["save"](out,"PRICE.json",pre) + else: + frozen = (out/"PRICE.json").read_bytes() + assert json.loads(frozen) == json.loads(json.dumps(pre)) + pin = sha256(frozen).hexdigest() + if args.stage == "price": + return + assert all(old["MOD"]%d for d in range(2,isqrt(old["MOD"])+1)) + checks = controls(old) + by_clock = {i:r for i,(r,mask) in jobs.items()} + remaining = [] + if args.stage != "body1": + earlier = old["previous"](out,"BODY1.json" if args.stage == "nonunit" else "NONUNIT.json",pin) + cases = list(map(tuple,earlier["survivors"])) + remaining = list(map(tuple,earlier["unvisited"])) + deadline = start+CAP[args.stage] + if args.stage in ("body1","nonunit"): + bodies = ((1,)*17,) if args.stage == "body1" else old["BODIES"] + if args.stage == "body1": + rows = old["modular_stage"](caller,by_clock,cases,bodies,deadline) + else: + rows = nonunit_stage(old,caller,jobs,cases,bodies,deadline) + survivors = [tuple(r["key"]) for r in rows if r["witness"] is None] + unvisited = remaining+cases[len(rows):] + upper,_ = compatible_upper([*survivors,*unvisited],weights) + singleton_matched = 0 + if args.stage == "body1": + for row in rows: + key = tuple(row["key"]) + if key in known_by_key: + assert row["witness"] == known_by_key[key] + singleton_matched += 1 + if len(rows) == len(cases): + assert singleton_matched == 544 + old["save"](out,"BODY1.json" if args.stage == "body1" else "NONUNIT.json",{ + "price_sha256":pin,"stage":args.stage,"scope":len(cases),"visited":len(rows), + "exclusions":len(rows)-len(survivors),"survivors":survivors,"unvisited":unvisited, + "unresolved_optimistic_upper":str(upper),"singleton_controls_matched":singleton_matched, + "prime":old["MOD"],"body_vectors":bodies,"records":rows,"controls":checks, + }) + return + rows = [] + for a,b in cases[:3]: + if monotonic() >= deadline: + break + status,mixed,clock = old["structural"](caller,a,b,by_clock[a],by_clock[b]) + rows.append({"key":[a,b],"status":status,"nondiagonal_transient":mixed,"stop_clock":clock}) + unvisited = remaining+cases[len(rows):] + unresolved = [r["key"] for r in rows if r["status"] != "formal_projector_transport"] + old["save"](out,"STRUCTURAL.json",{ + "price_sha256":pin,"scope":len(cases),"visited":len(rows),"unvisited":unvisited, + "unresolved":unresolved,"records":rows, + "support_survivors":[r["key"] for r in rows if r["status"] == "formal_projector_transport"], + "controls":checks, + }) + + +if __name__ == "__main__": + start = monotonic() + if not __debug__: + raise RuntimeError("Assertions required") + p = ArgumentParser(description=__doc__) + for name in ("round30","predecessor","caller-root","r52","r52-run","out"): + p.add_argument("--"+name,type=lambda x:Path(x).resolve(),required=True) + p.add_argument("--stage",choices=("price","body1","nonunit","structural"),default="body1") + args = p.parse_args() + args.out.mkdir(parents=True,exist_ok=True) + main(args,start) diff --git a/research/p104-even-idle-projector-bound/engines/independent_disjoint.py b/research/p104-even-idle-projector-bound/engines/independent_disjoint.py new file mode 100644 index 0000000000..fb27cfb012 --- /dev/null +++ b/research/p104-even-idle-projector-bound/engines/independent_disjoint.py @@ -0,0 +1,116 @@ +"""Independent exact rational prefix-conjugate projector test.""" +from argparse import ArgumentParser +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path +from signal import SIGALRM, alarm, signal + +CALLER = '255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc' + + +def basis(n): + return [[Q(i == j) for i in range(n)] for j in range(n)] + + +def mix(a,b,c,d): + return [c*x+d*y for x,y in zip(a,b,strict=True)] + + +def canonical(row,col): + assert sum(x*y for x,y in zip(row,col,strict=True)) == 1 + pivot = next(x for x in row if x) + return tuple(x/pivot for x in row),tuple(x*pivot for x in col) + + +def controls(): + R,C = basis(2),basis(2) + original = canonical(R[0],C[0]) + R.reverse() + C.reverse() + assert canonical(R[1],C[1]) == original + R[1] = mix(R[1],R[0],Q(1),Q(-2)) + C[0] = mix(C[0],C[1],Q(1),Q(2)) + assert canonical(R[1],C[1]) != original + return ['swap_projector_relabel','signed_shear_changes_projector'] + + +def sample(c,q): + ty = c['types']['B'] + offset,n = ty['offset'],ty['roles'] + R,C = basis(n),basis(n) + found = {} + for i,e in enumerate(c['events']): + if e[0]=='J': + s,t,alpha,beta = e[3] + s,t = s-offset,t-offset + a,b,cc,d = Q(1),Q(alpha)*q,1/(2*q),Q(beta) + assert a*d-b*cc == 1 + row_s,row_t = R[s],R[t] + col_s,col_t = C[s],C[t] + R[s],R[t] = mix(row_s,row_t,a,b),mix(row_s,row_t,cc,d) + C[s],C[t] = mix(col_s,col_t,d,-cc),mix(col_s,col_t,-b,a) + continue + if e[0]!='B': + continue + _,op,r,*args = e + r -= offset + if op=='IDLE_ONE': + assert args[0] and len(args[0]) == len(set(args[0])) + found[i] = (r+offset,tuple(args[0]),canonical(R[r],C[r])) + continue + if op=='SWAP': + s = args[0]-offset + R[r],R[s] = R[s],R[r] + C[r],C[s] = C[s],C[r] + elif op in ('QUERY','ADD'): + s = args[0]-offset + k = q**args[1] if op=='QUERY' else Q(args[1]) + R[r] = mix(R[r],R[s],Q(1),k) + C[s] = mix(C[s],C[r],Q(1),-k) + else: + assert op in ('LAMBDA','IDLE_ODD','SCALE') + k = Q(1) if op=='LAMBDA' else q**args[1] if op=='IDLE_ODD' else Q(args[0]) + assert k + R[r] = [x*k for x in R[r]] + C[r] = [x/k for x in C[r]] + assert len(found)==60 + for j,diag in enumerate(ty['diagonal']): + want = q**diag[0] + assert R[j] == [Q(k == j)*want for k in range(n)] + for k in range(n): + assert sum(a*b for a,b in zip(R[j],C[k],strict=True)) == (j==k) + return found + + +def run(c): + plus,minus = [sample(c,Q(q)) for q in (1,-1)] + assert list(plus)==list(minus) + checked = [] + for first,second in combinations(plus,2): + r,a,x = plus[first] + s,b,y = plus[second] + assert (r,a)==minus[first][:2] and (s,b)==minus[second][:2] + if not set(a).isdisjoint(b): + continue + p = x==y + m = minus[first][2]==minus[second][2] + checked.append({'clocks':[first,second],'roles':[r,s],'masks':[a,b], + 'plus':p,'minus':m}) + assert len(checked)<=1770 + return {'caller_sha256':CALLER,'checked':len(checked),'controls':controls(), + 'both_survivors':sum(r['plus'] and r['minus'] for r in checked), + 'rows':checked} + + +if __name__ == '__main__': + p = ArgumentParser(description=__doc__) + p.add_argument('caller',type=Path) + a = p.parse_args() + signal(SIGALRM,lambda *_: (_ for _ in ()).throw(TimeoutError('exact prefix watchdog'))) + alarm(25) + raw = a.caller.read_bytes() + assert sha256(raw).hexdigest()==CALLER + print(json.dumps(run(json.loads(raw)),indent=2,sort_keys=True)) + alarm(0) diff --git a/research/p104-even-idle-projector-bound/engines/independent_singleton.py b/research/p104-even-idle-projector-bound/engines/independent_singleton.py new file mode 100644 index 0000000000..2a0413369d --- /dev/null +++ b/research/p104-even-idle-projector-bound/engines/independent_singleton.py @@ -0,0 +1,116 @@ +"""Independent exact rational prefix-conjugate projector test.""" +from argparse import ArgumentParser +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path +from signal import SIGALRM, alarm, signal + +CALLER = '255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc' + + +def basis(n): + return [[Q(i == j) for i in range(n)] for j in range(n)] + + +def mix(a,b,c,d): + return [c*x+d*y for x,y in zip(a,b,strict=True)] + + +def canonical(row,col): + assert sum(x*y for x,y in zip(row,col,strict=True)) == 1 + pivot = next(x for x in row if x) + return tuple(x/pivot for x in row),tuple(x*pivot for x in col) + + +def controls(): + R,C = basis(2),basis(2) + original = canonical(R[0],C[0]) + R.reverse() + C.reverse() + assert canonical(R[1],C[1]) == original + R[1] = mix(R[1],R[0],Q(1),Q(-2)) + C[0] = mix(C[0],C[1],Q(1),Q(2)) + assert canonical(R[1],C[1]) != original + return ['swap_projector_relabel','signed_shear_changes_projector'] + + +def sample(c,q): + ty = c['types']['B'] + offset,n = ty['offset'],ty['roles'] + R,C = basis(n),basis(n) + found = {} + for i,e in enumerate(c['events']): + if e[0]=='J': + s,t,alpha,beta = e[3] + s,t = s-offset,t-offset + a,b,cc,d = Q(1),Q(alpha)*q,1/(2*q),Q(beta) + assert a*d-b*cc == 1 + row_s,row_t = R[s],R[t] + col_s,col_t = C[s],C[t] + R[s],R[t] = mix(row_s,row_t,a,b),mix(row_s,row_t,cc,d) + C[s],C[t] = mix(col_s,col_t,d,-cc),mix(col_s,col_t,-b,a) + continue + if e[0]!='B': + continue + _,op,r,*args = e + r -= offset + if op=='IDLE_ONE': + if len(args[0])==1: + found[i] = (r+offset,args[0][0],canonical(R[r],C[r])) + continue + if op=='SWAP': + s = args[0]-offset + R[r],R[s] = R[s],R[r] + C[r],C[s] = C[s],C[r] + elif op in ('QUERY','ADD'): + s = args[0]-offset + k = q**args[1] if op=='QUERY' else Q(args[1]) + R[r] = mix(R[r],R[s],Q(1),k) + C[s] = mix(C[s],C[r],Q(1),-k) + else: + assert op in ('LAMBDA','IDLE_ODD','SCALE') + k = Q(1) if op=='LAMBDA' else q**args[1] if op=='IDLE_ODD' else Q(args[0]) + assert k + R[r] = [x*k for x in R[r]] + C[r] = [x/k for x in C[r]] + assert len(found)==34 + for j,diag in enumerate(ty['diagonal']): + want = q**diag[0] + assert R[j] == [Q(k == j)*want for k in range(n)] + for k in range(n): + assert sum(a*b for a,b in zip(R[j],C[k],strict=True)) == (j==k) + return found + + +def run(c): + plus,minus = [sample(c,Q(q)) for q in (1,-1)] + assert list(plus)==list(minus) + checked = [] + for first,second in combinations(plus,2): + r,a,x = plus[first] + s,b,y = plus[second] + assert (r,a)==minus[first][:2] and (s,b)==minus[second][:2] + if a==b: + continue + p = x==y + m = minus[first][2]==minus[second][2] + checked.append({'clocks':[first,second],'roles':[r,s],'stages':[a,b], + 'plus':p,'minus':m}) + assert len(checked)==544 + return {'caller_sha256':CALLER,'checked':len(checked),'controls':controls(), + 'both_survivors':sum(r['plus'] and r['minus'] for r in checked), + 'rows':checked} + + +if __name__ == '__main__': + p = ArgumentParser(description=__doc__) + p.add_argument('caller',type=Path) + a = p.parse_args() + signal(SIGALRM,lambda *_: (_ for _ in ()).throw(TimeoutError('exact prefix watchdog'))) + alarm(25) + raw = a.caller.read_bytes() + assert sha256(raw).hexdigest()==CALLER + print(json.dumps(run(json.loads(raw)),indent=2,sort_keys=True)) + alarm(0) diff --git a/research/p104-even-idle-projector-bound/engines/singleton.py b/research/p104-even-idle-projector-bound/engines/singleton.py new file mode 100644 index 0000000000..8ccb073f0b --- /dev/null +++ b/research/p104-even-idle-projector-bound/engines/singleton.py @@ -0,0 +1,360 @@ +"""Priced Type B idle pairing and bounded signed projector transport.""" + +from argparse import ArgumentParser +from bisect import bisect_left, bisect_right +from collections import Counter, defaultdict +from fractions import Fraction as Q +import gzip +from hashlib import sha256 +from heapq import heapify, heappop, heappush +from itertools import combinations +import json +from math import isqrt +from pathlib import Path +import runpy +from time import monotonic + +HEAD = "ed090b57ed88f8859e5ff4643645099e6ba856ea" +CALLER_HEAD = "07a76c5e2738882c0cb322278e56f6cae3c9885d" +PINS = { + "round30/complex/source/inputs/WORD.json.gz": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "round30/complex/source/inputs/CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "round30/complex/source/inputs/EARLY-RESULT.json": "691025fe95c7938a6da211244d4d5b6187d88a9de1acff0862eeb7f0ce7deaa7", + "7298/verify.py": "4a4291c9019ef23c664ae9646b076dc57054b49f5c5ffd21908aa9f0edf19902", + "7298/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "7298/RESULT.json": "aaf594b981f37e7dbddb12fd052d9286cf5c8c95c8d5265ab6426408f6e58cc5", + "7113/research/signed-caller-8x9/replay/supplier7112/short-caller/check_odd_physical_binding.py": + "5c80c3b0415a7f91d216395248dd6f13297eed637732098e1ca8fb0548951b98", +} +MOD = 65521 +N = 36 +BODIES = (tuple(range(2,19)), (19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89)) +CAP = {"body1":22, "nonunit":22, "structural":42} + + +def unpack(raw): + return json.loads(gzip.decompress(raw) if raw[:2] == b"\x1f\x8b" else raw) + + +def save(out,name,payload): + raw = (json.dumps(payload,sort_keys=True,indent=2)+"\n").encode() + tmp = out/(name+".tmp") + tmp.write_bytes(raw) + tmp.replace(out/name) + return sha256(raw).hexdigest() + + +def authenticate(roots): + files = {} + for key, pin in PINS.items(): + label,path = key.split("/",1) + raw = (roots[label]/path).read_bytes() + if sha256(raw).hexdigest() != pin: + raise ValueError(f"Changed input {key}") + files[key] = raw + return files + + +def maximum_matching(jobs): + groups = defaultdict(list) + for clock,role,stage in jobs: + groups[stage].append(clock) + heap = [(-len(g),s) for s,g in groups.items()] + heapify(heap) + selected = [] + while len(heap) > 1: + na,a = heappop(heap) + nb,b = heappop(heap) + selected.append(sorted((groups[a].pop(),groups[b].pop()))) + if na < -1: + heappush(heap,(na+1,a)) + if nb < -1: + heappush(heap,(nb+1,b)) + counts = Counter(j[2] for j in jobs) + upper = min(len(jobs)//2,len(jobs)-max(counts.values(),default=0)) + assert len(selected) == upper and len({x for pair in selected for x in pair}) == 2*upper + return selected,counts + + +def price(roots): + files = authenticate(roots) + base = "round30/complex/source/inputs/" + word,caller,early = (unpack(files[base+name]) for name in ("WORD.json.gz","CALLER.json","EARLY-RESULT.json")) + old = runpy.run_path(str(roots["7298"]/"verify.py")) + audit = old["complex_scan"](word,caller,early) + assert json.loads(json.dumps(audit)) == unpack(files["7298/RESULT.json"])["complex"] + binding = next(raw for key,raw in files.items() if key.startswith("7113/")) + assert b"rank = 8*len(selected)" in binding + assert (caller["stages"],caller["types"]["B"]["offset"],caller["types"]["B"]["roles"]) == (17,36,36) + ports = len(caller["types"]["B"]["ports"]) + assert ports == 8 + jobs = [(i,e[2]-36,e[3][0]) for i,e in enumerate(caller["events"]) + if e[:2] == ["B","IDLE_ONE"] and len(e[3]) == 1] + assert len(jobs) == 34 and all(0 <= r < N and 1 <= stage <= 17 for _,r,stage in jobs) + cases = [(s[0],t[0]) for s,t in combinations(jobs,2) if s[2] != t[2]] + assert len(cases) == 544 + matching,counts = maximum_matching(jobs) + assert set(map(tuple,matching)) <= set(cases) + kappa = Q(audit["probe"]) + paid = Counter({int(k):v for k,v in early["invoice"]["P"].items()}) + targets = Counter({int(k):v for k,v in early["invoice"]["T"].items()}) + assert (sum(paid.values()),sum(targets.values()),audit["copies"]) == (110536,22461,17) + net = targets.copy() + net.subtract(paid) + delta = {8:2*ports,16:-ports} + changed = net.copy() + changed.update(delta) + cost = old["PRICING"]["cost"] + old_margin,new_margin,credit = cost(net,kappa),cost(changed,kappa),cost(delta,kappa) + assert old_margin[1] < 0 < new_margin[0] and credit[0] > 0 + h8 = old["PRICING"]["power_bounds"](8,kappa) + h16 = old["PRICING"]["power_bounds"](16,kappa) + report = { + "head":HEAD, "caller_head":CALLER_HEAD, "inputs":PINS, "crossing_upper":str(kappa), + "native_copies":audit["copies"], "type_b_ports":ports, "old_complete_paid":paid, + "old_complete_targets":targets, "old_complete_margin":list(map(str,old_margin)), + "one_pair_paid_old_minus_new":delta, "one_pair_complete_margin":list(map(str,new_margin)), + "one_pair_moment_credit":list(map(str,credit)), + "break_even_volume_factor":list(map(str,(2*h8[0]/h16[1],2*h8[1]/h16[0]))), + "whole_compatible_optimistic_upper":str(len(matching)*credit[1]), + "maximum_disjoint_pairs":len(matching), "illustrative_matching":matching, + "stage_counts":counts,"jobs":jobs,"pair_keys":cases, + "new_work_assumed_free_in_price":True, + "predeclared_followup":{"nonunit_body_vectors":BODIES,"nonunit_hard_seconds":25, + "structural_hard_seconds":45,"structural_max_cases":3}, + } + return report,caller + + +def field_scalar(raw): + q = Q(raw) + if q.denominator % MOD == 0: + raise ValueError("Nonunit modular denominator") + return q.numerator*pow(q.denominator,-1,MOD)%MOD + + +def compile_gates(caller,q,body): + gates = [] + for i,event in enumerate(caller["events"]): + kind,op,*args = event + if kind == "J": + s,t,a,b = args[1] + a,b = field_scalar(a),field_scalar(b) + m = body[op-1] + h = (m,m*a*q%MOD,m*b*q%MOD,m*(1+a*b)%MOD) + assert (h[0]*h[3]-h[1]*h[2])%MOD + gates.append((i,"J",s-36,t-36,h)) + elif kind == "B": + d = args[0]-36 + assert 0 <= d < N + if op == "ADD": + gates.append((i,op,d,args[1]-36,field_scalar(args[2]))) + elif op == "QUERY": + gates.append((i,"ADD",d,args[1]-36,pow(q,args[2]%4,MOD))) + elif op == "SWAP": + gates.append((i,op,d,args[1]-36,0)) + elif op == "SCALE": + value = field_scalar(args[1]) + assert value + gates.append((i,op,d,d,value)) + elif op in ("IDLE_ONE","IDLE_ODD"): + value = pow(q,args[2]%4,MOD) if op == "IDLE_ODD" else 1 + for stage in args[1]: + value = value*body[stage-1]%MOD + assert value + if value != 1: + gates.append((i,"SCALE",d,d,value)) + elif op != "LAMBDA": + raise ValueError(op) + return [g[0] for g in gates],gates + + +def transport(gates,initial,row,mod=None,dimension=N): + vec = [0]*dimension + vec[initial] = 1 + mixed = False + for _,op,d,s,c in reversed(gates) if row else gates: + if op == "ADD": + to,frm = (s,d) if row else (d,s) + vec[to] += c*vec[frm] + if mod: + vec[to] %= mod + elif op == "SCALE": + vec[d] *= c + if mod: + vec[d] %= mod + elif op == "SWAP": + vec[d],vec[s] = vec[s],vec[d] + elif op == "J": + a,b,x,y = c + if row: + b,x = x,b + u,v = vec[d],vec[s] + vec[d],vec[s] = (a*u+b*v)%mod,(x*u+y*v)%mod + else: + raise ValueError(op) + if mod is None and sum(bool(x) for x in vec) > 1: + mixed = True + assert any(vec) + return vec,mixed + + +def outside(vec,axis): + return next(([i,v] for i,v in enumerate(vec) if i != axis and v),None) + + +def controls(): + gates = [(0,"ADD",1,0,1),(1,"SCALE",0,0,2),(2,"ADD",1,0,-1)] + assert outside(transport(gates,0,False,MOD,2)[0],0) == [1,MOD-1] + gates[1] = (1,"SCALE",0,0,1) + assert outside(transport(gates,0,False,MOD,2)[0],0) is None + assert outside(transport(gates,0,True,MOD,2)[0],0) is None + assert transport(gates,0,False,None,2)[1] + read = [(0,"ADD",0,1,1)] + assert outside(transport(read,0,True,MOD,2)[0],0) == [1,1] + assert outside(transport(read,0,False,MOD,2)[0],0) is None + match,_ = maximum_matching([(i,0,s) for i,s in enumerate([1,1,1,1,2,3])]) + assert len(match) == 2 + caller = {"events":[["B","IDLE_ONE",36,[1]],["B","ADD",37,36,"1"], + ["B","ADD",37,36,"-1"],["B","IDLE_ONE",36,[2]]]} + assert structural(caller,0,3,0,0) == ("formal_projector_transport",True,None) + caller["events"][2] = ["B","ADD",37,36,"1"] + assert structural(caller,0,3,0,0) == ("unresolved_endpoint",True,3) + return ["body_one_false_positive","genuine_nondiagonal_transient","outside_read_only", + "distinct_mask_matching_does_not_double_spend"] + + +def modular_stage(caller,jobs,cases,bodies,deadline): + compiled = [(v,q,*compile_gates(caller,q,body)) + for v,body in enumerate(bodies) for q in (1,MOD-1)] + records = [] + for left,right in cases: + if monotonic() >= deadline: + break + source,target = jobs[left],jobs[right] + witness = None + for v,q,clocks,gates in compiled: + interval = gates[bisect_right(clocks,left):bisect_left(clocks,right)] + write,_ = transport(interval,source,False,MOD) + read,_ = transport(interval,target,True,MOD) + bad_col,bad_row = outside(write,target),outside(read,source) + if bad_col or bad_row: + witness = {"vector_index":v,"q":1 if q == 1 else -1, + "outside_write":bad_col,"outside_read":bad_row} + break + records.append({"key":[left,right],"witness":witness}) + return records + + +def structural(caller,left,right,source,target): + r = source + block = [] + mixed = False + + def flush(axis): + vec,m1 = transport(block,axis,False) + nz = [i for i,v in enumerate(vec) if v] + if len(nz) != 1: + return None,True + end = nz[0] + dual,m2 = transport(block,end,True) + return (None if outside(dual,axis) else end),m1 or m2 + + for clock,event in enumerate(caller["events"][left+1:right],left+1): + kind,op,*args = event + if kind == "B" and op in ("ADD","SCALE","SWAP"): + d = args[0]-36 + if op == "ADD": + block.append((clock,op,d,args[1]-36,Q(args[2]))) + elif op == "SCALE": + block.append((clock,op,d,d,Q(args[1]))) + else: + block.append((clock,op,d,args[1]-36,0)) + continue + if kind not in ("B","J"): + continue + r,inner = flush(r) + mixed |= inner + block.clear() + if r is None: + return "unresolved_constant_block",mixed,clock + if kind == "J" and r in {args[1][0]-36,args[1][1]-36}: + return "unresolved_active_j",True,clock + if kind == "B" and op == "QUERY" and r in {args[0]-36,args[1]-36}: + return "unresolved_query",True,clock + r,inner = flush(r) + mixed |= inner + if r != target: + return "unresolved_endpoint",mixed,right + return ("formal_projector_transport" if mixed else "diagonal_path_overlap_pending"),mixed,None + + +def previous(out,name,price_sha): + value = json.loads((out/name).read_text()) + assert value["price_sha256"] == price_sha + return value + + +def main(args,start): + roots = {"round30":args.round30,"7298":args.predecessor,"7113":args.caller_root} + pre,caller = price(roots) + out = args.out + if args.stage in ("price","body1"): + price_sha = save(out,"PRICE.json",pre) + else: + frozen = (out/"PRICE.json").read_bytes() + assert unpack(frozen) == json.loads(json.dumps(pre)) + price_sha = sha256(frozen).hexdigest() + if args.stage == "price": + return + jobs = {j[0]:j[1] for j in pre["jobs"]} + cases = pre["pair_keys"] + checks = controls() + assert all(MOD%d for d in range(2,isqrt(MOD)+1)) + prior_unvisited = [] + if args.stage != "body1": + first = previous(out,"BODY1.json",price_sha) + cases = first["survivors"] + prior_unvisited = first["unvisited"] + if args.stage == "structural": + second = previous(out,"NONUNIT.json",price_sha) + cases = second["survivors"] + prior_unvisited = second["unvisited"] + deadline = start+CAP[args.stage] + if args.stage in ("body1","nonunit"): + bodies = ((1,)*17,) if args.stage == "body1" else BODIES + rows = modular_stage(caller,jobs,cases,bodies,deadline) + survivors = [r["key"] for r in rows if r["witness"] is None] + save(out,("BODY1.json" if args.stage == "body1" else "NONUNIT.json"),{ + "stage":args.stage,"price_sha256":price_sha,"prime":MOD,"body_vectors":bodies, + "scope":len(cases),"visited":len(rows),"exclusions":len(rows)-len(survivors), + "survivors":survivors,"unvisited":[*prior_unvisited,*cases[len(rows):]], + "records":rows,"controls":checks, + }) + return + rows = [] + for a,b in cases[:3]: + if monotonic() >= deadline: + break + status,mixed,at = structural(caller,a,b,jobs[a],jobs[b]) + rows.append({"key":[a,b],"status":status,"nondiagonal_transient":mixed,"stop_clock":at}) + save(out,"STRUCTURAL.json",{ + "price_sha256":price_sha,"scope":len(cases),"visited":len(rows),"hard_seconds":45, + "unvisited":[*prior_unvisited,*cases[len(rows):]], + "support_survivors":[r["key"] for r in rows if r["status"] == "formal_projector_transport"], + "unresolved":[r["key"] for r in rows if r["status"] != "formal_projector_transport"], + "records":rows,"controls":checks, + }) + + +if __name__ == "__main__": + start = monotonic() + if not __debug__: + raise RuntimeError("Assertions required") + parser = ArgumentParser(description=__doc__) + for flag in ("round30","predecessor","caller-root","out"): + parser.add_argument("--"+flag,type=lambda x:Path(x).resolve(),required=True) + parser.add_argument("--stage",choices=("price","body1","nonunit","structural"),default="body1") + args = parser.parse_args() + args.out.mkdir(parents=True,exist_ok=True) + main(args,start) diff --git a/research/p104-even-idle-projector-bound/receipts/SHA256.json b/research/p104-even-idle-projector-bound/receipts/SHA256.json new file mode 100644 index 0000000000..4d23ff3ade --- /dev/null +++ b/research/p104-even-idle-projector-bound/receipts/SHA256.json @@ -0,0 +1,8 @@ +{ + "disjoint/BODY1.json": "69d6ca309cfc63ffb3b8afaeb09e2d339eb3076ff3b0fcfd949ddbb215c839b6", + "disjoint/INDEPENDENT.json": "c9a61b859f7d2d97c0d9a3c1e47e071758f26b174acb585b90a1c672c15e5337", + "disjoint/PRICE.json": "86f779c3eeb43563793e6ccb2227257ef732b2ca12fbbde2f9099988f903a484", + "singleton/BODY1.json": "487d2788192b1e9845a6b047c105050987dba7ba6f72aef413ce6261b1b9a3e5", + "singleton/INDEPENDENT.json": "35449ada90982a81e19b0248966cf1508e2dc51edc78e87fac777f597cceebae", + "singleton/PRICE.json": "95b4d2ca88d7716fcd86cbe07811703b9fadbad24dad15a3753b4bab49036e59" +} diff --git a/research/p104-even-idle-projector-bound/receipts/SUMMARY.json b/research/p104-even-idle-projector-bound/receipts/SUMMARY.json new file mode 100644 index 0000000000..a5ffbeee7e --- /dev/null +++ b/research/p104-even-idle-projector-bound/receipts/SUMMARY.json @@ -0,0 +1,41 @@ +{ + "caller_head": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "compatible_saving_after_support": "0", + "copies": 17, + "disjoint": { + "checked_pairs": 1348, + "exact_survivors": 0, + "excluded_pairs": 1348, + "jobs": 60, + "pre_support_compatible_upper": "11162471264108351139711286321123514505211941803639/312500000000000000000000000000000000000000000000", + "rank_signatures": 35, + "singleton_controls_matched": 544, + "unvisited": 0 + }, + "head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "kappa": "0.003645669928698", + "kappa_change": "0", + "singleton": { + "break_even_volume": [ + "158791632877538044859622909614073486275416195893004/158390875238660198284274137265104629227106331252243", + "26465272146256340809937151602345581045902699315501/26398479206443366380712356210850771537851055208707" + ], + "checked_pairs": 544, + "exact_survivors": 0, + "excluded_pairs": 544, + "jobs": 34, + "max_disjoint_pairs": 17, + "pair_complete_margin": [ + "3206061111022772602790178791730811442523751251741/10000000000000000000000000000000000000000000000000", + "3206061111022772602790178791730811442523751312653/10000000000000000000000000000000000000000000000000" + ], + "pair_credit": [ + "400757638877846575348772348968857048309864640761/1250000000000000000000000000000000000000000000000", + "100189409719461643837193087242214262077466160191/312500000000000000000000000000000000000000000000" + ], + "pre_support_compatible_upper": "1703219965230847945232282483117642455316924723247/312500000000000000000000000000000000000000000000", + "unvisited": 0 + }, + "type_b_ports": 8, + "unresolved": 0 +} diff --git a/research/p104-even-idle-projector-bound/replay.py b/research/p104-even-idle-projector-bound/replay.py new file mode 100644 index 0000000000..b17e38c7ae --- /dev/null +++ b/research/p104-even-idle-projector-bound/replay.py @@ -0,0 +1,168 @@ +"""Replay both even-idle pair stocks and their exact rational controls.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction as Q +import gzip +from hashlib import sha1, sha256 +import json +from pathlib import Path, PurePosixPath +import shutil +import subprocess +import sys +from tempfile import TemporaryDirectory + +HERE = Path(__file__).resolve().parent +CALLER = "round30/complex/source/inputs/CALLER.json" +HEAD = "ed090b57ed88f8859e5ff4643645099e6ba856ea" +CALLER_HEAD = "07a76c5e2738882c0cb322278e56f6cae3c9885d" + + +def unique(pairs): + result = dict(pairs) + if len(result) != len(pairs): + raise ValueError("duplicate JSON key") + return result + + +def read(path): + return json.loads(path.read_bytes(),object_pairs_hook=unique) + + +def authenticate(scratch): + pins = read(HERE / "LOCAL-PINS.json") + for key, expected in pins.items(): + rel = PurePosixPath(key) + if rel.is_absolute() or ".." in rel.parts or rel.as_posix() != key: + raise ValueError(f"invalid dependency path {key}") + if sha256((HERE / key).read_bytes()).hexdigest() != expected: + raise ValueError(f"changed dependency {key}") + deps = scratch / "dependencies" + shutil.copytree(HERE / "dependencies",deps) + provenance = read(HERE / "PROVENANCE.json")["files"] + assert len(provenance) == 7 and sum(p["uncompress"] for p in provenance.values()) == 2 + for key,pin in provenance.items(): + assert key in pins + raw = (HERE / key).read_bytes() + if pin["uncompress"]: + raw = gzip.decompress(raw) + (scratch / key).with_suffix("").write_bytes(raw) + assert sha256(raw).hexdigest() == pin["sha256"], key + assert sha1(f"blob {len(raw)}\0".encode()+raw).hexdigest() == pin["git_blob"], key + return deps + + +def run(script,*args): + done = subprocess.run([sys.executable,"-I","-B",str(script),*map(str,args)], + capture_output=True,check=True,timeout=25) + return done.stdout + + +def check_receipts(files,pins): + for key,path in files.items(): + if sha256(path.read_bytes()).hexdigest() != pins[key]: + raise ValueError(f"replay receipt changed: {key}") + + +def crosscheck(files,pins): + summary = read(HERE / "receipts/SUMMARY.json") + assert summary["head"] == HEAD and summary["caller_head"] == CALLER_HEAD + assert summary["copies"] == 17 and summary["type_b_ports"] == 8 + assert summary["unresolved"] == 0 and summary["compatible_saving_after_support"] == "0" + assert summary["kappa_change"] == "0" + results = {} + for scope,count in (("singleton",544),("disjoint",1348)): + p,b,i = (read(files[f"{scope}/{name}.json"]) for name in ("PRICE","BODY1","INDEPENDENT")) + assert p["head"] == HEAD and p["caller_head"] == CALLER_HEAD + assert p["native_copies"] == 17 and p["type_b_ports"] == 8 + assert b["price_sha256"] == pins[f"{scope}/PRICE.json"] + assert b["scope"] == b["visited"] == b["exclusions"] == i["checked"] == count + assert not b["unvisited"] and not b["survivors"] and i["both_survivors"] == 0 + assert i["caller_sha256"] == p["inputs"]["round30/complex/source/inputs/CALLER.json"] + modular = {tuple(row["key"]):row["witness"] for row in b["records"]} + exact = {tuple(row["clocks"]):row for row in i["rows"]} + assert len(modular) == len(exact) == count and modular.keys() == exact.keys() + jobs = {row[0]:(row[1],[row[2]] if scope == "singleton" else row[2]) + for row in p["jobs" if scope == "singleton" else "job_masks"]} + price_keys = {tuple(row[:2]) for row in p["pair_keys"]} + assert len(price_keys) == count and price_keys == exact.keys() + for key,witness in modular.items(): + row = exact[key] + assert not row["plus"] and not row["minus"] + assert witness["q"] in (-1,1) + assert not row["plus" if witness["q"] == 1 else "minus"] + assert any(v and v[1] for v in (witness["outside_read"],witness["outside_write"])) + roles,masks = zip(*(jobs[k] for k in key),strict=True) + row_masks = [[x] for x in row["stages"]] if scope == "singleton" else row["masks"] + assert row["roles"] == [r+36 for r in roles] + assert [sorted(m) for m in row_masks] == list(masks) + assert set(masks[0]).isdisjoint(masks[1]) + row = {"checked_pairs":count, "excluded_pairs":count, "unvisited":0, + "exact_survivors":0, "pre_support_compatible_upper":p["whole_compatible_optimistic_upper"]} + if scope == "singleton": + assert len(jobs) == 34 and p["maximum_disjoint_pairs"] == 17 + assert 17*Q(p["one_pair_moment_credit"][1]) == Q(p["whole_compatible_optimistic_upper"]) + row.update(jobs=34,max_disjoint_pairs=17,pair_credit=p["one_pair_moment_credit"], + pair_complete_margin=p["one_pair_complete_margin"], + break_even_volume=p["break_even_volume_factor"]) + else: + assert len(jobs) == 60 and len(p["price_by_rank_signature"]) == 35 + assert b["singleton_controls_matched"] == 544 and b["unresolved_optimistic_upper"] == "0" + endpoint_upper = Counter() + for a,t,k in p["pair_keys"]: + r,s = sorted(8*len(jobs[c][1]) for c in (a,t)) + assert k == f"{r}+{s}" + quote = p["price_by_rank_signature"][k] + assert quote["old_ranks"] == [r,s] and quote["new_rank"] == r+s + assert Q(quote["complete_margin"][0]) > 0 + credit = Q(quote["credit"][1]) + for c in (a,t): + endpoint_upper[c] = max(endpoint_upper[c],credit) + assert sum(endpoint_upper.values(),Q(0))/2 == Q(p["whole_compatible_optimistic_upper"]) + row.update(jobs=60,rank_signatures=35,singleton_controls_matched=544) + assert row == summary[scope] + results[scope] = (p,jobs,modular) + s,sjobs,sm = results["singleton"] + d,djobs,dm = results["disjoint"] + assert sm.keys() < dm.keys() and all(dm[k] == v for k,v in sm.items()) + assert sjobs == {k:v for k,v in djobs.items() if len(v[1]) == 1} + for key in ("crossing_upper","old_complete_paid","old_complete_targets","old_complete_margin"): + assert s[key] == d[key] + + +def replay(output): + with TemporaryDirectory(prefix="p104-even-idle-") as temp: + scratch = Path(temp) + deps = authenticate(scratch) + pins = read(HERE / "receipts/SHA256.json") + files = {} + earlier = scratch / "singleton" + engines = HERE / "engines" + options = ["--round30",deps/"round30","--predecessor",deps/"7298","--caller-root",deps/"7113"] + for scope,extra in ( + ("singleton",[]), + ("disjoint",["--r52",engines/"singleton.py","--r52-run",earlier]), + ): + result = scratch / scope + run(engines / (scope+".py"),*options,"--out",result,"--stage","body1",*extra) + (result/"INDEPENDENT.json").write_bytes(run(engines / f"independent_{scope}.py",deps/CALLER)) + current = {f"{scope}/{name}.json":result/f"{name}.json" + for name in ("PRICE","BODY1","INDEPENDENT")} + check_receipts(current,pins) + files.update(current) + assert files.keys() == pins.keys() + crosscheck(files,pins) + if output is not None: + output.mkdir(parents=True,exist_ok=False) + for key,path in files.items(): + target = output/key + target.parent.mkdir(parents=True,exist_ok=True) + shutil.copyfile(path,target) + print("PASS_EVEN_IDLE_PROJECTOR_BOUND singleton=544 disjoint=1348 exact_survivors=0 unresolved=0 saving_upper=0 kappa_change=0") + + +if __name__ == "__main__": + assert __debug__, "run with assertions enabled" + assert sys.version_info[:2] == (3,12), "Python 3.12 required" + p = ArgumentParser(description=__doc__) + p.add_argument("--out",type=Path,help="fresh directory for all six full receipts") + replay(p.parse_args().out)