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/4] 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/4] 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/4] 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() From cf62e701f52adf2196923ab7356539e69713d55b Mon Sep 17 00:00:00 2001 From: Clear1nsight <22630354+Clear1nsight@users.noreply.github.com> Date: Thu, 12 Nov 2026 19:13:32 +1100 Subject: [PATCH 4/4] Fuse two encoded CRT payload sorts into one --- .../encoded-crt-two-target-payload/README.md | 123 ++++++ .../RESULT.json | 265 +++++++++++ .../SOURCES.json | 145 ++++++ .../encoded-crt-two-target-payload/TASK.json | 83 ++++ .../VERIFY.json | 40 ++ .../encoded-crt-two-target-payload/replay.py | 414 ++++++++++++++++++ .../encoded-crt-two-target-payload/route.py | 150 +++++++ 7 files changed, 1220 insertions(+) create mode 100644 research/encoded-crt-two-target-payload/README.md create mode 100644 research/encoded-crt-two-target-payload/RESULT.json create mode 100644 research/encoded-crt-two-target-payload/SOURCES.json create mode 100644 research/encoded-crt-two-target-payload/TASK.json create mode 100644 research/encoded-crt-two-target-payload/VERIFY.json create mode 100644 research/encoded-crt-two-target-payload/replay.py create mode 100644 research/encoded-crt-two-target-payload/route.py diff --git a/research/encoded-crt-two-target-payload/README.md b/research/encoded-crt-two-target-payload/README.md new file mode 100644 index 0000000000..bd3066a36e --- /dev/null +++ b/research/encoded-crt-two-target-payload/README.md @@ -0,0 +1,123 @@ +# Fuse two encoded CRT payload sorts + +One live balanced CRT root now routes both right axes of the retained +`two_short_first` fixture. One combined destination key sorts its complete +16-record right-side rectangle in four literal radix passes. A matched +forward execution that sorts after each axis reaches the same exact frame in +eight passes. The fused inverse restores the entire input frame, encoded +source, physical backing and entry heads. + +The fixture has moduli `(5,7,3,2)`, declared widths `(3,3,2,2)` and input +source `(1,5,2,1)`. The source becomes `(1,5,0,0)` and then returns to +`(1,5,2,1)`. Original tag `293` moves from slot 0 to slot 5. The independent +CRT oracle checks all 16 slots before accepting restoration. The primary +execution covers one fixed left state and its full padded right rectangle. + +## Source and payload join + +1. Select the live root from the retained #7352 iterator. The encoded axis + cursor is at its first marker and the lease ends at the source suffix. + The forward leg pays for two earlier read-only leaves. The inverse sees + the root first and retires the remaining iterator after the root. +2. Walk the borrowed right source and numerical result in the same order. + Copy each physical unary width and modulus and the corresponding P-bit + offset. Consume each complete updated-coordinate field and require both + terminal markers. The width sum supplies the radix pass count. Check that + the borrowed tapes and their heads are unchanged before staging. +3. Run the existing encoded Beneš program once for each target on the same + private and output backing. For each call, scan the actual payload tape. + Two encoded position counters identify the current slot. Query all + physical switch rows for the selected axis and write only that axis's key + field. Skip the other field using its live unary width. Clear both ROM + outputs and the active headers before reusing the bank. +4. Sort the entire frame once with the unchanged literal binary radix + program. Stage the whole-node result, retire the numerical lease, then + commit the source. The inverse reverses the row sequence within each + target and repeats the same frame procedure. + +For the fixed current left source, the independent oracle solves +`k ≡ 1 mod 5` and `k ≡ 5*5 mod 7`, so `k = 11` in `[0,35)`. For the two +right axes it solves `35*c ≡ 11 mod 3` and `105*c ≡ 11 mod 2`. Both +positive offsets are 1. The two axis maps on their padded four-slot +coordinates are `f = [1,2,0,3]` and `g = [1,0,2,3]`. A padded coordinate +is fixed on its own axis while the other coordinate can still move. + +At physical position `4*a+b` the fused scan writes `f(a)` and `g(b)` into +the two fields before any record moves. The staged sort first puts that +record at `4*f(a)+b` with the key for its new physical slot. Counting +positions afresh at the second scan gives the same full key `4*f(a)+g(b)`. +This argument uses that the permutations act on separate fields and that +the offsets depend on the preserved left source and modulus prefix. Reversing +the layers of each axis inverts its permutation. Four stable last-bit passes +both sort the four-bit keys and restore their bit order. + +## Observed work and storage + +| Quantity | Fused forward | Staged forward | Fused inverse | +| --- | ---: | ---: | ---: | +| Literal radix passes | 4 | 8 | 4 | +| Literal radix bit and control instructions | 492,724 | 985,448 | 492,724 | +| Payload adapter bit actions, including bucket markers | 19,272 | 19,428 | 19,272 | +| Adapter symbol actions | 25,906 | 25,928 | 28,594 | +| Encoded source symbol actions | 373,976 | 373,976 | 264,989 | +| Beneš producer instructions | 9,681,707 | 9,681,707 | 9,681,707 | +| Actual row queries | 96 | 96 | 96 | +| Retained private symbol cells | 4,309 | 4,309 | 4,308 | +| Retained literal radix register bits | 288 | 576 | 288 | + +The forward comparison saves 492,724 radix instructions and 156 bit-tape +marker actions. The comparator uses the same full-frame radix ABI and +performs one complete sort after each of the two axis scans. It models this +specific staged route. The shared ROM backing retains 3,031 private/output +cells at the end of either target, apart from the charged header storage. +Each execution retains 30 Beneš register symbols, 1,092 bucket bits and 143 +private symbol roles. The fused round trip shares one 57-cell source and one +payload tape with a visited extent of 1,067 bits. The two legs retain their +private banks separately. + +Counts use the respective source, symbol and binary execution models. +Fixture serialization and independent observers sit outside the measured +call. A common literal tariff, a complete multiplication caller and a +change in the asymptotic saving κ remain open. + +## Replay and source credit + +Run the registered package or direct replay with Python 3.12. + +```sh +python3.12 -B scripts/research_package.py --package research/encoded-crt-two-target-payload +python3.12 -I -B research/encoded-crt-two-target-payload/replay.py +``` + +[RESULT.json](RESULT.json) records all three executions and the exact maps. +The dropped fast target control still commits the correct source but puts +tag `293` in slot 4. The retained `growing_bank` case separately checks +unequal widths and unequal offsets on the live header path. Reusing its +first offset for its second fails the ordered header oracle. The replay +also retains the noncommuting inverse-row-order and truncated-row controls. + +[SOURCES.json](SOURCES.json) binds the live inputs to canonical main +`e54523517d0f03e58352e647c403a5af3e525a57` and the exact [#7388 predecessor](https://github.com/CrocSwap/integer-mult-bounds/pull/7388) +`d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86`. This package imports its loader, +full-layer row traversal and literal radix wrapper without copying them. +The retained #7388 pins identify CubeJerry's [#7352](https://github.com/CrocSwap/integer-mult-bounds/pull/7352) +encoded endpoint and the shared forward writer from [#7351](https://github.com/CrocSwap/integer-mult-bounds/pull/7351). +Commdata2338's [#5519](https://github.com/CrocSwap/integer-mult-bounds/pull/5519) +at `53a034436f17ef5b8fdf7a02f5066528cdfe5446` supplies the fixture and +shared-bank alignment invariant. Ali Romman's +[#5625](https://github.com/CrocSwap/integer-mult-bounds/pull/5625) supplies +predecessor retirement evidence. 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 producer, row query and literal consumer. OpenAI Codex and ChatGPT Pro +materially assisted. Pro derived the independent slot map and checked the +isolated radix component with supplied keys. Apache-2.0. + +## Open next questions + +To transfer this result into an actual multiplier, first bind a caller's +full normalized transform returns, payload layout and original-coordinate +extraction to the encoded source contract across left states. The next +product-level acceptance check +must use a production-admitted catalogue, consume the actual transform +returns and recover an exact integer product through CRT and carry. diff --git a/research/encoded-crt-two-target-payload/RESULT.json b/research/encoded-crt-two-target-payload/RESULT.json new file mode 100644 index 0000000000..e73d1fc197 --- /dev/null +++ b/research/encoded-crt-two-target-payload/RESULT.json @@ -0,0 +1,265 @@ +{ + "controls": { + "dropped_fast_first_tag_actual_slot": 4, + "dropped_fast_first_tag_required_slot": 5, + "noncommuting_row_order": true, + "ordered_header_alignment": { + "case": "growing_bank", + "headers": [ + { + "h": "L01000000000R", + "modulus": "L11000000000R", + "offsets": "L00000000000|R", + "selected_layer": "L00000000000R", + "width": "L11R" + }, + { + "h": "L11000000000R", + "modulus": "L11100000000R", + "offsets": "L10100000000|R", + "selected_layer": "L00000000000R", + "width": "L111R" + } + ], + "stale_second_offset_rejected": true + }, + "truncated_layers_rejected": true + }, + "executions": [ + { + "adapter_symbol_actions": 25906, + "benes_instructions": 9681707, + "encoded_source_symbol_actions": 373976, + "headers": [ + { + "h": "L01000000000R", + "modulus": "L11000000000R", + "offsets": "L10000000000|R", + "selected_layer": "L00000000000R", + "width": "L11R" + }, + { + "h": "L01000000000R", + "modulus": "L01000000000R", + "offsets": "L10000000000|R", + "selected_layer": "L00000000000R", + "width": "L11R" + } + ], + "mode": "fused_forward", + "payload_adapter_bit_actions": 19272, + "payload_visited_bits": 1067, + "producer_calls": 2, + "radix_bit_control_instructions": 492724, + "radix_instructions_by_pass": [ + 123181, + 123181, + 123181, + 123181 + ], + "retained_benes_registers": 30, + "retained_bucket_bits": 1092, + "retained_radix_register_bits": 288, + "retained_rom_bank_cells_after_each_target": [ + 3031, + 3031 + ], + "retained_symbol_cells": 4309, + "retained_symbol_roles": 143, + "row_queries": 96, + "skipped_leases": 2 + }, + { + "adapter_symbol_actions": 28594, + "benes_instructions": 9681707, + "encoded_source_symbol_actions": 264989, + "headers": [ + { + "h": "L01000000000R", + "modulus": "L11000000000R", + "offsets": "L10000000000|R", + "selected_layer": "L00000000000R", + "width": "L11R" + }, + { + "h": "L01000000000R", + "modulus": "L01000000000R", + "offsets": "L10000000000|R", + "selected_layer": "L00000000000R", + "width": "L11R" + } + ], + "mode": "fused_inverse", + "payload_adapter_bit_actions": 19272, + "payload_visited_bits": 1067, + "producer_calls": 2, + "radix_bit_control_instructions": 492724, + "radix_instructions_by_pass": [ + 123181, + 123181, + 123181, + 123181 + ], + "retained_benes_registers": 30, + "retained_bucket_bits": 1092, + "retained_radix_register_bits": 288, + "retained_rom_bank_cells_after_each_target": [ + 3031, + 3031 + ], + "retained_symbol_cells": 4308, + "retained_symbol_roles": 143, + "row_queries": 96, + "skipped_leases": 0 + }, + { + "adapter_symbol_actions": 25928, + "benes_instructions": 9681707, + "encoded_source_symbol_actions": 373976, + "headers": [ + { + "h": "L01000000000R", + "modulus": "L11000000000R", + "offsets": "L10000000000|R", + "selected_layer": "L00000000000R", + "width": "L11R" + }, + { + "h": "L01000000000R", + "modulus": "L01000000000R", + "offsets": "L10000000000|R", + "selected_layer": "L00000000000R", + "width": "L11R" + } + ], + "mode": "staged_forward", + "payload_adapter_bit_actions": 19428, + "payload_visited_bits": 1067, + "producer_calls": 2, + "radix_bit_control_instructions": 985448, + "radix_instructions_by_pass": [ + 123181, + 123181, + 123181, + 123181, + 123181, + 123181, + 123181, + 123181 + ], + "retained_benes_registers": 30, + "retained_bucket_bits": 1092, + "retained_radix_register_bits": 576, + "retained_rom_bank_cells_after_each_target": [ + 3031, + 3031 + ], + "retained_symbol_cells": 4309, + "retained_symbol_roles": 143, + "row_queries": 96, + "skipped_leases": 2 + } + ], + "fixture": "two_short_first", + "forward_destinations": [ + 5, + 4, + 6, + 7, + 9, + 8, + 10, + 11, + 1, + 0, + 2, + 3, + 13, + 12, + 14, + 15 + ], + "forward_radix_instructions_saved": 492724, + "forward_source": [ + 1, + 5, + 0, + 0 + ], + "forward_tags": [ + 1472, + 1341, + 1603, + 1734, + 424, + 293, + 555, + 686, + 948, + 817, + 1079, + 1210, + 1996, + 1865, + 2127, + 2258 + ], + "input_source": [ + 1, + 5, + 2, + 1 + ], + "input_tags": [ + 293, + 424, + 555, + 686, + 817, + 948, + 1079, + 1210, + 1341, + 1472, + 1603, + 1734, + 1865, + 1996, + 2127, + 2258 + ], + "inverse_destinations": [ + 9, + 8, + 10, + 11, + 1, + 0, + 2, + 3, + 5, + 4, + 6, + 7, + 13, + 12, + 14, + 15 + ], + "moduli": [ + 5, + 7, + 3, + 2 + ], + "reconstructed_left": 11, + "restored_source_and_payload": true, + "source_retained_cells": 57, + "status": "PASS_ENCODED_CRT_TWO_TARGET_PAYLOAD", + "widths": [ + 3, + 3, + 2, + 2 + ] +} diff --git a/research/encoded-crt-two-target-payload/SOURCES.json b/research/encoded-crt-two-target-payload/SOURCES.json new file mode 100644 index 0000000000..b89191873a --- /dev/null +++ b/research/encoded-crt-two-target-payload/SOURCES.json @@ -0,0 +1,145 @@ +{ + "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" + }, + { + "git_blob": "41f6f41c98cd3728abc21a560543938b58b303e2", + "path": "research/encoded-crt-leaf-payload/INPUT-PINS.json", + "pin": "head:d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86:research/encoded-crt-leaf-payload/INPUT-PINS.json", + "sha256": "2e06f6515bef4166f987f06d678ae3bbb2837e4da6c48514c1ca7d82d86614fd", + "usage": "input" + }, + { + "git_blob": "75ad7270542d18704ae5b1f8b6ffa29e58741d00", + "path": "research/encoded-crt-leaf-payload/replay.py", + "pin": "head:d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86:research/encoded-crt-leaf-payload/replay.py", + "sha256": "31e6f9e4b91fb67c40ee27e4d8ee6b4d1b2674efd9bb7e361bf7de879c188761", + "usage": "input" + }, + { + "git_blob": "b6b5e1573a7984ee7189b85709085c73254e1569", + "path": "research/encoded-crt-leaf-payload/route.py", + "pin": "head:d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86:research/encoded-crt-leaf-payload/route.py", + "sha256": "d17eecceb43c5327a35dd7b903e33f48aef46c803d6b8a54dfc6ec54c2ec9b36", + "usage": "input" + }, + { + "git_blob": "b084d893bdb2ce5571ef00196a9ec6a60e723964", + "path": "research/encoded-crt-leaf-payload/frozen/endpoint.py", + "pin": "head:d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86:research/encoded-crt-leaf-payload/frozen/endpoint.py", + "sha256": "c24ae2c90d175d276120438809e7c7401b8a8c04dec139f1b7345e9778984ced", + "usage": "input" + }, + { + "git_blob": "8adbe2cfef74da9854ed0b70b6c221f5746efa9f", + "path": "research/encoded-crt-leaf-payload/frozen/frontend.py", + "pin": "head:d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86:research/encoded-crt-leaf-payload/frozen/frontend.py", + "sha256": "6ec9aab626a9d7a229b6f13ce6863e1ca77fa30ef65a4a66ae03a6ffaf2ee78c", + "usage": "input" + }, + { + "git_blob": "17abfb8500043bcdeb656094bb0213d911d986fc", + "path": "research/encoded-crt-leaf-payload/frozen/inverse_frontend.py", + "pin": "head:d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86:research/encoded-crt-leaf-payload/frozen/inverse_frontend.py", + "sha256": "0e5f4c9450372c90000f5ebf3c22dfbe7241dd53da9ae9bcce310af859b009ef", + "usage": "input" + }, + { + "git_blob": "46bf6ef4e2dfa53bca17ac668914b1a842eaba9e", + "path": "research/encoded-crt-leaf-payload/frozen/inverse_producer.py", + "pin": "head:d6f4a69202ad0bba4a915f4d4f3eaba1fe431c86:research/encoded-crt-leaf-payload/frozen/inverse_producer.py", + "sha256": "6acdebee7134fbc8e2d121060286bd05e7282900da8a28a78c80937dde7ea178", + "usage": "input" + }, + { + "git_blob": "81633db5c1fa0e4614891e7091d0ca82acd5f3c9", + "path": "research/crt-multitarget-row-audit/verify.py", + "sha256": "971111b8418d9b3234b0441bbfb424ede574bc45b9996839093a377b694c0a41", + "usage": "input" + } + ], + "schema_version": 1 +} diff --git a/research/encoded-crt-two-target-payload/TASK.json b/research/encoded-crt-two-target-payload/TASK.json new file mode 100644 index 0000000000..51ffcddb5b --- /dev/null +++ b/research/encoded-crt-two-target-payload/TASK.json @@ -0,0 +1,83 @@ +{ + "actual_scope": "One fixed-left, four-axis mixed-width root with two nonidentity right permutations and 16 marked records. Execute the fused forward and inverse, and the matched staged forward comparison.", + "ai_assistance": "OpenAI Codex and ChatGPT Pro materially assisted the formulation, audit, and verification.", + "author": "Clear1nsight", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "Route a full padded right rectangle from one actual two-target encoded CRT root and measure a one-sort versus two-sort execution.", + "budget_minutes": 60, + "evidence": "Separate CRT oracle, exact source and physical payload round trip, measured four versus eight literal passes, shared ROM histories and four controls.", + "open_questions": [ + { + "blocked_by": "The retained padded slice has a fixed left state. A complete normalized caller and common literal cost bound are outside this result.", + "first_step": "Bind one production-admitted catalogue, actual transform returns, original-coordinate extraction and the final CRT/carry boundary.", + "question": "Can a production normalized CRT/Tensor caller feed exact integer recovery?", + "why_it_matters": "The next product-level gate must compare the complete physical output against exact integer multiplication." + } + ], + "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": "Extend the previously executed #7388 leaf seam to the retained #5519 two_short_first root, using actual right headers and both key fields.", + "scope_status": "refined", + "stop_rule": "Stop at the retained one-root payload slice, its matched staged forward comparator and targeted controls. Preserve separate tariffs and do not infer a new bound.", + "task_id": "uniform-transfer-audit" +} diff --git a/research/encoded-crt-two-target-payload/VERIFY.json b/research/encoded-crt-two-target-payload/VERIFY.json new file mode 100644 index 0000000000..6bbd7be557 --- /dev/null +++ b/research/encoded-crt-two-target-payload/VERIFY.json @@ -0,0 +1,40 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Compare the exact live two-target source/payload round trip and staged forward; check same bank, paid counts and four controls.", + "timeout_seconds": 120 + } + ], + "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", + "research/encoded-crt-leaf-payload/INPUT-PINS.json", + "research/encoded-crt-leaf-payload/replay.py", + "research/encoded-crt-leaf-payload/route.py", + "research/encoded-crt-leaf-payload/frozen/endpoint.py", + "research/encoded-crt-leaf-payload/frozen/frontend.py", + "research/encoded-crt-leaf-payload/frozen/inverse_frontend.py", + "research/encoded-crt-leaf-payload/frozen/inverse_producer.py", + "research/crt-multitarget-row-audit/verify.py" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/encoded-crt-two-target-payload/replay.py b/research/encoded-crt-two-target-payload/replay.py new file mode 100644 index 0000000000..63614e3d9f --- /dev/null +++ b/research/encoded-crt-two-target-payload/replay.py @@ -0,0 +1,414 @@ +"""Replay a live two-target CRT root through the retained literal mover. Apache-2.0.""" + +from argparse import ArgumentParser +import ast +from hashlib import sha256 +from importlib.util import module_from_spec, spec_from_file_location +from itertools import product +import json +from math import prod +from pathlib import Path +from unittest.mock import patch + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +FIXTURE_SOURCE = 'research/crt-multitarget-row-audit/verify.py' +PREDECESSOR = 'research/encoded-crt-leaf-payload/replay.py' +TAGS = tuple(293 + 131 * i for i in range(16)) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load(name, path): + spec = spec_from_file_location(name, path) + module = module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def authenticate(): + for pin in json.loads((HERE / 'SOURCES.json').read_text())['files']: + if pin['usage'] == 'input': + content = (ROOT / pin['path']).read_bytes() + need(sha256(content).hexdigest() == pin['sha256'], f'input drift: {pin["path"]}') + + +def retained_cases(): + """Read the exact fixture literals without importing the audit's verifier.""" + tree = ast.parse((ROOT / FIXTURE_SOURCE).read_bytes()) + cases, = [statement.value for statement in tree.body if isinstance(statement, ast.Assign) + and any(isinstance(name, ast.Name) and name.id == 'CASES' for name in statement.targets)] + result = {} + for entry in cases.elts: + need(isinstance(entry, ast.Call) and isinstance(entry.func, ast.Name) + and entry.func.id == 'dict' and not entry.args, 'literal predecessor fixture') + case = {item.arg: ast.literal_eval(item.value) for item in entry.keywords} + result[case['name']] = case + return result + + +def source_fixture(m, case): + """Encode the fixed test input outside the measured call boundary.""" + source, fields = m.e.Port(m.w), [] + for width, modulus, value in zip(case['widths'], case['moduli'], case['state'], 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) + fields.append(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) + return source, fields + + +def packet(m, width, tags): + need(len(tags) == 1 << width and len(set(tags)) == len(tags) + and all(0 < t < 4096 for t in tags), 'all slots have distinct nonzero markers') + symbols = ['<'] + for position, tag in enumerate(tags): + symbols.extend((('R', tag), *format(position, f'0{width}b'))) + symbols.append('>') + return tuple(bit for symbol in symbols for bit in m.binary.bits(symbol)) + + +def oracle(case): + """Solve the left congruences by enumeration, then rotate each valid axis.""" + moduli, widths, state = case['moduli'], case['widths'], case['state'] + need(len(state) == 4 and all(x < p for x, p in zip(state[:2], moduli[:2])), + 'independent oracle for the retained valid-left four-axis root') + left, = [z for z in range(prod(moduli[:2])) if all( + (z - state[i] * prod(moduli[:i])) % moduli[i] == 0 for i in range(2))] + offsets = [] + for i in (2, 3): + modulus, prefix = moduli[i], prod(moduli[:i]) + c, = [v for v in range(modulus) if (prefix * v - left) % modulus == 0] + offsets.append(c) + + def shift(x, i, sign): + modulus = moduli[i + 2] + return (x + sign * offsets[i]) % modulus if x < modulus else x + + slow, fast = (1 << width for width in widths[2:]) + maps = [[fast * shift(a, 0, sign) + shift(b, 1, sign) + for a, b in product(range(slow), range(fast))] for sign in (1, -1)] + need(all(maps[1][j] == i for i, j in enumerate(maps[0])), 'direct inverse permutation') + updated = state[:2] + [shift(state[i + 2], i, 1) for i in range(2)] + return left, offsets, updated, maps + + +def expected_headers(case, offsets): + precision = 1 + sum(case['widths']) + + def word(number, suffix='R'): + return 'L' + format(number, f'0{precision}b')[::-1] + suffix + + return [dict(h=word(width), modulus=word(modulus), selected_layer=word(0), + offsets=word(offset, '|R'), width='L' + '1' * width + 'R') + for width, modulus, offset in zip(case['widths'][2:], case['moduli'][2:], offsets, strict=True)] + + +def new_headers(m, route): + headers = tuple({name: m.join.Tape() for name in route.HEADER_NAMES} for _ in range(2)) + return headers, (m.join.Tape(), m.join.Tape()), m.join.Tape() + + +def observe_headers(headers, widths): + return [dict({name: ''.join(tape.cells) for name, tape in header.items()}, + width=''.join(width.cells)) for header, width in zip(headers, widths, strict=True)] + + +def borrowed_ports(it, lease): + actual = lease.actual + return (it.source, actual.result['stream'], actual.guide, actual.left, actual.right, + it.counters['axis'], it.counters['half']) + + +def state_of(ports): + return [(id(t.cells), bytes(t.cells), t.head, t.meter.writes) for t in ports] + + +def make_endpoint(m, source, reverse): + return m.writer.Endpoint(m.reverse if reverse else m.f, m.w, m.r, m.e, + m.subtractive if reverse else m.numeric, m.owner, m.bridge, source) + + +def run_leg(previous, m, route, source, payload, *, reverse=False, staged=False): + source_before = previous.meter_actions(source.meter) + payload_before = previous.bit_actions((payload,)) + endpoint = make_endpoint(m, source, reverse) + it = endpoint.iterator + numeric_ports = (*it.bank.ports, *it.guards, *it.counters.values(), endpoint.staging) + headers, widths, combined = new_headers(m, route) + indices = tuple(m.join.Tape() for _ in range(2)) + scratch = tuple(m.join.Tape() for _ in range(3)) + header_ports = tuple(t for header in headers for t in header.values()) + bank = {name: ['_'] for name in (*m.rom.REGS, 'arena', 'spool', 'layers', 'rom')} + bank_ids = tuple(map(id, bank.values())) + layers, rom = m.join.Tape(bank['layers']), m.join.Tape(bank['rom']) + adapter = (*header_ports, *widths, combined, *indices, *scratch, layers, rom) + record = m.route.RecordTape(m.binary, payload) + buckets = m.bit_tape(), m.bit_tape() + runs, machines, bank_history, pass_counts = [], [], [], [] + radix_tape_actions = 0 + select_row_bit = m.join.select_row_bit + row_queries = 0 + + def count_query(row, countdown): + nonlocal row_queries + row_queries += 1 + return select_row_bit(row, countdown) + + with previous.seal_numerical_roles(m), patch.object(m.join, 'select_row_bit', count_query): + lease, arena_meters = route.open_root(it) + borrowed = borrowed_ports(it, lease) + need(all(port.head == 1 for port in borrowed), 'actual root borrow entry heads') + before = state_of(borrowed) + route.emit_root_headers(m, it, lease, headers, widths, combined) + header_receipt = observe_headers(headers, widths) + for target, header in enumerate(headers): + need(tuple(map(id, bank.values())) == bank_ids + and all(all(c == '_' for c in cells) for cells in bank.values()), + 'same blank ROM bank including old tails') + active = {name: tape.cells for name, tape in header.items()} + service = bank | active + run = m.rom.execute(m.rom_program, service) + need(run['status'] == 'accept' and all(h == 0 for h in run['heads'].values()), + 'live encoded producer accepts and returns every head') + need(tuple(map(id, bank.values())) == bank_ids + and all(service[name] is cells for name, cells in bank.items()), + 'producer retained the same backing identities') + need(all(''.join(cells).rstrip('_') == header_receipt[target][name] + for name, cells in active.items()), 'actual producer preserves each active header') + runs.append(run) + bank_history.append(sum(map(len, bank.values()))) + route.rekey_axis(m, record, layers, widths, indices, scratch, target, reverse) + layers.erase() + rom.erase() + for tape in header.values(): + tape.erase() + if staged or target == len(headers) - 1: + current_machines, tape_actions = previous.literal_radix(m, record, combined, buckets) + machines.extend(current_machines) + radix_tape_actions += tape_actions + pass_counts.extend(sum(machine.census.values()) for machine in current_machines) + need(state_of(borrowed) == before, 'actual borrows preserved before staging') + endpoint.stage(lease) + need(state_of(borrowed) == before, 'borrowed source still unchanged while staging') + lease.close() + endpoint.commit() + if not it.closed: + it.close() + + combined.erase() + for width in widths: + width.erase() + need(all(p.head == 1 and all(c == m.w.BLANK for c in p.cells) for p in numeric_ports), + 'all owned encoded CRT tapes retired') + need(all(p.head == 0 and all(c == '_' for c in p.cells) for p in adapter) + and all(all(c == '_' for c in cells) for cells in bank.values()), + 'all header, routing and shared ROM tapes 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 control histories retired') + need(source.head == 1 and payload.head == 0, 'both physical entry heads returned') + + symbol_cells = [p.cells for p in numeric_ports] + symbol_cells += [p.cells for p in adapter if p is not layers and p is not rom] + symbol_cells += list(bank.values()) + need(len({id(cells) for cells in symbol_cells}) == len(symbol_cells), 'no duplicate symbol backing') + receipt = dict( + mode='staged_forward' if staged else 'fused_inverse' if reverse else 'fused_forward', + headers=header_receipt, producer_calls=len(runs), row_queries=row_queries, + skipped_leases=len(arena_meters) - 1, + encoded_source_symbol_actions=sum(previous.meter_actions(p.meter) for p in (source, *numeric_ports)) + - source_before + sum(previous.meter_actions(meter) for meter in arena_meters), + adapter_symbol_actions=sum(p.actions for p in adapter), + benes_instructions=sum(run['steps'] for run in runs), + radix_bit_control_instructions=sum(pass_counts), radix_instructions_by_pass=pass_counts, + payload_adapter_bit_actions=previous.bit_actions((payload, *buckets)) + - payload_before - radix_tape_actions, + retained_symbol_roles=len(symbol_cells), retained_symbol_cells=sum(map(len, symbol_cells)), + retained_rom_bank_cells_after_each_target=bank_history, + retained_benes_registers=sum(len(run['registers']) for run in runs), + retained_radix_register_bits=sum(len(machine.registers) for machine in machines), + retained_bucket_bits=sum(tape.extent for tape in buckets), payload_visited_bits=payload.extent, + ) + return receipt, (symbol_cells, buckets, machines, runs) + + +def check_frame(m, previous, payload, expected, width): + need(previous.observe_payload(payload, width) == list(enumerate(expected)) + and payload.cells == m.bit_tape(packet(m, width, expected)).cells, + 'direct CRT forward frame mismatch') + + +def header_probe(previous, m, route, case): + source, _ = source_fixture(m, case) + it = make_endpoint(m, source, False).iterator + headers, widths, combined = new_headers(m, route) + with previous.seal_numerical_roles(m): + lease, _ = route.open_root(it) + ports = borrowed_ports(it, lease) + before = state_of(ports) + route.emit_root_headers(m, it, lease, headers, widths, combined) + need(state_of(ports) == before, 'control preserves live headers and source') + lease.close() + if not it.closed: + it.close() + observed = observe_headers(headers, widths) + for header, width in zip(headers, widths, strict=True): + for tape in (*header.values(), width): + tape.erase() + combined.erase() + return observed + + +def check_header_alignment(previous, m, route, case): + _, offsets, _, _ = oracle(case) + expected = expected_headers(case, offsets) + need(case['widths'][2] != case['widths'][3] and len(set(offsets)) == 2, + 'control distinguishes both ordered widths and offsets') + observed = header_probe(previous, m, route, case) + need(observed == expected, 'distinct live header alignment') + copy = m.join.copy_numeric_field + first = None + + def stale_offset(source, target, guide, words, delimiter, suffix): + nonlocal first + copy(source, target, guide, words, delimiter, suffix) + if first is None: + first = target + return + first.step(1) + target.step(1) + while first.read() in m.route.BITS: + target.write(first.read()) + first.step(1) + target.step(1) + need(first.read() == target.read() == '|', 'stale control preserves field shape') + first.rewind() + target.rewind() + + with patch.object(m.join, 'copy_numeric_field', stale_offset): + mutated = header_probe(previous, m, route, case) + need(mutated[0] == expected[0] and mutated[1] == (expected[1] | {'offsets': expected[0]['offsets']}) + and mutated != expected, 'stale offset must fail ordered header oracle') + return dict(case=case['name'], headers=observed, stale_second_offset_rejected=True) + + +def replay(previous, m, route, cases): + case = cases['two_short_first'] + left, offsets, forward_state, maps = oracle(case) + width = sum(case['widths'][2:]) + initial_packet = packet(m, width, TAGS) + forward_tags = [tag for _, tag in sorted(zip(maps[0], TAGS, strict=True))] + expected = expected_headers(case, offsets) + source, fields = source_fixture(m, case) + payload = m.bit_tape(initial_packet) + source_initial, payload_initial = bytes(source.cells), dict(payload.cells) + source_id, payload_id = id(source.cells), id(payload.cells) + target_source = bytearray(source_initial) + for field, value in zip(fields, forward_state, strict=True): + for bit, cell in enumerate(field): + target_source[cell] = (value >> bit) & 1 + + forward, forward_keep = run_leg(previous, m, route, source, payload) + check_frame(m, previous, payload, forward_tags, width) + need(bytes(source.cells) == target_source and id(source.cells) == source_id + and id(payload.cells) == payload_id, 'exact forward source and same backing') + inverse, inverse_keep = run_leg(previous, m, route, source, payload, reverse=True) + need(bytes(source.cells) == source_initial and payload.cells == payload_initial + and id(source.cells) == source_id and id(payload.cells) == payload_id, + 'exact inverse source, payload and backing') + need({id(c) for c in forward_keep[0]}.isdisjoint(id(c) for c in inverse_keep[0]), + 'only actual boundary tapes are shared across legs') + + staged_source, _ = source_fixture(m, case) + staged_payload = m.bit_tape(initial_packet) + staged, _staged_keep = run_leg(previous, m, route, staged_source, staged_payload, staged=True) + check_frame(m, previous, staged_payload, forward_tags, width) + need(bytes(staged_source.cells) == target_source, 'staged forward same source') + need(all(leg['headers'] == expected and leg['producer_calls'] == 2 for leg in (forward, inverse, staged)), + 'both independently checked live headers on every leg') + need(forward['row_queries'] == inverse['row_queries'] == staged['row_queries'] == 96, + 'all physical row queries executed') + same_forward = ('benes_instructions', 'encoded_source_symbol_actions', + 'retained_rom_bank_cells_after_each_target', 'retained_symbol_cells', + 'retained_bucket_bits', 'payload_visited_bits') + need(all(forward[key] == staged[key] for key in same_forward), 'matched source and routing work') + need(all(forward[key] <= staged[key] for key in ('adapter_symbol_actions', + 'payload_adapter_bit_actions', 'retained_radix_register_bits')), 'no measured adapter tradeoff') + need([len(leg['radix_instructions_by_pass']) for leg in (forward, inverse, staged)] == [4, 4, 8], + 'literal fused and staged pass counts') + need(forward['skipped_leases'] == staged['skipped_leases'] == 2 and inverse['skipped_leases'] == 0, + 'actual encoded forward and reverse root lease schedules') + need(staged['radix_bit_control_instructions'] > forward['radix_bit_control_instructions'], + 'strictly lower measured radix instruction count') + + drop_source, _ = source_fixture(m, case) + drop_payload = m.bit_tape(initial_packet) + rekey = route.rekey_axis + + def omit_fast(m, record, layers, widths, indices, scratch, target, reverse): + if target == 0: + rekey(m, record, layers, widths, indices, scratch, target, reverse) + + with patch.object(route, 'rekey_axis', omit_fast): + drop, _drop_keep = run_leg(previous, m, route, drop_source, drop_payload) + dropped_tags = [tag for _, tag in previous.observe_payload(drop_payload, width)] + dropped_slot = dropped_tags.index(TAGS[0]) + need(dropped_slot == 4 and maps[0][0] == 5 + and dropped_tags != forward_tags and bytes(drop_source.cells) == target_source + and drop['headers'] == expected and drop['row_queries'] == 48, + 'missing fast target fails physical placement despite correct source update') + previous.reverse_order_control(m) + previous.truncated_layers_control(m) + alignment = check_header_alignment(previous, m, route, cases['growing_bank']) + + return dict(status='PASS_ENCODED_CRT_TWO_TARGET_PAYLOAD', fixture=case['name'], + moduli=case['moduli'], widths=case['widths'], reconstructed_left=left, + input_source=case['state'], forward_source=forward_state, + input_tags=list(TAGS), forward_tags=forward_tags, + forward_destinations=maps[0], inverse_destinations=maps[1], + restored_source_and_payload=True, source_retained_cells=len(source.cells), + executions=[forward, inverse, staged], + forward_radix_instructions_saved=staged['radix_bit_control_instructions'] + - forward['radix_bit_control_instructions'], + controls=dict(dropped_fast_first_tag_actual_slot=dropped_slot, + dropped_fast_first_tag_required_slot=maps[0][0], + noncommuting_row_order=True, truncated_layers_rejected=True, + ordered_header_alignment=alignment)) + + +def main(): + parser = ArgumentParser(description=__doc__) + parser.add_argument('--write-result', action='store_true') + args = parser.parse_args() + authenticate() + previous = load('leaf_replay', ROOT / PREDECESSOR) + route = load('two_target_route', HERE / 'route.py') + result = replay(previous, previous.modules(), route, retained_cases()) + result_file = HERE / 'RESULT.json' + serialized = json.dumps(result, sort_keys=True, indent=2) + '\n' + if args.write_result: + result_file.write_text(serialized) + else: + need(result_file.read_text() == serialized, 'committed exact result differs') + print(f'{result["status"]} records=16 radix_passes=4/8 ' + f'radix_instructions_saved={result["forward_radix_instructions_saved"]} controls=4') + + +if __name__ == '__main__': + main() diff --git a/research/encoded-crt-two-target-payload/route.py b/research/encoded-crt-two-target-payload/route.py new file mode 100644 index 0000000000..8bbbd51c2e --- /dev/null +++ b/research/encoded-crt-two-target-payload/route.py @@ -0,0 +1,150 @@ +"""Tape adapter for a two-target encoded CRT root. Apache-2.0.""" + +HEADER_NAMES = ('h', 'modulus', 'selected_layer', 'offsets') + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def open_root(iterator): + """Find the root by the encoded node cursor and the lease's suffix flag.""" + meters = [] + while (lease := iterator.next()) is not None: + meters.append(lease.actual.context.arena.meter) + if iterator.counters['axis'].read() == iterator.r.STEP and lease.actual.last: + return lease, meters + lease.close() + raise ValueError('encoded root lease missing') + + +def emit_axis(m, iterator, guide, header, width, combined): + """Consume the next physical right record and emit its width and modulus.""" + leaf = m.route + w, r, source = iterator.w, iterator.r, iterator.source + leaf.zero_header(header['h'], guide, w) + leaf.zero_header(header['selected_layer'], guide, w) + need(source.read() == r.ROOT, 'ordered right source record') + source.step(1) + need(source.read() == w.ONE, 'positive right source width') + width.emit('L') + while source.read() == w.ONE: + width.emit('1') + combined.emit('1') + need(not leaf.increment(header['h']), 'source width fits precision guide') + source.step(1) + need(source.read() == r.WORD_END, 'right source width delimiter') + source.step(1) + leaf.end_word(width) + + modulus = header['modulus'] + modulus.emit('L') + width.step(1) + while width.read() == '1': + bit = source.read() + need(bit in (w.ZERO, w.ONE) and guide.read() == w.ONE, + 'right modulus fits precision guide') + modulus.emit('1' if bit == w.ONE else '0') + source.step(1) + guide.step(1) + width.step(1) + need(width.read() == 'R' and source.read() == r.WORD_END, 'right modulus delimiter') + width.rewind() + source.step(1) + while guide.read() == w.ONE: + modulus.emit('0') + guide.step(1) + need(guide.read() == w.BLANK, 'modulus padding delimiter') + leaf.end_word(modulus) + guide.rewind() + + width.step(1) + while width.read() == '1': + need(source.read() in (w.ZERO, w.ONE), 'right coordinate bit') + source.step(1) + width.step(1) + need(width.read() == 'R' and source.read() == r.RECORD_END, + 'complete padded right source record') + width.rewind() + source.step(1) + + +def emit_root_headers(m, iterator, lease, headers, widths, combined): + """Copy ordered headers, consuming both fields of each live result record.""" + w, r, source = iterator.w, iterator.r, iterator.source + axis, half = iterator.counters['axis'], iterator.counters['half'] + guide, result = lease.actual.guide, lease.actual.result['stream'] + need(axis.read() == r.STEP and lease.actual.last, 'complete root interval') + while half.read() == w.ONE: + iterator._record() + half.step(1) + need(half.read() == w.RIGHT, 'complete left half') + half.rewind() + + combined.emit('L') + for header, width in zip(headers, widths, strict=True): + need(half.read() == w.ONE, 'two encoded right targets') + emit_axis(m, iterator, guide, header, width, combined) + need(result.read() == r.ROOT, 'ordered right result record') + result.step(1) + m.join.copy_numeric_field(result, header['offsets'], guide, w, r.WORD_END, '|') + m.join.skip_numeric_field(result, guide, w, r.WORD_END) + need(result.read() == r.RECORD_END, 'both right result fields consumed') + result.step(1) + half.step(1) + need(half.read() == w.RIGHT and source.read() == w.RIGHT and result.read() == w.RIGHT, + 'all right source and result records consumed') + half.rewind() + source.rewind() + result.rewind() + m.route.end_word(combined) + + +def initialize_index(leaf, index, width): + index.emit('L') + width.step(1) + while width.read() == '1': + index.emit('0') + width.step(1) + need(width.read() == 'R', 'complete encoded position width') + width.rewind() + leaf.end_word(index) + + +def skip_key_field(record, width): + width.step(1) + while width.read() == '1': + need(record.matches('0') or record.matches('1'), 'untouched key field bit') + record.move_word(1) + width.step(1) + need(width.read() == 'R', 'complete untouched key field') + width.rewind() + + +def rekey_axis(m, record, layers, widths, indices, scratch, target, reverse): + """Assign this target's field using current physical positions as inputs.""" + leaf = m.route + address, countdown, row = scratch + slow, fast = indices + for index, width in zip(indices, widths, strict=True): + initialize_index(leaf, index, width) + need(record.matches('<'), 'physical payload frame origin') + record.move_word(1) + while True: + record.pass_payload() + if target == 1: + skip_key_field(record, widths[0]) + leaf.copy_bits(indices[target], address) + leaf.route_address(m.join, layers, widths[target], address, countdown, row, reverse) + record.rekey(address) + address.erase() + if target == 0: + skip_key_field(record, widths[1]) + if leaf.increment(fast) and leaf.increment(slow): + break + need(record.matches('>'), 'payload occupies precisely the padded right rectangle') + while not record.matches('<'): + record.move_word(-1) + for index in indices: + index.erase()