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-signed-factor-circuit-gauge/NOTICE b/research/p104-signed-factor-circuit-gauge/NOTICE new file mode 100644 index 0000000000..89c3cb07b3 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/NOTICE @@ -0,0 +1 @@ +Apache-2.0 contribution. Source lineage and exact predecessor paths are in PROVENANCE.json. OpenAI Codex and its subagents materially assisted the proof, implementation, independent verification and packaging. diff --git a/research/p104-signed-factor-circuit-gauge/PINS.txt b/research/p104-signed-factor-circuit-gauge/PINS.txt new file mode 100644 index 0000000000..427651ca99 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/PINS.txt @@ -0,0 +1,24 @@ +69f0be29c1ec509081505e4070b5ed8b4485194409c66a28e971095bf6edd25f closure/construct/RESULT.json +f946d4d02f0dc60fca48beaec5105f195257711fc9063f5b0aa0fd4a98cbe239 closure/construct/factorize.py +4dcf3462036fe196ce02346ad0d8b8f5136e295bd029e9ed27a465aef3633292 closure/construct/run.py +2a6c582059a54b8e97f44043b00d90cf537e45276b6d700f9e555f18ee1552d6 closure/independent/RESULT.json +91c17d100b8f06a1fd8b8bc8e5f4a1b2cc3bf5900d0a9e70f8faeb27e3da48df closure/independent/replay.py +ab74c834d4b94c63cda667338055889667e8e7a98c022ba6ed23afa35ff0acfe closure/lead/RESULT.json +82959a8be9c332698e402fc963e0c3af8dfac6522128100851dd96c767e162d5 closure/lead/dependency.py +064e11ecfedce9937ea1782e5baee37e89b3c9eebabed5b4a9ba84f412bbe078 closure/lead/inputs/7113-SHA256.json +ef03444360f02225138be9b38e2f9a85f313eeaa910d63a365de0f16d228cb8b closure/lead/inputs/7113-signed-child.py +255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc closure/lead/inputs/CALLER.json +49b7dbd3d08c56b16dc43f23bd6f410dde0b98040d922cee6f617786eb474834 closure/lead/inputs/R194.json +f6091c7c63b21145077808bbdacc61431f641d0da37f9fa648aea4b7ead3b472 closure/lead/inputs/R195.json +75d94780f9db49a4b08bb0e7fb4bd7fc04adb8cabbf73d83a809179c04c3d439 closure/lead/inputs/forward.py +223c521ab97dc43e6577ba5781b666c5282a5fc454f977322805dfb30b63688a closure/round209/construction/RESULT.json +f946d4d02f0dc60fca48beaec5105f195257711fc9063f5b0aa0fd4a98cbe239 closure/round209/construction/factorize.py +c92ffe2d09c17b0b6bb293304b53c64ec0b544866689aae3ecefa754113e3397 closure/round209/construction/run.py +3992ba3f17645e834f1d5aed3551d16e07a27e6234b2ef814e3dd87e1b00bb75 closure/round209/independent/RESULT.json +a76894295cfefdf697757c98f3fcc01943956696daca7e857d777ab13ef18f5b closure/round209/independent/replay.py +7f72ff06f411cf86ebed076ed004660e7ffb04fc9ef317efb1f4a2a5525e1884 closure/round209/lead/RESULT.json +be3cea9e2a190568f326423f43674cae42fb6db7c281707bf5a2e1c8785aa0fe closure/round209/lead/plane_gate.py +dc1fde12fa73744e8bb41461485db587cef31858fefac31141731ede55574437 closure/round210/independent/RESULT.json +e6a873f3242499b306b567cfddf1589c96428de11a9b6736f012bfbb89b07aa8 closure/round210/independent/replay.py +16311a16fa2f2143eeb951fc7c0600d1d6b5b407c60abe4d8fe362b4a3baf25e closure/round210/lead/RESULT.json +27a05f2e492ecc1d396ae8d26e3f4d7a61258c2bab2ade728302e716fe4db1db closure/round210/lead/body_gate.py diff --git a/research/p104-signed-factor-circuit-gauge/PROOF-FACTORS.md b/research/p104-signed-factor-circuit-gauge/PROOF-FACTORS.md new file mode 100644 index 0000000000..7fb272e3e9 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/PROOF-FACTORS.md @@ -0,0 +1,15 @@ +# Rank-minimal rational transvection factorization + +Let T be a determinant-one linear map over Q. Write D=T−I, F=ker D and k=rank D. A transvection has the form S=I+u f with u and f nonzero and f(u)=0. The exact minimum number of transvections for T is k when T is the identity or T²≠I, and k+1 when T is a nonidentity involution. + +A product of k−1 transvections has displacement rank at most k−1. If T=S U has rank k and U has displacement rank at most k−1, the decomposition D=(S−I)+S(U−I) has summands with disjoint image. Each therefore vanishes on F. Choose x fixed by U outside F. Then Dx=u f(x) is nonzero, f(x)≠0, and f(Dx)=0. If the action of T on V/F is λI for λ≠1, then f(Dx)=(λ−1)f(x) is nonzero, a contradiction. The determinant on V/F is one, so a rational nonidentity scalar quotient can only be −I. The condition on this quotient is equivalent to D²=−2D, hence to T²=I. + +For the construction, choose x outside F and f vanishing on F with f(x)=1 and f(Dx)=0. Set u=Dx and S=I+u f. The residual S⁻¹T fixes F and x. Rank subadditivity shows it drops exactly one. When T acts as identity on V/F, any x and a covector with f(x)=1 work because Dx is in F. The residual quotient also acts as identity. When T is nonscalar on V/F, choose x whose class and the class of Tx are independent. If the residual quotient has dimension at most one, its determinant-one action cannot be obstructed. Otherwise take a nonzero g vanishing on F, x and Tx. The two residual quotient maps from f and f+g differ by the nonzero rank-one operator −[Dx]gT. On a space of dimension at least two, two scalar operators cannot differ by rank one. At least one choice avoids the obstruction. Repeat to reach identity. All choices are rational row operations. If T is a nonidentity involution, split V into F and the −1 eigenspace. The latter has even positive dimension. Left-peel any nontrivial transvection supported there. The new residual still has displacement rank k and has a nonscalar action on V/F. The construction then uses k more factors. + +## Exact selected case + +The source is the `target_columns` of lead receipt `ab74c834d4b94c63cda667338055889667e8e7a98c022ba6ed23afa35ff0acfe`. The selected indices are `[0,2,4,6,8,10,12,14,18,19,20,22,24,26,28,30,32,34,36]`. Exact displacement rank is 18 and all 36 columns satisfy D²=−2D. The 19-factor control reconstructs every target column and checks every f(u)=0. Negating the image of the first factor leaves a transvection but fails exact product equality. The chosen 19-factor subset therefore cannot save one rank-one leg at the two real signs, even with arbitrary rational transvections. The other minimum support was not run. + +## Consequence for a distinct bounded follow-up + +Let R be the verified selected residual and B the product of the untouched old factors in chronological order. Because the complete 38-factor product equals −I, B=−R⁻¹. Thus B is a rank-18 involution, represented by 19 transvections. Delete any one factor from B and call the new product B′. Removing that factor is equivalent to left-peeling a conjugate of it. The rank of B′−I is at most 18 by the 18 remaining factors and at least 17 by the one-factor difference. The obstruction to a rank drop for an involution rules out rank 17. The new selected set of size 20 still contains the original full-suffix dependency, so its residual R′=−(B′)⁻¹ has displacement rank at most 19. Since the total displacement rank is 36, rank(R′−I) is 18 or 19. For rank 18 its +1 and −1 eigenspaces have dimensions 18 each, so it is an involution and needs 19 factors. For rank 19 the fixed-space dimension sum with B′ is 35, so it is not an involution and again needs 19 factors. This is an algebraic existence statement for the two real signs. It leaves unchanged-stage and physical cost, arbitrary body sectors, fourth-root central sectors, ownership, routing and restoration unverified. diff --git a/research/p104-signed-factor-circuit-gauge/PROOF-PLANES.md b/research/p104-signed-factor-circuit-gauge/PROOF-PLANES.md new file mode 100644 index 0000000000..ae5f28adb5 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/PROOF-PLANES.md @@ -0,0 +1,13 @@ +# Exact mixed-plane obligation for the selected 20-to-19 residual + +Pin the same 36-column normalized target `888ecc99fedd19dbf2f25cc962f775ab4566b45482165d87982b08972b5c7945` from `closure/round209/lead/RESULT.json` at `7f72ff06f411cf86ebed076ed004660e7ffb04fc9ef317efb1f4a2a5525e1884`. In the fixed 18+18 coordinate split write its blocks as A, upper-right, lower-left and B. Here A=−I₁₈, the upper-right is zero, the lower-left has rank 1 and 306 nonzero entries, and B−I is the rank-one block [[2,−2],[2,−2]] on the first two coordinates of the second plane. The rank of the complete displacement is 19. The deterministic rational factorizer supplies a 19-factor witness. Exact product replay and a first-factor sign mutation were checked. All its factors mix both fixed planes in both image and covector, and their outer-product entries are dyadic. + +The following argument is independent of that witness. In any factorization of this target by 19 transvections, let p and q count factors supported wholly in the first or second diagonal plane and let m=19−p−q count the remaining factors. Move all block-preserving factors to the right by conjugation. This preserves which factors are supported in a single plane. The result is T=W diag(P,Q), with W a product of m mixed factors, P a product of p first-plane transvections, and Q a product of q second-plane transvections. W is lower block triangular because T is, and its diagonal blocks A′ and B′ satisfy A=A′P and B=B′Q. + +Expanding the rank-one product gives W−I=UCV. U has the m original image columns and V the m original covector rows. For factors multiplied in their listed order, let Kᵢⱼ=fᵢ(uⱼ) when i0, peel the last factor of P on the right from −I₁₈=A′P. The resulting displacement would have rank at most r_A+p−1=17. A rank-one unipotent cannot reduce the displacement rank of −I: the difference is −2I plus a rank-one nilpotent, which is invertible. Hence p=0, and q≤1. If q=1, then m=18 and r_A=18, so U_A is invertible. The upper-right zero now gives V′_B=0, and the invertibility of C gives V_B=0. Each of the 18 mixed factors then has a covector that vanishes on the second plane. Each factor is lower block triangular and its A-block is a transvection or identity, since the nilpotence identity f(u)=0 reduces to f_A(u_A)=0. Their A-block product would realize −I₁₈ with 18 such factors, impossible by the same rank-drop obstruction. Therefore q=0 and m=19. Every one of the 19 factors must mix the two fixed planes. + +At length 19 the expansion also fixes the column and row spans of the factors. The full displacement rank implies im U=im(T−I) and row V=row(T−I). The projection of every factor covector on the second plane lies on the single line spanned by e₁₈*−e₁₉* in zero-based coordinates. Every second-plane image projection belongs to the span of the lower-left block’s column line and e₁₈+e₁₉. These lines are independent because the 306 nonzero lower-left entries occupy at least 17 rows, while e₁₈+e₁₉ has only two. This leaves exactly two shared second-plane image lanes and one shared covector lane at the normalized level. + +This covers fixed gathered relative coordinates at the two real signs. Conjugation from a different caller stage can change whether a factor is mixed in these coordinates. No arbitrary-body, nonreal-sector, physical routing, ownership, restoration, paid profile or κ result follows from this proof. diff --git a/research/p104-signed-factor-circuit-gauge/PROOF.md b/research/p104-signed-factor-circuit-gauge/PROOF.md new file mode 100644 index 0000000000..9ad59b1203 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/PROOF.md @@ -0,0 +1,19 @@ +# Signed factor circuits and one-body gauge + +Write the 38 chronological normalized relative factors as A₁,…,A₃₈ and let Q=A₃₈⋯A₁=−I. Transport factor i by the full suffix Sᵢ=A₃₈⋯Aᵢ₊₁. If U is the product of unselected factors in the original order, the selected transported product in increasing index order is Q U⁻¹ by cancellation. The product displacement is U₀ C V₀, where U₀ and V₀ are the transported image and covector families and C is unit triangular. A subset of size k has displacement rank k exactly when both restricted families have rank k. The full families each have rank 36 because Q−I has rank 36. Hence each 38-column coefficient kernel is two-dimensional. + +For either kernel write its two basis coordinates at index i as (aᵢ,bᵢ). A kernel vector is a nonzero linear combination of these bases. It always vanishes on coordinates with (aᵢ,bᵢ)=(0,0). Among remaining coordinates, its zeros can occupy exactly one projective slope class, or none. The largest slope class therefore gives minimum support. Both literal engines independently derive support 19 and the same lexicographic choice. The selected exact product is an involution of rank-18 displacement. [Exact factor length](PROOF-FACTORS.md). + +Adding index 1 makes the selected set size 20. The two engines agree on the rank-19 residual and its exact block form. The 19-factor replay is exact and a sign mutation fails. Any 19-factor realization needs all 19 factors to cross the fixed gathered split. These planes are in the gathered relative coordinates. A stage-specific change of basis can change which native operations cross. [Fixed-plane proof](PROOF-PLANES.md). + +## Legal D8 profile + +The binary Gaussian factor C fixes the plus Walsh vector and has eigenvalue i on the minus Walsh vector. For a fixed Type A port at admitted width f≥2, two central negative Walsh slices attain −1, with the all-plus central label attaining +1. In the disjoint stage-8 body block choose two negative Walsh bits to attain D8=−1, and leave the other bodies plus. The literal caller still scales all four J8 roles and the IDLE_ONE contacts that include stage 8. These body actions affect the relative prefixes even when the local body scale cancels between the two signs. Both engines verify the full comparator endpoint in each real sign and reject a missing body scale at basis role 0. + +The resulting residual equals E R E⁻¹, where R is the unit-body residual and E flips roles 9–17 and 27–35. Exactly 153 entries differ. At row 27, column 1 the value changes from −2 to +2. The independent rank-19 minor has determinant 524288. The replay transforms each actual witness factor I+u f to I+(Eu)(fE⁻¹), checks nilpotence and multiplies all 19 factors on all basis columns. Reusing the original witness without the gauge fails. This result covers one body profile and the two real signs. + +## Directed paid comparison + +The one-direct-host price p from the pinned #7420 receipt pays for 400 rank-eight body jobs, 16 Type B rank-one jobs and 96 Type A rank-one jobs, removing 6,279 native jobs and 1,101 productive helper credits. Its exact upper endpoint is `125835302963450101082086151823291979224042333232591/2500000000000000000000000000000000000000000000000`. This bounds the optimistic one-host saving above 50.33412118538 and below 50.33412118539 raw, before any additional charges introduced by lifting the factorization. + +The tested extension touches 17 hosts, with 18 hosted selected legs and two selected standalone QUERYs. Rebuilding all 17 hosts retains 16 old A legs and pays for 19 replacement A legs, retiring two standalone calls. The net is 33 Type A jobs at each of 96 ports. The exact upper bound is `17(p+96)−33×96`, strictly below −680.3199 raw. Additional routing cannot repair it. A positive route using the one-host quote would have to reuse the other 16 embedded hosts under their old body, mate and ownership contracts. No such realization or complete price is established. All-size operator, tape, precision and exponent claims remain open. diff --git a/research/p104-signed-factor-circuit-gauge/PROVENANCE.json b/research/p104-signed-factor-circuit-gauge/PROVENANCE.json new file mode 100644 index 0000000000..752abe5e54 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/PROVENANCE.json @@ -0,0 +1,80 @@ +{ + "ai_assistance": "OpenAI Codex and subagents materially assisted the proof, implementation, independent replay and packaging.", + "files": { + "closure/lead/inputs/7113-SHA256.json": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "git_blob": "5a7d6b80dc51aa918a5d521b60d18f9a6bbbc52e", + "path": "research/signed-caller-8x9/SHA256.json", + "sha256": "064e11ecfedce9937ea1782e5baee37e89b3c9eebabed5b4a9ba84f412bbe078", + "source": "https://github.com/rohanarun/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/SHA256.json" + }, + "closure/lead/inputs/7113-signed-child.py": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "git_blob": "0980a6559ba1939763de5c798c7947c8bdd51d67", + "path": "research/signed-caller-8x9/replay/supplier7112/short-caller/signed_child.py", + "sha256": "ef03444360f02225138be9b38e2f9a85f313eeaa910d63a365de0f16d228cb8b", + "source": "https://github.com/rohanarun/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/replay/supplier7112/short-caller/signed_child.py" + }, + "closure/lead/inputs/CALLER.json": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "git_blob": "9451ceaf6e8e037894680b549f3ef41c21b260d7", + "path": "research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json", + "sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "source": "https://github.com/rohanarun/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json" + }, + "closure/lead/inputs/R194.json": { + "commit": "a9809ce276aca6859e140404626c8772870215f2", + "git_blob": "53bb4c9b0cde9db92acd8261f6b9d2d9874a9319", + "path": "research/p104-signed-phase-leg-reuse-bound/receipts/R194-REVERSE.json", + "sha256": "49b7dbd3d08c56b16dc43f23bd6f410dde0b98040d922cee6f617786eb474834", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/a9809ce276aca6859e140404626c8772870215f2/research/p104-signed-phase-leg-reuse-bound/receipts/R194-REVERSE.json" + }, + "closure/lead/inputs/R195.json": { + "commit": "a9809ce276aca6859e140404626c8772870215f2", + "git_blob": "5a681a34ff6836d5830df4d2c51887e58cda9c13", + "path": "research/p104-signed-phase-leg-reuse-bound/receipts/R195-REVERSE.json", + "sha256": "f6091c7c63b21145077808bbdacc61431f641d0da37f9fa648aea4b7ead3b472", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/a9809ce276aca6859e140404626c8772870215f2/research/p104-signed-phase-leg-reuse-bound/receipts/R195-REVERSE.json" + }, + "closure/lead/inputs/forward.py": { + "commit": "a590edb3c5f7efd7404b1203e727c8cc3218493e", + "git_blob": "7842fd300e9aa30ea65a8526c92f761b7ea876b0", + "path": "research/p104-contiguous-direct-j-replacement-bound/engines/forward.py", + "sha256": "75d94780f9db49a4b08bb0e7fb4bd7fc04adb8cabbf73d83a809179c04c3d439", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/a590edb3c5f7efd7404b1203e727c8cc3218493e/research/p104-contiguous-direct-j-replacement-bound/engines/forward.py" + } + }, + "predecessors": [ + { + "contribution": "Exact complete comparator and paid/target context.", + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "pull_request": 7334, + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/7334" + }, + { + "contribution": "Literal signed Type A caller and physical Gaussian factors.", + "head": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "pull_request": 7113, + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/7113" + }, + { + "contribution": "All exact proper-window ranks and motivating directed price. The lead reuses the exact forward/rank engines.", + "head": "a590edb3c5f7efd7404b1203e727c8cc3218493e", + "pull_request": 7419, + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/7419" + }, + { + "contribution": "Exact original 38-factor relative word and fixed pair/triple certificates.", + "head": "a9809ce276aca6859e140404626c8772870215f2", + "pull_request": 7420, + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/7420" + }, + { + "contribution": "Fixed four-factor scope, authenticated input bytes and motivating directed price.", + "head": "3d1a62e154957f00aeeb4eec703cf6a07dfa3ef0", + "pull_request": 7435, + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/7435" + } + ], + "schema_version": 1 +} diff --git a/research/p104-signed-factor-circuit-gauge/README.md b/research/p104-signed-factor-circuit-gauge/README.md new file mode 100644 index 0000000000..2d3eac61f4 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/README.md @@ -0,0 +1,23 @@ +# Certify signed Type A factor circuits and gauge + +This package studies the exact 38-factor normalized Type A relative word from [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) at `07a76c5e2738882c0cb322278e56f6cae3c9885d` against [#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) at `aaeec8c0acf01e99a5f331ef363a698d9c084ace`. Unselected relative factors retain their chronology. The exact tests use 36 roles and central signs +1 and −1. **NO VERIFIED GAIN.** + +- With all bodies unit, two exact methods find minimum rank-dependent support 19, with two ties. The lexicographic choice has rank-18 displacement and is an involution. Its shortest rational transvection length is 19. +- Add the other leg of J1 to that choice. The new residual has rank 19 and an exact 19-factor witness. Any 19-factor realization crosses the fixed gathered 18+18 coordinate split in every factor. The witness uses dyadic entries. This is a normalized construction, with no native supplier. +- For the legal profile D8 = −1 and every other body unit, the same 20-factor residual is conjugated by a diagonal sign gauge on zero-based roles 9–17 and 27–35. Both literal engines agree on all 36 columns and rank 19. Conjugating the actual 19-factor witness also reproduces the complete residual. + +The literal 17-host direct rebuild loses more than 680.3199 raw before extra routing. The optimistic one-host quote is about +50.33412118538 raw, conditional on reusing the other 16 embedded hosts with their existing contracts. [Proof and invoice](PROOF.md). + +From a clean POSIX checkout with CPython 3.12: + +```sh +python3.12 -I -B research/p104-signed-factor-circuit-gauge/replay.py +``` + +The standard-library replay authenticates the bundled engines and exact receipts by path, runs both literal engines and independently multiplies the actual gauged factor witness. It requires no network, local cache, or user-specific paths. [Verification](VERIFICATION.md). + +## Open next questions + +Test one candidate direction in the actual frame of a reused J host. Require its image and covector to lie inside the old body projector, cross-annihilate the unchanged mate, and have a legal owned split. The other required 15 compatible hosts, arbitrary bodies, nonreal sectors, physical compilation and restoration, and the fully charged recurrence remain open. The other tied minimum subset is not factored here. + +[#7419](https://github.com/CrocSwap/integer-mult-bounds/pull/7419) supplied the proper-window ranks and forward engine. [#7420](https://github.com/CrocSwap/integer-mult-bounds/pull/7420) supplied the exact original relative factor labels and directed invoice. [#7435](https://github.com/CrocSwap/integer-mult-bounds/pull/7435) supplied the four-factor scope and the pinned source bundle. #7334 supplied the complete comparator and #7113 the literal signed caller and physical sector construction. OpenAI Codex and its subagents materially assisted proof, implementation, independent replay and packaging. diff --git a/research/p104-signed-factor-circuit-gauge/SOURCES.json b/research/p104-signed-factor-circuit-gauge/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/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-signed-factor-circuit-gauge/TASK.json b/research/p104-signed-factor-circuit-gauge/TASK.json new file mode 100644 index 0000000000..14e00d6a8c --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Exact #7334/#7113 normalized 38-factor caller at unit bodies and real signs; two two-dimensional kernel circuits, one shortest 19-factor case, one 20-factor J1 extension, and one legal D8 sign profile.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "Certify signed Type A factor circuits and gauge", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "A signed factor contraction must translate into fewer fully charged complex children at the exact comparator recurrence.", + "budget_minutes": 12, + "evidence": "No saving for the minimum lex subset; exact 20-to-19 rational witness for its J1 extension, universal fixed-plane crossing obligation, one legal D8 conjugation, and negative literal all-host price.", + "open_questions": [ + { + "blocked_by": "The full replacement of 17 native hosts loses raw cost before routing; the positive price requires 16 native hosts to reuse their embedded legs at their existing clocks.", + "first_step": "Check a proposed replacement factor in one exact reused host frame against its body projector, original mate, owned pairs and nonreal central sector.", + "question": "Can the normalized mixed factors be realized with fixed priced native hosts?", + "why_it_matters": "A successful local lift with a compatible count is needed before constructing a complete paid candidate." + } + ], + "original_card": { + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "existing_checks": [ + { + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4133: literal-slot defect", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "status": "author-checked" + }, + { + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4136: uniform commutation gap", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "status": "author-checked" + }, + { + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4140: uniform encoding gap", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "status": "author-checked" + }, + { + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "status": "author-checked" + }, + { + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4154: fiber-tag seam mismatch", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "status": "author-checked" + }, + { + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "status": "reviewed" + } + ], + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "id": "p104-side-correction", + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ] + }, + "outcome": "partial", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Find a minimum dependent signed subset exactly, construct one smaller normalized residual and test a legal nonunit body profile.", + "scope_status": "changed", + "stop_rule": "Two exact nullspaces and one 19-case factorization; one J1 extension and one D8 profile, with 20/60/30-second individual caps and independent replay.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-signed-factor-circuit-gauge/VERIFICATION.md b/research/p104-signed-factor-circuit-gauge/VERIFICATION.md new file mode 100644 index 0000000000..675e8062c2 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/VERIFICATION.md @@ -0,0 +1,11 @@ +# Verification and caps + +Run the one command in README.md on POSIX CPython 3.12. The verifier authenticates each bundled runner, input and receipt under `closure/` using path-keyed SHA-256 pins. Duplicate paths and unpinned closure files are rejected. The exact source paths and commits are in PROVENANCE.json. Outputs from both literal engines are matched byte-for-byte. The two factorization receipts match exactly after removing runner time. + +- Circuit screen: 38 factors, two exact nullspaces, 20 runner seconds. The independent literal engine checks every basis column of the −I endpoint, the exact slope minima and rank-18 selected residual. A corrupted original factor is rejected. +- Rank-18 obstruction and rank-19 witness: one selected residual per round, 60 runner seconds per case. The recorded shortest constructions multiply on all 36 basis columns. First-factor sign mutations are rejected. The successful shortest-control run took 0.1204s and the 20-to-19 witness took 0.1123s. An earlier shell wrapper for the same rank-18 case failed to retain the child exit after JSON emission. The corrected replay agreed on every field except time, with combined runner time 0.2408s. +- J1 extension: both literal engines independently reconstruct all 36 residual columns, with 306 off-block entries and rank one in the lower-left block. The independent engine rejects a corrupted unchanged factor. The fixed-plane proof uses these exact identities and the rank-minimal product expansion. +- D8 gate: one legal body profile, 30 runner seconds lead and 20 independent. Both exact literal endpoints agree and reject an omitted body action. The wrapper multiplies the 19 frozen witness factors after the exact sign gauge, verifies all 36 literal columns in both engines, and rejects the ungauged reuse on basis 1. +- Directed price: exact rational arithmetic reuses the two #7420 price endpoints. It checks the 33 net A calls at 96 ports and the negative 17-host upper bound. + +This checks the frozen normalized result and one profile. The remaining native, all-sector and all-size gates are in README.md and PROOF.md. diff --git a/research/p104-signed-factor-circuit-gauge/VERIFY.json b/research/p104-signed-factor-circuit-gauge/VERIFY.json new file mode 100644 index 0000000000..4f90a6925a --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Exact frozen source, independent signed circuits, rank-19 witness, fixed planes, D8 gauge on actual factors, directed price, and negative controls.", + "timeout_seconds": 190 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-signed-factor-circuit-gauge/closure/construct/RESULT.json b/research/p104-signed-factor-circuit-gauge/closure/construct/RESULT.json new file mode 100644 index 0000000000..5e456bb9d4 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/construct/RESULT.json @@ -0,0 +1 @@ +{"chosen": [0, 2, 4, 6, 8, 10, 12, 14, 18, 19, 20, 22, 24, 26, 28, 30, 32, 34, 36], "exact_diag_minus18_plus18": false, "factors": [[["-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"], ["0", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["4", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "-2", "-2", "-2", "-2", "-2", "-2", "-2", "-2", "-2", "-2", "-2", "-2", "-2", "-2", "-2", "-2", "-2"], ["1/2", "1", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "-1", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "1", "1", "1", "1", "1", "1", "1", "1", "1", "1", "1", "1", "1", "1", "1", "1", "1"], ["1", "0", "0", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "2", "4", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "-4", "-4", "-4", "-4", "-4", "-4", "-4", "-4", "-4", "-4", "-4", "-4", "-4", "-4", "-4", "-4", "-4"], ["-1/2", "0", "1/2", "1", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "-1", "0", "1", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "2", "2", "2", "2", "2", "2", "2", "2", "2", "2", "2", "2", "2", "2", "2", "2", "2"], ["1", "0", "-1", "0", "0", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "2", "0", "-2", "4", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "-6", "-6", "-6", "-6", "-6", "-6", "-6", "-6", "-6", "-6", "-6", "-6", "-6", "-6", "-6", "-6", "-6"], ["-1/2", "0", "1/2", "0", "1/2", "1", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "-1", "0", "1", "0", "1", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "3", "3", "3", "3", "3", "3", "3", "3", "3", "3", "3", "3", "3", "3", "3", "3", "3"], ["1", "0", "-1", "0", "-1", "0", "0", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "2", "0", "-2", "0", "-2", "4", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "-8", "-8", "-8", "-8", "-8", "-8", "-8", "-8", "-8", "-8", "-8", "-8", "-8", "-8", "-8", "-8", "-8"], ["-1/2", "0", "1/2", "0", "1/2", "0", "1/2", "1", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "-1", "0", "1", "0", "1", "0", "1", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "4", "4", "4", "4", "4", "4", "4", "4", "4", "4", "4", "4", "4", "4", "4", "4", "4"], ["1", "0", "-1", "0", "-1", "0", "-1", "0", "0", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "2", "0", "-2", "0", "-2", "0", "-2", "4", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "-10", "-10", "-10", "-10", "-10", "-10", "-10", "-10", "-10", "-10", "-10", "-10", "-10", "-10", "-10", "-10", "-10"], ["-1/2", "0", "1/2", "0", "1/2", "0", "1/2", "0", "1/2", "1", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "-1", "0", "1", "0", "1", "0", "1", "0", "1", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "5", "5", "5", "5", "5", "5", "5", "5", "5", "5", "5", "5", "5", "5", "5", "5", "5"], ["1", "0", "-1", "0", "-1", "0", "-1", "0", "-1", "0", "0", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "2", "0", "-2", "0", "-2", "0", "-2", "0", "-2", "4", "-2", "0", "0", "0", "0", "0", "0", "0", "-12", "-12", "-12", "-12", "-12", "-12", "-12", "-12", "-12", "-12", "-12", "-12", "-12", "-12", "-12", "-12", "-12"], ["-1/2", "0", "1/2", "0", "1/2", "0", "1/2", "0", "1/2", "0", "1/2", "1", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "-1", "0", "1", "0", "1", "0", "1", "0", "1", "0", "1", "-2", "0", "0", "0", "0", "0", "0", "6", "6", "6", "6", "6", "6", "6", "6", "6", "6", "6", "6", "6", "6", "6", "6", "6"], ["1", "0", "-1", "0", "-1", "0", "-1", "0", "-1", "0", "-1", "0", "0", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "2", "0", "-2", "0", "-2", "0", "-2", "0", "-2", "0", "-2", "4", "-2", "0", "0", "0", "0", "0", "-14", "-14", "-14", "-14", "-14", "-14", "-14", "-14", "-14", "-14", "-14", "-14", "-14", "-14", "-14", "-14", "-14"], ["-1/2", "0", "1/2", "0", "1/2", "0", "1/2", "0", "1/2", "0", "1/2", "0", "1/2", "1", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "-1", "0", "1", "0", "1", "0", "1", "0", "1", "0", "1", "0", "1", "-2", "0", "0", "0", "0", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7"], ["1", "0", "-1", "0", "-1", "0", "-1", "0", "-1", "0", "-1", "0", "-1", "0", "0", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "2", "0", "-2", "0", "-2", "0", "-2", "0", "-2", "0", "-2", "0", "-2", "4", "-2", "0", "0", "0", "-16", "-16", "-16", "-16", "-16", "-16", "-16", "-16", "-16", "-16", "-16", "-16", "-16", "-16", "-16", "-16", "-16"], ["-1/2", "0", "1/2", "0", "1/2", "0", "1/2", "0", "1/2", "0", "1/2", "0", "1/2", "0", "1/2", "1", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "-1", "0", "1", "0", "1", "0", "1", "0", "1", "0", "1", "0", "1", "0", "1", "-2", "0", "0", "8", "8", "8", "8", "8", "8", "8", "8", "8", "8", "8", "8", "8", "8", "8", "8", "8"], ["1", "0", "-1", "0", "-1", "0", "-1", "0", "-1", "0", "-1", "0", "-1", "0", "-1", "0", "0", "-2", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "2", "0", "-2", "0", "-2", "0", "-2", "0", "-2", "0", "-2", "0", "-2", "0", "-2", "4", "-2", "0", "-18", "-18", "-18", "-18", "-18", "-18", "-18", "-18", "-18", "-18", "-18", "-18", "-18", "-18", "-18", "-18", "-18"], ["-1/2", "0", "1/2", "0", "1/2", "0", "1/2", "0", "1/2", "0", "1/2", "0", "1/2", "0", "1/2", "0", "1/2", "1", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]], [["0", "-1", "0", "1", "0", "1", "0", "1", "0", "1", "0", "1", "0", "1", "0", "1", "0", "1", "0", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7", "7"], ["1", "0", "-1", "0", "-1", "0", "-1", "0", "-1", "0", "-1", "0", "-1", "0", "-1", "0", "-1", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0", "0"]]], "involution": true, "minimum_transvections": 19, "rank": 18, "seconds": 0.1203969158232212, "sign_flip_negative_control": "rejected", "source_sha256": "ab74c834d4b94c63cda667338055889667e8e7a98c022ba6ed23afa35ff0acfe", "target_sha256": "6bc534239a332546a93ffcdc1c8f803c145d7b9ba9c32543fef74256a035330a"} diff --git a/research/p104-signed-factor-circuit-gauge/closure/construct/factorize.py b/research/p104-signed-factor-circuit-gauge/closure/construct/factorize.py new file mode 100644 index 0000000000..736599b9be --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/construct/factorize.py @@ -0,0 +1,177 @@ +"""Exact deterministic shortest rational transvection factorization. + +Matrices are tuples of columns and a factor (u, f) acts as x -> x + u f(x). +The returned factors multiply from left to right in their listed order. +""" +from fractions import Fraction as F + + +def dot(left, right): + return sum((a * b for a, b in zip(left, right) if a and b), F(0)) + + +def add(left, right, scale=1): + return tuple(a + scale * b for a, b in zip(left, right)) + + +def column_matrix_vector(columns, vector): + return tuple(dot(row, vector) for row in zip(*columns)) + + +def identity(size): + return tuple(tuple(F(row == column) for row in range(size)) + for column in range(size)) + + +def displacement(columns): + return tuple(tuple(entry - (row == j) for row, entry in enumerate(column)) + for j, column in enumerate(columns)) + + +def determinant_and_rank(columns): + """Return determinant and rank, using exact column elimination.""" + width = len(columns) + pending = list(columns) + pivot_count = 0 + determinant = F(1) + for row in range(width): + pivot_at = next((j for j in range(pivot_count, width) + if pending[j][row]), None) + if pivot_at is None: + determinant = F(0) + continue + if pivot_at != pivot_count: + pending[pivot_count], pending[pivot_at] = pending[pivot_at], pending[pivot_count] + determinant = -determinant + pivot = pending[pivot_count] + determinant *= pivot[row] + for j in range(pivot_count + 1, width): + if pending[j][row]: + pending[j] = add(pending[j], pivot, -pending[j][row] / pivot[row]) + pivot_count += 1 + return determinant, pivot_count + + +def proportionality(first, second): + """Return the ratio second / first if proportional, else None.""" + i = next(j for j, value in enumerate(first) if value) + ratio = second[i] / first[i] + return ratio if all(b == ratio * a for a, b in zip(first, second)) else None + + +def select_displacement(columns): + """Return Dx and D²x independent, or Dx with Dbar = scalar I.""" + representative = None + ratio = None + for column in columns: + if not any(column): + continue + squared = column_matrix_vector(columns, column) + current = proportionality(column, squared) + if current is None: + return column, squared, None + if representative is None: + representative = column + ratio = current + elif current != ratio: + combined = tuple(ratio * a + current * b for a, b in zip(representative, column)) + return add(representative, column), combined, None + return representative, None, ratio + + +def inverse_left(columns, image, covector): + assert any(image) and any(covector) and dot(covector, image) == 0 + return tuple(add(column, image, -dot(covector, column)) for column in columns) + + +def obstructed(delta): + """A nonidentity rational SL involution requires one extra factor.""" + nonzero = False + for column in delta: + if not any(column): + continue + nonzero = True + if column_matrix_vector(delta, column) != tuple(-2 * x for x in column): + return False + return nonzero + + +def solve_two(image, squared, i, j, target, other): + determinant = image[i] * squared[j] - image[j] * squared[i] + return ((target * squared[j] - other * image[j]) / determinant, + (image[i] * other - squared[i] * target) / determinant) + + +def peel(columns, delta, image, squared, ratio): + """Choose a transvection whose removal drops displacement rank.""" + rows = tuple(zip(*delta)) + i = next(j for j, value in enumerate(image) if value) + if ratio == 0: + covector = tuple(x / image[i] for x in rows[i]) + return (image, covector), inverse_left(columns, image, covector) + j = next(j for j in range(len(columns)) + if image[i] * squared[j] != image[j] * squared[i]) + first, second = solve_two(image, squared, i, j, F(1), F(0)) + covector = tuple(first * x + second * y for x, y in zip(rows[i], rows[j])) + remainder = inverse_left(columns, image, covector) + if obstructed(displacement(remainder)): + for h, row in enumerate(rows): + first, second = solve_two(image, squared, i, j, image[h], squared[h]) + adjustment = tuple(z - first * x - second * y + for x, y, z in zip(rows[i], rows[j], row)) + if any(adjustment): + covector = add(covector, adjustment) + remainder = inverse_left(columns, image, covector) + break + else: + raise ArithmeticError("no independent adjustment for exceptional quotient") + assert not obstructed(displacement(remainder)) + return (image, covector), remainder + + +def factor_product(factors, size): + """Rebuild the listed product by exact independent column application.""" + columns = identity(size) + for image, covector in reversed(factors): + if not any(image) or not any(covector) or dot(covector, image): + raise ValueError("a supplied factor is not a nontrivial transvection") + columns = tuple(add(column, image, dot(covector, column)) for column in columns) + return columns + + +def factorize(columns): + """Return minimum length, displacement rank, obstruction and factors.""" + original = tuple(tuple(map(F, column)) for column in columns) + size = len(original) + if any(len(column) != size for column in original): + raise ValueError("matrix must be square and supplied in columns") + if determinant_and_rank(original)[0] != 1: + raise ValueError("matrix must have determinant one") + delta = displacement(original) + rank = determinant_and_rank(delta)[1] + exceptional = obstructed(delta) + current = original + factors = [] + if exceptional: + rows = tuple(zip(*delta)) + image = next(column for column in delta if any(column)) + i = next(j for j, value in enumerate(image) if value) + for j, row in enumerate(rows): + covector = add(row, rows[i], -image[j] / image[i]) + if any(covector): + break + else: + raise ArithmeticError("nonidentity rational SL involution has rank below two") + factors.append((image, covector)) + current = inverse_left(current, image, covector) + for _ in range(rank): + delta = displacement(current) + image, squared, ratio = select_displacement(delta) + if image is None or (ratio is not None and ratio != 0): + raise ArithmeticError("rank-dropping induction reached unexpected quotient") + factor, current = peel(current, delta, image, squared, ratio) + factors.append(factor) + if current != identity(size) or factor_product(factors, size) != original: + raise ArithmeticError("exact factorization verification failed") + return {"length": len(factors), "rank": rank, "involution": exceptional, + "factors": tuple(factors)} diff --git a/research/p104-signed-factor-circuit-gauge/closure/construct/run.py b/research/p104-signed-factor-circuit-gauge/closure/construct/run.py new file mode 100644 index 0000000000..46af7c1247 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/construct/run.py @@ -0,0 +1,59 @@ +"""Replay one pinned signed-factor residual under a 60-second cap.""" +import argparse +import hashlib +import json +from fractions import Fraction +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import perf_counter + +from factorize import displacement, factor_product, factorize, column_matrix_vector + + +def stop(*_): + raise TimeoutError("single residual 60-second cap reached") + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("receipt", type=Path) + parser.add_argument("sha256") + args = parser.parse_args() + signal(SIGALRM, stop) + alarm(60) + started = perf_counter() + try: + raw = args.receipt.read_bytes() + assert hashlib.sha256(raw).hexdigest() == args.sha256 + receipt = json.loads(raw) + assert receipt["chosen"] == [0, 2, 4, 6, 8, 10, 12, 14, 18, 19, 20, 22, 24, 26, 28, 30, 32, 34, 36] + target = tuple(tuple(map(Fraction, column)) for column in receipt["target_columns"]) + assert len(target) == 36 + result = factorize(target) + assert result["rank"] == 18 + factors = result["factors"] + negative = list(factors) + image, covector = negative[0] + negative[0] = (tuple(-x for x in image), covector) + assert factor_product(negative, 36) != target + delta = displacement(target) + rank_obstruction = all(column_matrix_vector(delta, d) == tuple(-2*x for x in d) + for d in delta) + assert rank_obstruction == result["involution"] + expected = tuple(tuple(Fraction((-1 if j < 18 else 1) if i == j else 0) + for i in range(36)) for j in range(36)) + output = { + "chosen": receipt["chosen"], "source_sha256": args.sha256, + "target_sha256": hashlib.sha256(json.dumps(receipt["target_columns"],separators=(",", ":")).encode()).hexdigest(), + "rank": result["rank"], "minimum_transvections": result["length"], + "involution": result["involution"], "exact_diag_minus18_plus18": target == expected, + "sign_flip_negative_control": "rejected", "seconds": perf_counter()-started, + "factors": [[list(map(str, u)), list(map(str, v))] for u,v in factors], + } + print(json.dumps(output, sort_keys=True)) + finally: + alarm(0) + + +if __name__ == "__main__": + main() diff --git a/research/p104-signed-factor-circuit-gauge/closure/independent/RESULT.json b/research/p104-signed-factor-circuit-gauge/closure/independent/RESULT.json new file mode 100644 index 0000000000..a9caa000a8 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/independent/RESULT.json @@ -0,0 +1,637 @@ +{ + "caller": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "corrupted_factor_rejected": true, + "covectors": { + "kernel": [ + [ + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 0, + 0, + 1, + -1, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0 + ], + [ + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + -1, + 1, + -1, + 0, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1 + ] + ], + "rank": 36, + "supports_checked": 3, + "ties": [ + [ + 0, + 2, + 4, + 6, + 8, + 10, + 12, + 14, + 18, + 19, + 20, + 22, + 24, + 26, + 28, + 30, + 32, + 34, + 36 + ] + ], + "witness": [ + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 0, + 0, + 1, + -1, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0 + ] + }, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "images": { + "kernel": [ + [ + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 0, + 1, + 1, + -1, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0 + ], + [ + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + -1, + 1, + 0, + 0, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1 + ] + ], + "rank": 36, + "supports_checked": 3, + "ties": [ + [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 16, + 17, + 21, + 23, + 25, + 27, + 29, + 31, + 33, + 35, + 37 + ] + ], + "witness": [ + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + -1, + 1, + 0, + 0, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0, + -1, + 0, + 1 + ] + }, + "labels": [ + [ + 43, + 1, + 0, + 0, + 1, + 1 + ], + [ + 43, + 1, + 1, + 18, + 19, + -1 + ], + [ + 137, + 2, + 0, + 0, + 2, + 1 + ], + [ + 137, + 2, + 1, + 18, + 20, + -1 + ], + [ + 268, + 3, + 0, + 0, + 3, + 1 + ], + [ + 268, + 3, + 1, + 18, + 21, + -1 + ], + [ + 432, + 4, + 0, + 0, + 4, + 1 + ], + [ + 432, + 4, + 1, + 18, + 22, + -1 + ], + [ + 633, + 5, + 0, + 0, + 5, + 1 + ], + [ + 633, + 5, + 1, + 18, + 23, + -1 + ], + [ + 867, + 6, + 0, + 0, + 6, + 1 + ], + [ + 867, + 6, + 1, + 18, + 24, + -1 + ], + [ + 1138, + 7, + 0, + 0, + 7, + 1 + ], + [ + 1138, + 7, + 1, + 18, + 25, + -1 + ], + [ + 1423, + 8, + 0, + 0, + 8, + 1 + ], + [ + 1423, + 8, + 1, + 18, + 26, + -1 + ], + [ + 1516, + 0, + 0, + 0, + 1, + 1 + ], + [ + 1580, + 0, + 0, + 0, + 1, + 1 + ], + [ + 1659, + 0, + 0, + 0, + 1, + 1 + ], + [ + 1721, + 0, + 0, + 0, + 1, + 1 + ], + [ + 3058, + 9, + 0, + 0, + 9, + 1 + ], + [ + 3058, + 9, + 1, + 18, + 27, + -1 + ], + [ + 3377, + 10, + 0, + 0, + 10, + 1 + ], + [ + 3377, + 10, + 1, + 18, + 28, + -1 + ], + [ + 3674, + 11, + 0, + 0, + 11, + 1 + ], + [ + 3674, + 11, + 1, + 18, + 29, + -1 + ], + [ + 3934, + 12, + 0, + 0, + 12, + 1 + ], + [ + 3934, + 12, + 1, + 18, + 30, + -1 + ], + [ + 4149, + 13, + 0, + 0, + 13, + 1 + ], + [ + 4149, + 13, + 1, + 18, + 31, + -1 + ], + [ + 4337, + 14, + 0, + 0, + 14, + 1 + ], + [ + 4337, + 14, + 1, + 18, + 32, + -1 + ], + [ + 4485, + 15, + 0, + 0, + 15, + 1 + ], + [ + 4485, + 15, + 1, + 18, + 33, + -1 + ], + [ + 4606, + 16, + 0, + 0, + 16, + 1 + ], + [ + 4606, + 16, + 1, + 18, + 34, + -1 + ], + [ + 4691, + 17, + 0, + 0, + 17, + 1 + ], + [ + 4691, + 17, + 1, + 18, + 35, + -1 + ] + ], + "least_support": [ + 0, + 2, + 4, + 6, + 8, + 10, + 12, + 14, + 18, + 19, + 20, + 22, + 24, + 26, + 28, + 30, + 32, + 34, + 36 + ], + "literal_rank": 18, + "pins": { + "inputs/7113-SHA256.json": "064e11ecfedce9937ea1782e5baee37e89b3c9eebabed5b4a9ba84f412bbe078", + "inputs/CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "inputs/R195.json": "f6091c7c63b21145077808bbdacc61431f641d0da37f9fa648aea4b7ead3b472" + }, + "runner_cap_seconds": 20 +} diff --git a/research/p104-signed-factor-circuit-gauge/closure/independent/replay.py b/research/p104-signed-factor-circuit-gauge/closure/independent/replay.py new file mode 100644 index 0000000000..5ff80240d0 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/independent/replay.py @@ -0,0 +1,210 @@ +"""Independent minimum-support replay using the positive signed prefix.""" +from fractions import Fraction as Q +from hashlib import sha256 +from json import dumps, loads +from math import gcd, lcm +from pathlib import Path +from signal import SIGALRM, alarm, signal +from sys import argv, implementation, version_info + +N = 36 +CAP = 20 +PINS = { + 'inputs/CALLER.json': '255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc', + 'inputs/R195.json': 'f6091c7c63b21145077808bbdacc61431f641d0da37f9fa648aea4b7ead3b472', + 'inputs/7113-SHA256.json': '064e11ecfedce9937ea1782e5baee37e89b3c9eebabed5b4a9ba84f412bbe078', +} +HEAD = 'aaeec8c0acf01e99a5f331ef363a698d9c084ace' +CALLER = '07a76c5e2738882c0cb322278e56f6cae3c9885d' + + +def unique(items): + obj = dict(items) + assert len(items) == len(obj) + return obj + + +def read(root, path): + raw = (root / path).read_bytes() + assert sha256(raw).hexdigest() == PINS[path], path + return loads(raw, object_pairs_hook=unique) + + +def unit(j): + return [Q(i == j) for i in range(N)] + + +def dot(u, v): + return sum(a * b for a, b in zip(u, v, strict=True) if a and b) + + +def axpy(u, v, scale): + return [a + scale * b for a, b in zip(u, v, strict=True)] if scale else u + + +def signed_prefix(tape, sign): + rows, inverse_cols = [unit(i) for i in range(N)], [unit(i) for i in range(N)] + factors, labels = [], [] + for clock, event in enumerate(tape): + if event[0] == 'B': + continue + if event[0] == 'J': + _, host, (a, b, c, d), _ = event + assert len({a, b, c, d}) == 4 + legs = [(b, a, 1), (c, d, -1)] + else: + assert event[0] == 'A' + _, operation, destination, *args = event + if operation == 'QUERY': + source, exponent = args + assert exponent == -1 + host, legs = 0, [(destination, source, 1)] + elif operation == 'ADD': + source, weight = args + weight = Q(weight) + rows[destination] = axpy(rows[destination], rows[source], weight) + inverse_cols[source] = axpy(inverse_cols[source], inverse_cols[destination], -weight) + continue + elif operation == 'SCALE': + weight = Q(args[0]) + rows[destination] = [x * weight for x in rows[destination]] + inverse_cols[destination] = [x / weight for x in inverse_cols[destination]] + continue + elif operation == 'SWAP': + source, = args + rows[destination], rows[source] = rows[source], rows[destination] + inverse_cols[destination], inverse_cols[source] = inverse_cols[source], inverse_cols[destination] + continue + else: + assert operation in ('IDLE_ONE', 'LAMBDA') + continue + for leg, (dst, src, weight) in enumerate(legs): + image = [2 * weight * x for x in inverse_cols[dst]] + covector = rows[src] + assert any(image) and any(covector) and not dot(image, covector) + factors.append((image, covector)) + labels.append([clock, host, leg, dst, src, weight]) + rows[dst] = axpy(rows[dst], rows[src], sign * weight) + inverse_cols[src] = axpy(inverse_cols[src], inverse_cols[dst], -sign * weight) + for i in range(N): + expected = [sign * x for x in unit(i)] + assert rows[i] == expected and inverse_cols[i] == expected + return factors, labels + + +def apply(word, column, inverse=False): + for image, covector in reversed(word) if inverse else word: + coefficient = dot(covector, column) + column = axpy(column, image, -coefficient if inverse else coefficient) + return column + + +def primitive(row): + g = gcd(*row) + return [x // g for x in row] if g > 1 else row + + +def integral(row): + denominator = lcm(*(x.denominator for x in row)) + return primitive([int(denominator * x) for x in row]) + + +def echelon(rows): + width = len(rows[0]) + basis = {} + for row in rows: + row = integral(row) + for pivot, old in sorted(basis.items()): + if row[pivot]: + a, b = old[pivot], row[pivot] + row = primitive([a * x - b * y for x, y in zip(row, old, strict=True)]) + pivot = next((i for i, v in enumerate(row) if v), None) + if pivot is not None: + basis[pivot] = row + assert all(len(row) == width for row in basis.values()) + return basis + + +def min_support(vectors): + equations = list(zip(*vectors, strict=True)) + basis = echelon(equations) + free = sorted(set(range(len(vectors))) - basis.keys()) + assert len(free) == 2 + kernel = [] + for selected in free: + vector = [Q(i == selected) for i in range(len(vectors))] + for pivot, row in sorted(basis.items(), reverse=True): + vector[pivot] = -Q(dot(row, vector)) / row[pivot] + assert all(not dot(row, vector) for row in equations) + kernel.append(integral(vector)) + # A minimum vector either has no cancellable coordinate or satisfies at + # least one nontrivial coordinate-zero equation. Test every such equation. + first, second = kernel + supports = {} + for a, b in [(1, 0), (0, 1), *((y, -x) for x, y in zip(first, second, strict=True) if x or y)]: + vector = [a * x + b * y for x, y in zip(first, second, strict=True)] + support = tuple(i for i, value in enumerate(vector) if value) + assert support and all(not dot(row, vector) for row in equations) + supports.setdefault(support, primitive(vector)) + minimum = min(map(len, supports)) + tied = sorted(key for key in supports if len(key) == minimum) + return {'rank': len(basis), 'kernel': kernel, 'ties': tied, + 'witness': supports[tied[0]], 'supports_checked': len(supports)} + + +def literal_rank(original, conjugates, selected): + selected = set(selected) + kept = [factor for i, factor in enumerate(original) if i not in selected] + # The product of increasing-index conjugates applies in reverse order. + grouped = [factor for i, factor in reversed(list(enumerate(conjugates))) if i in selected] + columns = [] + for j in range(N): + base = unit(j) + actual = apply(original, apply(kept, base, inverse=True)) + assert actual == apply(grouped, base), (sorted(selected), j) + columns.append(axpy(actual, base, -1)) + return len(echelon(columns)) + + +def stop(*_): + raise TimeoutError(f'{CAP}-second replay cap') + + +def main(): + assert __debug__ and implementation.name == 'cpython' and version_info[:2] == (3, 12) + assert len(argv) == 2, 'pass the pinned #7435 package root' + root = Path(argv[1]).resolve() + signal(SIGALRM, stop) + alarm(CAP) + caller = read(root, 'inputs/CALLER.json') + manifest = read(root, 'inputs/7113-SHA256.json') + predecessor = read(root, 'inputs/R195.json') + assert manifest['expected/ODD-TYPE-AB-CALLER.json'] == PINS['inputs/CALLER.json'] + assert (predecessor['head'], predecessor['caller']) == (HEAD, CALLER) + tape = caller['events'] + assert len(tape) == 4783 and caller['types']['A']['roles'] == N + original, labels = signed_prefix(tape, -1) + conjugates, positive_labels = signed_prefix(tape, 1) + assert len(labels) == 38 and labels == positive_labels == predecessor['factor_labels'] + for i in range(N): + assert apply(original, unit(i)) == [-x for x in unit(i)] + image, covector = original[-1] + mutation = [*original[:-1], ([2 * x for x in image], covector)] + assert any(apply(mutation, unit(i)) != [-x for x in unit(i)] for i in range(N)) + image_receipt = min_support([u for u, _ in conjugates]) + covector_receipt = min_support([v for _, v in conjugates]) + tied = image_receipt['ties'] + covector_receipt['ties'] + best = min(tied, key=lambda key: (len(key), key)) + controls = [(0, 36), (0, 2, 36), (0, 1, 2, 36), tuple(range(38))] + assert [literal_rank(original, conjugates, ids) for ids in controls] == [2, 3, 4, 36] + rank = literal_rank(original, conjugates, best) + assert rank < len(best) + alarm(0) + print(dumps({'head': HEAD, 'caller': CALLER, 'pins': PINS, 'runner_cap_seconds': CAP, + 'labels': labels, 'images': image_receipt, 'covectors': covector_receipt, + 'least_support': best, 'literal_rank': rank, 'corrupted_factor_rejected': True}, + indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/p104-signed-factor-circuit-gauge/closure/lead/RESULT.json b/research/p104-signed-factor-circuit-gauge/closure/lead/RESULT.json new file mode 100644 index 0000000000..e41e407c4f --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/lead/RESULT.json @@ -0,0 +1,2441 @@ +{ + "budget_seconds": 20, + "certificates": { + "covector": { + "always_zero": [], + "kernel": [ + [ + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "0", + "0", + "1", + "-1", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "1", + "-1", + "1", + "0", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1" + ] + ], + "pivots": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35 + ], + "witnesses": [ + { + "coefficients": [ + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "-1", + "1", + "-1", + "0", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1" + ], + "omitted": [ + 0, + 2, + 4, + 6, + 8, + 10, + 12, + 14, + 19, + 20, + 22, + 24, + 26, + 28, + 30, + 32, + 34, + 36 + ], + "slope": "0", + "support": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 16, + 17, + 18, + 21, + 23, + 25, + 27, + 29, + 31, + 33, + 35, + 37 + ] + }, + { + "coefficients": [ + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "0", + "0", + "1", + "-1", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0" + ], + "omitted": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 16, + 17, + 21, + 23, + 25, + 27, + 29, + 31, + 33, + 35, + 37 + ], + "slope": "infinity", + "support": [ + 0, + 2, + 4, + 6, + 8, + 10, + 12, + 14, + 18, + 19, + 20, + 22, + 24, + 26, + 28, + 30, + 32, + 34, + 36 + ] + }, + { + "coefficients": [ + "1", + "-1", + "-1", + "1", + "1", + "-1", + "-1", + "1", + "1", + "-1", + "-1", + "1", + "1", + "-1", + "-1", + "1", + "-1", + "1", + "0", + "-1", + "1", + "-1", + "-1", + "1", + "1", + "-1", + "-1", + "1", + "1", + "-1", + "-1", + "1", + "1", + "-1", + "-1", + "1", + "1", + "-1" + ], + "omitted": [ + 18 + ], + "slope": "1", + "support": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37 + ] + } + ] + }, + "image": { + "always_zero": [], + "kernel": [ + [ + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "0", + "1", + "1", + "-1", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "1", + "-1", + "0", + "0", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1" + ] + ], + "pivots": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35 + ], + "witnesses": [ + { + "coefficients": [ + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "-1", + "1", + "0", + "0", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1" + ], + "omitted": [ + 0, + 2, + 4, + 6, + 8, + 10, + 12, + 14, + 18, + 19, + 20, + 22, + 24, + 26, + 28, + 30, + 32, + 34, + 36 + ], + "slope": "0", + "support": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 16, + 17, + 21, + 23, + 25, + 27, + 29, + 31, + 33, + 35, + 37 + ] + }, + { + "coefficients": [ + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "0", + "1", + "1", + "-1", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0" + ], + "omitted": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 16, + 21, + 23, + 25, + 27, + 29, + 31, + 33, + 35, + 37 + ], + "slope": "infinity", + "support": [ + 0, + 2, + 4, + 6, + 8, + 10, + 12, + 14, + 17, + 18, + 19, + 20, + 22, + 24, + 26, + 28, + 30, + 32, + 34, + 36 + ] + }, + { + "coefficients": [ + "-1", + "-1", + "1", + "1", + "-1", + "-1", + "1", + "1", + "-1", + "-1", + "1", + "1", + "-1", + "-1", + "1", + "1", + "-1", + "0", + "-1", + "1", + "-1", + "-1", + "1", + "1", + "-1", + "-1", + "1", + "1", + "-1", + "-1", + "1", + "1", + "-1", + "-1", + "1", + "1", + "-1", + "-1" + ], + "omitted": [ + 17 + ], + "slope": "-1", + "support": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37 + ] + } + ] + } + }, + "chosen": [ + 0, + 2, + 4, + 6, + 8, + 10, + 12, + 14, + 18, + 19, + 20, + 22, + 24, + 26, + 28, + 30, + 32, + 34, + 36 + ], + "chosen_axis": "covector", + "controls": [ + [ + 0, + 37 + ], + [ + 1, + 20, + 36 + ], + [ + 0, + 4, + 33, + 37 + ] + ], + "dimension": 36, + "displacement_pivots": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17 + ], + "factor_count": 38, + "factor_keys": [ + [ + 43, + 0, + 1 + ], + [ + 43, + 18, + 19 + ], + [ + 137, + 0, + 2 + ], + [ + 137, + 18, + 20 + ], + [ + 268, + 0, + 3 + ], + [ + 268, + 18, + 21 + ], + [ + 432, + 0, + 4 + ], + [ + 432, + 18, + 22 + ], + [ + 633, + 0, + 5 + ], + [ + 633, + 18, + 23 + ], + [ + 867, + 0, + 6 + ], + [ + 867, + 18, + 24 + ], + [ + 1138, + 0, + 7 + ], + [ + 1138, + 18, + 25 + ], + [ + 1423, + 0, + 8 + ], + [ + 1423, + 18, + 26 + ], + [ + 1516, + 0, + 1 + ], + [ + 1580, + 0, + 1 + ], + [ + 1659, + 0, + 1 + ], + [ + 1721, + 0, + 1 + ], + [ + 3058, + 0, + 9 + ], + [ + 3058, + 18, + 27 + ], + [ + 3377, + 0, + 10 + ], + [ + 3377, + 18, + 28 + ], + [ + 3674, + 0, + 11 + ], + [ + 3674, + 18, + 29 + ], + [ + 3934, + 0, + 12 + ], + [ + 3934, + 18, + 30 + ], + [ + 4149, + 0, + 13 + ], + [ + 4149, + 18, + 31 + ], + [ + 4337, + 0, + 14 + ], + [ + 4337, + 18, + 32 + ], + [ + 4485, + 0, + 15 + ], + [ + 4485, + 18, + 33 + ], + [ + 4606, + 0, + 16 + ], + [ + 4606, + 18, + 34 + ], + [ + 4691, + 0, + 17 + ], + [ + 4691, + 18, + 35 + ] + ], + "full_signs": [ + 1, + -1 + ], + "minimum_support": 19, + "pins": { + "inputs/CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "inputs/forward.py": "75d94780f9db49a4b08bb0e7fb4bd7fc04adb8cabbf73d83a809179c04c3d439" + }, + "target_columns": [ + [ + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1" + ] + ], + "tied_supports": [ + [ + 0, + 2, + 4, + 6, + 8, + 10, + 12, + 14, + 18, + 19, + 20, + 22, + 24, + 26, + 28, + 30, + 32, + 34, + 36 + ], + [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 16, + 17, + 21, + 23, + 25, + 27, + 29, + 31, + 33, + 35, + 37 + ] + ] +} diff --git a/research/p104-signed-factor-circuit-gauge/closure/lead/dependency.py b/research/p104-signed-factor-circuit-gauge/closure/lead/dependency.py new file mode 100644 index 0000000000..7cb80295fe --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/lead/dependency.py @@ -0,0 +1,174 @@ +"""Exact minimum support in the full-suffix signed Type A configurations.""" +from fractions import Fraction as F +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal + +ROOT = Path(__file__).resolve().parent +PINS = { + "inputs/CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "inputs/forward.py": "75d94780f9db49a4b08bb0e7fb4bd7fc04adb8cabbf73d83a809179c04c3d439", +} +DIMENSION = 36 + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b, strict=True) if x and y) + + +def add(a, b, coefficient): + return [x + coefficient * y for x, y in zip(a, b, strict=True)] + + +def product(factors, column, inverse=False): + for u, v in reversed(factors) if inverse else factors: + column = add(column, u, (-1 if inverse else 1) * dot(v, column)) + return column + + +def rref(rows): + rows = [list(row) for row in rows] + pivots = [] + for col in range(len(rows[0])): + row = len(pivots) + pivot = next((i for i in range(row, len(rows)) if rows[i][col]), None) + if pivot is None: + continue + rows[row], rows[pivot] = rows[pivot], rows[row] + divisor = rows[row][col] + rows[row] = [x / divisor for x in rows[row]] + for i, other in enumerate(rows): + if i != row and other[col]: + rows[i] = add(other, rows[row], -other[col]) + pivots.append(col) + return rows, pivots + + +def nullspace(columns): + rows, pivots = rref(zip(*columns, strict=True)) + width = len(columns) + vectors = [] + for j in sorted(set(range(width)) - set(pivots)): + x = [F(i == j) for i in range(width)] + for row, pivot in zip(rows[:len(pivots)], pivots, strict=True): + x[pivot] = -row[j] + assert all(not dot(x, row) for row in zip(*columns, strict=True)) + vectors.append(x) + assert len(vectors) == 2 + return pivots, vectors + + +def supports(kernel): + slopes = {} + always_zero = [] + for j, (a, b) in enumerate(zip(*kernel, strict=True)): + if not a and not b: + always_zero.append(j) + continue + slope = b / a if a else "infinity" + slopes.setdefault(slope, []).append(j) + witnesses = [] + for slope, omitted in slopes.items(): + a, b = [vec[omitted[0]] for vec in kernel] + x = add([b * y for y in kernel[0]], kernel[1], -a) + support = [i for i, coeff in enumerate(x) if coeff] + assert set(range(len(x))) - set(support) == set(omitted) | set(always_zero) + witnesses.append({"slope": str(slope), "omitted": omitted, "support": support, + "coefficients": [str(y) for y in x]}) + return {"always_zero": always_zero, "witnesses": witnesses} + + +def source_factors(unit, apply, tape): + factors, keys = [], [] + for clock, event in enumerate(tape): + if event[0] == "J": + a, b, c, d = event[2] + shears = [(b, a, 1), (c, d, -1)] + elif event[:2] == ["A", "QUERY"]: + assert event[-1] == -1 + shears = [(event[2], event[3], 1)] + else: + continue + prefix = tape[:clock] + cols = [apply(prefix, unit(j), -1) for j in range(DIMENSION)] + for dest, source, sign in shears: + u = apply(prefix, unit(dest), -1, inverse=True) + v = [2 * sign * col[source] for col in cols] + assert any(u) and any(v) and not dot(u, v) + factors.append((u, v)) + keys.append([clock, dest, source]) + assert len(factors) == 38 + return factors, keys + + +def suffix_transport(factors): + result = [] + for i, (u, v) in enumerate(factors): + for a, b in factors[i + 1:]: + u = add(u, a, dot(b, u)) + v = add(v, b, -dot(v, a)) + assert not dot(u, v) + result.append((u, v)) + return result + + +def target(case, factors, transported, units): + unselected = [f for i, f in enumerate(factors) if i not in case] + selected = [transported[i] for i in reversed(case)] + cols = [product(selected, col) for col in units] + assert cols == [[-x for x in product(unselected, col, inverse=True)] for col in units] + delta = [add(col, e, -1) for col, e in zip(cols, units, strict=True)] + _, pivots = rref(zip(*delta, strict=True)) + return cols, pivots + + +def stop(*_): + raise TimeoutError("20-second exact nullspace and literal-product cap") + + +def main(): + assert __debug__ + signal(SIGALRM, stop) + alarm(20) + for name, digest in PINS.items(): + assert sha256((ROOT / name).read_bytes()).hexdigest() == digest + source = run_path(str(ROOT / "inputs/forward.py")) + unit, apply = source["unit"], source["apply"] + tape = loads((ROOT / "inputs/CALLER.json").read_bytes())["events"] + assert len(tape) == 4783 + factors, keys = source_factors(unit, apply, tape) + units = [unit(i) for i in range(DIMENSION)] + for e in units: + assert apply(tape, e, 1) == e + assert apply(tape, e, -1) == product(factors, e) == [-x for x in e] + transported = suffix_transport(factors) + certs, candidates = {}, [] + for axis, name in enumerate(("image", "covector")): + pivots, kernel = nullspace([f[axis] for f in transported]) + cert = supports(kernel) + cert["pivots"] = pivots + cert["kernel"] = [[str(x) for x in col] for col in kernel] + certs[name] = cert + candidates.extend((len(w["support"]), w["support"], name) for w in cert["witnesses"]) + controls = [[0, 37], [1, 20, 36], [0, 4, 33, 37]] + for case in controls: + assert len(target(case, factors, transported, units)[1]) == len(case) + minimum, chosen, axis = min(candidates) + tied = sorted({tuple(case) for length, case, _ in candidates if length == minimum}) + cols, pivots = target(chosen, factors, transported, units) + assert len(pivots) < minimum and chosen[0] < 2 and chosen[-1] >= 36 + result = { + "pins": PINS, "budget_seconds": 20, "factor_keys": keys, "factor_count": len(keys), + "dimension": DIMENSION, "minimum_support": minimum, "chosen": chosen, + "chosen_axis": axis, "tied_supports": tied, "displacement_pivots": pivots, + "target_columns": [[str(x) for x in col] for col in cols], "certificates": certs, + "full_signs": [1, -1], "controls": controls, + } + alarm(0) + print(dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-signed-factor-circuit-gauge/closure/lead/inputs/7113-SHA256.json b/research/p104-signed-factor-circuit-gauge/closure/lead/inputs/7113-SHA256.json new file mode 100644 index 0000000000..5a7d6b80dc --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/lead/inputs/7113-SHA256.json @@ -0,0 +1,69 @@ +{ + "replay/supplier7108/CALLER.json": "9557f713ab4ffb91ede05e8a6d5668c694b9940fc16f2f2d657e2f2b2cac2d3f", + "replay/supplier7112/RESULT.json": "7b808ff32d9803084aaaf820cd172ddc9001c7aebbd17e0324e779abeff91b30", + "replay/supplier7112/WORD.json.gz": "fe0b1dc3049a6b72760a705af2e698e0e9998e969e19862a696eba63434eb233", + "replay/supplier7112/short-caller/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "replay/supplier7112/short-caller/ODD-LOCALIZED-GROUPING.json": "8aac6b3d9e528bffbcf411bbd300c8e0f0b7bf75da45ab12badf3f3530ffcbe2", + "replay/supplier7112/short-caller/ODD-UNIT-DYADIC-TAPES.json": "c3195057f7a6723a81172ed540d0f1c4ba699ff3cb8dc37cbde7bb481d9b976c", + "replay/supplier7112/short-caller/ODD-UNIT-PREFIX-CLOSURES.json": "3b953e5d3e83e7573a3e908a5a23edb78773d4d22816aca54f766f0f0e9f5403", + "replay/supplier7112/short-caller/SHORT-ADMISSION-PARTIAL.json": "7977815fe72382738727e3d550eea3bc735923c9c57968872d4f863cb39cd401", + "replay/supplier7112/short-caller/SHORT-CALLER-RAW-PRICE.json": "a4f83d65d250efb40f6506658374d7414afdde11c96eb88b7d2fbb182aa090c1", + "replay/supplier7112/short-caller/SHORT-CATALOGUE-0-1000.log": "a916a76627fb79bf606b22f857ca93db6342891fb2c85b20658b5002c359e422", + "replay/supplier7112/short-caller/SHORT-CATALOGUE-1000-2000.log": "da633bfa408e98a2f2a958262a09d5e4274a9b25f7b4a6a73df5a97f37338f79", + "replay/supplier7112/short-caller/SHORT-CATALOGUE-2000-3047.log": "e8d500c0261a4a9e0cf3da2838d82806ed497ab9cf57cb8620ca6debfb98525c", + "replay/supplier7112/short-caller/SHORT-PRECISION.json": "68a00d2b83ee2eb944d2e05fc7f32bc9aa37282c45b968f0ab6fd500659ac028", + "replay/supplier7112/short-caller/SHORT-TYPE-A-ROOT.json": "e9812d720942d8149c219dfa28c1081ff1d353529e5282ca4624a04233f38f88", + "replay/supplier7112/short-caller/admission-source/ARCHIVE-CHAIN.json": "6de95c4eb396e69883fbeeb3989782bbbe232c22644af1c804050badca10f456", + "replay/supplier7112/short-caller/admission-source/FULL-RESULT.json": "d9ba709fa5dcefffe3f3abdcf34600ce188224703cfd743e6db8b58ba4816cb7", + "replay/supplier7112/short-caller/admission-source/INDEPENDENT-NOTICE.md": "cadbc642ca84311d2c7a6cf704c7828cb4cf77e3c784b66e4c6e8a5c28002fb8", + "replay/supplier7112/short-caller/admission-source/INDEPENDENT-SOURCES.json": "dced1457df5230466ba6202fd6d4595bc2b7fb2a65302806bf2720b1837ff350", + "replay/supplier7112/short-caller/admission-source/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "replay/supplier7112/short-caller/admission-source/NATIVE-INPUTS.json": "9bb6c1567783661334d6c1d23f715ce5635cbbb513678819ab9e020a34c7e4c0", + "replay/supplier7112/short-caller/admission-source/NOTICE": "da12736e2e824167ff56f2ecb623a5f88f75a270410360890f61dffc33bab249", + "replay/supplier7112/short-caller/admission-source/data/bit-admission.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "replay/supplier7112/short-caller/admission-source/data/caller.json": "3828d53e80ea97e8b866320f081af20b6b93bfebd58b95b56b85a7afe151af5e", + "replay/supplier7112/short-caller/admission-source/data/final.json.gz": "2b94953dc14a122e3ef089633f05b58ec689ec5156feb7c784ed3e137dc01883", + "replay/supplier7112/short-caller/admission-source/frozen/clifford_exact.py": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "replay/supplier7112/short-caller/admission-source/frozen/native_verify.py": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "replay/supplier7112/short-caller/admission-source/frozen/physical.py": "4e995d1158033d83bf69b671f23dc7924d66edbbe07623ba063ba7421234ea20", + "replay/supplier7112/short-caller/admission-source/frozen/verify_host3_odd.py": "e75ad2096ba2587d1dc9c8982b2c2eb7c6fd2636a80adcd943314ef2cf6fd258", + "replay/supplier7112/short-caller/admission-source/independent.py": "21f46a8340331abb1486b50bd4e04453f1968b0a5950d86ff7780dd368590874", + "replay/supplier7112/short-caller/admission-source/interval_gate.py": "60a743d13f668ef86db4b8215b4d5d04430a671ba6f1fe06d9c1c4c3dfe86da5", + "replay/supplier7112/short-caller/admission-source/precision_replay.py": "850d9098c5946ab27ef5228acc54d59df2196e72259d3e21588ec0c319c8f5ee", + "replay/supplier7112/short-caller/admission-source/retained/odd-native-common-grid/independent_bounds.py": "198521def614fe78fa728f1dde2b7fb820c0c0e0ac3ad0c9224dccbf51eac0d5", + "replay/supplier7112/short-caller/admission-source/retained/query-only-precision-envelope/envelopes.py": "783da6b5b450fc07434946cb9ec86070dfee01df6b5fa1c385cb024def2c9a9f", + "replay/supplier7112/short-caller/admission-source/retained/query-only-precision-envelope/source_binding.py": "624c459311c58f3847b7713b818bfd340153abf42919f02ac9aa8892ed52a2bd", + "replay/supplier7112/short-caller/assemble_odd_application.py": "6cdac39ab196a70c53ba2283c2555cd8dee30644dcc4769628b46fb53bd55a1f", + "replay/supplier7112/short-caller/candidate_gate.py": "e71097ca81a082afd7c647324a6c94cb357aeb1084693a095a0f3e0b45a9b11a", + "replay/supplier7112/short-caller/check_odd_caller_exact_grid.py": "abd5a5fd011b71e5b382cbc058855594d4f2fe7b049f375506675c0303180f54", + "replay/supplier7112/short-caller/check_odd_fixed_tape_counts.py": "e6246e9f8fbeae3077d82e585eafd3647c1a8758c58f33c7c13e7efa6c1e42bb", + "replay/supplier7112/short-caller/check_odd_partial_admission.py": "4416b1ea5f07f8a91028a2e500116588fbdfaed95a8ef9bac7a46bcb44b9478e", + "replay/supplier7112/short-caller/check_odd_physical_binding.py": "5c80c3b0415a7f91d216395248dd6f13297eed637732098e1ca8fb0548951b98", + "replay/supplier7112/short-caller/check_odd_precision.py": "b2d9c13577158157a587ace766d9dadb7819a0164b372722329d9754e1be6c61", + "replay/supplier7112/short-caller/connected.py": "469537b46fb92c5aca926d3b1497da5425408673b0a73ba1427f23d872b414e7", + "replay/supplier7112/short-caller/cut_library.py": "7ccb81af19db54ec7cdb44849af018d4ca8893f80f17277914f8566715985133", + "replay/supplier7112/short-caller/emit_odd_type_ab.py": "7a7993648433c6febad8c07b315aec1b96598835a3f587b62040423c33c3b71f", + "replay/supplier7112/short-caller/emit_odd_type_b.py": "d1fa8b67d98beacd6bb574b3d5fcbc94b8646a7ffbce91d2a6fd4d690d3c5329", + "replay/supplier7112/short-caller/host34.py": "bded1a8626d65ee40c4ba3b25780fc03f0fa08906f3c83f631892df072d9a9b7", + "replay/supplier7112/short-caller/independent.py": "21f46a8340331abb1486b50bd4e04453f1968b0a5950d86ff7780dd368590874", + "replay/supplier7112/short-caller/interval_gate.py": "60a743d13f668ef86db4b8215b4d5d04430a671ba6f1fe06d9c1c4c3dfe86da5", + "replay/supplier7112/short-caller/lower.py": "67345fdfc8e5bb816e24b37dfafad0396372c48ec4e1b95b8b69f019a8fdfdee", + "replay/supplier7112/short-caller/mirrored.py": "55dd441a3a7f504b351857d45fd701994a0950ae1baec6c4c2b4b0166fb69db3", + "replay/supplier7112/short-caller/odd_unit_dyadic_tapes.py": "3cdafa35635360a487ce400ec8d585f6134dd7c58209543528e98e7db178bbc7", + "replay/supplier7112/short-caller/screen.py": "01e3eaba4b710a080e6e393e53157e6a119fdf312620eed26e9185ca91f6bea6", + "replay/supplier7112/short-caller/short_dyadic_seam.py": "6e588b365618ab2df4fa2d1f16073d09a953a7cd6e826e1f96bbf87f950b672b", + "replay/supplier7112/short-caller/short_native_catalogue.py": "775695c379f407801910531565cc371012cee501b2cec5f5d718ecdccf06b64d", + "replay/supplier7112/short-caller/signed_child.py": "ef03444360f02225138be9b38e2f9a85f313eeaa910d63a365de0f16d228cb8b", + "replay/supplier7112/short-caller/signed_model.py": "f88c798b9a22c656ea0b755b4f32be411c1f80687dff1a1ac9e9c2a0b5f4203e", + "replay/supplier7112/short-caller/stage.py": "0ab5546e926dd98d3ad833909b534840b7d8d0467c4790ca09bc2b14b37313f5", + "replay/supplier7112/short-caller/upstream_application.py": "d98987db98553dc55bfc80e3ca47abfcd51c57af6f8cda61101391d8eae94184", + "replay/supplier7112/short-caller/upstream_native_catalogue.py": "6120e1ea1e07eeba757694d209437a38f121b0a377cc466889a30fa52c561472", + "expected/ODD-8X9-APPLICATION-CHECKS.json": "10512d62f540fe7bb839ec94b6a21bbdf4a3dfadf56b4ec9095d4b242bda19b8", + "expected/ODD-ADMISSION-PARTIAL.json": "75ec76e4393ef1622fcff9e2727dc411921076af4a506d97506665add140fa86", + "expected/ODD-CALLER-EXACT-GRID.json": "87d25d9fa3778bf4784e3a9e17f32ce5ba372663c6e97392cc62b87e6719042c", + "expected/ODD-FIXED-TAPE-COUNTS.json": "1a8bf36a966edca8c61f3be803cdbe136307095dec40245cdc93e79a9062fe99", + "expected/ODD-PHYSICAL-BINDING.json": "ade5f8cbb2e30677b1d48d23a1aa270b3d0b72e2504472ab9fdb71d124b075b5", + "expected/ODD-PRECISION.json": "9c03607288cc2afb80cb02c197f93360978233036418b32b09ad91be16f9c153", + "expected/ODD-TYPE-AB-CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "expected/ODD-TYPE-AB-REPLAY.json": "71fd0a7ad8b743266c6a75100f3543b48ea7d6fcbe45f008d3b61270e3b660a0" +} diff --git a/research/p104-signed-factor-circuit-gauge/closure/lead/inputs/7113-signed-child.py b/research/p104-signed-factor-circuit-gauge/closure/lead/inputs/7113-signed-child.py new file mode 100644 index 0000000000..0980a6559b --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/lead/inputs/7113-signed-child.py @@ -0,0 +1,146 @@ +"""Exact nine-slot signed child on the retained 153-coordinate field layout.""" + +from collections import Counter +from hashlib import sha256 +from pathlib import Path +from random import Random +import argparse +import json + +LAYOUT = 153 +EXPECTED_PORTS = (15, 17, 27, 34, 35, 42, 47, 55) +NOTE_SHA = '64c70926a8705874f1c9b42a2f703e42cad4e90f927f544458cfdf729540236c' +# Integer numerators over 2 in the exact C gate. +C = (((1, 1), (1, -1)), ((1, -1), (1, 1))) +PHASE = ((1, 0), (0, -1), (-1, 0), (0, 1)) + + +def multiply(x, y): + a, b = x + c, d = y + return a*c - b*d, a*d + b*c + + +def conjugate(z): + a, b = z + return a, -b + + +def matrix_product(a, b): + return tuple(tuple(tuple(sum(multiply(a[i][k], b[k][j])[c] for k in range(2)) + for c in range(2)) for j in range(2)) for i in range(2)) + + +def swap_blocks(label, a, b, width): + mask = (1 << width)-1 + delta = ((label >> (a*width)) ^ (label >> (b*width))) & mask + return label ^ (delta << (a*width)) ^ (delta << (b*width)) + + +def permute(label, swaps, width): + for a, b in swaps: + label = swap_blocks(label, a, b, width) + return label + + +def masks(stage, width): + return ((1 << width)-1, ((1 << (8*width))-1) << ((9+8*(stage-1))*width)) + + +def descriptor(stage): + assert 1 <= stage <= 18 + return tuple((j, 8*stage+j) for j in range(1, 9)) + + +def packed_kernel(row, col, width, mutate=None): + if (row ^ col) >> (9*width): + return (0, 0) + result = (1, 0) + for j in range(9*width): + result = multiply(result, C[(row >> j) & 1][(col >> j) & 1]) + q = (1 << width)-1 + if (row ^ col) & q and ((row ^ col) & q).bit_count() % 2: + result = -result[0], -result[1] + exponent = width if mutate != 'missing multiplicity' else 1 + return multiply(PHASE[exponent % 4] if mutate != 'missing global phase' else (1,0), result) + + +def separate_kernel(row, col, stage, width): + q, body = masks(stage, width) + if (row ^ col) & ~(q | body): + return (0,0) + result = (1,0) + for bit in range(width): + result = multiply(result, conjugate(C[(row >> bit) & 1][(col >> bit) & 1])) + start = (9+8*(stage-1))*width + for bit in range(start, start+8*width): + result = multiply(result, C[(row >> bit) & 1][(col >> bit) & 1]) + return result + + +def verify_route(stage, width): + swaps = descriptor(stage) + q, body = masks(stage, width) + front = (1 << (9*width))-1 + assert permute(q | body, swaps, width) == front + assert permute(q, swaps, width) == q + for i in range(LAYOUT*width): + x = 1 << i + assert permute(permute(x, swaps, width), reversed(swaps), width) == x + return swaps + + +def check_finite(stage, width, rng): + swaps = verify_route(stage, width) + q, body = masks(stage, width) + prefix = 9*width + active = q | body + parked = rng.getrandbits(LAYOUT*width) & ~active + if width == 1: + pairs = ((r,c) for r in range(1< x + u f(x). +The returned factors multiply from left to right in their listed order. +""" +from fractions import Fraction as F + + +def dot(left, right): + return sum((a * b for a, b in zip(left, right) if a and b), F(0)) + + +def add(left, right, scale=1): + return tuple(a + scale * b for a, b in zip(left, right)) + + +def column_matrix_vector(columns, vector): + return tuple(dot(row, vector) for row in zip(*columns)) + + +def identity(size): + return tuple(tuple(F(row == column) for row in range(size)) + for column in range(size)) + + +def displacement(columns): + return tuple(tuple(entry - (row == j) for row, entry in enumerate(column)) + for j, column in enumerate(columns)) + + +def determinant_and_rank(columns): + """Return determinant and rank, using exact column elimination.""" + width = len(columns) + pending = list(columns) + pivot_count = 0 + determinant = F(1) + for row in range(width): + pivot_at = next((j for j in range(pivot_count, width) + if pending[j][row]), None) + if pivot_at is None: + determinant = F(0) + continue + if pivot_at != pivot_count: + pending[pivot_count], pending[pivot_at] = pending[pivot_at], pending[pivot_count] + determinant = -determinant + pivot = pending[pivot_count] + determinant *= pivot[row] + for j in range(pivot_count + 1, width): + if pending[j][row]: + pending[j] = add(pending[j], pivot, -pending[j][row] / pivot[row]) + pivot_count += 1 + return determinant, pivot_count + + +def proportionality(first, second): + """Return the ratio second / first if proportional, else None.""" + i = next(j for j, value in enumerate(first) if value) + ratio = second[i] / first[i] + return ratio if all(b == ratio * a for a, b in zip(first, second)) else None + + +def select_displacement(columns): + """Return Dx and D²x independent, or Dx with Dbar = scalar I.""" + representative = None + ratio = None + for column in columns: + if not any(column): + continue + squared = column_matrix_vector(columns, column) + current = proportionality(column, squared) + if current is None: + return column, squared, None + if representative is None: + representative = column + ratio = current + elif current != ratio: + combined = tuple(ratio * a + current * b for a, b in zip(representative, column)) + return add(representative, column), combined, None + return representative, None, ratio + + +def inverse_left(columns, image, covector): + assert any(image) and any(covector) and dot(covector, image) == 0 + return tuple(add(column, image, -dot(covector, column)) for column in columns) + + +def obstructed(delta): + """A nonidentity rational SL involution requires one extra factor.""" + nonzero = False + for column in delta: + if not any(column): + continue + nonzero = True + if column_matrix_vector(delta, column) != tuple(-2 * x for x in column): + return False + return nonzero + + +def solve_two(image, squared, i, j, target, other): + determinant = image[i] * squared[j] - image[j] * squared[i] + return ((target * squared[j] - other * image[j]) / determinant, + (image[i] * other - squared[i] * target) / determinant) + + +def peel(columns, delta, image, squared, ratio): + """Choose a transvection whose removal drops displacement rank.""" + rows = tuple(zip(*delta)) + i = next(j for j, value in enumerate(image) if value) + if ratio == 0: + covector = tuple(x / image[i] for x in rows[i]) + return (image, covector), inverse_left(columns, image, covector) + j = next(j for j in range(len(columns)) + if image[i] * squared[j] != image[j] * squared[i]) + first, second = solve_two(image, squared, i, j, F(1), F(0)) + covector = tuple(first * x + second * y for x, y in zip(rows[i], rows[j])) + remainder = inverse_left(columns, image, covector) + if obstructed(displacement(remainder)): + for h, row in enumerate(rows): + first, second = solve_two(image, squared, i, j, image[h], squared[h]) + adjustment = tuple(z - first * x - second * y + for x, y, z in zip(rows[i], rows[j], row)) + if any(adjustment): + covector = add(covector, adjustment) + remainder = inverse_left(columns, image, covector) + break + else: + raise ArithmeticError("no independent adjustment for exceptional quotient") + assert not obstructed(displacement(remainder)) + return (image, covector), remainder + + +def factor_product(factors, size): + """Rebuild the listed product by exact independent column application.""" + columns = identity(size) + for image, covector in reversed(factors): + if not any(image) or not any(covector) or dot(covector, image): + raise ValueError("a supplied factor is not a nontrivial transvection") + columns = tuple(add(column, image, dot(covector, column)) for column in columns) + return columns + + +def factorize(columns): + """Return minimum length, displacement rank, obstruction and factors.""" + original = tuple(tuple(map(F, column)) for column in columns) + size = len(original) + if any(len(column) != size for column in original): + raise ValueError("matrix must be square and supplied in columns") + if determinant_and_rank(original)[0] != 1: + raise ValueError("matrix must have determinant one") + delta = displacement(original) + rank = determinant_and_rank(delta)[1] + exceptional = obstructed(delta) + current = original + factors = [] + if exceptional: + rows = tuple(zip(*delta)) + image = next(column for column in delta if any(column)) + i = next(j for j, value in enumerate(image) if value) + for j, row in enumerate(rows): + covector = add(row, rows[i], -image[j] / image[i]) + if any(covector): + break + else: + raise ArithmeticError("nonidentity rational SL involution has rank below two") + factors.append((image, covector)) + current = inverse_left(current, image, covector) + for _ in range(rank): + delta = displacement(current) + image, squared, ratio = select_displacement(delta) + if image is None or (ratio is not None and ratio != 0): + raise ArithmeticError("rank-dropping induction reached unexpected quotient") + factor, current = peel(current, delta, image, squared, ratio) + factors.append(factor) + if current != identity(size) or factor_product(factors, size) != original: + raise ArithmeticError("exact factorization verification failed") + return {"length": len(factors), "rank": rank, "involution": exceptional, + "factors": tuple(factors)} diff --git a/research/p104-signed-factor-circuit-gauge/closure/round209/construction/run.py b/research/p104-signed-factor-circuit-gauge/closure/round209/construction/run.py new file mode 100644 index 0000000000..bb4c239f75 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/round209/construction/run.py @@ -0,0 +1,95 @@ +"""Construct and replay one pinned 20-to-19 signed-sector factorization.""" +import argparse +import hashlib +import json +from fractions import Fraction +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from time import perf_counter + +HERE = Path(__file__).resolve().parent +FACTORIZER_SHA256 = "f946d4d02f0dc60fca48beaec5105f195257711fc9063f5b0aa0fd4a98cbe239" +CHOSEN = [0, 1, 2, 4, 6, 8, 10, 12, 14, 18, 19, 20, 22, 24, 26, 28, 30, 32, 34, 36] + + +def stop(*_): + raise TimeoutError("single R209 factorization 60-second cap reached") + + +def support(vector): + return [i for i, value in enumerate(vector) if value] + + +def planes(indices): + return sorted({index // 18 for index in indices}) + + +def shape(image, covector): + image_support = support(image) + covector_support = support(covector) + image_planes = planes(image_support) + covector_planes = planes(covector_support) + entries = [image[i] * covector[j] for i in image_support for j in covector_support] + return { + "image_support": image_support, + "covector_support": covector_support, + "image_planes": image_planes, + "covector_planes": covector_planes, + "mixed_image": len(image_planes) == 2, + "mixed_covector": len(covector_planes) == 2, + "pure_off_diagonal": len(image_planes) == len(covector_planes) == 1 and image_planes != covector_planes, + "cross_plane_entries": sum(i // 18 != j // 18 for i in image_support for j in covector_support), + "nondyadic_entries": sum(entry.denominator & (entry.denominator - 1) != 0 for entry in entries), + "max_denominator_bits": max(entry.denominator.bit_length() for entry in entries), + } + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("receipt", type=Path) + parser.add_argument("sha256") + args = parser.parse_args() + assert __debug__ + signal(SIGALRM, stop) + alarm(60) + started = perf_counter() + try: + raw = args.receipt.read_bytes() + assert hashlib.sha256(raw).hexdigest() == args.sha256 + src = HERE / "factorize.py" + assert hashlib.sha256(src.read_bytes()).hexdigest() == FACTORIZER_SHA256 + functions = run_path(str(src)) + receipt = json.loads(raw) + assert receipt["chosen"] == CHOSEN + columns = tuple(tuple(map(Fraction, column)) for column in receipt["target_columns"]) + assert len(columns) == 36 + result = functions["factorize"](columns) + factors = result["factors"] + assert result["length"] == 19 + mutant = list(factors) + image, covector = mutant[0] + mutant[0] = (tuple(-x for x in image), covector) + assert functions["factor_product"](mutant, 36) != columns + shapes = [shape(image, covector) for image, covector in factors] + report = { + "chosen": CHOSEN, "source_sha256": args.sha256, + "target_sha256": hashlib.sha256(json.dumps(receipt["target_columns"], separators=(",", ":")).encode()).hexdigest(), + "factorizer_sha256": FACTORIZER_SHA256, "rank": result["rank"], + "involution": result["involution"], "minimum_transvections": result["length"], + "mixed_image_factors": sum(s["mixed_image"] for s in shapes), + "mixed_covector_factors": sum(s["mixed_covector"] for s in shapes), + "pure_off_diagonal_factors": sum(s["pure_off_diagonal"] for s in shapes), + "cross_plane_factors": sum(s["cross_plane_entries"] > 0 for s in shapes), + "nondyadic_factors": sum(s["nondyadic_entries"] > 0 for s in shapes), + "sign_flip_negative_control": "rejected", "seconds": perf_counter() - started, + "shapes": shapes, + "factors": [[list(map(str, u)), list(map(str, v))] for u, v in factors], + } + print(json.dumps(report, sort_keys=True)) + finally: + alarm(0) + + +if __name__ == "__main__": + main() diff --git a/research/p104-signed-factor-circuit-gauge/closure/round209/independent/RESULT.json b/research/p104-signed-factor-circuit-gauge/closure/round209/independent/RESULT.json new file mode 100644 index 0000000000..f821598c07 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/round209/independent/RESULT.json @@ -0,0 +1,1470 @@ +{ + "blocks": [ + { + "column_plane": 0, + "displacement_rank": 18, + "first_nonzero": [ + 0, + 0, + "-2" + ], + "restriction_involution": true, + "row_plane": 0 + }, + { + "column_plane": 1, + "displacement_rank": 0, + "first_nonzero": null, + "row_plane": 0 + }, + { + "column_plane": 0, + "displacement_rank": 1, + "first_nonzero": [ + 18, + 1, + "4" + ], + "row_plane": 1 + }, + { + "column_plane": 1, + "displacement_rank": 1, + "first_nonzero": [ + 18, + 18, + "2" + ], + "restriction_involution": false, + "row_plane": 1 + } + ], + "caller": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "chosen": [ + 0, + 1, + 2, + 4, + 6, + 8, + 10, + 12, + 14, + 18, + 19, + 20, + 22, + 24, + 26, + 28, + 30, + 32, + 34, + 36 + ], + "corrupted_unchanged_factor_rejected": true, + "displacement_rank": 19, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "involution": false, + "kept": [ + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 16, + 17, + 21, + 23, + 25, + 27, + 29, + 31, + 33, + 35, + 37 + ], + "lower_plane_preserving_length_lower_bound": 20, + "nonpreserving_factors_lower_bound_if_length_19": 2, + "pins": { + "inputs/7113-SHA256.json": "064e11ecfedce9937ea1782e5baee37e89b3c9eebabed5b4a9ba84f412bbe078", + "inputs/CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "inputs/R195.json": "f6091c7c63b21145077808bbdacc61431f641d0da37f9fa648aea4b7ead3b472" + }, + "preserves_both_coordinate_planes": false, + "preserving_factorization_possible": false, + "r208_runner_sha256": "91c17d100b8f06a1fd8b8bc8e5f4a1b2cc3bf5900d0a9e70f8faeb27e3da48df", + "runner_cap_seconds": 20, + "target_columns": [ + [ + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "3", + "2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1" + ] + ] +} diff --git a/research/p104-signed-factor-circuit-gauge/closure/round209/independent/replay.py b/research/p104-signed-factor-circuit-gauge/closure/round209/independent/replay.py new file mode 100644 index 0000000000..08897cf176 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/round209/independent/replay.py @@ -0,0 +1,100 @@ +"""Exact unchanged-chronology replay of the single R209 J1 extension.""" +from fractions import Fraction as Q +from hashlib import sha256 +from json import dumps +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal +from sys import argv, implementation, version_info + +SECONDS = 20 +CHOSEN = (0, 1, 2, 4, 6, 8, 10, 12, 14, 18, 19, 20, 22, 24, 26, 28, 30, 32, 34, 36) +REPLAY_SHA = '91c17d100b8f06a1fd8b8bc8e5f4a1b2cc3bf5900d0a9e70f8faeb27e3da48df' + + +def multiply(columns, v): + return [sum(a * b for a, b in zip(row, v, strict=True) if a and b) + for row in zip(*columns, strict=True)] + + +def difference(columns): + return [[x - Q(i == j) for i, x in enumerate(column)] for j, column in enumerate(columns)] + + +def is_involution(columns): + return all(multiply(columns, column) == [Q(i == j) for i in range(len(columns))] + for j, column in enumerate(columns)) + + +def stop(*_): + raise TimeoutError(f'R209 independent {SECONDS}-second cap') + + +def main(): + assert __debug__ and implementation.name == 'cpython' and version_info[:2] == (3, 12) + assert len(argv) == 3, 'pass the authenticated R208 runner and #7435 package root' + predecessor, root = [Path(s).resolve() for s in argv[1:]] + assert sha256(predecessor.read_bytes()).hexdigest() == REPLAY_SHA + old = run_path(str(predecessor)) + signal(SIGALRM, stop) + alarm(SECONDS) + tape = old['read'](root, 'inputs/CALLER.json')['events'] + manifest = old['read'](root, 'inputs/7113-SHA256.json') + pins = old['PINS'] + assert manifest['expected/ODD-TYPE-AB-CALLER.json'] == pins['inputs/CALLER.json'] + predecessor_receipt = old['read'](root, 'inputs/R195.json') + assert (predecessor_receipt['head'], predecessor_receipt['caller']) == (old['HEAD'], old['CALLER']) + original, labels = old['signed_prefix'](tape, -1) + assert len(original) == 38 and labels == predecessor_receipt['factor_labels'] + assert labels[0][:3] == [43, 1, 0] and labels[1][:3] == [43, 1, 1] + kept = [factor for i, factor in enumerate(original) if i not in CHOSEN] + assert len(kept) == 18 + unit, apply, echelon = [old[k] for k in ('unit', 'apply', 'echelon')] + target = [] + for j in range(36): + basis = unit(j) + unchanged_inverse = apply(kept, basis, inverse=True) + assert apply(kept, unchanged_inverse) == basis + column = apply(original, unchanged_inverse) + assert column == [-x for x in unchanged_inverse] + target.append(column) + # The inverse old complement appears on the right, applied first. + target_delta = difference(target) + displacement_rank = len(echelon(target_delta)) + blocks = [] + split = (range(18), range(18, 36)) + for a, rows in enumerate(split): + for b, cols in enumerate(split): + data = [[target_delta[j][i] for i in rows] for j in cols] + witness = next(((i, j, str(target_delta[j][i])) for j in cols for i in rows if target_delta[j][i]), None) + item = {'row_plane': a, 'column_plane': b, 'displacement_rank': len(echelon(data)), 'first_nonzero': witness} + if a == b: + item['restriction_involution'] = is_involution([[target[j][i] for i in rows] for j in cols]) + blocks.append(item) + preserving = all(row['displacement_rank'] == 0 for row in blocks if row['row_plane'] != row['column_plane']) + assert displacement_rank == 19 and not is_involution(target) + assert not preserving, 'the stipulated coordinate-plane obstruction failed' + assert [b['displacement_rank'] for b in blocks] == [18, 0, 1, 1] + assert target[1][18] == 4 + assert all(target[j][:18] == [-x for x in unit(j)[:18]] for j in range(18)) + # Any lower-plane-preserving transvection changes at most one diagonal block. + # The quotient -I needs at least 19, and the lower block needs one more. + # Flip one unchanged factor's sign. The resulting exact matrix differs. + u, v = kept[0] + altered = [([-x for x in u], v), *kept[1:]] + assert any(apply(altered, unit(j), inverse=True) != apply(kept, unit(j), inverse=True) for j in range(36)) + alarm(0) + print(dumps({'head': old['HEAD'], 'caller': old['CALLER'], 'pins': pins, + 'r208_runner_sha256': REPLAY_SHA, 'runner_cap_seconds': SECONDS, + 'chosen': CHOSEN, 'kept': [i for i in range(38) if i not in CHOSEN], + 'displacement_rank': displacement_rank, 'involution': is_involution(target), + 'blocks': blocks, 'preserves_both_coordinate_planes': preserving, + 'preserving_factorization_possible': False, + 'lower_plane_preserving_length_lower_bound': 20, + 'nonpreserving_factors_lower_bound_if_length_19': 2, + 'corrupted_unchanged_factor_rejected': True, + 'target_columns': [[str(x) for x in c] for c in target]}, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/p104-signed-factor-circuit-gauge/closure/round209/lead/RESULT.json b/research/p104-signed-factor-circuit-gauge/closure/round209/lead/RESULT.json new file mode 100644 index 0000000000..70886f4087 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/round209/lead/RESULT.json @@ -0,0 +1,2938 @@ +{ + "added": 1, + "case_cap": 1, + "chosen": [ + 0, + 1, + 2, + 4, + 6, + 8, + 10, + 12, + 14, + 18, + 19, + 20, + 22, + 24, + 26, + 28, + 30, + 32, + 34, + 36 + ], + "fixed_partition_off_block": [ + [ + 18, + 1, + "4" + ], + [ + 19, + 1, + "2" + ], + [ + 20, + 1, + "-2" + ], + [ + 21, + 1, + "-2" + ], + [ + 22, + 1, + "-2" + ], + [ + 23, + 1, + "-2" + ], + [ + 24, + 1, + "-2" + ], + [ + 25, + 1, + "-2" + ], + [ + 26, + 1, + "-2" + ], + [ + 27, + 1, + "-2" + ], + [ + 28, + 1, + "-2" + ], + [ + 29, + 1, + "-2" + ], + [ + 30, + 1, + "-2" + ], + [ + 31, + 1, + "-2" + ], + [ + 32, + 1, + "-2" + ], + [ + 33, + 1, + "-2" + ], + [ + 34, + 1, + "-2" + ], + [ + 35, + 1, + "-2" + ], + [ + 18, + 2, + "-4" + ], + [ + 19, + 2, + "-2" + ], + [ + 20, + 2, + "2" + ], + [ + 21, + 2, + "2" + ], + [ + 22, + 2, + "2" + ], + [ + 23, + 2, + "2" + ], + [ + 24, + 2, + "2" + ], + [ + 25, + 2, + "2" + ], + [ + 26, + 2, + "2" + ], + [ + 27, + 2, + "2" + ], + [ + 28, + 2, + "2" + ], + [ + 29, + 2, + "2" + ], + [ + 30, + 2, + "2" + ], + [ + 31, + 2, + "2" + ], + [ + 32, + 2, + "2" + ], + [ + 33, + 2, + "2" + ], + [ + 34, + 2, + "2" + ], + [ + 35, + 2, + "2" + ], + [ + 18, + 3, + "4" + ], + [ + 19, + 3, + "2" + ], + [ + 20, + 3, + "-2" + ], + [ + 21, + 3, + "-2" + ], + [ + 22, + 3, + "-2" + ], + [ + 23, + 3, + "-2" + ], + [ + 24, + 3, + "-2" + ], + [ + 25, + 3, + "-2" + ], + [ + 26, + 3, + "-2" + ], + [ + 27, + 3, + "-2" + ], + [ + 28, + 3, + "-2" + ], + [ + 29, + 3, + "-2" + ], + [ + 30, + 3, + "-2" + ], + [ + 31, + 3, + "-2" + ], + [ + 32, + 3, + "-2" + ], + [ + 33, + 3, + "-2" + ], + [ + 34, + 3, + "-2" + ], + [ + 35, + 3, + "-2" + ], + [ + 18, + 4, + "-4" + ], + [ + 19, + 4, + "-2" + ], + [ + 20, + 4, + "2" + ], + [ + 21, + 4, + "2" + ], + [ + 22, + 4, + "2" + ], + [ + 23, + 4, + "2" + ], + [ + 24, + 4, + "2" + ], + [ + 25, + 4, + "2" + ], + [ + 26, + 4, + "2" + ], + [ + 27, + 4, + "2" + ], + [ + 28, + 4, + "2" + ], + [ + 29, + 4, + "2" + ], + [ + 30, + 4, + "2" + ], + [ + 31, + 4, + "2" + ], + [ + 32, + 4, + "2" + ], + [ + 33, + 4, + "2" + ], + [ + 34, + 4, + "2" + ], + [ + 35, + 4, + "2" + ], + [ + 18, + 5, + "4" + ], + [ + 19, + 5, + "2" + ], + [ + 20, + 5, + "-2" + ], + [ + 21, + 5, + "-2" + ], + [ + 22, + 5, + "-2" + ], + [ + 23, + 5, + "-2" + ], + [ + 24, + 5, + "-2" + ], + [ + 25, + 5, + "-2" + ], + [ + 26, + 5, + "-2" + ], + [ + 27, + 5, + "-2" + ], + [ + 28, + 5, + "-2" + ], + [ + 29, + 5, + "-2" + ], + [ + 30, + 5, + "-2" + ], + [ + 31, + 5, + "-2" + ], + [ + 32, + 5, + "-2" + ], + [ + 33, + 5, + "-2" + ], + [ + 34, + 5, + "-2" + ], + [ + 35, + 5, + "-2" + ], + [ + 18, + 6, + "-4" + ], + [ + 19, + 6, + "-2" + ], + [ + 20, + 6, + "2" + ], + [ + 21, + 6, + "2" + ], + [ + 22, + 6, + "2" + ], + [ + 23, + 6, + "2" + ], + [ + 24, + 6, + "2" + ], + [ + 25, + 6, + "2" + ], + [ + 26, + 6, + "2" + ], + [ + 27, + 6, + "2" + ], + [ + 28, + 6, + "2" + ], + [ + 29, + 6, + "2" + ], + [ + 30, + 6, + "2" + ], + [ + 31, + 6, + "2" + ], + [ + 32, + 6, + "2" + ], + [ + 33, + 6, + "2" + ], + [ + 34, + 6, + "2" + ], + [ + 35, + 6, + "2" + ], + [ + 18, + 7, + "4" + ], + [ + 19, + 7, + "2" + ], + [ + 20, + 7, + "-2" + ], + [ + 21, + 7, + "-2" + ], + [ + 22, + 7, + "-2" + ], + [ + 23, + 7, + "-2" + ], + [ + 24, + 7, + "-2" + ], + [ + 25, + 7, + "-2" + ], + [ + 26, + 7, + "-2" + ], + [ + 27, + 7, + "-2" + ], + [ + 28, + 7, + "-2" + ], + [ + 29, + 7, + "-2" + ], + [ + 30, + 7, + "-2" + ], + [ + 31, + 7, + "-2" + ], + [ + 32, + 7, + "-2" + ], + [ + 33, + 7, + "-2" + ], + [ + 34, + 7, + "-2" + ], + [ + 35, + 7, + "-2" + ], + [ + 18, + 8, + "-4" + ], + [ + 19, + 8, + "-2" + ], + [ + 20, + 8, + "2" + ], + [ + 21, + 8, + "2" + ], + [ + 22, + 8, + "2" + ], + [ + 23, + 8, + "2" + ], + [ + 24, + 8, + "2" + ], + [ + 25, + 8, + "2" + ], + [ + 26, + 8, + "2" + ], + [ + 27, + 8, + "2" + ], + [ + 28, + 8, + "2" + ], + [ + 29, + 8, + "2" + ], + [ + 30, + 8, + "2" + ], + [ + 31, + 8, + "2" + ], + [ + 32, + 8, + "2" + ], + [ + 33, + 8, + "2" + ], + [ + 34, + 8, + "2" + ], + [ + 35, + 8, + "2" + ], + [ + 18, + 9, + "4" + ], + [ + 19, + 9, + "2" + ], + [ + 20, + 9, + "-2" + ], + [ + 21, + 9, + "-2" + ], + [ + 22, + 9, + "-2" + ], + [ + 23, + 9, + "-2" + ], + [ + 24, + 9, + "-2" + ], + [ + 25, + 9, + "-2" + ], + [ + 26, + 9, + "-2" + ], + [ + 27, + 9, + "-2" + ], + [ + 28, + 9, + "-2" + ], + [ + 29, + 9, + "-2" + ], + [ + 30, + 9, + "-2" + ], + [ + 31, + 9, + "-2" + ], + [ + 32, + 9, + "-2" + ], + [ + 33, + 9, + "-2" + ], + [ + 34, + 9, + "-2" + ], + [ + 35, + 9, + "-2" + ], + [ + 18, + 10, + "-4" + ], + [ + 19, + 10, + "-2" + ], + [ + 20, + 10, + "2" + ], + [ + 21, + 10, + "2" + ], + [ + 22, + 10, + "2" + ], + [ + 23, + 10, + "2" + ], + [ + 24, + 10, + "2" + ], + [ + 25, + 10, + "2" + ], + [ + 26, + 10, + "2" + ], + [ + 27, + 10, + "2" + ], + [ + 28, + 10, + "2" + ], + [ + 29, + 10, + "2" + ], + [ + 30, + 10, + "2" + ], + [ + 31, + 10, + "2" + ], + [ + 32, + 10, + "2" + ], + [ + 33, + 10, + "2" + ], + [ + 34, + 10, + "2" + ], + [ + 35, + 10, + "2" + ], + [ + 18, + 11, + "4" + ], + [ + 19, + 11, + "2" + ], + [ + 20, + 11, + "-2" + ], + [ + 21, + 11, + "-2" + ], + [ + 22, + 11, + "-2" + ], + [ + 23, + 11, + "-2" + ], + [ + 24, + 11, + "-2" + ], + [ + 25, + 11, + "-2" + ], + [ + 26, + 11, + "-2" + ], + [ + 27, + 11, + "-2" + ], + [ + 28, + 11, + "-2" + ], + [ + 29, + 11, + "-2" + ], + [ + 30, + 11, + "-2" + ], + [ + 31, + 11, + "-2" + ], + [ + 32, + 11, + "-2" + ], + [ + 33, + 11, + "-2" + ], + [ + 34, + 11, + "-2" + ], + [ + 35, + 11, + "-2" + ], + [ + 18, + 12, + "-4" + ], + [ + 19, + 12, + "-2" + ], + [ + 20, + 12, + "2" + ], + [ + 21, + 12, + "2" + ], + [ + 22, + 12, + "2" + ], + [ + 23, + 12, + "2" + ], + [ + 24, + 12, + "2" + ], + [ + 25, + 12, + "2" + ], + [ + 26, + 12, + "2" + ], + [ + 27, + 12, + "2" + ], + [ + 28, + 12, + "2" + ], + [ + 29, + 12, + "2" + ], + [ + 30, + 12, + "2" + ], + [ + 31, + 12, + "2" + ], + [ + 32, + 12, + "2" + ], + [ + 33, + 12, + "2" + ], + [ + 34, + 12, + "2" + ], + [ + 35, + 12, + "2" + ], + [ + 18, + 13, + "4" + ], + [ + 19, + 13, + "2" + ], + [ + 20, + 13, + "-2" + ], + [ + 21, + 13, + "-2" + ], + [ + 22, + 13, + "-2" + ], + [ + 23, + 13, + "-2" + ], + [ + 24, + 13, + "-2" + ], + [ + 25, + 13, + "-2" + ], + [ + 26, + 13, + "-2" + ], + [ + 27, + 13, + "-2" + ], + [ + 28, + 13, + "-2" + ], + [ + 29, + 13, + "-2" + ], + [ + 30, + 13, + "-2" + ], + [ + 31, + 13, + "-2" + ], + [ + 32, + 13, + "-2" + ], + [ + 33, + 13, + "-2" + ], + [ + 34, + 13, + "-2" + ], + [ + 35, + 13, + "-2" + ], + [ + 18, + 14, + "-4" + ], + [ + 19, + 14, + "-2" + ], + [ + 20, + 14, + "2" + ], + [ + 21, + 14, + "2" + ], + [ + 22, + 14, + "2" + ], + [ + 23, + 14, + "2" + ], + [ + 24, + 14, + "2" + ], + [ + 25, + 14, + "2" + ], + [ + 26, + 14, + "2" + ], + [ + 27, + 14, + "2" + ], + [ + 28, + 14, + "2" + ], + [ + 29, + 14, + "2" + ], + [ + 30, + 14, + "2" + ], + [ + 31, + 14, + "2" + ], + [ + 32, + 14, + "2" + ], + [ + 33, + 14, + "2" + ], + [ + 34, + 14, + "2" + ], + [ + 35, + 14, + "2" + ], + [ + 18, + 15, + "4" + ], + [ + 19, + 15, + "2" + ], + [ + 20, + 15, + "-2" + ], + [ + 21, + 15, + "-2" + ], + [ + 22, + 15, + "-2" + ], + [ + 23, + 15, + "-2" + ], + [ + 24, + 15, + "-2" + ], + [ + 25, + 15, + "-2" + ], + [ + 26, + 15, + "-2" + ], + [ + 27, + 15, + "-2" + ], + [ + 28, + 15, + "-2" + ], + [ + 29, + 15, + "-2" + ], + [ + 30, + 15, + "-2" + ], + [ + 31, + 15, + "-2" + ], + [ + 32, + 15, + "-2" + ], + [ + 33, + 15, + "-2" + ], + [ + 34, + 15, + "-2" + ], + [ + 35, + 15, + "-2" + ], + [ + 18, + 16, + "-4" + ], + [ + 19, + 16, + "-2" + ], + [ + 20, + 16, + "2" + ], + [ + 21, + 16, + "2" + ], + [ + 22, + 16, + "2" + ], + [ + 23, + 16, + "2" + ], + [ + 24, + 16, + "2" + ], + [ + 25, + 16, + "2" + ], + [ + 26, + 16, + "2" + ], + [ + 27, + 16, + "2" + ], + [ + 28, + 16, + "2" + ], + [ + 29, + 16, + "2" + ], + [ + 30, + 16, + "2" + ], + [ + 31, + 16, + "2" + ], + [ + 32, + 16, + "2" + ], + [ + 33, + 16, + "2" + ], + [ + 34, + 16, + "2" + ], + [ + 35, + 16, + "2" + ], + [ + 18, + 17, + "4" + ], + [ + 19, + 17, + "2" + ], + [ + 20, + 17, + "-2" + ], + [ + 21, + 17, + "-2" + ], + [ + 22, + 17, + "-2" + ], + [ + 23, + 17, + "-2" + ], + [ + 24, + 17, + "-2" + ], + [ + 25, + 17, + "-2" + ], + [ + 26, + 17, + "-2" + ], + [ + 27, + 17, + "-2" + ], + [ + 28, + 17, + "-2" + ], + [ + 29, + 17, + "-2" + ], + [ + 30, + 17, + "-2" + ], + [ + 31, + 17, + "-2" + ], + [ + 32, + 17, + "-2" + ], + [ + 33, + 17, + "-2" + ], + [ + 34, + 17, + "-2" + ], + [ + 35, + 17, + "-2" + ] + ], + "pins": { + "lead/RESULT.json": "ab74c834d4b94c63cda667338055889667e8e7a98c022ba6ed23afa35ff0acfe", + "lead/dependency.py": "82959a8be9c332698e402fc963e0c3af8dfac6522128100851dd96c767e162d5", + "lead/inputs/CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "lead/inputs/forward.py": "75d94780f9db49a4b08bb0e7fb4bd7fc04adb8cabbf73d83a809179c04c3d439" + }, + "plane_preserving_length": null, + "planes": [], + "rank": 19, + "runner_cap_seconds": 20, + "target_columns": [ + [ + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "3", + "2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1" + ] + ] +} diff --git a/research/p104-signed-factor-circuit-gauge/closure/round209/lead/plane_gate.py b/research/p104-signed-factor-circuit-gauge/closure/round209/lead/plane_gate.py new file mode 100644 index 0000000000..d5aff02a6a --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/round209/lead/plane_gate.py @@ -0,0 +1,67 @@ +"""One full-J1 extension of the lexicographic Type A circuit.""" +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from runpy import run_path +from signal import SIGALRM, alarm, signal + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PINS = { + "lead/RESULT.json": "ab74c834d4b94c63cda667338055889667e8e7a98c022ba6ed23afa35ff0acfe", + "lead/dependency.py": "82959a8be9c332698e402fc963e0c3af8dfac6522128100851dd96c767e162d5", + "lead/inputs/CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "lead/inputs/forward.py": "75d94780f9db49a4b08bb0e7fb4bd7fc04adb8cabbf73d83a809179c04c3d439", +} + + +def stop(*_): + raise TimeoutError("20-second one-case plane gate") + + +def main(): + assert __debug__ + signal(SIGALRM, stop) + alarm(20) + for name, digest in PINS.items(): + assert sha256((ROOT / name).read_bytes()).hexdigest() == digest + lead = run_path(str(ROOT / "lead/dependency.py")) + source = run_path(str(ROOT / "lead/inputs/forward.py")) + unit, apply = source["unit"], source["apply"] + old = loads((ROOT / "lead/RESULT.json").read_bytes()) + tape = loads((ROOT / "lead/inputs/CALLER.json").read_bytes())["events"] + factors, keys = lead["source_factors"](unit, apply, tape) + assert keys == old["factor_keys"] and keys[0][0] == keys[1][0] == 43 + assert 1 not in old["chosen"] + chosen = sorted(old["chosen"] + [1]) + units = [unit(i) for i in range(36)] + assert all(lead["product"](factors, e) == [-x for x in e] for e in units) + cols, piv = lead["target"](chosen, factors, lead["suffix_transport"](factors), units) + assert len(chosen) == 20 and len(piv) == 19 + off_block = [[row, col, str(x)] for col, entries in enumerate(cols) + for row, x in enumerate(entries) if x and col // 18 != row // 18] + add, dot, rref = lead["add"], lead["dot"], lead["rref"] + planes = [] + for first in () if off_block else (0, 18): + field = slice(first, first + 18) + block = [col[field] for col in cols[field]] + basis = [e[field] for e in units[field]] + delta = [add(col, e, -1) for col, e in zip(block, basis, strict=True)] + rank = len(rref(zip(*delta, strict=True))[1]) + square = [[dot(row, col) for row in zip(*block, strict=True)] for col in block] + involution = square == basis + planes.append({"roles": list(range(first, first + 18)), "rank": rank, "involution": involution, + "length": rank + int(involution and rank > 0)}) + if not off_block: + assert sum(p["rank"] for p in planes) == len(piv) + alarm(0) + print(dumps({"pins": PINS, "chosen": chosen, "added": 1, "rank": len(piv), "planes": planes, + "fixed_partition_off_block": off_block, + "plane_preserving_length": None if off_block else sum(p["length"] for p in planes), + "case_cap": 1, + "runner_cap_seconds": 20, + "target_columns": [[str(x) for x in col] for col in cols]}, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-signed-factor-circuit-gauge/closure/round210/independent/RESULT.json b/research/p104-signed-factor-circuit-gauge/closure/round210/independent/RESULT.json new file mode 100644 index 0000000000..adac544078 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/round210/independent/RESULT.json @@ -0,0 +1,1562 @@ +{ + "caller": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "changed_body_scale_rejected_basis": 0, + "chosen": [ + 0, + 1, + 2, + 4, + 6, + 8, + 10, + 12, + 14, + 18, + 19, + 20, + 22, + 24, + 26, + 28, + 30, + 32, + 34, + 36 + ], + "displacement_columns": [ + [ + "-2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "-2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "-2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "-2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "-2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "-2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "2", + "2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "-2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ] + ], + "endpoint": { + "-1": [ + "1", + "1", + "1", + "1", + "1", + "1", + "1", + "1", + "1", + "-1", + "-1", + "-1", + "-1", + "-1", + "-1", + "-1", + "-1", + "-1", + "1", + "1", + "1", + "1", + "1", + "1", + "1", + "1", + "1", + "-1", + "-1", + "-1", + "-1", + "-1", + "-1", + "-1", + "-1", + "-1" + ], + "1": [ + "-1", + "-1", + "-1", + "-1", + "-1", + "-1", + "-1", + "-1", + "-1", + "1", + "1", + "1", + "1", + "1", + "1", + "1", + "1", + "1", + "-1", + "-1", + "-1", + "-1", + "-1", + "-1", + "-1", + "-1", + "-1", + "1", + "1", + "1", + "1", + "1", + "1", + "1", + "1", + "1" + ] + }, + "first_unit_target_change": [ + 27, + 1, + "4" + ], + "gauge_negative_roles": [ + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35 + ], + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "minor_cols": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18 + ], + "minor_determinant": "524288", + "minor_rows": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18 + ], + "pins": { + "inputs/7113-SHA256.json": "064e11ecfedce9937ea1782e5baee37e89b3c9eebabed5b4a9ba84f412bbe078", + "inputs/7113-signed-child.py": "ef03444360f02225138be9b38e2f9a85f313eeaa910d63a365de0f16d228cb8b", + "inputs/CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "inputs/R195.json": "f6091c7c63b21145077808bbdacc61431f641d0da37f9fa648aea4b7ead3b472" + }, + "profile": { + "D8": -1, + "other_D": 1, + "signs": [ + 1, + -1 + ] + }, + "rank": 19, + "runner_cap_seconds": 30, + "unit_result_sha256": "3992ba3f17645e834f1d5aed3551d16e07a27e6234b2ef814e3dd87e1b00bb75", + "unit_target_changes": 153, + "untouched_count": 18 +} diff --git a/research/p104-signed-factor-circuit-gauge/closure/round210/independent/replay.py b/research/p104-signed-factor-circuit-gauge/closure/round210/independent/replay.py new file mode 100644 index 0000000000..96452eeb69 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/round210/independent/replay.py @@ -0,0 +1,208 @@ +"""Exact non-unit signed profile from literal sparse prefix applications.""" +from ast import Assign, Name, literal_eval, parse +from fractions import Fraction as F +from hashlib import sha256 +from json import dumps, loads +from math import prod +from pathlib import Path +from signal import SIGALRM, alarm, signal +from sys import argv, implementation, version_info + +N = 36 +CAP = 30 +HEAD = 'aaeec8c0acf01e99a5f331ef363a698d9c084ace' +CALLER = '07a76c5e2738882c0cb322278e56f6cae3c9885d' +CHOSEN = (0, 1, 2, 4, 6, 8, 10, 12, 14, 18, 19, 20, 22, 24, 26, 28, 30, 32, 34, 36) +UNIT_SHA = '3992ba3f17645e834f1d5aed3551d16e07a27e6234b2ef814e3dd87e1b00bb75' +PINS = { + 'inputs/CALLER.json': '255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc', + 'inputs/R195.json': 'f6091c7c63b21145077808bbdacc61431f641d0da37f9fa648aea4b7ead3b472', + 'inputs/7113-SHA256.json': '064e11ecfedce9937ea1782e5baee37e89b3c9eebabed5b4a9ba84f412bbe078', + 'inputs/7113-signed-child.py': 'ef03444360f02225138be9b38e2f9a85f313eeaa910d63a365de0f16d228cb8b', +} + + +def unique(items): + out = dict(items) + assert len(out) == len(items) + return out + + +def pin(root, name): + raw = (root / name).read_bytes() + assert sha256(raw).hexdigest() == PINS[name], name + return raw + + +def steps(caller, sign, omit_one_body=False): + result, labels = [], [] + for clock, event in enumerate(caller['events']): + if event[0] == 'B': + continue + if event[0] == 'J': + _, host, (a, b, c, d), _ = event + assert len({a, b, c, d}) == 4 + alpha = F(caller['types']['A']['alpha2']) + assert alpha == -1 + for leg, (dst, src, coeff) in enumerate(((b, a, 1), (c, d, int(alpha)))): + labels.append(([clock, host, leg, dst, src, coeff], len(result))) + result.append(('add', dst, src, F(sign * coeff))) + if host == 8: + for row in (a, b, c, d): + if not (omit_one_body and row == a): + result.append(('scale', row, row, F(-1))) + continue + assert event[0] == 'A' + _, op, dst, *args = event + if op == 'ADD': + src, coeff = args + result.append(('add', dst, src, F(coeff))) + elif op == 'QUERY': + src, exp = args + assert exp == -1 + labels.append(([clock, 0, 0, dst, src, 1], len(result))) + result.append(('add', dst, src, F(sign))) + elif op == 'SCALE': + result.append(('scale', dst, dst, F(args[0]))) + elif op == 'SWAP': + result.append(('swap', dst, args[0], F(1))) + elif op == 'IDLE_ONE': + if args[0].count(8) % 2: + result.append(('scale', dst, dst, F(-1))) + else: + assert op == 'LAMBDA' and sign * sign == 1 + return result, labels + + +def replay(word, coordinate, inverse=False, pullback=False): + assert not (inverse and pullback) + out = [F(0)] * N + out[coordinate] = F(1) + for op, dst, src, factor in reversed(word) if inverse or pullback else word: + if op == 'add': + if pullback: + dst, src = src, dst + if out[src]: + out[dst] += (-factor if inverse else factor) * out[src] + elif op == 'swap': + out[dst], out[src] = out[src], out[dst] + elif out[dst]: + out[dst] = out[dst] / factor if inverse else out[dst] * factor + return out + + +def dot(u, v): + return sum(a * b for a, b in zip(u, v, strict=True) if a and b) + + +def relative(word, column, inverse=False): + for u, v in reversed(word) if inverse else word: + coefficient = dot(v, column) + if coefficient: + sign = -coefficient if inverse else coefficient + column = [a + sign*b for a, b in zip(column, u, strict=True)] + return column + + +def minor(columns): + pivots, col_ids = [], [] + reduced = [] + for j, column in enumerate(columns): + x = column.copy() + for p, basis in zip(pivots, reduced, strict=True): + if x[p]: + a = x[p] / basis[p] + x = [s - a*t for s, t in zip(x, basis, strict=True)] + pivot = next((i for i, value in enumerate(x) if value), None) + if pivot is not None: + pivots.append(pivot) + col_ids.append(j) + reduced.append(x) + # Operations use earlier selected columns only and leave the determinant + # of the recorded ordered square minor unchanged. The reduced minor is triangular. + return pivots, col_ids, prod(x[p] for p, x in zip(pivots, reduced, strict=True)) + + +def stop(*_): + raise TimeoutError('R210 independent 30-second cap') + + +def main(): + assert __debug__ and implementation.name == 'cpython' and version_info[:2] == (3, 12) + assert len(argv) == 3, 'pass exact #7435 package root and R209 independent RESULT.json' + root = Path(argv[1]).resolve() + signal(SIGALRM, stop) + alarm(CAP) + raw_caller, raw_receipt, raw_manifest, signed_child = (pin(root, path) for path in PINS) + caller, prior, manifest = [loads(x, object_pairs_hook=unique) for x in (raw_caller, raw_receipt, raw_manifest)] + assert manifest['expected/ODD-TYPE-AB-CALLER.json'] == PINS['inputs/CALLER.json'] + assert manifest['replay/supplier7112/short-caller/signed_child.py'] == PINS['inputs/7113-signed-child.py'] + assert (prior['head'], prior['caller']) == (HEAD, CALLER) + unit_raw = Path(argv[2]).read_bytes() + assert sha256(unit_raw).hexdigest() == UNIT_SHA + unit_receipt = loads(unit_raw, object_pairs_hook=unique) + assert tuple(unit_receipt['chosen']) == CHOSEN + binary = next(literal_eval(n.value) for n in parse(signed_child).body + if isinstance(n, Assign) and isinstance(n.targets[0], Name) and n.targets[0].id == 'C') + for sign, twice_eigen in ((1, (2, 0)), (-1, (0, 2))): + for i in range(2): + assert tuple(binary[i][0][k] + sign*binary[i][1][k] for k in range(2)) == tuple(sign**i*x for x in twice_eigen) + assert len(caller['events']) == 4783 and caller['types']['A']['roles'] == N + expected = {sign: [] for sign in (1, -1)} + for q, z, *bits in caller['types']['A']['diagonal']: + assert z == 0 and len(bits) == 17 and all(bit in (0, 1) for bit in bits) + for sign in (1, -1): + expected[sign].append(F(sign) ** q * (-1) ** bits[7]) + signed = {} + for sign in (1, -1): + word, labels = steps(caller, sign) + assert [a for a, _ in labels] == prior['factor_labels'] and len(labels) == 38 + signed[sign] = (word, labels) + for j in range(N): + assert replay(word, j) == [F(i == j) * expected[sign][j] for i in range(N)] + broken, _ = steps(caller, 1, omit_one_body=True) + bad = next(j for j in range(N) if replay(broken, j) != replay(signed[1][0], j)) + neg, labels = signed[-1] + original = [] + for (_, _, _, dst, src, coefficient), cut in labels: + prefix = neg[:cut] + u = [2 * coefficient * x for x in replay(prefix, dst, inverse=True)] + v = replay(prefix, src, pullback=True) + assert not dot(u, v) and any(u) and any(v) + original.append((u, v)) + complement = [f for i, f in enumerate(original) if i not in CHOSEN] + assert len(complement) == 18 + columns = [] + for j in range(N): + unit = [F(i == j) for i in range(N)] + assert relative(original, unit) == [-x for x in unit] + inverse = relative(complement, unit, inverse=True) + assert relative(complement, inverse) == unit + columns.append([-x - y for x, y in zip(inverse, unit, strict=True)]) + rows, cols, determinant = minor(columns) + unit_target = [[F(x) for x in col] for col in unit_receipt['target_columns']] + flipped_roles = [i for i in range(N) if i % 18 >= 9] + diag = [(-1 if i in flipped_roles else 1) for i in range(N)] + changes = [] + for j, col in enumerate(columns): + for i, value in enumerate(col): + target = value + int(i == j) + before = unit_target[j][i] + assert target == diag[i] * before * diag[j] + if target != before: + changes.append([i, j, str(target - before)]) + assert len(changes) == 153 and changes[0] == [27, 1, '4'] + alarm(0) + assert len(rows) == 19 and determinant == 524288 + assert determinant and len(rows) == len(cols) + print(dumps({'head': HEAD, 'caller': CALLER, 'pins': PINS, 'profile': {'D8': -1, 'other_D': 1, 'signs': [1, -1]}, + 'chosen': CHOSEN, 'untouched_count': 18, 'endpoint': {s: list(map(str, d)) for s, d in expected.items()}, + 'unit_result_sha256': UNIT_SHA, 'gauge_negative_roles': flipped_roles, + 'unit_target_changes': len(changes), 'first_unit_target_change': changes[0], + 'changed_body_scale_rejected_basis': bad, 'rank': len(rows), 'minor_rows': rows, + 'minor_cols': cols, 'minor_determinant': str(determinant), 'runner_cap_seconds': CAP, + 'displacement_columns': [list(map(str, c)) for c in columns]}, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/p104-signed-factor-circuit-gauge/closure/round210/lead/RESULT.json b/research/p104-signed-factor-circuit-gauge/closure/round210/lead/RESULT.json new file mode 100644 index 0000000000..bfb7fb29d2 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/round210/lead/RESULT.json @@ -0,0 +1,2538 @@ +{ + "case": [ + 0, + 1, + 2, + 4, + 6, + 8, + 10, + 12, + 14, + 18, + 19, + 20, + 22, + 24, + 26, + 28, + 30, + 32, + 34, + 36 + ], + "case_cap": 1, + "changed_entries": [ + [ + 27, + 1, + "-2", + "2" + ], + [ + 28, + 1, + "-2", + "2" + ], + [ + 29, + 1, + "-2", + "2" + ], + [ + 30, + 1, + "-2", + "2" + ], + [ + 31, + 1, + "-2", + "2" + ], + [ + 32, + 1, + "-2", + "2" + ], + [ + 33, + 1, + "-2", + "2" + ], + [ + 34, + 1, + "-2", + "2" + ], + [ + 35, + 1, + "-2", + "2" + ], + [ + 27, + 2, + "2", + "-2" + ], + [ + 28, + 2, + "2", + "-2" + ], + [ + 29, + 2, + "2", + "-2" + ], + [ + 30, + 2, + "2", + "-2" + ], + [ + 31, + 2, + "2", + "-2" + ], + [ + 32, + 2, + "2", + "-2" + ], + [ + 33, + 2, + "2", + "-2" + ], + [ + 34, + 2, + "2", + "-2" + ], + [ + 35, + 2, + "2", + "-2" + ], + [ + 27, + 3, + "-2", + "2" + ], + [ + 28, + 3, + "-2", + "2" + ], + [ + 29, + 3, + "-2", + "2" + ], + [ + 30, + 3, + "-2", + "2" + ], + [ + 31, + 3, + "-2", + "2" + ], + [ + 32, + 3, + "-2", + "2" + ], + [ + 33, + 3, + "-2", + "2" + ], + [ + 34, + 3, + "-2", + "2" + ], + [ + 35, + 3, + "-2", + "2" + ], + [ + 27, + 4, + "2", + "-2" + ], + [ + 28, + 4, + "2", + "-2" + ], + [ + 29, + 4, + "2", + "-2" + ], + [ + 30, + 4, + "2", + "-2" + ], + [ + 31, + 4, + "2", + "-2" + ], + [ + 32, + 4, + "2", + "-2" + ], + [ + 33, + 4, + "2", + "-2" + ], + [ + 34, + 4, + "2", + "-2" + ], + [ + 35, + 4, + "2", + "-2" + ], + [ + 27, + 5, + "-2", + "2" + ], + [ + 28, + 5, + "-2", + "2" + ], + [ + 29, + 5, + "-2", + "2" + ], + [ + 30, + 5, + "-2", + "2" + ], + [ + 31, + 5, + "-2", + "2" + ], + [ + 32, + 5, + "-2", + "2" + ], + [ + 33, + 5, + "-2", + "2" + ], + [ + 34, + 5, + "-2", + "2" + ], + [ + 35, + 5, + "-2", + "2" + ], + [ + 27, + 6, + "2", + "-2" + ], + [ + 28, + 6, + "2", + "-2" + ], + [ + 29, + 6, + "2", + "-2" + ], + [ + 30, + 6, + "2", + "-2" + ], + [ + 31, + 6, + "2", + "-2" + ], + [ + 32, + 6, + "2", + "-2" + ], + [ + 33, + 6, + "2", + "-2" + ], + [ + 34, + 6, + "2", + "-2" + ], + [ + 35, + 6, + "2", + "-2" + ], + [ + 27, + 7, + "-2", + "2" + ], + [ + 28, + 7, + "-2", + "2" + ], + [ + 29, + 7, + "-2", + "2" + ], + [ + 30, + 7, + "-2", + "2" + ], + [ + 31, + 7, + "-2", + "2" + ], + [ + 32, + 7, + "-2", + "2" + ], + [ + 33, + 7, + "-2", + "2" + ], + [ + 34, + 7, + "-2", + "2" + ], + [ + 35, + 7, + "-2", + "2" + ], + [ + 27, + 8, + "2", + "-2" + ], + [ + 28, + 8, + "2", + "-2" + ], + [ + 29, + 8, + "2", + "-2" + ], + [ + 30, + 8, + "2", + "-2" + ], + [ + 31, + 8, + "2", + "-2" + ], + [ + 32, + 8, + "2", + "-2" + ], + [ + 33, + 8, + "2", + "-2" + ], + [ + 34, + 8, + "2", + "-2" + ], + [ + 35, + 8, + "2", + "-2" + ], + [ + 18, + 9, + "4", + "-4" + ], + [ + 19, + 9, + "2", + "-2" + ], + [ + 20, + 9, + "-2", + "2" + ], + [ + 21, + 9, + "-2", + "2" + ], + [ + 22, + 9, + "-2", + "2" + ], + [ + 23, + 9, + "-2", + "2" + ], + [ + 24, + 9, + "-2", + "2" + ], + [ + 25, + 9, + "-2", + "2" + ], + [ + 26, + 9, + "-2", + "2" + ], + [ + 18, + 10, + "-4", + "4" + ], + [ + 19, + 10, + "-2", + "2" + ], + [ + 20, + 10, + "2", + "-2" + ], + [ + 21, + 10, + "2", + "-2" + ], + [ + 22, + 10, + "2", + "-2" + ], + [ + 23, + 10, + "2", + "-2" + ], + [ + 24, + 10, + "2", + "-2" + ], + [ + 25, + 10, + "2", + "-2" + ], + [ + 26, + 10, + "2", + "-2" + ], + [ + 18, + 11, + "4", + "-4" + ], + [ + 19, + 11, + "2", + "-2" + ], + [ + 20, + 11, + "-2", + "2" + ], + [ + 21, + 11, + "-2", + "2" + ], + [ + 22, + 11, + "-2", + "2" + ], + [ + 23, + 11, + "-2", + "2" + ], + [ + 24, + 11, + "-2", + "2" + ], + [ + 25, + 11, + "-2", + "2" + ], + [ + 26, + 11, + "-2", + "2" + ], + [ + 18, + 12, + "-4", + "4" + ], + [ + 19, + 12, + "-2", + "2" + ], + [ + 20, + 12, + "2", + "-2" + ], + [ + 21, + 12, + "2", + "-2" + ], + [ + 22, + 12, + "2", + "-2" + ], + [ + 23, + 12, + "2", + "-2" + ], + [ + 24, + 12, + "2", + "-2" + ], + [ + 25, + 12, + "2", + "-2" + ], + [ + 26, + 12, + "2", + "-2" + ], + [ + 18, + 13, + "4", + "-4" + ], + [ + 19, + 13, + "2", + "-2" + ], + [ + 20, + 13, + "-2", + "2" + ], + [ + 21, + 13, + "-2", + "2" + ], + [ + 22, + 13, + "-2", + "2" + ], + [ + 23, + 13, + "-2", + "2" + ], + [ + 24, + 13, + "-2", + "2" + ], + [ + 25, + 13, + "-2", + "2" + ], + [ + 26, + 13, + "-2", + "2" + ], + [ + 18, + 14, + "-4", + "4" + ], + [ + 19, + 14, + "-2", + "2" + ], + [ + 20, + 14, + "2", + "-2" + ], + [ + 21, + 14, + "2", + "-2" + ], + [ + 22, + 14, + "2", + "-2" + ], + [ + 23, + 14, + "2", + "-2" + ], + [ + 24, + 14, + "2", + "-2" + ], + [ + 25, + 14, + "2", + "-2" + ], + [ + 26, + 14, + "2", + "-2" + ], + [ + 18, + 15, + "4", + "-4" + ], + [ + 19, + 15, + "2", + "-2" + ], + [ + 20, + 15, + "-2", + "2" + ], + [ + 21, + 15, + "-2", + "2" + ], + [ + 22, + 15, + "-2", + "2" + ], + [ + 23, + 15, + "-2", + "2" + ], + [ + 24, + 15, + "-2", + "2" + ], + [ + 25, + 15, + "-2", + "2" + ], + [ + 26, + 15, + "-2", + "2" + ], + [ + 18, + 16, + "-4", + "4" + ], + [ + 19, + 16, + "-2", + "2" + ], + [ + 20, + 16, + "2", + "-2" + ], + [ + 21, + 16, + "2", + "-2" + ], + [ + 22, + 16, + "2", + "-2" + ], + [ + 23, + 16, + "2", + "-2" + ], + [ + 24, + 16, + "2", + "-2" + ], + [ + 25, + 16, + "2", + "-2" + ], + [ + 26, + 16, + "2", + "-2" + ], + [ + 18, + 17, + "4", + "-4" + ], + [ + 19, + 17, + "2", + "-2" + ], + [ + 20, + 17, + "-2", + "2" + ], + [ + 21, + 17, + "-2", + "2" + ], + [ + 22, + 17, + "-2", + "2" + ], + [ + 23, + 17, + "-2", + "2" + ], + [ + 24, + 17, + "-2", + "2" + ], + [ + 25, + 17, + "-2", + "2" + ], + [ + 26, + 17, + "-2", + "2" + ] + ], + "factor_keys": [ + [ + 43, + 0, + 1 + ], + [ + 43, + 18, + 19 + ], + [ + 137, + 0, + 2 + ], + [ + 137, + 18, + 20 + ], + [ + 268, + 0, + 3 + ], + [ + 268, + 18, + 21 + ], + [ + 432, + 0, + 4 + ], + [ + 432, + 18, + 22 + ], + [ + 633, + 0, + 5 + ], + [ + 633, + 18, + 23 + ], + [ + 867, + 0, + 6 + ], + [ + 867, + 18, + 24 + ], + [ + 1138, + 0, + 7 + ], + [ + 1138, + 18, + 25 + ], + [ + 1423, + 0, + 8 + ], + [ + 1423, + 18, + 26 + ], + [ + 1516, + 0, + 1 + ], + [ + 1580, + 0, + 1 + ], + [ + 1659, + 0, + 1 + ], + [ + 1721, + 0, + 1 + ], + [ + 3058, + 0, + 9 + ], + [ + 3058, + 18, + 27 + ], + [ + 3377, + 0, + 10 + ], + [ + 3377, + 18, + 28 + ], + [ + 3674, + 0, + 11 + ], + [ + 3674, + 18, + 29 + ], + [ + 3934, + 0, + 12 + ], + [ + 3934, + 18, + 30 + ], + [ + 4149, + 0, + 13 + ], + [ + 4149, + 18, + 31 + ], + [ + 4337, + 0, + 14 + ], + [ + 4337, + 18, + 32 + ], + [ + 4485, + 0, + 15 + ], + [ + 4485, + 18, + 33 + ], + [ + 4606, + 0, + 16 + ], + [ + 4606, + 18, + 34 + ], + [ + 4691, + 0, + 17 + ], + [ + 4691, + 18, + 35 + ] + ], + "mutant_basis": 0, + "nonunit_stage": 8, + "pins": { + "lead/dependency.py": "82959a8be9c332698e402fc963e0c3af8dfac6522128100851dd96c767e162d5", + "lead/inputs/CALLER.json": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "lead/inputs/forward.py": "75d94780f9db49a4b08bb0e7fb4bd7fc04adb8cabbf73d83a809179c04c3d439", + "round209/lead/RESULT.json": "7f72ff06f411cf86ebed076ed004660e7ffb04fc9ef317efb1f4a2a5525e1884" + }, + "pivots": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18 + ], + "rank": 19, + "runner_cap_seconds": 30, + "target_columns": [ + [ + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "0", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "0", + "4", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "-4", + "-2", + "2", + "2", + "2", + "2", + "2", + "2", + "2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2", + "-2" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "3", + "2", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-2", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1" + ] + ] +} diff --git a/research/p104-signed-factor-circuit-gauge/closure/round210/lead/body_gate.py b/research/p104-signed-factor-circuit-gauge/closure/round210/lead/body_gate.py new file mode 100644 index 0000000000..b174cd93f0 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/closure/round210/lead/body_gate.py @@ -0,0 +1,74 @@ +"""Expand the one nonunit stage into exact sign scales at its literal body contacts.""" +import hashlib +import json +from pathlib import Path +import runpy +import signal + +ROOT = Path(__file__).resolve().parents[2] +PINS = { + 'lead/dependency.py': '82959a8be9c332698e402fc963e0c3af8dfac6522128100851dd96c767e162d5', + 'lead/inputs/forward.py': '75d94780f9db49a4b08bb0e7fb4bd7fc04adb8cabbf73d83a809179c04c3d439', + 'lead/inputs/CALLER.json': '255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc', + 'round209/lead/RESULT.json': '7f72ff06f411cf86ebed076ed004660e7ffb04fc9ef317efb1f4a2a5525e1884', +} + + +def expand(events, skip_host_body=False): + for event in events: + yield event + if event[:2] == ['J', 8] and not skip_host_body: + for role in event[2]: + yield ['A', 'SCALE', role, '-1'] + elif event[:2] == ['A', 'IDLE_ONE'] and 8 in event[3]: + yield ['A', 'SCALE', event[2], '-1'] + + +def stop(*_): + raise TimeoutError('30-second one-profile body gate') + + +def main(): + assert __debug__ + signal.signal(signal.SIGALRM, stop) + signal.alarm(30) + for name, digest in PINS.items(): + assert hashlib.sha256((ROOT / name).read_bytes()).hexdigest() == digest + lead = runpy.run_path(str(ROOT / 'lead/dependency.py')) + source = runpy.run_path(str(ROOT / 'lead/inputs/forward.py')) + unit, apply = source['unit'], source['apply'] + caller = json.loads((ROOT / 'lead/inputs/CALLER.json').read_bytes()) + a = caller['types']['A'] + tape = caller['events'] + old = json.loads((ROOT / 'round209/lead/RESULT.json').read_bytes()) + case = old['chosen'] + assert a['alpha2'] == '-1' and len(case) == 20 and case[:2] == [0, 1] + + def evaluate(events, col, q, inverse=False): + return apply(list(expand(events)), col, q, inverse) + + units = [unit(i) for i in range(36)] + factors, keys = lead['source_factors'](unit, evaluate, tape) + for i, col in enumerate(units): + exponents = a['diagonal'][i] + assert exponents[:2] == [-1, 0] and len(exponents) == 19 + for q in (1, -1): + expected = [x * q * (-1) ** exponents[9] for x in col] + assert evaluate(tape, col, q) == expected + assert evaluate(tape, expected, q, inverse=True) == col + assert lead['product'](factors, col) == [-x for x in col] + cols, pivots = lead['target'](case, factors, lead['suffix_transport'](factors), units) + cols = [[str(x) for x in col] for col in cols] + changes = [[i, j, old_entry, new_entry] for j, (a, b) in enumerate(zip(old['target_columns'], cols, strict=True)) + for i, (old_entry, new_entry) in enumerate(zip(a, b, strict=True)) if old_entry != new_entry] + mutant = list(expand(tape, skip_host_body=True)) + mutant_basis = next(i for i, col in enumerate(units) if apply(mutant, col, 1) != evaluate(tape, col, 1)) + signal.alarm(0) + print(json.dumps({'pins': PINS, 'case': case, 'factor_keys': keys, 'nonunit_stage': 8, + 'rank': len(pivots), 'pivots': pivots, 'target_columns': cols, + 'changed_entries': changes, 'mutant_basis': mutant_basis, 'case_cap': 1, + 'runner_cap_seconds': 30}, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/p104-signed-factor-circuit-gauge/replay.py b/research/p104-signed-factor-circuit-gauge/replay.py new file mode 100644 index 0000000000..a1e44d8b30 --- /dev/null +++ b/research/p104-signed-factor-circuit-gauge/replay.py @@ -0,0 +1,134 @@ +"""Replay the pinned signed-factor scope and check the actual D8-gauged witness.""" +from fractions import Fraction as Q +from hashlib import sha256 +from json import loads +from pathlib import Path +from subprocess import run +from sys import executable, implementation, version_info + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE / 'closure' + + +def check_pins(): + pins = {} + for line in (PACKAGE / 'PINS.txt').read_text().splitlines(): + digest, path = line.split() + assert path not in pins and sha256((PACKAGE / path).read_bytes()).hexdigest() == digest, path + pins[path] = digest + assert set(pins) == {f.relative_to(PACKAGE).as_posix() for f in ROOT.rglob('*') if f.is_file()} + + +def checked(script, expected, args=(), timeout=30, isolated=True): + flags = ['-I', '-B'] if isolated else ['-E', '-B'] + proc = run([executable, *flags, str(ROOT / script), *map(str, args)], + capture_output=True, check=True, timeout=timeout) + assert not proc.stderr, script + actual = loads(proc.stdout) + stored = loads((ROOT / expected).read_bytes()) + if 'seconds' in actual: + assert 0 <= actual.pop('seconds') < 60 + assert 0 <= stored.pop('seconds') < 60 + else: + assert proc.stdout == (ROOT / expected).read_bytes(), script + assert actual == stored, script + return actual + + +def matrix(columns): + return [[Q(x) for x in c] for c in columns] + + +def unit(size, j): + return [Q(i == j) for i in range(size)] + + +def dot(left, right): + return sum(a*b for a,b in zip(left, right, strict=True) if a and b) + + +def apply(factors, column): + for image, covector in reversed(factors): + assert any(image) and any(covector) and dot(image, covector) == 0 + val = dot(covector, column) + column = [x + val * y for x, y in zip(column, image, strict=True)] + return column + + +def compare_profiles(unit_target, literal, independent, witness): + size = 36 + flipped = [*range(9, 18), *range(27, 36)] + assert independent['gauge_negative_roles'] == flipped + e = [(-1 if i in flipped else 1) for i in range(size)] + target = matrix(literal['target_columns']) + assert len(target) == size + assert literal['rank'] == independent['rank'] == witness['rank'] == 19 + assert independent['minor_determinant'] == '524288' + assert len(literal['changed_entries']) == independent['unit_target_changes'] == 153 + assert independent['first_unit_target_change'] == [27, 1, '4'] + assert literal['mutant_basis'] == independent['changed_body_scale_rejected_basis'] == 0 + for j, d in enumerate(matrix(independent['displacement_columns'])): + assert [x+u for x,u in zip(d, unit(size,j), strict=True)] == target[j] + factors = [(list(map(Q, u)), list(map(Q, v))) for u, v in witness['factors']] + assert len(factors) == 19 + gauged = [([s*x for s,x in zip(e,u,strict=True)], [s*x for s,x in zip(e,v,strict=True)]) for u,v in factors] + assert target != unit_target + for j in range(size): + assert apply(factors, unit(size,j)) == unit_target[j] + assert apply(gauged, unit(size,j)) == target[j] + assert [e[i]*value*e[j] for i,value in enumerate(unit_target[j])] == target[j] + assert apply(factors, unit(size,1)) != target[1] + + +def price(): + low, high = map(Q, loads((ROOT/'lead/inputs/R194.json').read_bytes())['price']) + assert Q('50.33412118538') < low < high < Q('50.33412118539') + paid = 16 + 19 - 2 + assert paid == 33 + all_direct_upper = 17*(high+96)-paid*96 + assert all_direct_upper == Q('-1700799849621348281604535419004036353191280335045953/2500000000000000000000000000000000000000000000000') + assert all_direct_upper < Q('-680.3199') + + +def main(): + assert __debug__ and implementation.name == 'cpython' and version_info[:2] == (3,12) + check_pins() + lead208 = checked('lead/dependency.py','lead/RESULT.json') + ind208 = checked('independent/replay.py','independent/RESULT.json',(ROOT/'lead',)) + assert lead208['minimum_support'] == len(ind208['least_support']) == 19 + assert lead208['chosen'] == ind208['least_support'] and ind208['literal_rank'] == 18 + frozen208 = ROOT/'lead/RESULT.json' + short208 = checked('construct/run.py','construct/RESULT.json', + (frozen208,sha256(frozen208.read_bytes()).hexdigest()),timeout=62,isolated=False) + assert short208['rank'] == 18 and short208['involution'] and short208['minimum_transvections'] == 19 + lead209 = checked('round209/lead/plane_gate.py','round209/lead/RESULT.json') + ind209 = checked('round209/independent/replay.py','round209/independent/RESULT.json', + (ROOT/'independent/replay.py', ROOT/'lead')) + assert lead209['target_columns'] == ind209['target_columns'] + assert lead209['rank'] == ind209['displacement_rank'] == 19 + unit_target = matrix(lead209['target_columns']) + for j,col in enumerate(unit_target): + assert col[:18] == [Q(-1 if i == j else 0) for i in range(18)] + if j >= 18: + diagonal = unit(36,j)[18:] + if j in (18,19): + diagonal[0] += 2 if j==18 else -2 + diagonal[1] += 2 if j==18 else -2 + assert col[18:] == diagonal + assert sum(bool(x) for c in unit_target[:18] for x in c[18:]) == 306 + assert ind209['blocks'][2]['displacement_rank'] == 1 + frozen209 = ROOT/'round209/lead/RESULT.json' + short209 = checked('round209/construction/run.py','round209/construction/RESULT.json', + (frozen209,sha256(frozen209.read_bytes()).hexdigest()),timeout=62) + assert short209['minimum_transvections'] == short209['cross_plane_factors'] == 19 + assert short209['nondyadic_factors'] == 0 + lead210 = checked('round210/lead/body_gate.py','round210/lead/RESULT.json',timeout=35) + ind210 = checked('round210/independent/replay.py','round210/independent/RESULT.json', + (ROOT/'lead',ROOT/'round209/independent/RESULT.json'),timeout=35) + compare_profiles(unit_target, lead210, ind210, short209) + price() + print('PASS_SIGNED_FACTOR_CIRCUITS: minimum 19, 20-to-19 witness, 19 crossings, exact D8 gauge and negative direct-host price') + + +if __name__ == '__main__': + main()