From bb36fc65ee0b161229169505f4840c436c5ca2b9 Mon Sep 17 00:00:00 2001 From: Clear1nsight <22630354+Clear1nsight@users.noreply.github.com> Date: Wed, 11 Nov 2026 14:22:27 +1100 Subject: [PATCH 1/3] Reuse #7147 selected replay navigation for onboarding This is the exact documentation prerequisite retained by #7156. It points the onboarding check to the selected #7000/#7001 review. Credit to Rohan Arun and the source authors. --- docs/ci-verification.md | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) 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). From d2e54af81f9dda6487636b79d4964a2385d89b2b Mon Sep 17 00:00:00 2001 From: Clear1nsight <22630354+Clear1nsight@users.noreply.github.com> Date: Wed, 11 Nov 2026 21:53:51 +1100 Subject: [PATCH 2/3] Replay the historical selected check at its inspected commit MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The PR #6292 rejection census and package plan are statements about 2485805. Load its exact sources and planner in a private sparse checkout, keeping all source hashes, 19 expected rejections, nine package selections and the empty-plan control. Subsequent edits to the live Makefile and CI guide no longer invalidate this historical check. The original audit is by unpaidmoon, building on Dennis’s historical replay gate. The pinned repository view follows the precedent of Matarener’s PR #5434. Repair prepared with substantial OpenAI Codex assistance. --- .../historical-selected-replay-gap/README.md | 6 +- .../SOURCES.json | 60 +++++++++--------- .../VERIFY.json | 31 +-------- .../historical-selected-replay-gap/verify.py | 63 ++++++++++++++----- 4 files changed, 82 insertions(+), 78 deletions(-) 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") From d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86 Mon Sep 17 00:00:00 2001 From: Clear1nsight <22630354+Clear1nsight@users.noreply.github.com> Date: Thu, 12 Nov 2026 18:38:50 +1100 Subject: [PATCH 3/3] Route a marked payload fiber from an encoded CRT leaf --- .../encoded-crt-leaf-payload/INPUT-PINS.json | 115 +++++ research/encoded-crt-leaf-payload/README.md | 125 ++++++ research/encoded-crt-leaf-payload/RESULT.json | 98 +++++ .../encoded-crt-leaf-payload/SOURCES.json | 90 ++++ research/encoded-crt-leaf-payload/TASK.json | 83 ++++ research/encoded-crt-leaf-payload/VERIFY.json | 32 ++ .../frozen/endpoint.py | 157 +++++++ .../frozen/frontend.py | 277 +++++++++++++ .../frozen/inverse_frontend.py | 52 +++ .../frozen/inverse_producer.py | 174 ++++++++ research/encoded-crt-leaf-payload/replay.py | 392 ++++++++++++++++++ research/encoded-crt-leaf-payload/route.py | 277 +++++++++++++ 12 files changed, 1872 insertions(+) create mode 100644 research/encoded-crt-leaf-payload/INPUT-PINS.json create mode 100644 research/encoded-crt-leaf-payload/README.md create mode 100644 research/encoded-crt-leaf-payload/RESULT.json create mode 100644 research/encoded-crt-leaf-payload/SOURCES.json create mode 100644 research/encoded-crt-leaf-payload/TASK.json create mode 100644 research/encoded-crt-leaf-payload/VERIFY.json create mode 100644 research/encoded-crt-leaf-payload/frozen/endpoint.py create mode 100644 research/encoded-crt-leaf-payload/frozen/frontend.py create mode 100644 research/encoded-crt-leaf-payload/frozen/inverse_frontend.py create mode 100644 research/encoded-crt-leaf-payload/frozen/inverse_producer.py create mode 100644 research/encoded-crt-leaf-payload/replay.py create mode 100644 research/encoded-crt-leaf-payload/route.py diff --git a/research/encoded-crt-leaf-payload/INPUT-PINS.json b/research/encoded-crt-leaf-payload/INPUT-PINS.json new file mode 100644 index 0000000000..41f6f41c98 --- /dev/null +++ b/research/encoded-crt-leaf-payload/INPUT-PINS.json @@ -0,0 +1,115 @@ +{ + "base": "e54523517d0f03e58352e647c403a5af3e525a57", + "canonical": [ + { + "path": "research/r437-preparation-composition/predecessor4025/source/words.py", + "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9", + "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50", + "bytes": 13794 + }, + { + "path": "research/r437-preparation-composition/predecessor4025/source/records.py", + "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372", + "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3", + "bytes": 9888 + }, + { + "path": "research/encoded-crt-entry-lifecycle/entry.py", + "sha256": "0537ec98f306270c8ff6a424841886cf53f675d9947029347090c7dc779616d7", + "git_blob": "1fa2b0cb88320d4f5b623554bb0fc6de332b773c", + "bytes": 6377 + }, + { + "path": "research/encoded-current-crt/producer.py", + "sha256": "88dab4ca02a92164a67826db361214fa1405e4b4a588f8c4279a21bcee95ab76", + "git_blob": "a327b0161eca57a1cc44ec2aa8e3defed2167ddc", + "bytes": 7891 + }, + { + "path": "research/crt-persistent-numerical-owner/owner.py", + "sha256": "1d73f432f8de9c791260c43335eb207d82bbb3f5b190cc76d0d914a4db076f41", + "git_blob": "20ef3519b6fef691ec92b7315e320b5e8ce9bf18", + "bytes": 2980 + }, + { + "path": "research/crt-mixed-row-entry/bridge.py", + "sha256": "89c38638c0d66da731566c903c32e7fa1ad31088d29cfd2634fce823dd07c1f9", + "git_blob": "57f6853e262a6136bc616f1e47a31d0ace28495c", + "bytes": 3864 + }, + { + "path": "research/crt-current-row-query/join.py", + "sha256": "11c9ac1175a45edae80869b22c041e31a1b5cc75f4389ec2e073de37e547bf35", + "git_blob": "676582b4a376db375237ec52df84a3ddaf231827", + "bytes": 9955 + }, + { + "path": "research/crt-encoded-benes-rom-producer/microcode.py", + "sha256": "d4af5350854a87b67484840800b94e1e53cff82c78ec0f2a91753fed9ea70af7", + "git_blob": "052b01a83bc910c176b83a012b9f46f0e9525b9d", + "bytes": 23823 + }, + { + "path": "research/crt-uniform-rom-query/machine.py", + "sha256": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d", + "git_blob": "88292ce98d31d540c7dba6960bfe4c19f06a8077", + "bytes": 12431 + }, + { + "path": "research/crt-binary-key-port/binary.py", + "sha256": "50a3dea7fc087715b4e605e85629566ed31903026540f916df6b8cbaa536182d", + "git_blob": "ec574f26d6f64ead00d7c2cf5b808c0498b460cf", + "bytes": 5658 + }, + { + "path": "research/crt-binary-radix-consumer/radix.py", + "sha256": "f4200a495d9c445474275214254d46e9a8e03967a635263905a4c9192bb36f1f", + "git_blob": "f558019fe70c46bcb2f087464c1d2aa021b7188d", + "bytes": 4072 + }, + { + "path": "research/crt-paid-row-reentry/RESULT.json", + "sha256": "d818bffac4647dffaf525ed68dbb79dc575a00303af3315c6d4fe39b60f49a13", + "git_blob": "832d3312df223d1b151e5c620cc3d4e295f49e05", + "bytes": 15482 + } + ], + "retained": [ + { + "path": "research/encoded-balanced-crt-inverse/source/research/encoded-balanced-crt-entry/frontend.py", + "sha256": "6ec9aab626a9d7a229b6f13ce6863e1ca77fa30ef65a4a66ae03a6ffaf2ee78c", + "git_blob": "8adbe2cfef74da9854ed0b70b6c221f5746efa9f", + "bytes": 10737, + "file": "frontend.py", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "8c0e55c9ba25ff2c8199b01539a4d56ae71a1473" + }, + { + "path": "research/encoded-balanced-crt-inverse/source/research/encoded-balanced-crt-endpoint/endpoint.py", + "sha256": "c24ae2c90d175d276120438809e7c7401b8a8c04dec139f1b7345e9778984ced", + "git_blob": "b084d893bdb2ce5571ef00196a9ec6a60e723964", + "bytes": 6038, + "file": "endpoint.py", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "8c0e55c9ba25ff2c8199b01539a4d56ae71a1473" + }, + { + "path": "research/encoded-balanced-crt-inverse/inverse_frontend.py", + "sha256": "0e5f4c9450372c90000f5ebf3c22dfbe7241dd53da9ae9bcce310af859b009ef", + "git_blob": "17abfb8500043bcdeb656094bb0213d911d986fc", + "bytes": 2167, + "file": "inverse_frontend.py", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "8c0e55c9ba25ff2c8199b01539a4d56ae71a1473" + }, + { + "path": "research/encoded-balanced-crt-inverse/inverse_producer.py", + "sha256": "6acdebee7134fbc8e2d121060286bd05e7282900da8a28a78c80937dde7ea178", + "git_blob": "46bf6ef4e2dfa53bca17ac668914b1a842eaba9e", + "bytes": 8041, + "file": "inverse_producer.py", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "8c0e55c9ba25ff2c8199b01539a4d56ae71a1473" + } + ] +} diff --git a/research/encoded-crt-leaf-payload/README.md b/research/encoded-crt-leaf-payload/README.md new file mode 100644 index 0000000000..03b23be98a --- /dev/null +++ b/research/encoded-crt-leaf-payload/README.md @@ -0,0 +1,125 @@ +# Route a marked payload from an encoded CRT leaf + +The live encoded CRT leaf now drives the existing Beneš row query and +literal binary radix mover for one padded right-axis fiber. On the +retained non-root fixture, slots 0 and 1 exchange their payloads and +padded slots 2 and 3 preserve theirs. The inverse restores the same +physical payload tape, its keys, the encoded source, and their heads. + +| Boundary | Source coordinates | Payload tags in physical order | +| --- | --- | --- | +| Input | (3, 2, 1, 1) | 293, 730, 905, 3681 | +| Forward | (3, 2, 1, 0) | 730, 293, 905, 3681 | +| Inverse | (3, 2, 1, 1) | 293, 730, 905, 3681 | + +The input uses moduli (5, 7, 3, 2) and declared widths (3, 3, 2, 2) from +the `nonroot_roundtrip` case of [#5625](https://github.com/CrocSwap/integer-mult-bounds/pull/5625). +Each payload is an opaque 12-bit record in the binary radix format. +The replay checks the entire frame, including its two-bit position +keys and its physical backing identity. It also checks the source's +metadata and inaccessible historical tail. + +## Source and payload join + +1. Acquire the retained encoded iterator and its clean private roles. + Select its last leaf at the level with unary half length one, with + a nonempty axis prefix. Retire earlier numerical leases without + writing their coordinates. Both directions pay for every visited + lease, including the skipped leases. +2. While the selected lease is live, scan the actual right record for + its unary width and modulus and copy the offset from the numerical + result stream using the existing precision guide. The measured + fields give width 2, modulus 2, precision 5 and offset 1 in both + directions. The source and result return to their entry heads + with their bytes preserved before source staging. +3. Run the unchanged encoded Beneš producer on those framed headers. + For each physical input slot, follow all produced rows by the + existing row-bit query. The adapter keeps the slot address on a + binary tape, walks the target bit from low to high and back, and + writes the destination as an MSB-first key in the allocated + radix cells. It reads the row tape backwards by rows for the + inverse, keeping the bits of each row in wire order. +4. Run the literal radix pass once per unary width mark. Its stable + last-bit pass rotates that bit to the front, so two passes sort + the two-bit destination keys and return them to their initial + orientation. Each tag moves with its key on the actual bit tape. + Stage the coordinate result, retire the numerical lease, commit + the source and clear the adapter and bucket storage. + +For the selected leaf the left modulus and coordinate are 3 and 1. +The direct CRT oracle solves 3c ≡ 1 modulo 2, giving c = 1. It maps +valid positions x to (x+c) modulo 2 and fixes the two padded positions. +The offset depends on the left child, which is preserved here. The +inverse therefore uses the same offset and the switch layers in reverse +order. Every switch layer is its own inverse, so the reversed layer +product undoes the forward product. The independent oracle checks the +nonidentity forward placement before checking exact restoration. + +The input positions are enumerated by an encoded counter. The adapter +uses the existing key cells for storage and derives its addresses from +physical positions. Fixture serialization and all independent +observers are outside the measured runtime. + +## Measured work and storage + +| Quantity | Forward | Inverse | +| --- | ---: | ---: | +| Encoded source symbol actions, including numerical work | 113,295 | 372,489 | +| Adapter symbol actions | 3,481 | 3,817 | +| Beneš producer instructions | 2,363,816 | 2,363,816 | +| Payload adapter bit actions | 1,694 | 1,694 | +| Literal radix instructions, including finite control | 43,162 | 43,162 | +| Retained private symbol roles | 136 | 136 | +| Retained private symbol cells | 2,253 | 2,633 | +| Retained bucket bit extent | 208 | 208 | +| Retained radix register bits | 144 | 144 | +| Retained Beneš registers | 15 | 15 | + +The symbol counts include header and key-address preparation, row +scans, source staging and retirement. The bit counts include the +physical key writes and bucket initialization and retirement, with +radix instructions counted separately. Both directions' private roles +remain retained for the measurement. They share one 57-cell source +and the original payload tape, whose visited extent is 183 bits. +These are observations in the respective execution models. A common +literal tariff for the combined source controller and payload path +requires further lowering. + +## Replay and source credit + +From a checkout or an official Git-free export with the declared +inputs, run: + +```sh +python3.12 -I -B research/encoded-crt-leaf-payload/replay.py +``` + +[RESULT.json](RESULT.json) records the observed headers, exact +endpoints, cost and backing. The checks include a separate direct CRT +oracle, noncommuting layers that distinguish reverse traversal, a +truncated layer stream that must fail, and suppressed switches that +must fail the forward-placement check. + +[INPUT-PINS.json](INPUT-PINS.json) binds the runtime to canonical main +`e54523517d0f03e58352e647c403a5af3e525a57` and four byte-exact +runtime files from CubeJerry's [#7352](https://github.com/CrocSwap/integer-mult-bounds/pull/7352) +at `8c0e55c9ba25ff2c8199b01539a4d56ae71a1473`. The forward writer +is also byte-identical to the one in [#7351](https://github.com/CrocSwap/integer-mult-bounds/pull/7351). +Ali Romman's [#5625](https://github.com/CrocSwap/integer-mult-bounds/pull/5625) +supplies the fixture and the paid retirement boundary. +JoyboyBrian's [#5092](https://github.com/CrocSwap/integer-mult-bounds/pull/5092), +[#5496](https://github.com/CrocSwap/integer-mult-bounds/pull/5496) +and [#5015](https://github.com/CrocSwap/integer-mult-bounds/pull/5015) +supply the encoded producer, physical row query and literal payload +consumer, respectively. OpenAI Codex and ChatGPT Pro materially assisted +the work. Pro produced a separate witness with the same placement and +restoration using different tags and a different input-key policy. +Apache-2.0. + +## Open next questions + +A complete balanced payload stage must route all right-axis fibers in +order, including idle and padded rows. A concrete next test is to +bind one retained multi-target fixture and check its synchronized +row and header streams. This package establishes one finite fiber. +A full integer product and a combined cost proof remain open. diff --git a/research/encoded-crt-leaf-payload/RESULT.json b/research/encoded-crt-leaf-payload/RESULT.json new file mode 100644 index 0000000000..8503cd80b7 --- /dev/null +++ b/research/encoded-crt-leaf-payload/RESULT.json @@ -0,0 +1,98 @@ +{ + "benes_program_instructions": 10648, + "control_cases": [ + "noncommuting rows distinguish traversal order", + "truncated width-two layer stream rejected", + "suppressed switches fail the forward oracle" + ], + "fixture": "nonroot_roundtrip", + "forward_and_inverse": [ + { + "adapter_symbol_actions": 3481, + "benes_instructions": 2363816, + "direction": "forward", + "encoded_source_symbol_actions": 113295, + "observed_headers": { + "h": "L01000R", + "modulus": "L01000R", + "offsets": "L10000|R", + "selected_layer": "L00000R", + "width": "L11R" + }, + "payload_adapter_bit_actions": 1694, + "radix_bit_control_instructions": 43162, + "radix_passes": 2, + "retained_benes_registers": 15, + "retained_bucket_bits": 208, + "retained_radix_register_bits": 144, + "retained_symbol_cells": 2253, + "retained_symbol_roles": 136, + "selected_nodes": 1, + "skipped_nodes": 1 + }, + { + "adapter_symbol_actions": 3817, + "benes_instructions": 2363816, + "direction": "inverse", + "encoded_source_symbol_actions": 372489, + "observed_headers": { + "h": "L01000R", + "modulus": "L01000R", + "offsets": "L10000|R", + "selected_layer": "L00000R", + "width": "L11R" + }, + "payload_adapter_bit_actions": 1694, + "radix_bit_control_instructions": 43162, + "radix_passes": 2, + "retained_benes_registers": 15, + "retained_bucket_bits": 208, + "retained_radix_register_bits": 144, + "retained_symbol_cells": 2633, + "retained_symbol_roles": 136, + "selected_nodes": 1, + "skipped_nodes": 2 + } + ], + "forward_destinations": [ + 1, + 0, + 2, + 3 + ], + "forward_source": [ + 3, + 2, + 1, + 0 + ], + "forward_tags": [ + 730, + 293, + 905, + 3681 + ], + "input_tags": [ + 293, + 730, + 905, + 3681 + ], + "moduli": [ + 5, + 7, + 3, + 2 + ], + "payload_bits_visited": 183, + "radix_program_instructions": 3885, + "restored_source_and_payload": true, + "source_cells_retained": 57, + "status": "PASS_ENCODED_CRT_LEAF_PAYLOAD", + "widths": [ + 3, + 3, + 2, + 2 + ] +} diff --git a/research/encoded-crt-leaf-payload/SOURCES.json b/research/encoded-crt-leaf-payload/SOURCES.json new file mode 100644 index 0000000000..acfe3ca127 --- /dev/null +++ b/research/encoded-crt-leaf-payload/SOURCES.json @@ -0,0 +1,90 @@ +{ + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50", + "path": "research/r437-preparation-composition/predecessor4025/source/words.py", + "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9", + "usage": "input" + }, + { + "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3", + "path": "research/r437-preparation-composition/predecessor4025/source/records.py", + "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372", + "usage": "input" + }, + { + "git_blob": "1fa2b0cb88320d4f5b623554bb0fc6de332b773c", + "path": "research/encoded-crt-entry-lifecycle/entry.py", + "sha256": "0537ec98f306270c8ff6a424841886cf53f675d9947029347090c7dc779616d7", + "usage": "input" + }, + { + "git_blob": "a327b0161eca57a1cc44ec2aa8e3defed2167ddc", + "path": "research/encoded-current-crt/producer.py", + "sha256": "88dab4ca02a92164a67826db361214fa1405e4b4a588f8c4279a21bcee95ab76", + "usage": "input" + }, + { + "git_blob": "20ef3519b6fef691ec92b7315e320b5e8ce9bf18", + "path": "research/crt-persistent-numerical-owner/owner.py", + "sha256": "1d73f432f8de9c791260c43335eb207d82bbb3f5b190cc76d0d914a4db076f41", + "usage": "input" + }, + { + "git_blob": "57f6853e262a6136bc616f1e47a31d0ace28495c", + "path": "research/crt-mixed-row-entry/bridge.py", + "sha256": "89c38638c0d66da731566c903c32e7fa1ad31088d29cfd2634fce823dd07c1f9", + "usage": "input" + }, + { + "git_blob": "676582b4a376db375237ec52df84a3ddaf231827", + "path": "research/crt-current-row-query/join.py", + "sha256": "11c9ac1175a45edae80869b22c041e31a1b5cc75f4389ec2e073de37e547bf35", + "usage": "input" + }, + { + "git_blob": "052b01a83bc910c176b83a012b9f46f0e9525b9d", + "path": "research/crt-encoded-benes-rom-producer/microcode.py", + "sha256": "d4af5350854a87b67484840800b94e1e53cff82c78ec0f2a91753fed9ea70af7", + "usage": "input" + }, + { + "git_blob": "88292ce98d31d540c7dba6960bfe4c19f06a8077", + "path": "research/crt-uniform-rom-query/machine.py", + "sha256": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d", + "usage": "input" + }, + { + "git_blob": "ec574f26d6f64ead00d7c2cf5b808c0498b460cf", + "path": "research/crt-binary-key-port/binary.py", + "sha256": "50a3dea7fc087715b4e605e85629566ed31903026540f916df6b8cbaa536182d", + "usage": "input" + }, + { + "git_blob": "f558019fe70c46bcb2f087464c1d2aa021b7188d", + "path": "research/crt-binary-radix-consumer/radix.py", + "sha256": "f4200a495d9c445474275214254d46e9a8e03967a635263905a4c9192bb36f1f", + "usage": "input" + }, + { + "git_blob": "832d3312df223d1b151e5c620cc3d4e295f49e05", + "path": "research/crt-paid-row-reentry/RESULT.json", + "sha256": "d818bffac4647dffaf525ed68dbb79dc575a00303af3315c6d4fe39b60f49a13", + "usage": "input" + }, + { + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "path": "certificates/selected-result.json", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1", + "usage": "provenance" + }, + { + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "path": "docs/research/agent-task-catalog.json", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "usage": "provenance" + } + ], + "schema_version": 1 +} diff --git a/research/encoded-crt-leaf-payload/TASK.json b/research/encoded-crt-leaf-payload/TASK.json new file mode 100644 index 0000000000..e64c896a07 --- /dev/null +++ b/research/encoded-crt-leaf-payload/TASK.json @@ -0,0 +1,83 @@ +{ + "actual_scope": "One nonroot mixed-width padded right fiber from #5625, with live #7352 encoded fields, physical four-tag forward placement and inverse restoration, and measured separate source, ROM and radix costs.", + "ai_assistance": "OpenAI Codex and ChatGPT Pro materially assisted formulation, independent audit and replay.", + "author": "Clear1nsight", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Join an actual encoded CRT address-state node to physical payload movement at one admitted leaf boundary.", + "budget_minutes": 60, + "evidence": "Direct CRT oracle, byte-for-byte source and literal payload round trip, exact header receipt, two actual producer calls, four literal radix passes, and three targeted failure/order controls.", + "open_questions": [ + { + "blocked_by": "The current join addresses one fiber. The multi-target layout, compilation bill and integer recovery remain separate obligations.", + "first_step": "Pin one multi-target fixture, then show that the ordered row and header streams deliver every marked record and retire each borrow.", + "question": "Can a mixed-width node with more than one right axis use the same physical payload boundary?", + "why_it_matters": "A complete balanced payload stage needs synchronization across the right-axis fibers." + } + ], + "original_card": { + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal 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." + ], + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "existing_checks": [ + { + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "status": "author-checked" + }, + { + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "status": "reviewed" + } + ], + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "id": "uniform-transfer-audit", + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ] + }, + "outcome": "completed", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Continue the encoded balanced inverse at one released nonroot payload boundary, using the existing physical ROM query and literal radix consumer.", + "scope_status": "refined", + "stop_rule": "Stop at the released nonroot fixture and its one marked right-axis fiber. Charge all actual leases, metadata, tape work and retained backing.", + "task_id": "uniform-transfer-audit" +} diff --git a/research/encoded-crt-leaf-payload/VERIFY.json b/research/encoded-crt-leaf-payload/VERIFY.json new file mode 100644 index 0000000000..498e3a0316 --- /dev/null +++ b/research/encoded-crt-leaf-payload/VERIFY.json @@ -0,0 +1,32 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Replay live encoded node, unchanged ROM and literal radix, independent tagged endpoints, retirement and backing, order and missing-switch controls.", + "timeout_seconds": 70 + } + ], + "inputs": [ + "research/r437-preparation-composition/predecessor4025/source/words.py", + "research/r437-preparation-composition/predecessor4025/source/records.py", + "research/encoded-crt-entry-lifecycle/entry.py", + "research/encoded-current-crt/producer.py", + "research/crt-persistent-numerical-owner/owner.py", + "research/crt-mixed-row-entry/bridge.py", + "research/crt-current-row-query/join.py", + "research/crt-encoded-benes-rom-producer/microcode.py", + "research/crt-uniform-rom-query/machine.py", + "research/crt-binary-key-port/binary.py", + "research/crt-binary-radix-consumer/radix.py", + "research/crt-paid-row-reentry/RESULT.json" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/encoded-crt-leaf-payload/frozen/endpoint.py b/research/encoded-crt-leaf-payload/frozen/endpoint.py new file mode 100644 index 0000000000..b084d893bd --- /dev/null +++ b/research/encoded-crt-leaf-payload/frozen/endpoint.py @@ -0,0 +1,157 @@ +"""Paid whole-node CRT result projection into the actual encoded source. + +Prepared for Jerry Chen / CubeJerry with substantial OpenAI assistance. +Apache-2.0. The fixed predecessor providers are pinned in INPUT-PINS.json. +No coordinate, modulus, width, level or axis count enters host control. +""" + + +class Endpoint: + """One encoded forward balanced address-state traversal, 79 owned roles.""" + + def __init__(self, frontend, words, records, entry, numeric, owner, + canonical, source): + self.w, self.r, self.source = words, records, source + self.iterator = frontend.Iterator(words, records, entry, numeric, + owner, canonical, source) + self.staging = entry.Port(words) + self.staging.retire() + self.pending = False + + def _copy(self, expected): + w = self.w + w.need(self.source.read() == expected, 'preserved source delimiter') + self.staging.append(expected) + self.source.step(1) + + def _field(self, width): + w = self.w + while width.read() == w.ONE: + bit = self.source.read() + w.need(bit in (w.ZERO, w.ONE), 'source padded bit') + self.staging.append(bit) + self.source.step(1) + width.step(1) + w.need(width.read() == w.RIGHT, 'source width extent') + width.rewind() + + def _updated(self, width, result, guide): + w, r = self.w, self.r + w.need(result.read() == r.ROOT, 'whole-node result record') + result.step(1) + while guide.read() == w.ONE: + w.need(result.read() in (w.ZERO, w.ONE), 'offset bit') + result.step(1) + guide.step(1) + w.need(guide.read() == w.BLANK and result.read() == r.WORD_END, + 'whole offset consumed') + result.step(1) + guide.rewind() + while width.read() == w.ONE: + old, new = self.source.read(), result.read() + w.need(old in (w.ZERO, w.ONE) and new in (w.ZERO, w.ONE), + 'current and updated coordinate bits') + w.need(guide.read() == w.ONE, 'updated field covers source width') + self.staging.append(new) + self.source.step(1) + result.step(1) + width.step(1) + guide.step(1) + w.need(width.read() == w.RIGHT, 'updated source width') + width.rewind() + while guide.read() == w.ONE: + w.need(result.read() == w.ZERO, 'updated value fits declared width') + result.step(1) + guide.step(1) + w.need(guide.read() == w.BLANK and result.read() == r.WORD_END, + 'complete updated field') + result.step(1) + guide.rewind() + w.need(result.read() == r.RECORD_END, 'whole-node result end') + result.step(1) + + def _record(self, result=None, guide=None): + w, r = self.w, self.r + width = self.iterator.counters['width'] + self._copy(r.ROOT) + seen = False + while self.source.read() == w.ONE: + seen = True + self.staging.append(w.ONE) + width.append(w.ONE) + self.source.step(1) + w.need(seen, 'positive source width') + self._copy(r.WORD_END) + width.append(w.RIGHT) + width.rewind() + self._field(width) + self._copy(r.WORD_END) + if result is None: + self._field(width) + else: + self._updated(width, result, guide) + self._copy(r.RECORD_END) + width.clear() + + def stage(self, lease): + """Snapshot the next complete source while its numerical lease is live.""" + w, r, it = self.w, self.r, self.iterator + w.need(it.live and not self.pending, 'one live unstaged node result') + self.staging.step(-1) + w.need(self.staging.read() == w.BLANK, 'retired staging origin') + self.staging.write(w.LEFT) + self.staging.step(1) + axis, half = it.counters['axis'], it.counters['half'] + result, guide = lease.actual.result['stream'], lease.actual.guide + while axis.read() != r.STEP: + w.need(axis.read() == w.ONE, 'current node prefix') + self._record() + axis.step(1) + for selected in (False, True): + while half.read() == w.ONE: + w.need(axis.read() in (w.ONE, r.STEP), 'complete current node') + self._record(result if selected else None, guide) + axis.step(1) + half.step(1) + w.need(half.read() == w.RIGHT, 'current node half extent') + half.rewind() + w.need(result.read() == w.RIGHT, 'all right-coordinate results consumed') + while self.source.read() != w.RIGHT: + w.need(axis.read() in (w.ONE, r.VALUE), 'unchanged source suffix') + self._record() + axis.step(1) + w.need(axis.read() == w.RIGHT, 'complete source and cursor extents') + self.staging.append(w.RIGHT) + self.staging.rewind() + self.source.rewind() + axis.rewind() + result.rewind() + self.pending = True + + def commit(self): + """After retirement, overwrite equal-length source and erase the copy.""" + w, it = self.w, self.iterator + w.need(self.pending and not it.live and not it.bank.busy, + 'source update follows numerical retirement') + while self.staging.read() != w.RIGHT: + self.source.write(self.staging.read()) + self.source.step(1) + self.staging.step(1) + w.need(self.source.read() == w.RIGHT, 'preserved full source extent') + self.source.rewind() + self.staging.retire() + self.pending = False + + def step(self): + self.w.need(not self.pending, 'previous staged update must commit') + lease = self.iterator.next() + if lease is None: + return False + self.stage(lease) + lease.close() + self.commit() + return True + + def run(self): + while self.step(): + pass diff --git a/research/encoded-crt-leaf-payload/frozen/frontend.py b/research/encoded-crt-leaf-payload/frozen/frontend.py new file mode 100644 index 0000000000..8adbe2cfef --- /dev/null +++ b/research/encoded-crt-leaf-payload/frozen/frontend.py @@ -0,0 +1,277 @@ +"""Tape-driven balanced-node selection into the unchanged CRT numerical entry. + +No runtime width, axis count, start, level or precision is decoded. All variable +iteration is driven by local symbols on the supplied source or owned unary +tapes. Numeric arithmetic and its 63-role bank are pinned predecessor code. +Prepared for CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from types import SimpleNamespace + + +COUNTERS = ('axis', 'depth', 'halve_a', 'halve_b', 'half', 'double', 'width') +GUARDS = ('g0', 'g1', 'g2', 'g3', 'g4', 'g5', 'g6', 'g7') + + +class Iterator: + """One numerical result at a time; source contents stay read-only. + +The supplied source has the #5353 tagged padded-axis encoding and enters at +head one. Construction charges shape manufacture. next() takes no geometry +arguments. The physical interface is linear-use: consume the current lease +once before the next result and relinquish its borrowed aliases. Historical +Python-handle identity checks are interpreter guards, not a tape service. +""" + def __init__(self, words, records, entry, numeric, owner, canonical, source): + self.w, self.r, self.e = words, records, entry + self.numeric, self.canonical, self.source = numeric, canonical, source + self.bank = owner.Bank(words, entry) + self.guards = tuple(entry.Port(words) for _ in GUARDS) + for port in self.guards: + port.retire() + self.counters = {name: entry.Port(words) for name in COUNTERS} + self.live, self.closed = False, False + try: + self._shape() + except ValueError: + # Source framing errors and nondyadic counts precede numerical entry. + source.rewind() + for port in self.counters.values(): + port.retire() + self.closed = True + raise + + def _record(self, target=None, guide=None): + """Read one exact axis record; optionally project its canonical pair.""" + w, r, source = self.w, self.r, self.source + width = self.counters['width'] + width.clear() + w.need(source.read() == r.ROOT, 'axis tag') + source.step(1) + if target is not None: + target.append(r.ROOT) + seen = False + while source.read() == w.ONE: + seen = True + width.append(w.ONE) + if guide is not None: + guide.append(w.ONE) + source.step(1) + w.need(seen and source.read() == r.WORD_END, 'positive unary width') + source.step(1) + width.append(w.RIGHT) + width.rewind() + for delimiter in (r.WORD_END, r.RECORD_END): + while width.read() == w.ONE: + bit = source.read() + w.need(bit in (w.ZERO, w.ONE), 'padded source bit') + if target is not None: + target.append(bit) + source.step(1) + width.step(1) + w.need(width.read() == w.RIGHT and source.read() == delimiter, + 'exact source field extent') + source.step(1) + width.rewind() + if target is not None: + self.canonical.canonical_end(target, w, r) + if target is not None: + target.append(r.RECORD_END) + width.clear() + + def _many(self, port): + w = self.w + w.need(port.read() == w.ONE, 'nonempty reduction count') + port.step(1) + symbol = port.read() + w.need(symbol in (w.ONE, w.RIGHT), 'unary reduction shape') + port.rewind() + return symbol == w.ONE + + def _shape(self): + w, source = self.w, self.source + axis, depth = self.counters['axis'], self.counters['depth'] + current, spare = self.counters['halve_a'], self.counters['halve_b'] + while source.read() != w.RIGHT: + self._record() + axis.append(w.ONE) + current.append(w.ONE) + source.rewind() + axis.append(w.RIGHT) + axis.rewind() + current.append(w.RIGHT) + current.rewind() + w.need(self._many(current), 'at least two source axes') + while self._many(current): + depth.append(w.ONE) + odd = False + while current.read() == w.ONE: + odd = not odd + if not odd: + spare.append(w.ONE) + current.step(1) + w.need(current.read() == w.RIGHT and not odd, 'dyadic source axis count') + spare.append(w.RIGHT) + spare.rewind() + current.clear() + current, spare = spare, current + current.clear() + spare.clear() + depth.append(w.RIGHT) + depth.rewind() + half = self.counters['half'] + half.append(w.ONE) + half.append(w.RIGHT) + half.rewind() + w.need(axis.read() == w.ONE, 'first axis') + axis.write(self.r.STEP) # Unique current-node marker. + + def _prepare_guards(self, guide): + w = self.w + for port in self.guards: + port.step(-1) + w.need(port.read() == w.BLANK, 'retired protected marker') + port.write(w.LEFT) + port.step(1) + while guide.read() == w.ONE: + w.need(port.read() == w.BLANK, 'retired protected body') + port.write(w.ZERO) + port.step(1) + guide.step(1) + w.need(guide.read() == w.BLANK and port.read() == w.BLANK, + 'current protected extent') + port.write(w.RIGHT) + port.rewind() + guide.rewind() + + def _entry(self, w, r, adapter, numeric, source, dirty, + widths, ell, level, start, row): + # Bank.open's fixed call signature is preserved. Geometry is never supplied. + w.need(widths is None and ell is None and level is None and + start is None and row is None, 'no host geometry arguments') + w.need(source is self.source and dirty is self.guards, 'actual borrowed ports') + return NodeEntry(self, adapter) + + def next(self): + self.w.need(not self.live, 'previous node result must close') + if self.closed: + return None + self.w.need(self.counters['depth'].read() == self.w.ONE, 'active encoded level') + self.live = True + bridge = SimpleNamespace(RowEntry=self._entry) + lease = self.bank.open(self.r, self.numeric, bridge, self.source, self.guards, + None, None, None, None, None) + return NodeLease(self, lease) + + def _double_half(self): + w = self.w + half, temporary = self.counters['half'], self.counters['double'] + while half.read() == w.ONE: + temporary.append(w.ONE) + half.step(1) + w.need(half.read() == w.RIGHT, 'half-size delimiter') + half.write(w.BLANK) + temporary.append(w.RIGHT) + temporary.rewind() + while temporary.read() == w.ONE: + half.append(w.ONE) + temporary.step(1) + w.need(temporary.read() == w.RIGHT, 'copied half size') + half.append(w.RIGHT) + half.rewind() + temporary.clear() + + def _advance(self, last): + w, r = self.w, self.r + axis, depth = self.counters['axis'], self.counters['depth'] + while axis.read() != r.STEP: + w.need(axis.read() == w.ONE, 'preserved current cursor') + axis.step(1) + axis.write(w.ONE) + if last: + while axis.read() != w.RIGHT: + w.need(axis.read() == w.ONE, 'last-node suffix') + axis.step(1) + axis.rewind() + depth.step(1) + if depth.read() == w.RIGHT: + self.close() + return + w.need(depth.read() == w.ONE, 'next encoded level') + self._double_half() + axis.write(r.STEP) + else: + while axis.read() != r.VALUE: + w.need(axis.read() == w.ONE, 'next-node interval') + axis.step(1) + axis.write(r.STEP) + axis.rewind() + + def close(self): + self.w.need(not self.live and not self.closed, 'retired iterator closes once') + for port in self.counters.values(): + port.retire() + self.closed = True + + +class NodeEntry: + """Actual canonical streams and precision guide into unchanged Entry.""" + def __init__(self, iterator, adapter): + self.iterator = iterator + w, r, source = iterator.w, iterator.r, iterator.source + self.guide, self.left, self.right = (adapter.Port(w), adapter.Port(w), adapter.Port(w)) + self.inputs = (self.guide, self.left, self.right) + self.active = True + axis, half = iterator.counters['axis'], iterator.counters['half'] + while axis.read() != r.STEP: + w.need(axis.read() == w.ONE, 'prefix cursor') + iterator._record() + axis.step(1) + for target in (self.left, self.right): + while half.read() == w.ONE: + w.need(axis.read() in (w.ONE, r.STEP), 'complete selected node') + iterator._record(target, self.guide) + axis.step(1) + half.step(1) + w.need(half.read() == w.RIGHT, 'encoded half extent') + half.rewind() + target.append(w.RIGHT) + target.rewind() + self.last = axis.read() == w.RIGHT + if not self.last: + w.need(axis.read() == w.ONE, 'following source axis') + axis.write(r.VALUE) # Pending next cursor; current cursor survives handoff. + axis.rewind() + source.rewind() + self.guide.append(w.ONE) + self.guide.rewind() + iterator._prepare_guards(self.guide) + self.context = adapter.Entry(w, r, self.guide, iterator.guards) + self.result = self.context.invoke(iterator.numeric, self.left, self.right) + + def close(self): + self.context.consume(self.result) + self.context.close() + for port in self.inputs: + port.retire() + for port in self.iterator.guards: + port.retire() + + +class NodeLease: + """Interpreter wrapper for the single current linear-use continuation. + +The closed flag also guards stale Python references, but the fixed-role +physical theorem does not implement an unbounded stale-handle history. +""" + def __init__(self, iterator, lease): + self.iterator, self.lease = iterator, lease + self.actual = lease.actual + self.closed = False + + def close(self): + self.iterator.w.need(not self.closed, 'node lease closes once') + last = self.actual.last + self.lease.close() + self.closed = True + self.iterator.live = False + self.iterator._advance(last) diff --git a/research/encoded-crt-leaf-payload/frozen/inverse_frontend.py b/research/encoded-crt-leaf-payload/frozen/inverse_frontend.py new file mode 100644 index 0000000000..17abfb8500 --- /dev/null +++ b/research/encoded-crt-leaf-payload/frozen/inverse_frontend.py @@ -0,0 +1,52 @@ +"""Encoded descending balanced levels through the existing frontend hook. + +Prepared for Jerry Chen / CubeJerry with substantial OpenAI assistance. +Apache-2.0. See SEAMS.json for the exact inherited interface. +""" +from types import SimpleNamespace + + +def bind(forward): + """Bind one fixed provider; no geometry or numeric value is an argument.""" + class Iterator(forward.Iterator): + def __init__(self, words, records, entry, numeric, owner, canonical, source): + super().__init__(words, records, entry, numeric, owner, canonical, source) + # The inherited shape proof gives k depth tokens and half=1. + # Skip one token, then double once per remaining token: d/2. + depth = self.counters['depth'] + depth.step(1) + while depth.read() == self.w.ONE: + forward.Iterator._double_half(self) + depth.step(1) + self.w.need(depth.read() == self.w.RIGHT, 'complete reverse depth') + depth.rewind() + + def _double_half(self): + """Compatibility hook: the inherited next-level call now halves. + + Startup calls the base doubling method explicitly; every call + through this hook is a descending transition after a level ends. + """ + w = self.w + half = self.counters['half'] + temporary = self.counters['double'] + odd = False + while half.read() == w.ONE: + odd = not odd + if not odd: + temporary.append(w.ONE) + half.step(1) + w.need(half.read() == w.RIGHT and not odd, 'even reverse half size') + temporary.append(w.RIGHT) + temporary.rewind() + w.need(temporary.read() == w.ONE, 'nonempty next reverse half') + half.clear() + while temporary.read() == w.ONE: + half.append(w.ONE) + temporary.step(1) + w.need(temporary.read() == w.RIGHT, 'complete halved size') + half.append(w.RIGHT) + half.rewind() + temporary.clear() + + return SimpleNamespace(Iterator=Iterator) diff --git a/research/encoded-crt-leaf-payload/frozen/inverse_producer.py b/research/encoded-crt-leaf-payload/frozen/inverse_producer.py new file mode 100644 index 0000000000..46bf6ef4e2 --- /dev/null +++ b/research/encoded-crt-leaf-payload/frozen/inverse_producer.py @@ -0,0 +1,174 @@ +# Inverse specialization for CubeJerry with OpenAI assistance. Apache-2.0. +# Exactly one scientific line differs from the pinned #5053 producer. +"""Encoded current-child CRT reconstruction and complete right-node update. + +JoyboyBrian, substantial OpenAI Codex assistance. Apache-2.0. +Only finite symbols/carries and fixed register ownership enter host control. +""" + +class Arithmetic: + """New loose-width residue interface; the frozen Ring guard is unchanged.""" + def __init__(self, arena, words): + self.arena, self.w = arena, words + self.raw = words.Unsigned(arena) + self.one = arena.literal(1) + + def admit(self, modulus): + self.w.need(self.raw.compare(modulus, self.one) > 0, 'CRT modulus exceeds one') + modulus.msb(); high = modulus.read(); modulus.rewind() + self.w.need(high == self.w.ZERO, 'CRT modulus high-bit margin') + + def remainder(self, value, modulus): + quotient, rest = self.raw.divmod(value, modulus) + self.arena.free(quotient) + return rest + + def add(self, left, right, modulus): + total, carry = self.raw.add(left, right) + self.w.need(not carry, 'modular addition margin') + if self.raw.compare(total, modulus) >= 0: + reduced = self.raw.subtract_exact(total, modulus) + self.arena.free(total); total = reduced + return total + + def subtract(self, left, right, modulus): + if self.raw.compare(left, right) >= 0: + return self.raw.subtract_exact(left, right) + larger, carry = self.raw.add(left, modulus) + self.w.need(not carry, 'modular subtraction margin') + result = self.raw.subtract_exact(larger, right) + self.arena.free(larger) + return result + + def multiply(self, left, right, modulus): + scan, result = self.arena.copy(right), self.arena.zero() + scan.msb() + while scan.read() != self.w.LEFT: + doubled = self.add(result, result, modulus) + self.arena.free(result); result = doubled + if scan.read() == self.w.ONE: + added = self.add(result, left, modulus) + self.arena.free(result); result = added + scan.step(-1) + scan.step(1); self.arena.free(scan) + return result + + def inverse(self, value, modulus): + r0, r1 = self.arena.copy(modulus), self.arena.copy(value) + t0, t1 = self.arena.zero(), self.arena.copy(self.one) + while not r1.zero(): + quotient, r2 = self.raw.divmod(r0, r1) + qmod = self.remainder(quotient, modulus) + product = self.multiply(qmod, t1, modulus) + t2 = self.subtract(t0, product, modulus) + self.arena.free_many(quotient, qmod, product, r0, t0) + r0, r1, t0, t1 = r1, r2, t1, t2 + unit = self.raw.compare(r0, self.one) == 0 + self.arena.free_many(r0, r1, t1) + if unit: return t0 + self.arena.free(t0) + return None + + def product(self, left, right): + scan, result = self.arena.copy(right), self.arena.zero() + scan.msb() + while scan.read() != self.w.LEFT: + doubled, carry = self.raw.add(result, result) + self.w.need(not carry, 'CRT product word capacity') + self.arena.free(result); result = doubled + if scan.read() == self.w.ONE: + added, carry = self.raw.add(result, left) + self.w.need(not carry, 'CRT product word capacity') + self.arena.free(result); result = added + scan.step(-1) + scan.step(1); self.arena.free(scan) + result.msb(); high = result.read(); result.rewind() + self.w.need(high == self.w.ZERO, 'CRT complete product high-bit margin') + return result + + +def produce(arena, left, right, words, records, *, fault=None): + """Both borrowed streams contain ROOT + two fixed-width words + RECORD_END. + + LEFT is unique at cell zero, RIGHT terminates the stream; heads enter at one. + Return owned lower/product words and (offset,new-value) records. The right + prefix includes all preceding right moduli, exactly as source balanced(). + """ + w = words + w.need(left is not right, 'distinct CRT descriptor roles') + protected = set(arena.live) + w.need(arena.capacity == 64 and arena.bits >= 4 and len(protected) <= 8, + 'fixed CRT numerical entry inventory') + output = records.Tape(); keep = set(); succeeded = False + + def pair(stream): + w.need(stream.read() == records.ROOT, 'CRT paired descriptor tag') + stream.step(1) + modulus = records.read_word(stream, arena) + value = records.read_word(stream, arena) + w.need(stream.read() == records.RECORD_END, 'CRT paired descriptor end') + stream.step(1) + return modulus, value + + try: + a = Arithmetic(arena, words) + lower, prefix = arena.zero(), arena.copy(a.one) + valid, seen_left = True, False + while left.read() != w.RIGHT: + seen_left = True + modulus, value = pair(left); a.admit(modulus) + valid = valid and a.raw.compare(value, modulus) < 0 + base = a.remainder(prefix, modulus) + inverse = a.inverse(base, modulus) + w.need(inverse is not None, 'pairwise coprime CRT prefix') + local = a.remainder(lower, modulus) + scaled = a.multiply(local, inverse, modulus) + digit = a.remainder(value, modulus) + adjustment = arena.copy(digit) if fault == 'treat_current_as_original' else a.subtract(digit, scaled, modulus) + term = a.product(prefix, adjustment) + updated, carry = a.raw.add(lower, term) + w.need(not carry, 'CRT reconstruction capacity') + total = a.product(prefix, modulus) + arena.free_many(modulus, value, base, inverse, local, scaled, digit, + adjustment, term, lower, prefix) + lower, prefix = updated, total + w.need(seen_left, 'nonempty current CRT left group') + if not valid: + arena.free(lower); lower = arena.zero() + left_product = arena.copy(prefix) + seen_right = False + while right.read() != w.RIGHT: + seen_right = True + modulus, value = pair(right); a.admit(modulus) + base = a.remainder(prefix, modulus) + inverse = a.inverse(base, modulus) + w.need(inverse is not None, 'pairwise coprime CRT right prefix') + local = a.remainder(lower, modulus) + offset = a.multiply(local, inverse, modulus) + if fault == 'omit_right_prefix': + arena.free(offset) + original_base = a.remainder(left_product, modulus) + original_inverse = a.inverse(original_base, modulus) + offset = a.multiply(local, original_inverse, modulus) + arena.free_many(original_base, original_inverse) + if a.raw.compare(value, modulus) < 0 or fault == 'rotate_padding': + canonical = a.remainder(value, modulus) + updated = a.subtract(canonical, offset, modulus) + arena.free(canonical) + else: updated = arena.copy(value) + output.append(records.ROOT) + records.append_word(output, offset); records.append_word(output, updated) + output.append(records.RECORD_END) + total = a.product(prefix, modulus) + arena.free_many(modulus, value, base, inverse, local, offset, updated, prefix) + prefix = total + w.need(seen_right, 'nonempty current CRT right group') + output.append(w.RIGHT); output.rewind() + keep = {lower.slot, left_product.slot}; succeeded = True + return dict(lower=lower, product=left_product, stream=output, left_valid=valid) + finally: + left.rewind(); right.rewind() + for slot in tuple(arena.live): + if slot not in protected and slot not in keep: + arena.free(arena.words[slot]) + if not succeeded: output.clear() diff --git a/research/encoded-crt-leaf-payload/replay.py b/research/encoded-crt-leaf-payload/replay.py new file mode 100644 index 0000000000..75ad727054 --- /dev/null +++ b/research/encoded-crt-leaf-payload/replay.py @@ -0,0 +1,392 @@ +"""Source-bound finite replay of one encoded CRT payload fiber. Apache-2.0.""" + +from argparse import ArgumentParser +from contextlib import contextmanager +from hashlib import sha1, sha256 +from pathlib import Path +from types import ModuleType, SimpleNamespace +import json +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PINS = json.loads((HERE / 'INPUT-PINS.json').read_text()) +TAGS = (0x125, 0x2DA, 0x389, 0xE61) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def authenticate(path, pin): + data = path.read_bytes() + need(len(data) == pin['bytes'] and sha256(data).hexdigest() == pin['sha256'], + f'source bytes changed: {pin["path"]}') + git_blob = b'blob ' + str(len(data)).encode() + b'\0' + data + need(sha1(git_blob).hexdigest() == pin['git_blob'], 'source Git blob changed') + + +def load(name, path): + module = ModuleType(name) + module.__file__ = str(path) + sys.modules[name] = module + exec(compile(path.read_bytes(), str(path), 'exec'), module.__dict__) + return module + + +def modules(): + for pin in PINS['canonical']: + authenticate(ROOT / pin['path'], pin) + for pin in PINS['retained']: + authenticate(HERE / 'frozen' / pin['file'], pin) + canonical = {Path(p['path']).name: ROOT / p['path'] for p in PINS['canonical']} + w = load('words', canonical['words.py']) # The retained records module imports this name. + r = load('payload_records', canonical['records.py']) + e = load('payload_entry', canonical['entry.py']) + numeric = load('payload_numeric', canonical['producer.py']) + owner = load('payload_owner', canonical['owner.py']) + bridge = load('payload_bridge', canonical['bridge.py']) + f = load('payload_forward_frontend', HERE / 'frozen/frontend.py') + reverse = load('payload_reverse_frontend', HERE / 'frozen/inverse_frontend.py').bind(f) + writer = load('payload_writer', HERE / 'frozen/endpoint.py') + subtractive = load('payload_subtractive', HERE / 'frozen/inverse_producer.py') + join = load('payload_query', canonical['join.py']) + rom = load('payload_benes', canonical['microcode.py']) + binary = load('payload_binary', canonical['binary.py']) + radix = load('payload_radix', canonical['radix.py']) + builder = load('payload_radix_builder', canonical['machine.py']) + program, _, registers = binary.compile_program(radix.assemble(builder), lifecycle=True) + route = load('payload_route', HERE / 'route.py') + fixture = next(case for case in json.loads(canonical['RESULT.json'].read_text())['cases'] + if case['name'] == 'nonroot_roundtrip') + + class MeasuredBitTape(binary.BitTape): + def __init__(self, initial=()): + super().__init__(initial) + self.extent = max(1, len(initial)) + + def move(self, direction): + super().move(direction) + self.extent = max(self.extent, self.head + 1) + + return SimpleNamespace(w=w, r=r, e=e, numeric=numeric, owner=owner, bridge=bridge, + f=f, reverse=reverse, writer=writer, subtractive=subtractive, + join=join, rom=rom, binary=binary, program=program, + registers=registers, rom_program=rom.producer_program(), + route=route, fixture=fixture, bit_tape=MeasuredBitTape) + + +@contextmanager +def seal_numerical_roles(m): + def deny(*_args, **_kwargs): + raise ValueError('new numerical role or host word inspection during execution') + + owners = ((m.e.Port, '__init__'), (m.w.Word, '__init__'), (m.w.Arena, '__init__'), + (m.w.Word, 'inspect')) + originals = [getattr(kind, method) for kind, method in owners] + for kind, method in owners: + setattr(kind, method, deny) + try: + yield + finally: + for (kind, method), original in zip(owners, originals, strict=True): + setattr(kind, method, original) + + +def bit_actions(tapes): + return sum(sum(tape.actions.values()) for tape in tapes) + + +def meter_actions(meter): + return meter.reads + meter.writes + meter.moves + + +def literal_radix(m, record, width, buckets): + for bucket in buckets: + origin = m.route.RecordTape(m.binary, bucket) + origin.emit('<') + origin.move_word(-1) + + tapes = dict(zip(('bad', 'b0', 'b1'), (record.tape, *buckets))) + before = bit_actions(tapes.values()) + machines = [] + width.step(1) + while width.read() == '1': + machine = m.binary.Machine(m.program, len(m.registers), tapes) + need(machine.run() == 'accept', 'retained binary consumer accepts') + machines.append(machine) + width.step(1) + need(width.read() == 'R', 'encoded radix pass limit') + width.rewind() + low_level_radix = bit_actions(tapes.values()) - before + for bucket in buckets: + origin = m.route.RecordTape(m.binary, bucket) + for _ in origin.codes['<']: + bucket.write(0) + bucket.move(1) + origin.move_word(-1) + return machines, low_level_radix + + +def run_leg(m, source, payload, reverse): + """Execute one actual selected leaf. Geometry and destination keys come from tapes.""" + source_before = meter_actions(source.meter) + borrowed_source = bytes(source.cells), source.head + payload_before = bit_actions((payload,)) + front = m.reverse if reverse else m.f + numeric = m.subtractive if reverse else m.numeric + endpoint = m.writer.Endpoint(front, m.w, m.r, m.e, numeric, m.owner, m.bridge, source) + it = endpoint.iterator + numeric_ports = (*it.bank.ports, *it.guards, *it.counters.values(), endpoint.staging) + + headers = {name: m.join.Tape() for name in ('h', 'modulus', 'selected_layer', 'offsets')} + width, index, address, countdown, row = (m.join.Tape() for _ in range(5)) + service = {name: ['_'] for name in (*m.rom.REGS, 'arena', 'spool', 'layers', 'rom')} + service.update({name: port.cells for name, port in headers.items()}) + layers, rom = m.join.Tape(service['layers']), m.join.Tape(service['rom']) + adapter_ports = (*headers.values(), width, index, address, countdown, row, layers, rom) + record = m.route.RecordTape(m.binary, payload) + buckets = (m.bit_tape(), m.bit_tape()) + arena_meters = [] + + with seal_numerical_roles(m): + lease = it.next() + while lease is not None: + arena_meters.append(lease.actual.context.arena.meter) + if m.route.selected_leaf(it, lease): + break + lease.close() + lease = it.next() + need(lease is not None, 'selected physical nonroot leaf') + borrowed_result = lease.actual.result['stream'] + result_before = bytes(borrowed_result.cells), borrowed_result.head + m.route.emit_headers(m.join, it, lease, headers, width) + observed_headers = {name: ''.join(tape.cells) for name, tape in headers.items()} + observed_headers['width'] = ''.join(width.cells) + produced = m.rom.execute(m.rom_program, service) + need(produced['status'] == 'accept' and all(h == 0 for h in produced['heads'].values()), + 'actual encoded ROM production and head return') + m.route.prepare_keys(m.join, record, layers, width, index, address, countdown, row, reverse) + machines, radix_tape_actions = literal_radix(m, record, width, buckets) + need((bytes(source.cells), source.head) == borrowed_source and + (bytes(borrowed_result.cells), borrowed_result.head) == result_before and + lease.actual.guide.head == 1 and it.counters['axis'].head == 1 and + it.counters['half'].head == 1, + 'live source, result and borrowed heads preserved before staging') + endpoint.stage(lease) + lease.close() + endpoint.commit() + if not it.closed: + it.close() + + width.erase() + layers.erase() + rom.erase() + for tape in headers.values(): + tape.erase() + need(all(p.head == 1 and all(c == m.w.BLANK for c in p.cells) for p in numeric_ports), + 'all acquired encoded CRT ports retired') + need(all(p.head == 0 and all(c == '_' for c in p.cells) for p in adapter_ports) + and all(all(c == '_' for c in cells) for cells in service.values()), + 'all encoded metadata and ROM histories retired') + need(all(t.head == 0 and not t.cells for t in buckets) and + all(machine.status == 'accept' and not any(machine.registers) for machine in machines), + 'all literal bucket and finite control histories retired') + need(source.head == 1 and payload.head == 0, 'both physical boundary heads returned') + + symbol_cells = [p.cells for p in numeric_ports] + symbol_cells += [width.cells, index.cells, address.cells, countdown.cells, row.cells] + symbol_cells += list(service.values()) + need(len({id(cells) for cells in symbol_cells}) == len(symbol_cells), + 'disjoint retained symbol roles') + receipt = dict( + direction='inverse' if reverse else 'forward', + selected_nodes=1, + skipped_nodes=len(arena_meters) - 1, + observed_headers=observed_headers, + encoded_source_symbol_actions=sum(meter_actions(p.meter) for p in (source, *numeric_ports)) + - source_before + sum(meter_actions(meter) for meter in arena_meters), + adapter_symbol_actions=sum(p.actions for p in adapter_ports), + benes_instructions=produced['steps'], + radix_bit_control_instructions=sum(sum(machine.census.values()) for machine in machines), + radix_passes=len(machines), + payload_adapter_bit_actions=bit_actions((payload, *buckets)) - payload_before - radix_tape_actions, + retained_symbol_roles=len(symbol_cells), + retained_symbol_cells=sum(map(len, symbol_cells)), + retained_bucket_bits=sum(t.extent for t in buckets), + retained_radix_register_bits=sum(len(machine.registers) for machine in machines), + retained_benes_registers=len(produced['registers']), + ) + return receipt, (symbol_cells, buckets, machines, produced) + + +def initial_fixture(m): + # External fixture encoding happens before the measured input boundary. + case = m.fixture + source, coordinates = m.e.Port(m.w), [] + for width, modulus, value in zip(case['widths'], case['moduli'], case['initial'], strict=True): + source.append(m.r.ROOT) + for _ in range(width): + source.append(m.w.ONE) + source.append(m.r.WORD_END) + for bit in range(width): + source.append((modulus >> bit) & 1) + source.append(m.r.WORD_END) + cells = [] + for bit in range(width): + cells.append(source.head) + source.append((value >> bit) & 1) + coordinates.append(tuple(cells)) + source.append(m.r.RECORD_END) + source.append(m.w.RIGHT) + source.rewind() + source.cells.extend([m.w.ONE, m.w.ZERO, m.w.BLANK] * 3) + + width = case['widths'][-1] + need(len(TAGS) == 1 << width and len(set(TAGS)) == len(TAGS) and all(TAGS), 'marked fixture') + symbols = ['<'] + for position, tag in enumerate(TAGS): + symbols.extend((('R', tag), *format(position, f'0{width}b'))) + symbols.append('>') + packet = tuple(bit for symbol in symbols for bit in m.binary.bits(symbol)) + return source, m.bit_tape(packet), coordinates + + +def coordinates(source, fields): + return [sum(source.cells[cell] << bit for bit, cell in enumerate(field)) for field in fields] + + +def observe_payload(tape, width): + # The observer sees sparse physical bit backing. The runtime above never decodes a key. + def codeword(position): + return sum(tape.cells.get(13 * position + bit, 0) << bit for bit in range(13)) + need(codeword(0) == 5, 'observed payload origin') + observed = [] + at = 1 + while codeword(at) != 6: + payload = codeword(at) + need(4096 <= payload < 8192, 'observed opaque code') + key = 0 + at += 1 + for _ in range(width): + symbol = codeword(at) + need(symbol in (2, 3), 'observed key bit') + key = 2 * key + symbol - 2 + at += 1 + observed.append((key, payload - 4096)) + return observed + + +def direct_oracle(case): + start = case['start'] + left, right = case['moduli'][start:start + 2] + lower = case['initial'][start] + need(case['level'] == 1 and lower < left, 'oracle for a valid two-axis leaf') + offset, = [i for i in range(right) if (left * i - lower) % right == 0] + dest = [(x + offset) % right if x < right else x for x in range(len(TAGS))] + need(len(set(dest)) == len(TAGS), 'direct CRT permutation') + return dest, sorted(zip(dest, TAGS, strict=True)) + + +def reverse_order_control(m): + # Two noncommuting involutions make the control sensitive to row order, + # since the fixture's modulus-two rotation alone cannot distinguish it. + def observed(reverse): + out = [] + for initial in range(4): + address = m.join.Tape(list('L' + format(initial, '02b')[::-1] + 'R')) + layers = m.join.Tape(list('L1100|0101|0000|R')) + width = m.join.Tape(list('L11R')) + m.route.route_address(m.join, layers, width, address, m.join.Tape(), m.join.Tape(), reverse) + out.append(sum(int(bit) << i for i, bit in enumerate(address.cells[1:3]))) + return out + need(observed(False) == [3, 0, 2, 1] and observed(True) == [1, 3, 2, 0], + 'reversed noncommuting row control') + return 'noncommuting rows distinguish traversal order' + + +def truncated_layers_control(m): + try: + m.route.route_address(m.join, m.join.Tape(list('L1100|R')), m.join.Tape(list('L11R')), + m.join.Tape(list('L00R')), m.join.Tape(), m.join.Tape(), False) + except ValueError as exc: + need(str(exc) == 'missing descending ROM layers', 'specific truncated-layer rejection') + return 'truncated width-two layer stream rejected' + raise ValueError('truncated layer stream accepted') + + +def replay(m): + source, payload, fields = initial_fixture(m) + source_cells, payload_cells = id(source.cells), id(payload.cells) + source_initial = bytes(source.cells), source.head + payload_initial = dict(payload.cells), payload.head + oracle_dest, oracle_forward = direct_oracle(m.fixture) + forward, first = run_leg(m, source, payload, False) + observed = observe_payload(payload, m.fixture['widths'][-1]) + need(observed == oracle_forward and oracle_dest != list(range(len(TAGS))), + 'independent nonidentity forward payload placement') + need(coordinates(source, fields) == m.fixture['forward'], 'retained independent source endpoint') + coordinate_cells = set().union(*fields) + need(len(source.cells) == len(source_initial[0]) and + all(source.cells[i] == bit for i, bit in enumerate(source_initial[0]) + if i not in coordinate_cells), 'source metadata and inaccessible tail unchanged') + inverse, second = run_leg(m, source, payload, True) + need((bytes(source.cells), source.head) == source_initial and id(source.cells) == source_cells, + 'actual full source and head restored') + need((payload.cells, payload.head) == payload_initial and id(payload.cells) == payload_cells, + 'actual full payload frame, keys and head restored') + all_symbol_cells = [*first[0], *second[0]] + need(len({id(c) for c in all_symbol_cells}) == len(all_symbol_cells), + 'both directions retain distinct symbol histories') + + expected_headers = {'h': 'L01000R', 'modulus': 'L01000R', 'selected_layer': 'L00000R', + 'offsets': 'L10000|R', 'width': 'L11R'} + need(forward['observed_headers'] == inverse['observed_headers'] == expected_headers, + 'same live encoded offset and width in both directions') + controls = [reverse_order_control(m), truncated_layers_control(m)] + prior_query = m.join.select_row_bit + def suppress(*args): + prior_query(*args) + return '0' + try: + m.join.select_row_bit = suppress + bad_source, bad_payload, _ = initial_fixture(m) + run_leg(m, bad_source, bad_payload, False) + need(observe_payload(bad_payload, m.fixture['widths'][-1]) == list(enumerate(TAGS)) + and list(enumerate(TAGS)) != oracle_forward, + 'no-switch control must fail the forward oracle') + finally: + m.join.select_row_bit = prior_query + controls.append('suppressed switches fail the forward oracle') + return { + 'status': 'PASS_ENCODED_CRT_LEAF_PAYLOAD', + 'fixture': m.fixture['name'], + 'moduli': m.fixture['moduli'], + 'widths': m.fixture['widths'], + 'input_tags': TAGS, + 'forward_destinations': oracle_dest, + 'forward_tags': [value for _, value in observed], + 'forward_source': m.fixture['forward'], + 'restored_source_and_payload': True, + 'source_cells_retained': len(source.cells), + 'payload_bits_visited': payload.extent, + 'forward_and_inverse': [forward, inverse], + 'control_cases': controls, + 'benes_program_instructions': len(m.rom_program), + 'radix_program_instructions': len(m.program), + } + + +if __name__ == '__main__': + parser = ArgumentParser(description=__doc__) + parser.add_argument('--write-result', type=Path) + args = parser.parse_args() + result = replay(modules()) + text = json.dumps(result, indent=2, sort_keys=True) + '\n' + if args.write_result: + with args.write_result.open('x') as stream: + stream.write(text) + else: + need(text == (HERE / 'RESULT.json').read_text(), 'exact committed payload receipt') + print(result['status'], 'markers=4 padded=2 forward_and_inverse=2 controls=3') diff --git a/research/encoded-crt-leaf-payload/route.py b/research/encoded-crt-leaf-payload/route.py new file mode 100644 index 0000000000..b6b5e1573a --- /dev/null +++ b/research/encoded-crt-leaf-payload/route.py @@ -0,0 +1,277 @@ +"""Join an encoded CRT leaf to the existing physical payload mover. Apache-2.0.""" + +BITS = ('0', '1') + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def end_word(tape): + tape.write('R') + tape.rewind() + + +def increment(tape): + """Increment a framed little-endian binary word, returning its carry.""" + tape.step(1) + carry = True + while tape.read() != 'R': + bit = tape.read() + need(bit in BITS, 'binary counter bit') + if carry: + tape.write('0' if bit == '1' else '1') + carry = bit == '1' + tape.step(1) + tape.rewind() + return carry + + +def copy_bits(source, target): + target.emit('L') + source.step(1) + while source.read() != 'R': + bit = source.read() + need(bit in BITS, 'framed binary word') + target.emit(bit) + source.step(1) + source.rewind() + end_word(target) + + +def zero_header(target, guide, words): + target.emit('L') + while guide.read() == words.ONE: + target.emit('0') + guide.step(1) + need(guide.read() == words.BLANK, 'precision guide terminator') + guide.rewind() + end_word(target) + + +def selected_leaf(iterator, lease): + half, axis = iterator.counters['half'], iterator.counters['axis'] + words = iterator.w + need(half.read() == words.ONE, 'nonempty current half') + half.step(1) + one = half.read() == words.RIGHT + half.rewind() + return one and lease.actual.last and axis.read() != iterator.r.STEP + + +def emit_headers(join, iterator, lease, headers, width): + words, records, source = iterator.w, iterator.r, iterator.source + axis = iterator.counters['axis'] + guide = lease.actual.guide + result = lease.actual.result['stream'] + zero_header(headers['h'], guide, words) + zero_header(headers['selected_layer'], guide, words) + while axis.read() != records.STEP: + need(axis.read() == words.ONE, 'encoded nonroot prefix') + iterator._record() + axis.step(1) + iterator._record() # The admitted leaf has exactly one left record. + + need(source.read() == records.ROOT, 'right axis record') + source.step(1) + width.emit('L') + while source.read() == words.ONE: + width.emit('1') + need(not increment(headers['h']), 'encoded width fits precision guide') + source.step(1) + need(source.read() == records.WORD_END, 'right width delimiter') + source.step(1) + end_word(width) + + modulus = headers['modulus'] + modulus.emit('L') + width.step(1) + while width.read() == '1': + bit = source.read() + need(bit in (words.ZERO, words.ONE) and guide.read() == words.ONE, + 'right modulus fits precision guide') + modulus.emit('1' if bit == words.ONE else '0') + source.step(1) + guide.step(1) + width.step(1) + need(width.read() == 'R' and source.read() == records.WORD_END, + 'right modulus delimiter') + width.rewind() + source.step(1) + while guide.read() == words.ONE: + modulus.emit('0') + guide.step(1) + need(guide.read() == words.BLANK, 'modulus padding terminator') + end_word(modulus) + guide.rewind() + + width.step(1) + while width.read() == '1': + need(source.read() in (words.ZERO, words.ONE), 'right coordinate bit') + width.step(1) + source.step(1) + need(width.read() == 'R' and source.read() == records.RECORD_END, + 'right coordinate delimiter') + source.step(1) + need(source.read() == words.RIGHT, 'selected right axis is last') + source.rewind() + axis.rewind() + width.rewind() + + need(result.read() == records.ROOT, 'actual offset record') + result.step(1) + join.copy_numeric_field(result, headers['offsets'], guide, words, records.WORD_END, '|') + result.rewind() + + +def toggle_target(width, address, switch): + # The physical mark records the current target. Both counters are scanned + # by their symbols, and the width head returns to the marked bit. + need(width.read() == '1', 'target is a width cell') + width.write('|') + width.rewind() + width.step(1) + address.step(1) + while width.read() == '1': + width.step(1) + address.step(1) + bit = address.read() + need(width.read() == '|' and bit in BITS and switch in BITS, 'target bit') + if switch == '1': + address.write('1' if bit == '0' else '0') + width.write('1') + address.rewind() + + +def next_target(width, ascending): + width.step(1 if ascending else -1) + if ascending and width.read() == 'R': + width.step(-1) + width.step(-1) + ascending = False + need(width.read() == '1', 'more layers than encoded target positions') + return ascending + + +def previous_delimiter(layers): + layers.step(-1) + while layers.read() in BITS: + layers.step(-1) + need(layers.read() in ('L', '|'), 'physical layer prefix') + + +def route_address(join, layers, width, address, countdown, row, reverse): + """Follow all physical rows using the retained selected-row query.""" + layers.step(1) + if reverse: + while layers.read() != 'R': + need(layers.read() in (*BITS, '|'), 'complete layer tape') + layers.step(1) + layers.step(-1) + width.step(1) + ascending = True + while True: + if reverse: + need(layers.read() == '|', 'reverse layer end') + previous_delimiter(layers) + layers.step(1) + row.emit('L') + seen = False + while layers.read() in BITS: + seen = True + row.emit(layers.read()) + layers.step(1) + need(seen and layers.read() == '|', 'nonempty delimited ROM row') + end_word(row) + copy_bits(address, countdown) + switch = join.select_row_bit(row, countdown) + toggle_target(width, address, switch) + row.erase() + + if reverse: + previous_delimiter(layers) + done = layers.read() == 'L' + else: + layers.step(1) + done = layers.read() == 'R' + if done: + break + ascending = next_target(width, ascending) + if ascending: + width.step(1) + need(width.read() == 'R', 'missing descending ROM layers') + width.step(-1) + width.step(-1) + need(width.read() == 'L', 'complete palindromic target sequence') + layers.rewind() + + +class RecordTape: + """Paid scans and writes on the retained literal radix ABI.""" + def __init__(self, binary, tape): + self.tape = tape + self.codes = {symbol: binary.bits(symbol) for symbol in ('<', '>', '0', '1')} + + def move_word(self, direction): + for _ in self.codes['<']: + self.tape.move(direction) + + def matches(self, symbol): + equal = True + for bit in self.codes[symbol]: + actual = self.tape.read() + equal = equal and actual == bit + self.tape.move(1) + self.move_word(-1) + return equal + + def emit(self, symbol): + for bit in self.codes[symbol]: + self.tape.write(bit) + self.tape.move(1) + + def pass_payload(self): + # Twelve opaque bits and one tag, in the pinned 13-bit ABI. + for _ in range(12): + self.tape.move(1) + need(self.tape.read() == 1, 'actual opaque payload codeword') + self.tape.move(1) + + def rekey(self, address): + address.step(1) + while address.read() in BITS: + address.step(1) + need(address.read() == 'R', 'destination key terminator') + address.step(-1) + while address.read() != 'L': + bit = address.read() + need(bit in BITS and (self.matches('0') or self.matches('1')), + 'one allocated key bit') + self.emit(bit) + address.step(-1) + + +def prepare_keys(join, record, layers, width, index, address, countdown, row, reverse): + need(record.matches('<'), 'physical payload frame begins at origin') + record.move_word(1) + index.emit('L') + width.step(1) + while width.read() == '1': + index.emit('0') + width.step(1) + need(width.read() == 'R', 'encoded payload width') + width.rewind() + end_word(index) + while True: + record.pass_payload() + copy_bits(index, address) + route_address(join, layers, width, address, countdown, row, reverse) + record.rekey(address) + address.erase() + if increment(index): + break + need(record.matches('>'), 'payload occupies precisely the padded rectangle') + while not record.matches('<'): + record.move_word(-1) + index.erase()