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-idle-child-volume-bound/AUDIT.json b/research/p104-idle-child-volume-bound/AUDIT.json new file mode 100644 index 0000000000..ea48b90227 --- /dev/null +++ b/research/p104-idle-child-volume-bound/AUDIT.json @@ -0,0 +1,170 @@ +{ + "controls": { + "duplicate_axis_rejected": true, + "exhaustive_small_signed_patterns": 126, + "spectator_translation_checked": true, + "wrong_sign_detected": true + }, + "even_translation_defect_lower": "12750684159/8589934592", + "fixed_pairs_checked": 1, + "identity_bypass_minus_i_requirement": "33/64", + "maximum_rank73_displacement_fraction": "206158430209/274877906944", + "minimum_volume_translation": "408021893088/206158430209", + "minimum_volume_two_parity_scalars": "266287972320/206158430209", + "old_roles": [ + 68, + 36 + ], + "phase_multiplicities": { + "9": [ + 136, + 120, + 120, + 136 + ], + "64": [ + 4611686020574871552, + 4611686018427387904, + 4611686016279904256, + 4611686018427387904 + ], + "73": [ + 2361183241469182345216, + 2361183241400462868480, + 2361183241400462868480, + 2361183241469182345216 + ] + }, + "physical_site_tests": 0, + "port_layouts": [ + { + "central": 81, + "port": 15, + "rank": [ + 9, + 64, + 73 + ] + }, + { + "central": 273, + "port": 17, + "rank": [ + 9, + 64, + 73 + ] + }, + { + "central": 262, + "port": 27, + "rank": [ + 9, + 64, + 73 + ] + }, + { + "central": 98, + "port": 34, + "rank": [ + 9, + 64, + 73 + ] + }, + { + "central": 290, + "port": 35, + "rank": [ + 9, + 64, + 73 + ] + }, + { + "central": 268, + "port": 42, + "rank": [ + 9, + 64, + 73 + ] + }, + { + "central": 164, + "port": 47, + "rank": [ + 9, + 64, + 73 + ] + }, + { + "central": 280, + "port": 55, + "rank": [ + 9, + 64, + 73 + ] + } + ], + "quotes": { + "moonshot": { + "affordable_volume_upper": "8694420563333237576161521658465600983001612376437/11480888644886462271324450403755400395535817125548", + "k": "10018846261809/2500000000000000", + "old_margin": [ + "-35046259140897474942389472864147556348879828607881/250000000000000000000000000000000000000000000000", + "-70092518281794949884778945728295112697759657187079/500000000000000000000000000000000000000000000000" + ], + "optimistic_unit_volume_margin": [ + "-34830851019415308689536609316122492656677559378243/250000000000000000000000000000000000000000000000", + "-2786468081553224695162928745289799412534204749111/20000000000000000000000000000000000000000000000" + ], + "required_volume_margin_upper": "-1264794462764898851594058193916408350295579021854349888246027/4123168604180000000000000000000000000000000000000000000000" + }, + "old_crossing_upper": { + "affordable_volume_upper": "575721211650496238728823700100967452120809427074579/574936375783233515579855785604479852905719019943760", + "k": "91141748217473298207420876011401/25000000000000000000000000000000000", + "old_margin": [ + "-1002247197758299781/500000000000000000000000000000000000000000000000", + "-2004494395516543389/1000000000000000000000000000000000000000000000000" + ], + "optimistic_unit_volume_margin": [ + "392417933631361574483957248243799607545203537299/500000000000000000000000000000000000000000000000", + "784835867262723148967914496487599215090407130819/1000000000000000000000000000000000000000000000000" + ], + "required_volume_margin_upper": "-34408860488437058184631722532707140807127338644337621027166189/206158430209000000000000000000000000000000000000000000000000" + }, + "trial": { + "affordable_volume_upper": "575007606199184157246671021211010854884686158501099/574931861488676214810193693630614004446146632349360", + "k": "1459/400000", + "old_margin": [ + "-354740019024486253707723531092675176862662827421/500000000000000000000000000000000000000000000000", + "-709480038048972507415447062185350353725325598877/1000000000000000000000000000000000000000000000000" + ], + "optimistic_unit_volume_margin": [ + "37872355253971218238663790198425219269763047859/500000000000000000000000000000000000000000000000", + "75744710507942436477327580396850438539526151739/1000000000000000000000000000000000000000000000000" + ], + "required_volume_margin_upper": "-34554774165724023048342923019434562331473853215490462008415509/206158430209000000000000000000000000000000000000000000000000" + } + }, + "site": [ + 1339, + 2324 + ], + "source_head": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "source_pins": { + "inputs/CALLER.json.gz": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "inputs/INVOICE-7277.json.gz": "42fc7d18689c9d4e04e0e6d893682bdd4fd9ce42eba6acee46755844c75ec1d1", + "inputs/TYPE-B-PORTS.json": "b51a161bf3bfaf3a6b3572056ad4f858781bb66007df2793357f0bfa6f796c53", + "inputs/check_odd_physical_binding.py.gz": "5c80c3b0415a7f91d216395248dd6f13297eed637732098e1ca8fb0548951b98", + "inputs/upstream_application.py.gz": "d98987db98553dc55bfc80e3ca47abfcd51c57af6f8cda61101391d8eae94184" + }, + "status": "PASS_SCOPED_ONE_CHILD_DISPLACEMENT_AND_VOLUME_EXCLUSION", + "two_parity_scalar_defect_lower": "8321499135/8589934592", + "twofold_carrier_max_one_root_capacity": "68719476737/137438953472", + "volume_price_linear": true +} diff --git a/research/p104-idle-child-volume-bound/NOTICE b/research/p104-idle-child-volume-bound/NOTICE new file mode 100644 index 0000000000..9162f44d41 --- /dev/null +++ b/research/p104-idle-child-volume-bound/NOTICE @@ -0,0 +1,12 @@ +One-child volume bound for the signed Type-B idle pair, Apache-2.0. + +The literal signed caller and physical binding come from Rohan Arun's +#7113, retaining the #7112 predecessor sources and source-specific +notices. The #7277 invoice comes from Rohan Arun's terminal rechart, +retaining Clear1nsight's #7274/#7244 constructions and all inherited +source-specific notices. PROVENANCE.json records the precise public +paths and exact source-byte digests for both. The eight port masks are +a projection of the exact #7277 native word. + +OpenAI Codex and subagents materially assisted proof, implementation, +independent audit and packaging. diff --git a/research/p104-idle-child-volume-bound/PROOF.md b/research/p104-idle-child-volume-bound/PROOF.md new file mode 100644 index 0000000000..9d424ce34c --- /dev/null +++ b/research/p104-idle-child-volume-bound/PROOF.md @@ -0,0 +1,129 @@ +# One-child displacement bound for Type-B idle events 1339 and 2324 + +**NO VERIFIED GAIN.** Exact #7277 benchmark head +ed090b57ed88f8859e5ff4643645099e6ba856ea and #7113 caller. +The test covers this one fixed-contact pair, replicated across the +eight corresponding Type-B ports. Roles 68 and 36 may share boundary +2324 or 2325. Retain their arbitrary-input fields and the signed +adjoint, ownership, restoration, scalar, tape and precision contracts. + +## Literal action + +In the common Fourier character chart of the retained phase-polynomial +physical binding, the two old maps multiply each character by +`i^{p_9(x)}` and `i^{p_{64}(x)}`, respectively. +The first polynomial is minus the port's central bit plus all eight +stage-8 bits. The second is the sum of all bits in stages 9 through +16. An even translation on the central axis converts its positive +coefficient to a negative one. Every port's 73 axes are orthonormal, so characters +realize every active bit tuple equally often. All spectator axes are +retained. The proposed rank-73 phase child has one signed central +axis and those 72 stage axes. The proof grants arbitrary ordinary +linear setup and extraction as long as the erased-child program has +one of the stated block-diagonal actions. + +For one field of dimension `d`, one child on carrier dimension `d'`, +and arbitrary linear input setup `A` and extraction `B`, let `C` +act as that child on its carrier and identity everywhere else. The +full intended action is `E=BCA` and the erased-child action is +`E_0=BA`. Then +```text +rank(E - E0) = rank(B(C - I)A) <= rank(C - I). +``` +The bound grants away all setup and routing restrictions and remains +necessary when forward and adjoint, ownership and restoration are +required. In particular it is unaffected by the amount of unaffected +outside storage. With two arbitrary inputs, the wanted map is +`E = D9 direct_sum D64`. + +## Exact spectra and all tensor widths + +For signed independent axes with coefficients `epsilon_j = +/-1`, +the residue multiplicity is +```text +N_k = 2^(r-2) + (1/2) Re(i^(-k) product_j(1 + i^(epsilon_j))). +``` +This follows by the four-root filter. The negative root's product +vanishes. For odd `r` the real and imaginary parts have equal +magnitude `2^{(r-1)/2}`. For even `r` exactly one part is zero, +and the other has magnitude `2^{r/2}`. The four fractions differ +from `1/4` by at most `delta_r = 2^(-(r+3)/2)` for odd `r` or +`2^{-(r+2)/2}` for even `r`. The two residue parity classes +have equal mass. For the literal pair at width one the fractions +come from `N_9=(136,120,120,136)` and +`N_{64}=(2^{62}+2^{31},2^{62},2^{62}-2^{31},2^{62})`. +At every positive integer tensor width `f` the signs repeat +on `rf` independent axes. Since `delta_(rf) <= delta_r` and +`64f` stays even, the same bounds hold uniformly. The +all-width assertion covers repeated phase cores. Other compiler +representations require a separate argument. + +A whole even linear character phase changes active signs, up to +a global fourth root. If its translation has a nonzero spectator +component, conditioning on that spectator balances `k` and `k+2` +and gives four equal masses. Therefore a retained block-diagonal +erased program of independent whole translations and global fourth +roots requires at least `d(3/2-2^{-6}-2^{-33})` displaced dimensions. +This exceeds the capacity of even an arbitrary one-field operator. + +Give the erased program additional freedom. On each field allow +`(aI+bD_r^2)` followed by such a translation, with separate +arbitrary complex `a,b`. Within each original parity class there +is one scalar value to match. The two original parity classes +contribute at most `1/2 + 2 delta_9` and `1/2 + delta_64` agreements +on their respective fields. The second improvement uses the fact +that one residue parity class is exactly balanced for even rank. +Consequently the desired map differs from this relaxed baseline +in at least `d(31/32-2^{-33})` dimensions. The canonical rank-73 +child can displace at most `d'(3/4+2^{-38})`, even under signed +active-axis phases and global fourth roots. The minimum volume +ratios are therefore +```text +d'/d >= 408021893088/206158430209 +or +d'/d >= 266287972320/206158430209. +``` +for the translation or parity-scalar baseline, respectively. +The parity-scalar bound is approximately 1.291666666505181. + +There is a separate width-one check for a doubled carrier and +identity erased action. If setup and extraction are invertible on +the full field state and both programs restore all ancillary fields, +the encoded input subspace is invariant under `C`. To see this, +write `BAJ=JE_0` and `BCAJ=JE` for the zero-scratch embedding `J`. +Then `CAJ=AJE_0^{-1}E`. The wanted `-i` eigenspace of `E` has +dimension `33d/64`. The twofold rank-73 carrier has at most +`2d(1/4+2^{-38})` dimensions at any one nonidentity root, strictly +less. This supplemental spectral bound needs actual full-state +restoration even in the erased run. + +## Price and limits + +The original pinned 17-stage caller has 110,536 paid occurrences, +22,461 productive positions and signed rank surplus 1,424. At fixed +rank-73 debit linear in physical volume `v=d'/d`, one candidate +invoice changes the eight old rank-9 and eight old rank-64 costs to +eight rank-73 costs at volume `v`. Give away all ordinary, +setup, routing, precision, tape and restoration overhead and keep +every other old occurrence. The upper bound for a nonnegative full +raw margin `M` is equivalent to +```text +v <= (w_9^+ + w_64^+ + M_old^+/8) / w_73^-. +``` +Directed powers give 1.001365082990607 at the incumbent crossing +upper, 1.000131745543397 at the 0.0036475 probe, and 0.757295086840312 +at the fixed moonshot. At the relaxed parity-scalar minimum carrier +size the incumbent directed upper raw margin is approximately +−166.904940310003. The exact rational value is in AUDIT.json. +The unit-volume optimistic price would clear the incumbent by about +0.7848358673, so even one additional rank-1 debit kills that quote. + +The equal-width exclusion is algebraic. The larger-volume conclusion +uses the stated volume-linear debit. Changed address permutations, field-mixing erased baselines, +noncanonical operators, other volume tariffs and other caller pairs +remain open. The scoped mathematical and price tests require only the +retained construction. Credits: #7113 physical signed caller and #7277 complete +invoice, #7166 bounded rectangular support, #7163 no-child rank +method, #1920 reciprocal trace, #1924 clean selectors, #7144 +distinct same-field gauge, and the R30 fixed-contact window bound. +OpenAI Codex materially assisted. diff --git a/research/p104-idle-child-volume-bound/PROVENANCE.json b/research/p104-idle-child-volume-bound/PROVENANCE.json new file mode 100644 index 0000000000..24151a08a5 --- /dev/null +++ b/research/p104-idle-child-volume-bound/PROVENANCE.json @@ -0,0 +1,44 @@ +{ + "bundled": { + "inputs/CALLER.json.gz": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "path": "research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json", + "git_blob": "9451ceaf6e8e037894680b549f3ef41c21b260d7", + "sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/expected/ODD-TYPE-AB-CALLER.json" + }, + "inputs/INVOICE-7277.json.gz": { + "commit": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "path": "research/p104-terminal-cut-rechart/RESULT.json", + "git_blob": "fc0ddfb979177a0791ffa60d94c1d0f50ee59872", + "sha256": "42fc7d18689c9d4e04e0e6d893682bdd4fd9ce42eba6acee46755844c75ec1d1", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/RESULT.json" + }, + "inputs/check_odd_physical_binding.py.gz": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "path": "research/signed-caller-8x9/replay/supplier7112/short-caller/check_odd_physical_binding.py", + "git_blob": "def1e6a18439bd40d1b12af04c6347bbf6b74c55", + "sha256": "5c80c3b0415a7f91d216395248dd6f13297eed637732098e1ca8fb0548951b98", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/replay/supplier7112/short-caller/check_odd_physical_binding.py" + }, + "inputs/upstream_application.py.gz": { + "commit": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "path": "research/signed-caller-8x9/replay/supplier7112/short-caller/upstream_application.py", + "git_blob": "1a6d358cbec88e70615e5314cdfca9e123124f83", + "sha256": "d98987db98553dc55bfc80e3ca47abfcd51c57af6f8cda61101391d8eae94184", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/07a76c5e2738882c0cb322278e56f6cae3c9885d/research/signed-caller-8x9/replay/supplier7112/short-caller/upstream_application.py" + } + }, + "word_reference": { + "commit": "ed090b57ed88f8859e5ff4643645099e6ba856ea", + "path": "research/p104-terminal-cut-rechart/WORD.json.gz", + "git_blob": "077bf48c35db0ddafae81f1bfa0ffacc30894b2b", + "sha256": "2c523ce6fdd6092d758fedc3602a0bcedb692b9766f1e41f903351ba4dee1756", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/WORD.json.gz" + }, + "port_projection": { + "path": "inputs/TYPE-B-PORTS.json", + "source": "word_reference, ports[port] for each Type-B port in the pinned literal caller", + "sha256": "b51a161bf3bfaf3a6b3572056ad4f858781bb66007df2793357f0bfa6f796c53" + } +} diff --git a/research/p104-idle-child-volume-bound/README.md b/research/p104-idle-child-volume-bound/README.md new file mode 100644 index 0000000000..665886cdd9 --- /dev/null +++ b/research/p104-idle-child-volume-bound/README.md @@ -0,0 +1,100 @@ +# One-child volume bound for a signed Type-B idle pair + +The fixed Type-B idle events 1339 and 2324 of #7113 have signed ranks +9 and 64 on each of their eight corresponding ports. A canonical +rank-73 child with arbitrary linear setup and extraction needs volume +at least `266287972320/206158430209` times one field under the relaxed +parity-scalar erased-child contract. The complete #7277 invoice can +afford at most approximately 1.001365082990607 times one field at the +incumbent crossing upper. The directed raw margin upper is +approximately −166.904940310003. **NO VERIFIED GAIN.** Conditional κ +change is 0%. + +## Scope and evidence + +The proof computes exact signed phase multiplicities and bounds the +displacement rank when the child is erased. It treats both an independent +translation on each field and the larger class that also allows two +arbitrary parity scalars per field. The closed multiplicity formula +applies at every positive integer tensor width of the repeated phase +cores. A supplementary invariant-subspace argument rules out a twofold +carrier at width one under reversible setup, identity erased action and +full-state restoration in both runs. + +The exact volume price grants free incremental setup, routing, ordinary +work, precision, tape and restoration. The rest of the complete signed +caller remains charged. The scope is one fixed caller pair, repeated on +eight corresponding ports. All eight signed layouts and three directed +price probes are covered. [Written proof](PROOF.md) [Exact receipt](AUDIT.json) + +## Replay + +From a clean checkout with CPython 3.12 and assertions enabled: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-idle-child-volume-bound +``` + +The standalone replay also works without Git or network from a verified +package export: + +```sh +python3.12 -I -B research/p104-idle-child-volume-bound/verify.py +``` + +It authenticates the bundled literal caller, frozen complete invoice and +two inherited physical binding files by their Git blob IDs and +uncompressed SHA-256 hashes. It reconstructs the pair windows, checks the +bundled eight-port projection, verifies all eight layouts, tests five +tensor widths per signed rank, checks 126 small signed patterns, and +reprices the complete histogram with directed rational bounds. The +width-uniform conclusion uses the written phase identity. The full +predecessor physical and compiler replays are separate. + +To regenerate and authenticate the port projection directly against +the exact public native word, run this from the checkout or export root: + +```sh +( +set -e +word=$(mktemp) +trap 'rm -f "$word"' EXIT +curl -fsSL https://raw.githubusercontent.com/CrocSwap/integer-mult-bounds/ed090b57ed88f8859e5ff4643645099e6ba856ea/research/p104-terminal-cut-rechart/WORD.json.gz -o "$word" +python3.12 -I -B research/p104-idle-child-volume-bound/verify.py --word "$word" +) +``` + +The same receipt is expected. Both forms check immutable inputs, and +the optional command additionally reproduces the projection from the +whole original word. [Source manifest](PROVENANCE.json) + +## Open next questions + +Can a field-mixing erased-child map reduce the displacement for these two +signed fields? First find or exclude one exact candidate under the same +affordable carrier and signed phase contract. A survivor needs arbitrary-input +forward and adjoint verification, restored ownership, precision, tape and a +fully charged invoice. Another canonical pair or a different rank or volume +tariff has a separate price test. + +## Credit + +#7113 supplies the literal caller and signed physical binding. #7277 and +#7274/#7244 supply the complete comparable invoice and retained native +construction. #7166 supplies the related rectangular-adapter argument, +#7163 the no-child rank method for BIT reflections, and #1920/#1924 the +related reciprocal and clean-invariant Clifford encoding contracts. +#7144 proves the related fixed-caller gauge obstruction and #7295 bounds +the complete fixed-contact rank-additive stock. This proof adds a volume +lower bound for one exact complex pair and compares it with the signed +incumbent price. [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) +[#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277) +[#7166](https://github.com/CrocSwap/integer-mult-bounds/pull/7166) +[#7163](https://github.com/CrocSwap/integer-mult-bounds/pull/7163) +[#1920](https://github.com/CrocSwap/integer-mult-bounds/pull/1920) +[#1924](https://github.com/CrocSwap/integer-mult-bounds/pull/1924) +[#7144](https://github.com/CrocSwap/integer-mult-bounds/pull/7144) +[#7295](https://github.com/CrocSwap/integer-mult-bounds/pull/7295) + +OpenAI Codex and subagents materially assisted the proof, implementation, +independent audit and packaging. Apache-2.0. [Notice](NOTICE) diff --git a/research/p104-idle-child-volume-bound/SOURCES.json b/research/p104-idle-child-volume-bound/SOURCES.json new file mode 100644 index 0000000000..5335fa97d9 --- /dev/null +++ b/research/p104-idle-child-volume-bound/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/p104-idle-child-volume-bound/TASK.json b/research/p104-idle-child-volume-bound/TASK.json new file mode 100644 index 0000000000..0dbe5e405f --- /dev/null +++ b/research/p104-idle-child-volume-bound/TASK.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "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" + ], + "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." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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." + }, + "first_experiment": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "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." + ], + "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." + ], + "overlap_terms": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "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.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Literal Type-B signed IDLE events 1339 and 2324 on the #7113 caller. One canonical rank-73 child on all eight ports with block-diagonal translation or parity-scalar erased-child baselines and a volume-linear tariff.", + "scope_change_reason": "Test the exact operator and volume needed by one concrete distinct-field idle pair, keeping the rest of the #7277 caller and native invoice fixed.", + "bottleneck_link": "The optimistic equal-volume price clears the incumbent crossing by only about 0.784836 raw units; actual parity-scalar displacement needs larger volume.", + "budget_minutes": 4, + "stop_rule": "One literal pair across eight ports. Verify the phase identities and full directed price. Stop when the minimum volume exceeds the incumbent affordability upper.", + "outcome": "negative-result", + "evidence": "PROOF.md, exact input source manifest, AUDIT.json, source-bound eight-port projection and clean replay of the complete directed budget and spectral controls.", + "author": "Round 32 research campaign", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent audit and packaging.", + "open_questions": [ + { + "question": "Can a field-mixing erased-child map lower the two-field displacement?", + "why_it_matters": "The two blocked erased-child classes keep fields separate.", + "first_step": "For these exact two signed phases, exhibit or exclude one erased-child matrix with a rank defect within the affordable canonical carrier bound.", + "blocked_by": "A favorable defect would still need exact forward and adjoint action, returned ownership, restoration, precision, tape and charged routing." + } + ] +} diff --git a/research/p104-idle-child-volume-bound/VERIFY.json b/research/p104-idle-child-volume-bound/VERIFY.json new file mode 100644 index 0000000000..f08dcf781a --- /dev/null +++ b/research/p104-idle-child-volume-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Verify the eight literal Type-B port layouts, signed residue identities, scope controls and complete directed one-child price." + } + ] +} diff --git a/research/p104-idle-child-volume-bound/contact.py b/research/p104-idle-child-volume-bound/contact.py new file mode 100644 index 0000000000..155a170cce --- /dev/null +++ b/research/p104-idle-child-volume-bound/contact.py @@ -0,0 +1,46 @@ +"""Trace unchanged caller contacts through logical SWAPs.""" +from bisect import bisect_left, bisect_right +from collections import defaultdict + + +def backward(caller): + events = caller["events"] + # Name each lineage by its final slot, then translate names to initial slots. + lineage = list(range(caller["roles"])) + contacts = defaultdict(list) + idle = [] + for clock in range(len(events)-1,-1,-1): + e = events[clock] + if e[0] == "J": + roles = (*e[2],*e[3][:2]) + else: + ty,op,a,*args = e + match op: + case "SWAP": + b = args[0] + lineage[a],lineage[b] = lineage[b],lineage[a] + continue + case "IDLE_ONE" | "IDLE_ODD": + idle.append((clock,ty,op,a,lineage[a],args[0])) + continue + case "ADD" | "QUERY": + roles = (a,args[0]) + case "LAMBDA" | "SCALE": + roles = (a,) + case _: + raise ValueError(f"unknown caller contact {op}") + for slot in roles: + contacts[lineage[slot]].append(clock) + + initial_name = {token:slot for slot,token in enumerate(lineage)} + result = [] + for clock,ty,op,slot,token,stages in reversed(idle): + hits = [-1,*reversed(contacts[token]),len(events)] + p,q = bisect_left(hits,clock),bisect_right(hits,clock) + assert p==q + result.append({"clock":clock,"kind":ty,"slot":slot, + "role":initial_name[token],"op":op, + "rank":8*len(stages)+int(op=="IDLE_ODD"), + "ports":len(caller["types"][ty]["ports"]), + "selected_stages":stages,"window":[hits[p-1]+1,hits[q]]}) + return result diff --git a/research/p104-idle-child-volume-bound/inputs/CALLER.json.gz b/research/p104-idle-child-volume-bound/inputs/CALLER.json.gz new file mode 100644 index 0000000000..290ef7c9c5 Binary files /dev/null and b/research/p104-idle-child-volume-bound/inputs/CALLER.json.gz differ diff --git a/research/p104-idle-child-volume-bound/inputs/INVOICE-7277.json.gz b/research/p104-idle-child-volume-bound/inputs/INVOICE-7277.json.gz new file mode 100644 index 0000000000..0505fff870 Binary files /dev/null and b/research/p104-idle-child-volume-bound/inputs/INVOICE-7277.json.gz differ diff --git a/research/p104-idle-child-volume-bound/inputs/TYPE-B-PORTS.json b/research/p104-idle-child-volume-bound/inputs/TYPE-B-PORTS.json new file mode 100644 index 0000000000..9e4824f3c4 --- /dev/null +++ b/research/p104-idle-child-volume-bound/inputs/TYPE-B-PORTS.json @@ -0,0 +1,10 @@ +{ + "15": 81, + "17": 273, + "27": 262, + "34": 98, + "35": 290, + "42": 268, + "47": 164, + "55": 280 +} diff --git a/research/p104-idle-child-volume-bound/inputs/check_odd_physical_binding.py.gz b/research/p104-idle-child-volume-bound/inputs/check_odd_physical_binding.py.gz new file mode 100644 index 0000000000..0f473fb46d Binary files /dev/null and b/research/p104-idle-child-volume-bound/inputs/check_odd_physical_binding.py.gz differ diff --git a/research/p104-idle-child-volume-bound/inputs/upstream_application.py.gz b/research/p104-idle-child-volume-bound/inputs/upstream_application.py.gz new file mode 100644 index 0000000000..ab535369b2 Binary files /dev/null and b/research/p104-idle-child-volume-bound/inputs/upstream_application.py.gz differ diff --git a/research/p104-idle-child-volume-bound/pricing.py b/research/p104-idle-child-volume-bound/pricing.py new file mode 100644 index 0000000000..ae43b50a6a --- /dev/null +++ b/research/p104-idle-child-volume-bound/pricing.py @@ -0,0 +1,46 @@ +"""Directed arithmetic for the complete signed price.""" +from fractions import Fraction as F +from functools import cache + +TARGET = F(10018846261809, 2500000000000000) +GRID = 10**48 + + +def round_interval(a, b): + a, b = a*GRID, b*GRID + return F(a.numerator//a.denominator, GRID), F(-((-b.numerator)//b.denominator), GRID) + + +@cache +def log_unit(x): + y = (x-1)/(x+1) + p = sum((2*y**j/j for j in range(1, 111, 2)), F(0)) + return round_interval(p, p+2*y**111/(111*(1-y*y))) + + +@cache +def power(rank, k): + e = rank.bit_length()-1 + lo,hi = [q+e*d for q,d in zip(log_unit(F(rank, 2**e)),log_unit(F(2)),strict=True)] + + def exp_negative(x, n): + term = total = F(1) + assert 0 <= x < 1 + for i in range(1,n+1): + term *= -x/i + total += term + return total + + return round_interval(rank*exp_negative(k*hi, 39), rank*exp_negative(k*lo, 40)) + + +def moment(P, T, k): + lower = upper = F(0) + for r in P.keys()|T.keys(): + n = T[r]-P[r] + lo,hi = power(r,k) + if n < 0: + lo,hi = hi,lo + lower += n*lo + upper += n*hi + return lower,upper diff --git a/research/p104-idle-child-volume-bound/verify.py b/research/p104-idle-child-volume-bound/verify.py new file mode 100644 index 0000000000..a16945ebdb --- /dev/null +++ b/research/p104-idle-child-volume-bound/verify.py @@ -0,0 +1,206 @@ +"""Exact displacement and optimistic volume price for one fixed caller pair.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha1, sha256 +from itertools import product +from pathlib import Path +import gzip +import json +import runpy + +PACKAGE = Path(__file__).resolve().parent +CALLER = "inputs/CALLER.json.gz" +INVOICE = "inputs/INVOICE-7277.json.gz" +PHYSICAL = "inputs/check_odd_physical_binding.py.gz" +APPLICATION = "inputs/upstream_application.py.gz" + + +def authenticate(raw, pin, name): + blob = f"blob {len(raw)}\0".encode() + raw + if sha256(raw).hexdigest() != pin["sha256"] or sha1(blob).hexdigest() != pin["git_blob"]: + raise ValueError(f"Changed source: {name}") + + +def load(word_path): + manifest = json.loads((PACKAGE / "PROVENANCE.json").read_bytes()) + pins = manifest["bundled"] + assert set(pins) == {CALLER, INVOICE, PHYSICAL, APPLICATION} + raw = {} + for name, pin in pins.items(): + source = gzip.decompress((PACKAGE / name).read_bytes()) + authenticate(source, pin, name) + raw[name] = source + projection = manifest["port_projection"] + assert projection["path"] == "inputs/TYPE-B-PORTS.json" + port_bytes = (PACKAGE / projection["path"]).read_bytes() + assert sha256(port_bytes).hexdigest() == projection["sha256"] + ports = json.loads(port_bytes) + if word_path is not None: + native = word_path.read_bytes() + authenticate(native, manifest["word_reference"], "complete #7277 word") + original = json.loads(gzip.decompress(native))["ports"] + assert {p: original[int(p)] for p in ports} == ports + source_hashes = {name: pin["sha256"] for name, pin in pins.items()} + source_hashes[projection["path"]] = projection["sha256"] + return raw, ports, source_hashes + + +UPPER = Q('0.00364566992869893192829683504045604') +TRIAL = Q('0.0036475') +HEAD = 'ed090b57ed88f8859e5ff4643645099e6ba856ea' + + +def counts(signs): + c = [1, 0, 0, 0] + for a in signs: + assert a in (-1, 1) + c = [c[k] + c[(k - a) % 4] for k in range(4)] + return c + + +def imbalance(r): + assert r > 0 + return Q(1, 1 << ((r + 2) // 2 if r % 2 == 0 else (r + 3) // 2)) + + +def audit_counts(signs, got): + r = len(signs) + neg = signs.count(-1) + # Independent product of Gaussian factors and roots-of-unity filter. + re, im = 1, 0 + for j in range(r): + a = -1 if j < neg else 1 + re, im = re-a*im, im+a*re + assert got == [(2**r + 2*v)//4 for v in (re, im, -re, -im)] + assert got[0]+got[2] == got[1]+got[3] == 1 << (r-1) + assert max(abs(Q(v, 2**r) - Q(1, 4)) for v in got) == imbalance(r) + if r % 2: + assert all(got[j] != got[j+2] for j in (0, 1)) + else: + assert sum(got[j] == got[j+2] for j in (0, 1)) == 1 + + +def orthonormal(axes): + return all((a & b).bit_count() % 2 == (i == j) + for i, a in enumerate(axes) for j, b in enumerate(axes)) + + +def controls(): + # Full truth tables for every plus/minus pattern up to rank 6 and a + # spectator translation. The added spectator toggles phase by 2. + cases = 0 + for r in range(1, 7): + for signs in product((-1, 1), repeat=r): + brute = Counter(sum(a*b for a,b in zip(signs,bits,strict=True)) % 4 + for bits in product((0, 1), repeat=r)) + got = counts(signs) + assert got == [brute[k] for k in range(4)] + audit_counts(signs, got) + assert [got[k]+got[(k+2)%4] for k in range(4)] == [2**(r-1)]*4 + cases += 1 + # Ranks alone do not certify signs. A positive central axis permutes + # the two odd multiplicities for the actual rank-9 child. + assert counts((1,)*9) != counts((-1,)+(1,)*8) + assert not orthonormal([1, 2, 2]) + return {'exhaustive_small_signed_patterns':cases, 'wrong_sign_detected':True, + 'duplicate_axis_rejected':True, 'spectator_translation_checked':True} + + +def run(word_path=None): + raw, central_ports, source_hashes = load(word_path) + caller = json.loads(raw[CALLER]) + receipt = json.loads(raw[INVOICE]) + patch = raw[PHYSICAL].decode() + binding = raw[APPLICATION].decode() + assert receipt["caller_sha256"] == source_hashes[CALLER] + assert receipt["checks"]["ODD-PHYSICAL-BINDING.json"]["source_reviewer_sha256"] == source_hashes[APPLICATION] + assert all(s in patch for s in ("len(selected)==1 and a[1:]==[-1]", "signed=sub(pos,terms([(q,2)]))", + "translation(sub(pos,signed))==q")) + assert all(s in binding for s in ("parity(sum x_i)", "v == 2", "rank = 8*len(selected)")) + assert caller['ambient_rank']==145 and receipt['checks']['ODD-FIXED-TAPE-COUNTS.json']['compiler_ambient_cap']==153 + assert caller['events'][1339]==['B','IDLE_ODD',68,[8],-1] + assert caller['events'][2324]==['B','IDLE_ONE',36,[16,15,14,13,12,11,10,9]] + contact = runpy.run_path(str(PACKAGE / 'contact.py')) + timed = {r['clock']:r for r in contact['backward'](caller)} + assert len(timed) == 94 + assert (timed[1339]['role'],timed[2324]['role'])==(68,36) + assert (timed[1339]['window'],timed[2324]['window'])==([0,4783],[2324,2325]) + assert caller['types']['B']['ports']==[15,17,27,34,35,42,47,55] + assert set(central_ports) == set(map(str,caller['types']['B']['ports'])) + axes = {stage:[1 << (9+8*(stage-1)+j) for j in range(8)] for stage in range(8,17)} + layouts = [] + for port in caller['types']['B']['ports']: + first = [central_ports[str(port)],*axes[8]] + second = sum((axes[stage] for stage in range(16,8,-1)),[]) + assert (len(first),len(second))==(9,64) + assert orthonormal(first+second) and max(first+second).bit_length()<=145 + layouts.append({'port':port,'central':first[0], 'rank':[9,64,73]}) + signs = {9:(-1,)+(1,)*8,64:(1,)*64,73:(-1,)+(1,)*72} + residue = {r:counts(s) for r,s in signs.items()} + for r,s in signs.items(): + for f in (1,2,3,4,8): + audit_counts(s*f, counts(s*f)) + assert imbalance(r*f)<=imbalance(r) + assert residue[9]==[136,120,120,136] + assert residue[64]==[2**62+2**31,2**62,2**62-2**31,2**62] + assert residue[73]==[2**71+2**35,2**71-2**35,2**71-2**35,2**71+2**35] + identity_defect = sum(1-Q(residue[r][0],2**r) for r in (9,64)) + translation_defect = Q(3,2)-imbalance(9)-imbalance(64) + parity_bypass_defect = 1-2*imbalance(9)-imbalance(64) + child_capacity = Q(3,4)+imbalance(73) + v_min = translation_defect/child_capacity + v_min_parity = parity_bypass_defect/child_capacity + assert identity_defect==translation_defect>1 + assert 1 < v_min_parity < v_min + # Under clean reversible embeddings a twofold wider canonical + # carrier still lacks enough -i eigenvectors for identity bypass. + target_minus_i = Q(residue[9][3],2**9)+Q(residue[64][3],2**64) + max_twofold_root = 2*(Q(1,4)+imbalance(73)) + assert target_minus_i > max_twofold_root + invoice = receipt['price']['after'] + P,T = (Counter({int(r):n for r,n in invoice[k].items()}) for k in ('P','T')) + assert sum(P.values())==110536 and sum(T.values())==22461 + assert sum(r*(T[r]-P[r]) for r in P.keys()|T.keys())==invoice['S']==1424 + assert P[9]>=8 and P[64]>=8 + assert Q(receipt['price']['price']['independent_raw_bracket'][1])==UPPER + maths = runpy.run_path(str(PACKAGE/'pricing.py')) + quotes = {} + for label,k in (('old_crossing_upper',UPPER), ('trial',TRIAL), ('moonshot',maths['TARGET'])): + cost = {r:maths['power'](r,k) for r in (9,64,73)} + mlo,mhi = maths['moment'](P,T,k) + optimistic = (cost[9][1]+cost[64][1]+mhi/8)/cost[73][0] + one = (mlo+8*(cost[9][0]+cost[64][0]-cost[73][1]), + mhi+8*(cost[9][1]+cost[64][1]-cost[73][0])) + assert optimistic < v_min_parity + assert mhi+8*(cost[9][1]+cost[64][1]-v_min_parity*cost[73][0]) < 0 + assert one[1] < 1 + if label=='old_crossing_upper': + assert mhi<0