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/paired-bit-axis-volume-bound/AXIS.json b/research/paired-bit-axis-volume-bound/AXIS.json new file mode 100644 index 0000000000..a47a990d29 --- /dev/null +++ b/research/paired-bit-axis-volume-bound/AXIS.json @@ -0,0 +1,253 @@ +{ + "all_width_aligned_lower": "sum(V_i*r_i) >= 112V for the exact two-field target", + "build": "REJECTED_AT_PAID_GATE", + "directed_prices_per_original_volume": { + "10018846261809/2500000000000000": { + "complete_old_raw_deficit": [ + "1502597480478683846599820932032388206481822134974419886612337024425207154047163729/25000000000000000000000000000000000000000000000000000000000000000000000000000000", + "1502597480478683846599820932032388206481822134974419886612337024425207154056605593/25000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "credit_per_pair_over_all_222_to_cover_deficit": [ + "1692114279818337665089888436973410142434484386232454827266145297776134182485543/6250000000000000000000000000000000000000000000000000000000000000000000000000000", + "27073828477093402641438214991574562278951750179719277236258324764418146919938873/100000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "literal_four_rank28_tariff": [ + "690714381261616238964014156039427472065187913179644519953631024248342517184105033/6250000000000000000000000000000000000000000000000000000000000000000000000000000", + "138142876252323247792802831207885494413037582635928903990726204849668503436821099/1250000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "literal_split_surcharge": [ + "1916013692119177231182156375980328726341261073584863611290944562547470314177267/6250000000000000000000000000000000000000000000000000000000000000000000000000000", + "1916013692119177231182156375980328726341261073584863611290944562547470314178191/6250000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "old_pair_tariff": [ + "86099795946187132716603999957930892917355831513257457042792509960724380858740913/781250000000000000000000000000000000000000000000000000000000000000000000000000", + "344399183784748530866415999831723571669423326053029828171170039842897523434963883/3125000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "proper_rank_surcharge_lowers_by_cap": { + "49": [ + "1474787304267437577547896359008817738771881040958237305989125274627982029288761/25000000000000000000000000000000000000000000000000000000000000000000000000000000", + "5899149217069750310191585436035270955087524163832949223956501098511928117169989/100000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "55": [ + "795837212828597064838683431429573434082715549623257054557667863786709934077837/100000000000000000000000000000000000000000000000000000000000000000000000000000000", + "7958372128285970648386834314295734340827155496232570545576678637867099340929/1000000000000000000000000000000000000000000000000000000000000000000000000000000" + ] + }, + "rank49_min_reference_minor_rank_fraction_over_222": [ + "149514625143370550839709291328468914906659263699230724974878019732814442194051/50000000000000000000000000000000000000000000000000000000000000000000000000000000", + "149514625143370550839709291328468914906659263699230724974878019732814442194891/50000000000000000000000000000000000000000000000000000000000000000000000000000000" + ] + }, + "1002040748181/250000000000000": { + "complete_old_raw_deficit": [ + "1508649518108296133439099805441247369369954037474358092796307749315623322655221551/25000000000000000000000000000000000000000000000000000000000000000000000000000000", + "754324759054148066719549902720623684684977018737179046398153874657811661332401039/12500000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "credit_per_pair_over_all_222_to_cover_deficit": [ + "6795718550037369970446395520005618780945738907542153571154539411331636588537027/25000000000000000000000000000000000000000000000000000000000000000000000000000000", + "3397859275018684985223197760002809390472869453771076785577269705665818294290099/12500000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "literal_four_rank28_tariff": [ + "690712943940545500556245141820569766787022554811850128712596223267229988396131263/6250000000000000000000000000000000000000000000000000000000000000000000000000000", + "27628517757621820022249805672822790671480902192474005148503848930689199535845269/250000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "literal_split_surcharge": [ + "383261571813893708413390340946479927704146643244200742035405267845434459488301/1250000000000000000000000000000000000000000000000000000000000000000000000000000", + "1916307859069468542066951704732399638520733216221003710177026339227172297442443/6250000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "old_pair_tariff": [ + "344398318040738016007089095057918683574250910797814562501209598464001408049344641/3125000000000000000000000000000000000000000000000000000000000000000000000000000", + "344398318040738016007089095057918683574250910797814562501209598464001408049344879/3125000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "proper_rank_surcharge_lowers_by_cap": { + "49": [ + "1475013471534050227676510271221866804009460774488781862712759682971719126751981/25000000000000000000000000000000000000000000000000000000000000000000000000000000", + "5900053886136200910706041084887467216037843097955127450851038731886876507023093/100000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "55": [ + "795959230412340244978059966921806288034180283498734828847256720175625155615933/100000000000000000000000000000000000000000000000000000000000000000000000000000000", + "198989807603085061244514991730451572008545070874683707211814180043906288907749/25000000000000000000000000000000000000000000000000000000000000000000000000000000" + ] + }, + "rank49_min_reference_minor_rank_fraction_over_222": [ + "30002711062505992906677076606966021045588093507798114813794604799976497353059/10000000000000000000000000000000000000000000000000000000000000000000000000000000", + "150013555312529964533385383034830105227940467538990574068973023999882486766147/50000000000000000000000000000000000000000000000000000000000000000000000000000000" + ] + } + }, + "finite_controls": [ + { + "digit_cardinality": 3, + "exact_basis_columns": 18, + "field_volume_each": 9, + "grades": [ + { + "coordinate": 0, + "cross_minor_size_and_rank": 6, + "grade_swapping_right_matcher_moved_labels": 12, + "nonidentity_grade_preserving_control_columns": 18, + "true_address_changing_reference_rank": 0 + }, + { + "coordinate": 1, + "cross_minor_size_and_rank": 6, + "grade_swapping_right_matcher_moved_labels": 12, + "nonidentity_grade_preserving_control_columns": 18, + "true_address_changing_reference_rank": 0 + } + ], + "missing_split_mutation_failures": 12 + }, + { + "digit_cardinality": 5, + "exact_basis_columns": 50, + "field_volume_each": 25, + "grades": [ + { + "coordinate": 0, + "cross_minor_size_and_rank": 20, + "grade_swapping_right_matcher_moved_labels": 40, + "nonidentity_grade_preserving_control_columns": 50, + "true_address_changing_reference_rank": 0 + }, + { + "coordinate": 1, + "cross_minor_size_and_rank": 20, + "grade_swapping_right_matcher_moved_labels": 40, + "nonidentity_grade_preserving_control_columns": 50, + "true_address_changing_reference_rank": 0 + } + ], + "missing_split_mutation_failures": 40 + }, + { + "digit_cardinality": 9, + "exact_basis_columns": 162, + "field_volume_each": 81, + "grades": [ + { + "coordinate": 0, + "cross_minor_size_and_rank": 72, + "grade_swapping_right_matcher_moved_labels": 144, + "nonidentity_grade_preserving_control_columns": 162, + "true_address_changing_reference_rank": 0 + }, + { + "coordinate": 1, + "cross_minor_size_and_rank": 72, + "grade_swapping_right_matcher_moved_labels": 144, + "nonidentity_grade_preserving_control_columns": 162, + "true_address_changing_reference_rank": 0 + } + ], + "missing_split_mutation_failures": 144 + } + ], + "literal_pair": { + "body_chart": 525, + "body_stages": [ + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9 + ], + "equal_complete_volume_each": "V", + "head_chart": 2, + "intervening_contacts_to_pair": 0, + "old_events": [ + 19, + 24 + ], + "orthogonal_projector_axes": [ + [ + 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 + ], + [ + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63 + ] + ], + "port": 0, + "rank": 56, + "roles": [ + 2, + 21 + ] + }, + "literal_pilot": { + "changed_scalar_operations": 0, + "new_owned_lifetimes": 0, + "new_physical_compiler_or_tape_run": false, + "new_productive_helpers": 0, + "new_spectator_rows": 0, + "paid_profile": { + "28": 4 + }, + "replaced_paid_profile": { + "56": 2 + } + }, + "source_pins": { + "bit/EFREE-CALLER.json.gz": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b", + "bit/EFREE-RESULT.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "bit/independent/interval_gate.py": "8dc2bc4c64cba3f83c664373984a075f1a14b4d53958084091345c8cab189dec", + "bit/retained/inputs/BIT-NATIVE-WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + } +} diff --git a/research/paired-bit-axis-volume-bound/PROOF.md b/research/paired-bit-axis-volume-bound/PROOF.md new file mode 100644 index 0000000000..73ce45b1d4 --- /dev/null +++ b/research/paired-bit-axis-volume-bound/PROOF.md @@ -0,0 +1,33 @@ +# Axis-aligned lower-rank price for two BIT IDLE fields + +## One exact two-field action + +Take zero-based IDLE_ONE events 19 and 24, roles 2 and 21, same port 0 and stage mask [2,3,4,5,6,7,8,9] in the exact [#7001 source](https://github.com/CrocSwap/integer-mult-bounds/tree/e54523517d0f03e58352e647c403a5af3e525a57/research/paired-query-only-bit). No intervening caller event touches either role. The caller prefix is a reversible map on complete fields, so the two fields can be arbitrary and independent. Both use the same ambient 127-dimensional embedding and complete volume V. The pinned native quartet for port 0 uses head chart 2 and body chart 525, the coordinate line and its standard complementary seven axes. Every selected stage contributes seven distinct axes and leaves the head unchanged. + +In sum/difference address coordinates over the odd address ring, where two is invertible, the projector job is identity on the sum bank and sign reversal on the difference image. Set A to stage axes 2–5 and B to stage axes 6–9. Each subset has 28 axes. Their projectors are orthogonal with disjoint support and sum to the old rank-56 projector, so +`D_A D_B = D_B D_A = D_(A+B)` +as exact address permutations, on each field. Conjugating both by the same cover row and allowed external weight retains the identity. Use two rank-28 calls in each of the original logical IDLE slots. The output and reverse actions agree on arbitrary arrays, with no cross-role map, changed scalar operation, new productive helper, or new owned lifetime. The inherited compiler charges every additional paid child. The price exclusion grants the extra ordinary setup, routing and return free. This is a scoped price test on exact address actions. There was no changed compiler, finite-tail proof, physical tape run or full candidate replay. + +At the moonshot κ, two old rank-56 calls cost 110.20773881111953 and the four rank-28 calls cost 110.5143010018586 per original bank volume, for a positive surcharge of approximately 0.3065621907390684 before ordinary work. At the stricter raw trial 0.004008162992724 the surcharge is approximately 0.30660925745111495. Directed endpoints are in [Axis receipt](AXIS.json). + +## Necessary price for the aligned family + +Allow arbitrary rectangular preparation, scalar role/cover mixing, spectators, interleaving and work banks. Assume every action between paid children preserves every tracked coordinate value, with grading measured in the common normalized difference coframe. A paid child of rank r acts as a sign flip on r labeled complete axes, or on a subset of the tracked ones and further untracked axes. All banks have the common digit cardinality s = q^(wf) for each tracked axis, and an active coordinate is uniform over a complete fibre. The child may have any complete volume V_i. Charge the retained V_i H_r tariff, H_r = r^(1−κ). The argument grants setup, restoration, ownership and routing free. + +Fix one of the 56 coordinates. For each child that flips it, replace that child by its original action restricted to coordinate zero and identity off that fibre. The replacement preserves the coordinate everywhere. Its difference from the child has binary rank V_i(1−1/s)/2, counting exactly the nonzero-coordinate transpositions in the linear action on binary data. A child that does not flip the coordinate needs no replacement. The edited external operator therefore preserves this coordinate. The target T consists of two independent full flips. Its cross-grade permutation minor has V(1−1/s) pivots, one from each transposition crossing this coordinate. Choose rows on a fixed half of the nonzero coordinate sign pairs and corresponding columns on the other half. The edited operator has zero on the whole minor, even with arbitrary within-grade mixing. Telescoping the child replacements and using rank subadditivity gives sum V_i ≥ 2V over the children flipping this coordinate. Sum over the 56 coordinates. Each child appears at most r_i times. Thus sum V_i r_i ≥ 112V for all admitted widths. + +For 0<κ and ranks at most R≤56, H_r/r is decreasing, so the charged tariff is at least 112V H_R/R. At R=56 that equals the old tariff, with strict surcharge if any lower rank appears on positive volume. At R=49 the directed surcharge lower per original bank volume is approximately 0.05899149217069750 at the moonshot target and 0.05900053886136201 at the stricter raw trial. At R=55 the corresponding lower bounds are approximately 0.00795837212828597 and 0.00795959230412340. This closes the declared aligned family without a larger build. + +An old right matcher can change g to gS without changing the physical address z. The tracked normalized labels then change from g⁻¹z to S⁻¹g⁻¹z. Arbitrary old matchers or oblique native projectors need not preserve the individual labels. No claim about them follows from this family bound. A closed exact rechart around one already aligned job is a conjugation, with the inverse route returning the tracked coordinate. Transport the grade into the child coordinates when forming the zero-fibre reference. After returning, that reference preserves the original grade and creates zero cross-grade rank. A persistent route or an oblique child that does not implement an aligned returned job needs a new check. + +## Address-changing threshold and next gate + +For an aligned rank-at-most-49 candidate with grade-changing adapters, let H_j be the reference word formed by the same child replacements for coordinate j. In the previous cross-grade minor define d_j as the binary rank of H_j on those selected rows and columns. The same telescope allows at most a reduction of 2 sum d_j/(1−1/s) in the bound on sum V_i r_i. At the strict raw trial, even granting all 222 largest available pairings, an address-changing route must supply at least the exact interval threshold in AXIS.json, approximately 0.30002711062506% of the summed selected-minor ranks to account for the whole current raw deficit, before extra ordinary costs. The threshold applies if the equal-volume pair invoices are separate and allows arbitrary allocation of the required credit among those invoices. Shared children across different pairs require a new global common-grade telescope. It is a necessary rank test, with neither chronological feasibility nor a paid route established. + +The first concrete implementation step for this route is to extract the actual fixed role/cover maps for one IDLE slot at port 0 from the retained compiler binding. Record each right multiplier S and its tariff. Compute the exact change of normalized grades and the selected-minor rank after substituting the zero-coordinate references for one proposed rank-at-most-49 bank. Cap at one two-field action or 12 minutes and stop if there is no qualifying grade-changing map or its optimistic paid price is insufficient. If an exact fixed route is unavailable, test one oblique projector with a finite path list at the same pair, using equality of its rational address-action matrices with the target as the cheapest gate. No such test or build ran. + +## Reproduction and credit + +Use the clean CPython 3.12 registered replay in README.md. The source manifest binds the exact #7001 and #6726 inputs. The verifier tests 230 binary basis columns at odd cardinalities 3, 5 and 9, verifies the unchanged split action and reversal, checks the missing-half mutation and the full-rank minor under a nonidentity grade-preserving reference. A grade-changing reference gives rank zero as a scope control. A changed source byte is rejected. + +Credit #6726/#6834/#6980/#7001 for the word and caller, the delayed-cover bridge for the projector identities, and #673 and #7163 for the reflection defect and cross-address minor. #7188 is a separate mask-incidence obstruction. OpenAI Codex and subagents materially assisted. Apache-2.0. diff --git a/research/paired-bit-axis-volume-bound/README.md b/research/paired-bit-axis-volume-bound/README.md new file mode 100644 index 0000000000..183e3e5066 --- /dev/null +++ b/research/paired-bit-axis-volume-bound/README.md @@ -0,0 +1,25 @@ +# Bound aligned BIT child volume for two rank-56 fields + +**κ change 0%.** The exact #7001 IDLE_ONE events 19 and 24 at port 0 act on two arbitrary independent full-fibre fields. Replacing each rank-56 job by two rank-28 jobs preserves both outputs and reverses exactly. Its paid surcharge is about **0.30656219** per original field volume before ordinary work at κ = **10018846261809/2500000000000000**. + +The [per-axis proof](PROOF.md) also allows arbitrary banks, linear adapters and interleaving. With all intermediate routes preserving each tracked normalized coordinate, a zero-coordinate-fibre substitution forces total paid rank-volume of at least **112V**. Here V is one original field volume. Rank cap 56 already costs the old price, and any use of positive-volume lower ranks increases it. The rank-49 cap has directed surcharge about 0.05899149 even with free routing and restoration. + +[#7163](https://github.com/CrocSwap/integer-mult-bounds/pull/7163) bounds packing rank-one reflections using total address defect. This proof starts from the exact rank-56 pair and applies a separate selected-minor inequality to every tracked coordinate. [#7188](https://github.com/CrocSwap/integer-mult-bounds/pull/7188) addresses a different regrouping of individually charged body masks. Oblique projectors, changed grade routes, and different physical primitives remain separate cases. + +## Clean replay + +From a clean checkout, use CPython 3.12 with assertions: + +~~~sh +python3.12 -B scripts/research_package.py --package research/paired-bit-axis-volume-bound +~~~ + +Four in-tree inputs are authenticated at exact canonical commit e54523517d0f03e58352e647c403a5af3e525a57. The replay matches the directed receipt, checks 230 exact binary basis columns, and rejects a missing split half and a changed caller byte. Grade-preserving and grade-changing reference controls exercise the rank argument. No changed physical compiler, tape, or complete application was run. + +## Open next questions + +Extract the literal fixed role and cover maps for the port-0 pair and check their normalized coordinate action before pricing a changed primitive. A new route must account for the missing cross-grade rank, preserve the complete signed outputs and return, and fit the full paid, ordinary and tape budgets. + +## Credit + +Credit #6726/#6834/#6980/#7001 for the retained native and caller, the delayed-cover bridge for projector and matcher actions, and #673/#7163 for reflection-rank methods. OpenAI Codex and subagents materially assisted. Apache-2.0. diff --git a/research/paired-bit-axis-volume-bound/SOURCES.json b/research/paired-bit-axis-volume-bound/SOURCES.json new file mode 100644 index 0000000000..08ead28e85 --- /dev/null +++ b/research/paired-bit-axis-volume-bound/SOURCES.json @@ -0,0 +1,42 @@ +{ + "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" + }, + { + "path": "research/paired-query-only-bit/EFREE-CALLER.json.gz", + "usage": "input", + "git_blob": "f022272a8d51ede841778dec76e2bfb24b614d04", + "sha256": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b" + }, + { + "path": "research/paired-query-only-bit/EFREE-RESULT.json", + "usage": "input", + "git_blob": "575f76487f9999ecc3e7b1b70f9f71bc582ef8a8", + "sha256": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b" + }, + { + "path": "research/paired-query-only-bit/independent/interval_gate.py", + "usage": "input", + "git_blob": "6d5a751dde7554b2bb3ccb9a958a3508d74ea155", + "sha256": "8dc2bc4c64cba3f83c664373984a075f1a14b4d53958084091345c8cab189dec" + }, + { + "path": "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz", + "usage": "input", + "git_blob": "b718d6b2848215ad785022106dfa9f871a3d1c0c", + "sha256": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + } + ] +} diff --git a/research/paired-bit-axis-volume-bound/TASK.json b/research/paired-bit-axis-volume-bound/TASK.json new file mode 100644 index 0000000000..5162214375 --- /dev/null +++ b/research/paired-bit-axis-volume-bound/TASK.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. 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.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact #7001 IDLE_ONE events 19 and 24 at port 0, two arbitrary independent equal-volume rank-56 fields, and per-axis price for lower-rank aligned replacement words.", + "scope_change_reason": "Test the paid volume of a smaller aligned child primitive for a literal BIT pair, retaining the old endpoint and field contract.", + "bottleneck_link": "Rank deflation cannot remove the BIT raw deficit if lower-rank children must collectively carry the full selected-minor volume.", + "budget_minutes": 60, + "stop_rule": "Check the exact two-field action and full-fibre coordinate rank inequality. Reject the aligned family when its optimistic paid bill exceeds the predecessor. Do not scale an unpriced grade-changing primitive.", + "outcome": "negative-result", + "evidence": "Exact signed-address identity, 230 binary basis columns and grade/minor controls, directed positive tariff surcharge, corrupted source rejection.", + "author": "ToikY", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation and independent review.", + "open_questions": [ + { + "question": "Can a fixed grade-changing matcher or oblique paid child lower the complete two-field price?", + "why_it_matters": "The proved bound requires every nonchild map to preserve each tracked normalized coordinate.", + "first_step": "Extract the fixed role and cover maps for the literal port-0 IDLE pair, measure the changed-reference minor, then price one complete lower-rank action.", + "blocked_by": "A changed physical word, exact returns, compiler/tape and complete application remain open." + } + ] +} diff --git a/research/paired-bit-axis-volume-bound/VERIFY.json b/research/paired-bit-axis-volume-bound/VERIFY.json new file mode 100644 index 0000000000..9c6795bfbb --- /dev/null +++ b/research/paired-bit-axis-volume-bound/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/paired-query-only-bit/EFREE-CALLER.json.gz", + "research/paired-query-only-bit/EFREE-RESULT.json", + "research/paired-query-only-bit/independent/interval_gate.py", + "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Reproduce the exact paired BIT action and directed aligned price with grade-preserving and grade-changing controls." + } + ] +} diff --git a/research/paired-bit-axis-volume-bound/axis_gate.py b/research/paired-bit-axis-volume-bound/axis_gate.py new file mode 100644 index 0000000000..f0e0eafb13 --- /dev/null +++ b/research/paired-bit-axis-volume-bound/axis_gate.py @@ -0,0 +1,182 @@ +"""Price whole-fibre lower-rank, axis-aligned splits at one literal BIT pair.""" + +import argparse +from collections import Counter +from fractions import Fraction +import gzip +from hashlib import sha256 +from importlib.util import module_from_spec, spec_from_file_location +from itertools import product +import json +from pathlib import Path + +PINS = { + 'EFREE-CALLER.json.gz': '757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b', + 'EFREE-RESULT.json': 'a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b', + 'independent/interval_gate.py': '8dc2bc4c64cba3f83c664373984a075f1a14b4d53958084091345c8cab189dec', + 'retained/inputs/BIT-NATIVE-WORD.json.gz': '51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78', +} +TARGET = Fraction('0.0040075385047236') +RAW = Fraction('0.004008162992724') + + +def authenticate(root, key): + path = root / key + raw = path.read_bytes() + if sha256(raw).hexdigest() != PINS[key]: + raise ValueError(f'SHA-256 mismatch: bit/{key}') + return raw + + +def contacts(event): + if event[0] == 'LOCAL': + return event[2:] + if event[0] == 'IDLE_ONE': + return event[1:2] + if event[0] in ('ADD', 'SWAP', 'QUERY'): + return event[1:] + raise ValueError(event[0]) + + +def axes(stages): + return tuple(a for stage in stages for a in range(1 + 7 * (stage - 1), 1 + 7 * stage)) + + +def rank_binary(rows): + basis = {} + for row in rows: + while row: + pivot = row.bit_length() - 1 + if pivot not in basis: + basis[pivot] = row + break + row ^= basis[pivot] + return len(basis) + + +def control(s): + addresses = list(product(range(s), repeat=2)) + states = list(product(range(2), addresses)) + order = {state: i for i, state in enumerate(states)} + + def reflect(state, flip): + role, point = state + return role, tuple((-x if i in flip else x) % s for i, x in enumerate(point)) + + target = {state: reflect(state, {0, 1}) for state in states} + assert all(reflect(reflect(x, {0}), {1}) == target[x] for x in states) + assert all(reflect(target[x], {0, 1}) == x for x in states) + assert sum(reflect(x, {0}) != target[x] for x in states) == 2 * s * (s - 1) + controls = [] + for axis in (0, 1): + edges = [(a, b) for a, b in target.items() if a[1][axis] < b[1][axis]] + edges.sort(key=lambda edge: (edge[0][1][axis], order[edge[0]])) + grade_zero_reference = { + state: target[state] if state[1][axis] == 0 else state + for state in states + } + assert all(grade_zero_reference[x][1][axis] == x[1][axis] for x in states) + assert sum(target[x] != grade_zero_reference[x] for x in states) == 2 * len(edges) + same_grade = { + state: (1 - state[0], reflect(state, {1 - axis})[1]) + for state in states + } + assert all(same_grade[x] != x and same_grade[x][1][axis] == x[1][axis] for x in states) + selected_minor = [ + sum( + ((target[b] == a) ^ (same_grade[b] == a)) << j + for j, (_, b) in enumerate(edges) + ) + for a, _ in edges + ] + assert len(edges) == s * (s - 1) + assert rank_binary(selected_minor) == len(edges) + assert rank_binary([(1 << i) ^ (1 << i) for i in range(len(edges))]) == 0 + swap_grade = sum((p[0] != p[1]) for _, p in states) + controls.append({'coordinate': axis, 'cross_minor_size_and_rank': len(edges), + 'nonidentity_grade_preserving_control_columns': len(states), + 'grade_swapping_right_matcher_moved_labels': swap_grade, + 'true_address_changing_reference_rank': 0}) + return {'digit_cardinality': s, 'field_volume_each': len(addresses), + 'exact_basis_columns': len(states), 'missing_split_mutation_failures': 2 * s * (s - 1), + 'grades': controls} + + +def run(root): + data = {key: authenticate(root, key) for key in PINS} + caller = json.loads(gzip.decompress(data['EFREE-CALLER.json.gz'])) + native = json.loads(gzip.decompress(data['retained/inputs/BIT-NATIVE-WORD.json.gz'])) + invoice = json.loads(data['EFREE-RESULT.json']) + path = root / 'independent/interval_gate.py' + spec = spec_from_file_location('interval_gate', path) + gate = module_from_spec(spec) + spec.loader.exec_module(gate) + + stages = tuple(range(2, 10)) + first, second = 19, 24 + roles = (2, 21) + events = caller['events'] + assert [events[i] for i in (first, second)] == [ + ['IDLE_ONE', role, list(stages)] for role in roles + ] + assert all(not (set(contacts(e)) & set(roles)) for e in events[first + 1:second]) + assert (caller['ambient_rank'], caller['body_rank'], caller['ports']) == (127, 7, 111) + n = caller['ports'] + head, body = native['start'][0], native['final'][n] + assert (head, body) == (2, 525) + frame = native['frames'][str(body)] + unit = [[int(i == j) for i in range(8)] for j in range(8)] + assert native['frames'][str(head)] == {'dim': 1, 'B': unit[:1], 'A': unit[1:]} + assert frame == {'dim': 7, 'B': unit[1:], 'A': unit[:1]} + left, right = axes(stages[:4]), axes(stages[4:]) + assert len(left) == len(right) == 28 and not set(left) & set(right) + assert left + right == axes(stages) + + old = Counter({int(k): v for k, v in invoice['targets'].items()}) + old.subtract({int(k): v for k, v in invoice['paid'].items()}) + pair_stock = sum(e[0] == 'IDLE_ONE' and len(e[2]) == 8 for e in events) * n // 2 + assert pair_stock == 222 + prices = {} + for k in (TARGET, RAW): + h = {r: gate.power(r, k) for r in (28, 49, 55, 56)} + old_pair = gate.smul(h[56], 2) + new_pair = gate.smul(h[28], 4) + surcharge = gate.sub(new_pair, old_pair) + smaller = {r: gate.sub(gate.smul(h[r], Fraction(112, r)), old_pair) for r in (49, 55)} + assert surcharge[0] > 0 and all(x[0] > 0 for x in smaller.values()) + deficit = gate.smul(gate.moment(old, k), -1) + fair_share = gate.smul(deficit, Fraction(1, pair_stock)) + # Fraction of the total selected-minor rank that the modified references + # must cover, allowing every available pair the same optimistic credit. + cap49 = gate.smul(h[49], Fraction(112, 49)) + reference = gate.sub(gate.exact(1), gate.div(gate.sub(old_pair, fair_share), cap49)) + assert deficit[0] > 0 and reference[0] > 0 + prices[str(k)] = {'old_pair_tariff': gate.show(old_pair), 'literal_four_rank28_tariff': gate.show(new_pair), + 'literal_split_surcharge': gate.show(surcharge), + 'proper_rank_surcharge_lowers_by_cap': {r: gate.show(v) for r, v in smaller.items()}, + 'complete_old_raw_deficit': gate.show(deficit), + 'credit_per_pair_over_all_222_to_cover_deficit': gate.show(fair_share), + 'rank49_min_reference_minor_rank_fraction_over_222': gate.show(reference)} + return { + 'source_pins': {f'bit/{key}': val for key, val in PINS.items()}, + 'literal_pair': {'old_events': [first, second], 'roles': roles, 'port': 0, 'rank': 56, + 'head_chart': head, 'body_chart': body, 'body_stages': stages, + 'intervening_contacts_to_pair': 0, 'equal_complete_volume_each': 'V', + 'orthogonal_projector_axes': [left, right]}, + 'literal_pilot': {'paid_profile': {28: 4}, 'replaced_paid_profile': {56: 2}, + 'changed_scalar_operations': 0, 'new_owned_lifetimes': 0, + 'new_productive_helpers': 0, 'new_spectator_rows': 0, + 'new_physical_compiler_or_tape_run': False}, + 'all_width_aligned_lower': 'sum(V_i*r_i) >= 112V for the exact two-field target', + 'directed_prices_per_original_volume': prices, + 'finite_controls': [control(s) for s in (3, 5, 9)], + 'build': 'REJECTED_AT_PAID_GATE', + } + + +if __name__ == '__main__': + if not __debug__: + raise RuntimeError('Run with assertions enabled') + p = argparse.ArgumentParser(description=__doc__) + p.add_argument('--bit-package', type=Path, required=True) + print(json.dumps(run(p.parse_args().bit_package), sort_keys=True, indent=2)) diff --git a/research/paired-bit-axis-volume-bound/verify.py b/research/paired-bit-axis-volume-bound/verify.py new file mode 100644 index 0000000000..53561d4549 --- /dev/null +++ b/research/paired-bit-axis-volume-bound/verify.py @@ -0,0 +1,37 @@ +"""Replay the scoped paired BIT address and paid-volume certificate.""" + +from importlib.util import module_from_spec, spec_from_file_location +import json +from pathlib import Path +from tempfile import TemporaryDirectory + +PACKAGE = Path(__file__).resolve().parent +BIT = PACKAGE.parent / "paired-query-only-bit" + + +def main(): + if not __debug__: + raise RuntimeError("Run with assertions enabled") + spec = spec_from_file_location("axis_gate", PACKAGE / "axis_gate.py") + axis = module_from_spec(spec) + spec.loader.exec_module(axis) + actual = json.dumps(axis.run(BIT), indent=2, sort_keys=True) + "\n" + if actual != (PACKAGE / "AXIS.json").read_text(): + raise ValueError("regenerated axis receipt differs") + + key = "EFREE-CALLER.json.gz" + with TemporaryDirectory() as directory: + mutant = Path(directory) + (mutant / key).write_bytes((BIT / key).read_bytes() + b"\n") + try: + axis.authenticate(mutant, key) + except ValueError as error: + if str(error) != "SHA-256 mismatch: bit/" + key: + raise + else: + raise ValueError("accepted changed caller source") + print("PASS_PAIRED_BIT_AXIS_VOLUME_BOUND rank_mass=112V basis_columns=230 no_new_kappa") + + +if __name__ == "__main__": + main()