From c84b0e619c4afb249fe65f568751858f5f1d0c83 Mon Sep 17 00:00:00 2001 From: Jerry Jiaheng Chen <80299683+CubeJerry@users.noreply.github.com> Date: Wed, 11 Nov 2026 22:46:30 +0800 Subject: [PATCH 1/2] Drive the padded balanced CRT inverse from encoded source and retain all 79 role histories across precision changes --- .../CHECKPOINT.json | 32 + .../INDEPENDENT-RESULT.json | 523 ++ .../INPUT-PINS.json | 84 + .../PEER-REVIEW.md | 204 + .../PR-DESCRIPTION.md | 134 + .../encoded-balanced-crt-inverse/PR-TITLE.txt | 1 + .../encoded-balanced-crt-inverse/PROOF.md | 429 ++ .../encoded-balanced-crt-inverse/README.md | 145 + .../encoded-balanced-crt-inverse/RESULT.json | 4199 +++++++++++++++++ .../encoded-balanced-crt-inverse/REVIEW.md | 80 + .../encoded-balanced-crt-inverse/SEAMS.json | 20 + .../encoded-balanced-crt-inverse/SOURCES.json | 61 + .../encoded-balanced-crt-inverse/TASK.json | 101 + .../VALIDATION.json | 50 + .../encoded-balanced-crt-inverse/VERIFY.json | 46 + .../independent_check.py | 257 + .../inverse_frontend.py | 52 + .../inverse_producer.py | 174 + .../research/crt-mixed-row-entry/bridge.py | 93 + .../crt-persistent-numerical-owner/owner.py | 77 + .../encoded-balanced-crt-endpoint/endpoint.py | 157 + .../encoded-balanced-crt-entry/frontend.py | 277 ++ .../encoded-crt-entry-lifecycle/entry.py | 117 + .../research/encoded-current-crt/producer.py | 172 + .../predecessor4025/source/records.py | 271 ++ .../predecessor4025/source/words.py | 415 ++ .../check_batched_crt.py | 265 ++ .../encoded-balanced-crt-inverse/verify.py | 429 ++ 28 files changed, 8865 insertions(+) create mode 100644 research/encoded-balanced-crt-inverse/CHECKPOINT.json create mode 100644 research/encoded-balanced-crt-inverse/INDEPENDENT-RESULT.json create mode 100644 research/encoded-balanced-crt-inverse/INPUT-PINS.json create mode 100644 research/encoded-balanced-crt-inverse/PEER-REVIEW.md create mode 100644 research/encoded-balanced-crt-inverse/PR-DESCRIPTION.md create mode 100644 research/encoded-balanced-crt-inverse/PR-TITLE.txt create mode 100644 research/encoded-balanced-crt-inverse/PROOF.md create mode 100644 research/encoded-balanced-crt-inverse/README.md create mode 100644 research/encoded-balanced-crt-inverse/RESULT.json create mode 100644 research/encoded-balanced-crt-inverse/REVIEW.md create mode 100644 research/encoded-balanced-crt-inverse/SEAMS.json create mode 100644 research/encoded-balanced-crt-inverse/SOURCES.json create mode 100644 research/encoded-balanced-crt-inverse/TASK.json create mode 100644 research/encoded-balanced-crt-inverse/VALIDATION.json create mode 100644 research/encoded-balanced-crt-inverse/VERIFY.json create mode 100644 research/encoded-balanced-crt-inverse/independent_check.py create mode 100644 research/encoded-balanced-crt-inverse/inverse_frontend.py create mode 100644 research/encoded-balanced-crt-inverse/inverse_producer.py create mode 100644 research/encoded-balanced-crt-inverse/source/research/crt-mixed-row-entry/bridge.py create mode 100644 research/encoded-balanced-crt-inverse/source/research/crt-persistent-numerical-owner/owner.py create mode 100644 research/encoded-balanced-crt-inverse/source/research/encoded-balanced-crt-endpoint/endpoint.py create mode 100644 research/encoded-balanced-crt-inverse/source/research/encoded-balanced-crt-entry/frontend.py create mode 100644 research/encoded-balanced-crt-inverse/source/research/encoded-crt-entry-lifecycle/entry.py create mode 100644 research/encoded-balanced-crt-inverse/source/research/encoded-current-crt/producer.py create mode 100644 research/encoded-balanced-crt-inverse/source/research/r437-preparation-composition/predecessor4025/source/records.py create mode 100644 research/encoded-balanced-crt-inverse/source/research/r437-preparation-composition/predecessor4025/source/words.py create mode 100644 research/encoded-balanced-crt-inverse/source/research/unconditional-batched-crt/check_batched_crt.py create mode 100644 research/encoded-balanced-crt-inverse/verify.py diff --git a/research/encoded-balanced-crt-inverse/CHECKPOINT.json b/research/encoded-balanced-crt-inverse/CHECKPOINT.json new file mode 100644 index 0000000000..6480d540ae --- /dev/null +++ b/research/encoded-balanced-crt-inverse/CHECKPOINT.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "updated_utc": "2026-11-11T14:45:43.584841+00:00", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "phase": "root_and_separate_peer_review_passed_final_package_replays_passed", + "published_forward_commit": "532b60ac427f47191175aba2e1317db0f3508d51", + "package_target": "research/encoded-balanced-crt-inverse", + "core_sha256": { + "inverse_frontend.py": "0e5f4c9450372c90000f5ebf3c22dfbe7241dd53da9ae9bcce310af859b009ef", + "inverse_producer.py": "6acdebee7134fbc8e2d121060286bd05e7282900da8a28a78c80937dde7ea178", + "verify.py": "8ca14c361bd32666e6f94b8f5827b43879ecfc6b90fc56eff5ceaf77612c902d", + "PROOF.md": "edbeb16bd8d088ab75b73b22adf5fc8aeef1ec93e8333bf74d4ad8e7f2f3d51f", + "INPUT-PINS.json": "eb9d2159d9a0a8d66470544fd9ec5bfa91898220f00139fb1bf5be80983a7646", + "SEAMS.json": "3a942dc7e32f898037362c00def8abddcfd41cf0ec3cb66899dd66c5380a9e97", + "RESULT.json": "da72e6b1660c514459e12ebf4013a41ef38855fcc9679aff6911d6f1d42c44ce" + }, + "python": "3.12.14 (main, Aug 25 2026, 14:00:49) [Clang 22.1.3 ]", + "executed_commands": [ + "python -I -W error -B verify.py", + "python -I -O -W error -B verify.py" + ], + "expected_stdout": "PASS_ENCODED_BALANCED_CRT_INVERSE cases=53 nodes=380 roles=79/158 controls=11", + "main_measured_source_actions": 85291890, + "extra_unscheduled_run_nodes": 3, + "next_action": "Publish only after exact tree and branch checks; further literal-machine refinement remains a separate research scope.", + "no_new_kappa": true, + "independent_reviews": [ + "REVIEW.md", + "PEER-REVIEW.md", + "INDEPENDENT-RESULT.json" + ] +} diff --git a/research/encoded-balanced-crt-inverse/INDEPENDENT-RESULT.json b/research/encoded-balanced-crt-inverse/INDEPENDENT-RESULT.json new file mode 100644 index 0000000000..b61341ecea --- /dev/null +++ b/research/encoded-balanced-crt-inverse/INDEPENDENT-RESULT.json @@ -0,0 +1,523 @@ +{ + "status": "PASS", + "method": "subtractive CRT idempotents plus independent global inverse reconstruction", + "cases": 20, + "nodes": 52, + "negative_controls": [ + "stale-coordinate commit rejected" + ], + "rows": [ + { + "axes": 4, + "widths": [ + 2, + 2, + 3, + 3 + ], + "nodes": 3, + "original": [ + 0, + 1, + 2, + 1 + ], + "result": [ + 0, + 1, + 0, + 0 + ], + "adapter_actions": 4983, + "numeric_actions": 326500, + "staging_backing": 48, + "staging_visited": 49 + }, + { + "axes": 4, + "widths": [ + 2, + 2, + 3, + 3 + ], + "nodes": 3, + "original": [ + 1, + 3, + 1, + 1 + ], + "result": [ + 1, + 3, + 1, + 5 + ], + "adapter_actions": 4983, + "numeric_actions": 326423, + "staging_backing": 48, + "staging_visited": 49 + }, + { + "axes": 2, + "widths": [ + 2, + 2 + ], + "nodes": 1, + "original": [ + 0, + 0 + ], + "result": [ + 0, + 0 + ], + "adapter_actions": 771, + "numeric_actions": 34410, + "staging_backing": 22, + "staging_visited": 23 + }, + { + "axes": 2, + "widths": [ + 2, + 2 + ], + "nodes": 1, + "original": [ + 1, + 2 + ], + "result": [ + 1, + 0 + ], + "adapter_actions": 771, + "numeric_actions": 34582, + "staging_backing": 22, + "staging_visited": 23 + }, + { + "axes": 2, + "widths": [ + 2, + 2 + ], + "nodes": 1, + "original": [ + 3, + 2 + ], + "result": [ + 3, + 2 + ], + "adapter_actions": 771, + "numeric_actions": 34844, + "staging_backing": 22, + "staging_visited": 23 + }, + { + "axes": 2, + "widths": [ + 3, + 3 + ], + "nodes": 1, + "original": [ + 2, + 7 + ], + "result": [ + 2, + 7 + ], + "adapter_actions": 977, + "numeric_actions": 61723, + "staging_backing": 28, + "staging_visited": 29 + }, + { + "axes": 2, + "widths": [ + 4, + 3 + ], + "nodes": 1, + "original": [ + 4, + 6 + ], + "result": [ + 4, + 1 + ], + "adapter_actions": 1080, + "numeric_actions": 80432, + "staging_backing": 31, + "staging_visited": 32 + }, + { + "axes": 2, + "widths": [ + 9, + 9 + ], + "nodes": 1, + "original": [ + 16, + 256 + ], + "result": [ + 16, + 119 + ], + "adapter_actions": 2213, + "numeric_actions": 345294, + "staging_backing": 64, + "staging_visited": 65 + }, + { + "axes": 2, + "widths": [ + 9, + 9 + ], + "nodes": 1, + "original": [ + 511, + 256 + ], + "result": [ + 511, + 256 + ], + "adapter_actions": 2213, + "numeric_actions": 346130, + "staging_backing": 64, + "staging_visited": 65 + }, + { + "axes": 2, + "widths": [ + 9, + 9 + ], + "nodes": 1, + "original": [ + 16, + 511 + ], + "result": [ + 16, + 511 + ], + "adapter_actions": 2213, + "numeric_actions": 331249, + "staging_backing": 64, + "staging_visited": 65 + }, + { + "axes": 4, + "widths": [ + 3, + 4, + 3, + 4 + ], + "nodes": 3, + "original": [ + 1, + 2, + 4, + 6 + ], + "result": [ + 1, + 0, + 3, + 0 + ], + "adapter_actions": 6219, + "numeric_actions": 529623, + "staging_backing": 60, + "staging_visited": 61 + }, + { + "axes": 4, + "widths": [ + 3, + 4, + 3, + 4 + ], + "nodes": 3, + "original": [ + 2, + 1, + 4, + 6 + ], + "result": [ + 2, + 1, + 4, + 1 + ], + "adapter_actions": 6219, + "numeric_actions": 530025, + "staging_backing": 60, + "staging_visited": 61 + }, + { + "axes": 4, + "widths": [ + 3, + 4, + 3, + 4 + ], + "nodes": 3, + "original": [ + 1, + 3, + 4, + 6 + ], + "result": [ + 1, + 3, + 4, + 1 + ], + "adapter_actions": 6219, + "numeric_actions": 527760, + "staging_backing": 60, + "staging_visited": 61 + }, + { + "axes": 4, + "widths": [ + 3, + 4, + 3, + 4 + ], + "nodes": 3, + "original": [ + 1, + 2, + 5, + 6 + ], + "result": [ + 1, + 0, + 5, + 2 + ], + "adapter_actions": 6219, + "numeric_actions": 520056, + "staging_backing": 60, + "staging_visited": 61 + }, + { + "axes": 4, + "widths": [ + 3, + 4, + 3, + 4 + ], + "nodes": 3, + "original": [ + 1, + 2, + 4, + 7 + ], + "result": [ + 1, + 0, + 3, + 7 + ], + "adapter_actions": 6219, + "numeric_actions": 517264, + "staging_backing": 60, + "staging_visited": 61 + }, + { + "axes": 4, + "widths": [ + 3, + 4, + 3, + 4 + ], + "nodes": 3, + "original": [ + 7, + 15, + 7, + 15 + ], + "result": [ + 7, + 15, + 7, + 15 + ], + "adapter_actions": 6219, + "numeric_actions": 508155, + "staging_backing": 60, + "staging_visited": 61 + }, + { + "axes": 4, + "widths": [ + 4, + 3, + 4, + 3 + ], + "nodes": 3, + "original": [ + 0, + 2, + 3, + 5 + ], + "result": [ + 0, + 2, + 4, + 5 + ], + "adapter_actions": 6219, + "numeric_actions": 530254, + "staging_backing": 60, + "staging_visited": 61 + }, + { + "axes": 4, + "widths": [ + 4, + 3, + 4, + 3 + ], + "nodes": 3, + "original": [ + 1, + 0, + 2, + 4 + ], + "result": [ + 1, + 1, + 4, + 1 + ], + "adapter_actions": 6219, + "numeric_actions": 531833, + "staging_backing": 60, + "staging_visited": 61 + }, + { + "axes": 8, + "widths": [ + 4, + 4, + 4, + 5, + 5, + 4, + 5, + 5 + ], + "nodes": 7, + "original": [ + 1, + 2, + 4, + 6, + 10, + 12, + 16, + 18 + ], + "result": [ + 1, + 0, + 3, + 0, + 2, + 8, + 12, + 0 + ], + "adapter_actions": 34085, + "numeric_actions": 5997770, + "staging_backing": 142, + "staging_visited": 143 + }, + { + "axes": 8, + "widths": [ + 4, + 4, + 4, + 5, + 5, + 4, + 5, + 5 + ], + "nodes": 7, + "original": [ + 1, + 3, + 4, + 6, + 10, + 15, + 16, + 31 + ], + "result": [ + 1, + 3, + 4, + 1, + 10, + 15, + 16, + 31 + ], + "adapter_actions": 34085, + "numeric_actions": 5869971, + "staging_backing": 142, + "staging_visited": 143 + } + ], + "pins": { + "independent_check.py": "2db9feb63c21257fc36d1db428d66f3ebf48c0c15fd6d689020b026627ea91ad", + "inverse_frontend.py": "0e5f4c9450372c90000f5ebf3c22dfbe7241dd53da9ae9bcce310af859b009ef", + "inverse_producer.py": "6acdebee7134fbc8e2d121060286bd05e7282900da8a28a78c80937dde7ea178", + "source/research/crt-mixed-row-entry/bridge.py": "89c38638c0d66da731566c903c32e7fa1ad31088d29cfd2634fce823dd07c1f9", + "source/research/crt-persistent-numerical-owner/owner.py": "1d73f432f8de9c791260c43335eb207d82bbb3f5b190cc76d0d914a4db076f41", + "source/research/encoded-balanced-crt-endpoint/endpoint.py": "c24ae2c90d175d276120438809e7c7401b8a8c04dec139f1b7345e9778984ced", + "source/research/encoded-balanced-crt-entry/frontend.py": "6ec9aab626a9d7a229b6f13ce6863e1ca77fa30ef65a4a66ae03a6ffaf2ee78c", + "source/research/encoded-crt-entry-lifecycle/entry.py": "0537ec98f306270c8ff6a424841886cf53f675d9947029347090c7dc779616d7", + "source/research/encoded-current-crt/producer.py": "88dab4ca02a92164a67826db361214fa1405e4b4a588f8c4279a21bcee95ab76", + "source/research/r437-preparation-composition/predecessor4025/source/records.py": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372", + "source/research/r437-preparation-composition/predecessor4025/source/words.py": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9", + "source/research/unconditional-batched-crt/check_batched_crt.py": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e", + "verify.py": "8ca14c361bd32666e6f94b8f5827b43879ecfc6b90fc56eff5ceaf77612c902d" + }, + "inverse_sha256": "0e5f4c9450372c90000f5ebf3c22dfbe7241dd53da9ae9bcce310af859b009ef" +} diff --git a/research/encoded-balanced-crt-inverse/INPUT-PINS.json b/research/encoded-balanced-crt-inverse/INPUT-PINS.json new file mode 100644 index 0000000000..c05a016261 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/INPUT-PINS.json @@ -0,0 +1,84 @@ +[ + { + "path": "research/r437-preparation-composition/predecessor4025/source/words.py", + "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9", + "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50", + "bytes": 13794, + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "export_path": "source/research/r437-preparation-composition/predecessor4025/source/words.py" + }, + { + "path": "research/r437-preparation-composition/predecessor4025/source/records.py", + "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372", + "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3", + "bytes": 9888, + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "export_path": "source/research/r437-preparation-composition/predecessor4025/source/records.py" + }, + { + "path": "research/encoded-crt-entry-lifecycle/entry.py", + "sha256": "0537ec98f306270c8ff6a424841886cf53f675d9947029347090c7dc779616d7", + "git_blob": "1fa2b0cb88320d4f5b623554bb0fc6de332b773c", + "bytes": 6377, + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "export_path": "source/research/encoded-crt-entry-lifecycle/entry.py" + }, + { + "path": "research/encoded-current-crt/producer.py", + "sha256": "88dab4ca02a92164a67826db361214fa1405e4b4a588f8c4279a21bcee95ab76", + "git_blob": "a327b0161eca57a1cc44ec2aa8e3defed2167ddc", + "bytes": 7891, + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "export_path": "source/research/encoded-current-crt/producer.py" + }, + { + "path": "research/crt-persistent-numerical-owner/owner.py", + "sha256": "1d73f432f8de9c791260c43335eb207d82bbb3f5b190cc76d0d914a4db076f41", + "git_blob": "20ef3519b6fef691ec92b7315e320b5e8ce9bf18", + "bytes": 2980, + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "export_path": "source/research/crt-persistent-numerical-owner/owner.py" + }, + { + "path": "research/crt-mixed-row-entry/bridge.py", + "sha256": "89c38638c0d66da731566c903c32e7fa1ad31088d29cfd2634fce823dd07c1f9", + "git_blob": "57f6853e262a6136bc616f1e47a31d0ace28495c", + "bytes": 3864, + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "export_path": "source/research/crt-mixed-row-entry/bridge.py" + }, + { + "path": "research/encoded-balanced-crt-entry/frontend.py", + "sha256": "6ec9aab626a9d7a229b6f13ce6863e1ca77fa30ef65a4a66ae03a6ffaf2ee78c", + "git_blob": "8adbe2cfef74da9854ed0b70b6c221f5746efa9f", + "bytes": 10737, + "repository": "CubeJerry/integer-mult-bounds", + "commit": "cc35ecedce6f208d5056fab6d17c58555affc73c", + "export_path": "source/research/encoded-balanced-crt-entry/frontend.py" + }, + { + "path": "research/encoded-balanced-crt-endpoint/endpoint.py", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "532b60ac427f47191175aba2e1317db0f3508d51", + "sha256": "c24ae2c90d175d276120438809e7c7401b8a8c04dec139f1b7345e9778984ced", + "git_blob": "b084d893bdb2ce5571ef00196a9ec6a60e723964", + "bytes": 6038, + "export_path": "source/research/encoded-balanced-crt-endpoint/endpoint.py" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e", + "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc", + "bytes": 11520, + "export_path": "source/research/unconditional-batched-crt/check_batched_crt.py", + "usage": "verifier oracle only" + } +] diff --git a/research/encoded-balanced-crt-inverse/PEER-REVIEW.md b/research/encoded-balanced-crt-inverse/PEER-REVIEW.md new file mode 100644 index 0000000000..eb26172f8c --- /dev/null +++ b/research/encoded-balanced-crt-inverse/PEER-REVIEW.md @@ -0,0 +1,204 @@ +# Independent proof, control and cost review of the encoded CRT inverse + +Reviewer: `/root/tape_dispatch`, separate from the author, with OpenAI +assistance for @CubeJerry's research run. Date: 2026-11-11. + +## Outcome and scope + +**PASS for the stated source-relative theorem and source-model resource +bounds. No blocking proof or control defect found.** The review preserves +the documented distinction between encoded source operations and an emitted +literal binary machine, and between the address-state inverse and a payload +converter or selected outer-caller implementation. No new kappa follows. + +This review read the changed frontend and producer, the entire proof, and the +unchanged frontend, endpoint writer, owner, entry adapter, word arithmetic and +record routines. It independently traced the symbolic control and lifecycle +invariants and checked the cost/space sums below. It did **not** rerun the +author's tests or use them as proof. The orchestrator's separate numerical +inverse/CRT-idempotent execution is complementary evidence, not an experiment +performed by this reviewer. + +The reviewed frozen package is `work/analytic_recovery/encoded_crt_inverse` +on scientific base `e54523517d0f03e58352e647c403a5af3e525a57`: + +| File | SHA256 | +| --- | --- | +| `inverse_frontend.py` | `0e5f4c9450372c90000f5ebf3c22dfbe7241dd53da9ae9bcce310af859b009ef` | +| `inverse_producer.py` | `6acdebee7134fbc8e2d121060286bd05e7282900da8a28a78c80937dde7ea178` | +| `PROOF.md` | `edbeb16bd8d088ab75b73b22adf5fc8aeef1ec93e8333bf74d4ad8e7f2f3d51f` | + +Static authentication independently matched all nine exported inputs by +byte length, Git blob and SHA256 against `INPUT-PINS.json`. A byte comparison +also confirmed that the producer is exactly the original source with the two +declared credit comments and its one add-to-subtract replacement. No author +file was edited. + +## 1. Reverse topology and the half-size invariant + +The base `_shape` leaves the unary depth word `ONE^k RIGHT`, half-size one, +the first axis marked STEP, and all relevant heads at one for d=2^k. The new +constructor moves the depth head once, explicitly calls the **base** doubling +method for each remaining ONE, sees RIGHT and rewinds. Therefore it makes +exactly k-1 doublings and initializes H=d/2. For d=2 it makes none. Explicit +base-method dispatch prevents the new halving override from running during +bootstrap. + +At a level, unchanged `NodeEntry` scans exactly two H-axis blocks and records +only the next start via VALUE. `_advance` either moves STEP to that marker or +finishes the level, advances depth by one token, and invokes the override. +The override scans H unary tokens with a finite parity flag and emits H/2 +tokens. The even/nonempty checks are valid: a transition is needed only when +another depth token remains, which means H>=2. The old half stream is cleared, +the temporary is copied back, both delimiters are manufactured explicitly, +and the temporary is cleared. All heads return to one. + +The resulting widths are d/2,d/4,...,1, with increasing aligned starts at each +level. Their node counts are 1,2,...,d/2, summing to d-1. No new Port, per-level +inventory, decoded level, start or host node list enters this construction. +The inherited temporary is empty after each base doubling and each halving, +so the next append is to blank space. Its older erased suffix is not rescanned +or discarded. + +## 2. Subtraction and current-left reconstruction + +The inherited reconstruction loop maintains a prefix product and adds + + prefix * ((x_i - lower*prefix^-1) mod s_i) + +to `lower`. The new value is below `prefix*s_i`, preserves the earlier +congruences, and is congruent to `x_i*prefix` modulo s_i. This proves the +current-coordinate congruences used in section 2 of the proof. Even if a left +coordinate is padding, its arithmetic uses its reduced digit, so intermediate +capacity remains valid before the final `left_valid` branch sets lower to zero. + +The right prefix includes every preceding right modulus, independent of +coordinate validity. The inverse changes only the final rotation to +`(canonical-offset) mod modulus`. For fixed current left coordinates, this +is exactly the inverse of the old positive rotation on valid right values; +padded right values are copied unchanged. The offset record remains the same +positive offset, which is correct because the writer skips that field and +copies the separately serialized updated value. + +The modular subtraction seam is safe in both branches. For 0<=u,v=v. Otherwise `(u+s)-v` lies in [0,s), and +u+s<2s<2^P_G, so the inherited word addition cannot overflow. It needs at most +two newly live words, then frees the intermediate. The old add-and-reduce +branch also permitted two words at its peak. Borrowed operand heads return +through the same raw arithmetic methods. Thus neither the inventory bound nor +the inherited linear modular-primitive class is enlarged. + +Each node fixes its left coordinates; nodes within a level have disjoint +support and controls. Consequently reversing the level order and inverting +the right rotations gives both composition identities on the full padded +rectangle. A globally invalid input need not be fixed by every lower node; +the proof correctly avoids that stronger false assertion. + +## 3. Staging, retired commits and exact physical restoration + +The unchanged writer stages the complete next logical source while the current +numerical lease remains live. It writes only the staging role and restores +source/result/guide/axis/half heads before returning. `lease.close()` consumes +the numerical output, retires guide/canonical input/guard data, releases the +bank and advances the topology. Only then can `commit()` write the staged +source. The final-node case is valid even if topology has already retired: +commit requires only source and staging. + +All source headers, widths, moduli and delimiters are copied unchanged. Only +the prescribed coordinate fields differ. The staged source has exactly the +same logical extent, so commit writes within existing source backing and does +not grow or replace it. It never accesses the historical nonblank tail after +RIGHT. The next numerical entry reads coordinates from the actual committed +source, including after undoing the root; it does not reuse earlier left +coordinates or a cached reconstruction. + +Projection remains valid with subtraction. Every updated valid value is below +s_i<2^h_i, and every unchanged padded value is below 2^h_i. Their higher +P_G-h_i bits are zero, precisely the writer's existing checked projection +condition. There is no signed output or extra field to transport. + +## 4. Precision shrinkage followed by regrowth + +The proof correctly separates level boundaries from successive nodes. For +widths (2,2,3,3), the reverse sequence is exactly 11,5,7. In general the +minimum width m is at least two, and an n-axis level has minimum precision +1+nm while the next level has maximum 1+(n/2)(m+1). The asserted strict +cross-level decrease by at least n(m-1)/2 is correct. It does not imply +within-level monotonicity. + +I checked the actual entry/owner methods for the required regrowth. Every +guard is rebuilt from the current unary guide; RIGHT is placed at the current +P_G+1, not at the far end of historical backing. Each numerical word uses the +current template and current RIGHT delimiter. `Word.msb`, `erase`, arithmetic +loops and `Port.clear` stop at current symbols. They do not use the historical +last allocated cell as the current precision. + +On retirement, every live current word and its delimiter are erased. Any +older suffix was already erased on its previous retirement. Hence decreasing +11 to 5 exposes only blank old tail, and increasing 5 to 7 reuses blank cells +without a stale delimiter or digit. This induction also explains why retirement +need not scan the whole largest historical extent at every smaller node. +The bank's local blank checks alone would not prove the invariant; the +producer/entry erasures supply the missing global induction. + +## 5. Complete time and capacity accounting + +The new half-size work is linear in its processed unary lengths. Bootstrap +lengths sum to less than d/2; descending input lengths sum to less than d. +The displayed loops perform a fixed number of symbol operations per token, +including temporary copies, rewinds and `clear`. The conservative 1024(d+2) +additional raw-action allowance is sufficient. The old writer/frontend +2^18(M+2)^2 envelope therefore fits within the new 2^19(M+2)^2 raw allowance. +The unknown finite-control refinement constant C_inv is explicitly retained. + +The new subtraction uses only a comparison, one or two inherited linear +word operations, and at most one intermediate-word erasure. It stays inside +the existing modular subtraction tariff and the old two-temporary-word +envelope. The numerical proof may therefore retain its structural degree +bound; the new 2^21(P_G+2)^4 allowance is conservative. There is no basis here +to cancel any entry, owner-release or source-copy occurrence. + +I independently recomputed the writer sum. At n-axis level, the groups +partition the widths, so their total n(P_G+2) is 3d+nA. Summing n=2,4,...,d +gives exactly + + 3d log2(d) + 2A(d-1). + +There are d-1 complete M-sized source stagings/commits. With A>=2d and +M=2+3A+4d, these are quadratic source costs. For the numerical terms, +P_G+2<=3nm and the geometric cube sum is less than 8d^3/7. Thus the stated +fourth-power total is less than (648/7)A^4. The squared total is O(A^2). +These calculations establish the complete O(A^4) source budget as stated, +not a new multiplication rate. + +The 63-role numerical history expression has the correct inventory: one +guide, two canonical source streams, 56 numerical words plus one template, +and three padded/result streams. The eight protected guards and seven +topology roles are additional, and the staging role brings the total to 79. +Every term bounds a maximum for its physical role across the full invocation; +precision shrinkage does not delete old backing. The new half-size temporary +stays within its old d+2 allowance. + +The staging allocation is at most M stored cells but can visit head index M. +The proof explicitly distinguishes M allocated cells from M+1 visited cells, +and does not relabel this mixed predecessor backing model as a literal binary +space certificate. That qualification is necessary and correctly retained. +An arbitrary source history is separately charged by K_source. Two fresh +invocations retain both 79-role inventories: K_source+2D and 158 private +histories. Reusing one inventory is not established or silently credited. + +## Acceptance boundary + +The result is accepted under the stated successful linear-use lifecycle, +valid source framing/coprimality/width promises, clean initial private +inventory and pinned numerical/entry/owner source contracts. Arbitrary dirty +acquisition, stale borrowed handles, malformed-input rollback, crash recovery, +same-bank restarting, payload routing, common global-row choreography and +selected caller admission remain outside the theorem. + +The proof appropriately claims a finite-symbol **source-relative** evaluator +and source-operation costs. It does not supply an emitted common binary +instruction table or numerical value for C_inv. The independent numerical +checker may strengthen executable evidence, but it does not change this +computational-model boundary. No further author correction is requested by +this review for the pinned snapshot. diff --git a/research/encoded-balanced-crt-inverse/PR-DESCRIPTION.md b/research/encoded-balanced-crt-inverse/PR-DESCRIPTION.md new file mode 100644 index 0000000000..3f3452c7a5 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/PR-DESCRIPTION.md @@ -0,0 +1,134 @@ +## Result + +This supplies the encoded reverse schedule and subtractive whole-node consumer +left open by the [source-pinned forward endpoint](https://github.com/CubeJerry/integer-mult-bounds/tree/532b60ac427f47191175aba2e1317db0f3508d51/research/encoded-balanced-crt-endpoint). +On that same padded owned-source interface, the actual encoded program now +evaluates the inverse balanced CRT address-state map, and both compositions +are identity on the entire admitted padded rectangle. Runtime receives no +decoded node start, level, precision, coordinate or traversal list. + +**No new kappa.** This is a source-relative construction and ownership/precision +proof, not a complete multiplication theorem. The selected conditional bound +and all five foundational assumptions are unchanged. + +## Exact changes and why they matter + +- Add a fixed encoded reverse frontend. It uses the physical depth stream to + manufacture the root half-size and performs paid unary halving between + levels. It inherits every other #7154 frontend method unchanged. +- Specialize #5053 by one authenticated scientific line: use its already + proved modular subtraction for the whole-node updated coordinate. Current + left reconstruction, positive offsets, padded-right handling and lifecycle + code remain unchanged. +- Reuse the published forward projection/retirement/commit writer byte for + byte. Source mutation happens only after the numerical result is retired; + the next node rereads the actual current source. +- Prove the complete source-model O(A^4) bill and K_source+O(A^2) retained + backing, including source copying, guards, head returns and cleanup. There + are 79 private roles per invocation. Fresh forward/inverse round trips + retain **158 histories**; no unproved restart discards the first inventory. + +Precision decreases across levels, but can regrow within a level: declared +widths (2,2,3,3) give the inverse precision sequence 11,5,7. The proof and +checks use exact current extents and preserve/clear every older history. + +## Novelty and pinned predecessors + +#4100 and #4195 already establish balanced inverse algebra and logical padded +callers. #7152 already gives complete physical forward/reverse source-state +trees at compiled geometry; #7154 gives an encoded forward iterator. This +package supplies their narrowly scoped encoded reverse join on the published +forward writer's same physical interface. It does not claim those earlier +inverse results again. + +#4024 already provides an encoded bidirectional triangular payload converter, +used after recovery by #5095. Its format, padded extension and routing contract +are different. The raw compact macro inverse in #4169 is another separate +interface. This helper does not substitute for either cost or caller proof. + +Canonical base: `e54523517d0f03e58352e647c403a5af3e525a57`. +The #7154 frontend is pinned at `cc35ecedce6f208d5056fab6d17c58555affc73c`; +the unchanged forward writer at `532b60ac427f47191175aba2e1317db0f3508d51`; +the #7152 comparison source at `66adbede4bd4ab603ba3e0a7f6708403905b753c`. +All nine byte-exact exports are authenticated by SHA256 and Git blob in +`INPUT-PINS.json`; the numerical specialization is checked byte for byte. + +## Reproduction and executed checks + +From `research/encoded-balanced-crt-inverse`, Python 3.12, standard library: + +```sh +python3.12 -I -W error -B verify.py +python3.12 -I -O -W error -B verify.py +``` + +Both executed modes produce: + +```text +PASS_ENCODED_BALANCED_CRT_INVERSE cases=53 nodes=380 roles=79/158 controls=11 +``` + +The bounded family covers both composition orders on all 32 padded pairs for +(3,5), fifteen four-axis states, four composite-modulus states and two eight-axis +states. An independent exhaustive congruence oracle checks every current node; +the pinned balanced oracle checks complete endpoints. A separate actual +`run()` test supplies no iteration count or schedule. The main family measures +85,291,890 source actions; no universal bound is inferred from that number. + +Eleven controls detect wrong level order/sign, stale pre-root left data, old +precision, dirty older tails, an extra physical role, wrong unary transition, +silently forgotten backing, original/current-coordinate confusion, a global +invalidity shortcut and premature source writing. Checks preserve source +metadata and nonblank inaccessible tails, all boundary heads, role identities, +current guard extents and both inventories' historical capacity. Runtime host +geometry names are poisoned and new physical constructors sealed after entry. + +## Limits and open obligations + +This evaluates one address-state vector. It supplies neither payload routing +nor a raw compact inverse, exceptional-key epoch or full selected caller. +Source construction in the admitted encoding, clean private acquisition, +binary lowering and analytic/integer-recovery obligations remain explicit. +Same-bank restart is not established; failure controls are not universal +malformed-input or crash rollback. The numerical value of the complete +finite-control refinement constant is not certified. Finite tests and AI +review are not proof-kernel or independent human acceptance. + +`PROOF.md` contains the quantified proof and complete bill. `TASK.json` records +the open caller join, restart, balanced payload scheduling and binary-tariff +questions with their first steps and blockers. + +## Credit + +Prepared for Jerry Chen / @CubeJerry with substantial OpenAI assistance. +Retain the #7154/#7152 and published forward-endpoint work prepared for +CubeJerry; JoyboyBrian's #5053/#5219/#5505 numerical, entry and owner contracts; +Ali Romman's #5353 encoding and #5625 retired-write boundary; Cinna Davis's +#4100 balanced construction; Hiroki KUMAZAKI's current-state/mixed-width/raw +inverse work; Tekalign's #4024 converter; ToikY's arena lineage; +commdata2338's history accounting; and every unchanged source notice. +Apache-2.0. The known CRT inverse identities are credited predecessors; the +contribution is this exact encoded reverse consumer and its lifecycle proof. + +## Independent acceptance checks + +The orchestrator's [REVIEW.md](REVIEW.md) and separate +[PEER-REVIEW.md](PEER-REVIEW.md) accept the frozen source-relative theorem. +The peer authenticated all nine exports and independently checked reverse +control, current-left reconstruction, retirement, precision regrowth and +complete cost/history sums without rerunning the author verifier. + +A separate CRT-idempotent and global mixed-radix inverse oracle passes 20 +cases and 52 actual nodes, including padded axes, eight-axis cases, widths +up to nine bits, historical tails, the 11,5,7 precision sequence and a rejected +stale-coordinate mutation. Its portable command is: + +```sh +python3 -I -W error -B research/encoded-balanced-crt-inverse/independent_check.py +``` + +`INDEPENDENT-RESULT.json` records the full domain and exact code hashes. +The author normal and optimized replays also pass from this final packaged +directory with identical output. These are independent AI checks; no human +or formal-kernel acceptance is claimed. The full proposed PR description +is committed in `PR-DESCRIPTION.md`. diff --git a/research/encoded-balanced-crt-inverse/PR-TITLE.txt b/research/encoded-balanced-crt-inverse/PR-TITLE.txt new file mode 100644 index 0000000000..568d8bcd01 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/PR-TITLE.txt @@ -0,0 +1 @@ +Drive the padded balanced CRT inverse from encoded source and retain all 79 role histories across precision changes diff --git a/research/encoded-balanced-crt-inverse/PROOF.md b/research/encoded-balanced-crt-inverse/PROOF.md new file mode 100644 index 0000000000..281cd5ea86 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/PROOF.md @@ -0,0 +1,429 @@ +# Uniform encoded inverse of the padded balanced CRT address-state map + +Prepared for Jerry Chen / @CubeJerry with substantial OpenAI assistance. +Apache-2.0. Canonical base: `e54523517d0f03e58352e647c403a5af3e525a57`. +This is a source-relative inverse construction, **no new kappa**. + +## 1. Exact claim, full budget and dependencies + +Use the physical padded axis encoding of CrocSwap/integer-mult-bounds#5353 +and CrocSwap/integer-mult-bounds#7154. There are d >= 2 axes, d is a power +of two, widths h_i belong to {ell-1,ell}, ell >= 2, the moduli satisfy +2 <= s_i < 2^h_i and are pairwise coprime, and 0 <= x_i < 2^h_i. These +conditions imply h_i >= 2. The physical records, including their unary +widths, modulus bits, coordinate bits and delimiters, are already supplied. +The source head enters at one. Put + + A = sum_i h_i, M = 2 + 3A + 4d, + P_G = 1 + sum_(i in G) h_i, P* = A+1. + +The source has a retained backing of K_source >= M cells. Its inaccessible +historical tail after RIGHT can be nonblank and is preserved and charged. +Private backing enters clean. Each numerical invocation borrows the source +read-only; the enclosing endpoint evaluator owns source mutation. + +**Theorem, relative to the pinned source contracts.** Binding +`inverse_frontend.bind(frontend)` and `inverse_producer` into the unchanged +published `endpoint.Endpoint` gives a fixed finite-symbol evaluator of the +complete inverse of the padded balanced CRT address-state map. `run()` +takes no node list, level, start, precision or runtime numerical parameter. +It enumerates decreasing balanced levels and increasing starts within each +level, reading the actual current source at each node. On the whole padded +rectangle both compositions with the pinned forward evaluator are identity. + +Only coordinate bits change during an invocation. All other source bytes, +backing identity, backing length and the incoming head are preserved. The +invocation uses exactly 79 private roles, and every historical private cell +is blank with its head at one at successful completion. A fresh forward +invocation followed by a fresh inverse invocation has **158 retained private +histories**, not 79. Reusing one retired inventory for a second invocation +is not established here. + +The complete source-operation bound is + + C_inv (M+2)^2 + 4096 + + sum_G [2^21(P_G+2)^4 + 2^16(P_G+2)^2 + 4096]. (1) + +C_inv is a fixed input-independent control refinement constant, whose exact +value is not certified. The raw frontend/adapter reads, writes and unit +moves fit 2^19(M+2)^2; (1) adds numerical, entry and owner traffic. Section +6 proves O(A^4) source time and K_source + O(A^2) retained backing. Thus +A <= p gives an O(p^4) helper bill in this source model. No selected +application is charged this bill without a separately proved caller join. + +### Exact changed and unchanged sources + +`INPUT-PINS.json` records nine byte-exact exports by repository, commit, +Git blob and SHA256. The forward writer is unchanged from +CubeJerry/integer-mult-bounds commit +`532b60ac427f47191175aba2e1317db0f3508d51`, +`research/encoded-balanced-crt-endpoint/endpoint.py` (SHA256 +`c24ae2c90d175d276120438809e7c7401b8a8c04dec139f1b7345e9778984ced`). +Its frontend is the unchanged CrocSwap/integer-mult-bounds#7154 source at +`cc35ecedce6f208d5056fab6d17c58555affc73c`. Its numerical, entry, owner, +word, record and canonicalization sources are pinned at the canonical base. + +There are exactly two implementation seams, described in `SEAMS.json`. +The new frontend subclasses the pinned frontend, changes initial half-size +manufacture, and overrides the existing level-transition hook with unary +halving. Every other method is inherited unchanged. The inverse producer +is the original CrocSwap/integer-mult-bounds#5053 producer with two credit +comments and exactly one scientific line changed: + + updated = a.add(canonical, offset, modulus) + updated = a.subtract(canonical, offset, modulus) + +The verifier checks this replacement byte for byte. The already present, +proved modular-subtraction implementation is unchanged. The ninth export, +canonical `unconditional-batched-crt/check_batched_crt.py`, is a verifier +oracle only; none of its host geometry or numerical values enters runtime. + +### Predecessors and scope of novelty + +CrocSwap/integer-mult-bounds#4100 already gives the reverse-level, +subtractive balanced algebra. CrocSwap/integer-mult-bounds#4195 already +supplies a logical mixed-width forward/reverse caller on padded addresses. +CrocSwap/integer-mult-bounds#7152, pinned at +`66adbede4bd4ab603ba3e0a7f6708403905b753c`, supplies physical forward and +inverse complete source-state trees using compiled geometry and 127 roles. +CrocSwap/integer-mult-bounds#7154 supplies encoded forward node selection. +The published forward writer explicitly leaves this reverse encoded +schedule/subtractive consumer as its first open next question. + +CrocSwap/integer-mult-bounds#4024 already has an encoded bidirectional +triangular payload converter. Its original-lower-coordinate format, +payload/router contract and padded extension are different. The inverse +consumer in CrocSwap/integer-mult-bounds#5095 uses that converter after +integer recovery. No first CRT inverse or first encoded inverse is claimed. +The raw compact macro S^-1 in CrocSwap/integer-mult-bounds#4169 is another +different interface; this package cannot be substituted for its invoice. + +The new result is the exact encoded reverse join on the published forward +writer's same owned-source interface, including current-left reconstruction, +real precision changes, retired source commits and full history accounting. +It supplies no physical payload conversion, synchronized row schedule, +exceptional-key epoch, raw compact macro or selected outer caller. + +## 2. One inverse node and the full padded permutation + +Let G=[a,a+2H), with left child L and right child R. In the current source, +the pinned producer reconstructs k_L in [0,S_L), S_L=product_(i in L)s_i, +from the left coordinates. If any of those coordinates is invalid padding, +it uses k_L=0. Otherwise the defining congruences are + + k_L = x_i product_(a <= j < i)s_j (mod s_i), i in L. (2) + +These are current transformed coordinates, not original mixed-radix +digits. The source reconstruction loop is unchanged. For each right axis +i, define Q_i=product_(a <= j < i)s_j and + + c_i = k_L Q_i^-1 mod s_i. + +Pairwise coprimality gives the inverse. Every preceding right modulus is +included in Q_i, regardless of coordinate validity. The changed output is + + y_i = (x_i-c_i) mod s_i, if x_i < s_i; + y_i = x_i, if x_i >= s_i. (3) + +For 0 <= u,v < s, the inherited `Arithmetic.subtract(u,v,s)` computes +u-v directly when u>=v, and (u+s)-v otherwise. In the second branch +u+s<2s<2^P_G, so the raw addition cannot overflow. Both branches return +the unique representative in [0,s). The second branch needs at most two +new numerical words at once, just as the old add-and-reduce branch. It +uses the same borrowed operands and returns their heads. The unchanged +producer frees these words and serializes its positive offset followed +by the new coordinate. No offset is negated in the stored offset field. + +Because (3) is in [0,2^h_i), all bits above the declared destination width +are zero. The unchanged writer can therefore use exactly its existing +projection: skip the full P_G-bit offset, copy h_i updated bits, and reject +any nonzero high remainder. Invalid right padding is copied unchanged. + +For fixed left coordinates, the forward and inverse node maps keep the +left child unchanged and apply inverse rotations to each valid right +coordinate, fixing its padded values. Their controls depend only on the +unchanged left child and moduli. Thus they are mutual inverses on the +entire padded product, even when the left child is invalid. Different +nodes of one level have disjoint support and controls, so commute. + +Writing F_j for the complete forward level j, the forward endpoint is +F_k ... F_1, k=log2(d). Its inverse is F_1^-1 ... F_k^-1, executed by +levels k,k-1,...,1. This proves both composition identities once Sections +3-4 establish that the physical reverse caller uses these actual maps +in this order. It does not require the input to be in the all-valid box. + +In particular, global invalidity does not make the whole inverse identity. +For moduli (2,3,5,7), widths (2,2,3,3), the input (1,3,1,1) maps under +the inverse to (1,3,1,5): an invalid left subtree disables its parent +offset, while the disjoint valid right-child node still acts. Conversely, +subtracting at forward rather than reverse levels is wrong: the forward +image (0,1,2,1) of (0,1,0,0) would return (0,1,0,1). + +## 3. Encoded descending topology without a traversal list + +The inherited `_shape` reads the actual stream and establishes d=2^k, +k>=1, by repeated exact unary halving. It leaves k ONE tokens on `depth`, +one ONE on `half`, and a unique STEP at the first axis on `axis`. All +heads are at one; the temporary `double` role is blank. These are actual +symbol streams, not decoded k, d or H. + +The reverse constructor steps past the first depth token, then invokes +the *base* doubling method once for each remaining ONE. This produces +H=2^(k-1)=d/2 on `half`, sees RIGHT after exactly k-1 doublings, and +restores `depth` to one. At d=2 there are no doublings. No new tape or +iteration counter is acquired; the existing depth stream drives the work. + +At the j-th processed level, the invariant is: + +1. `half` contains H=2^(k-j) ONE tokens followed by RIGHT, at head one. +2. STEP marks the first axis of the current aligned group of 2H axes. +3. The inherited scanner's temporary VALUE, when present during a lease, + marks exactly the next group start; there is no saved node list. +4. `depth` is on its j-th ONE token and the numerical bank is retired + outside the single active lease. + +The inherited `NodeEntry` consumes two passes over the encoded half-size, +copies the actual chosen source fields and derives its precision guide +from their actual unary widths. The same marker argument as the forward +frontend visits increasing group starts without host indices. On closing +a nonlast node, unchanged `_advance` moves STEP to the saved VALUE. + +On closing the last node of a level, `_advance` consumes one depth token. +If it sees RIGHT, it retires all topology roles and ends the traversal. +Otherwise it calls the overridable `_double_half` hook. In this adapter +that compatibility hook performs **halving**: a finite parity flag emits +one ONE to `double` per pair of ONE tokens in `half`, checks an even +nonempty result, clears the old logical half word, copies the temporary +back, and clears the temporary. The inherited code then places STEP at +the first axis. H is at least two whenever this transition is needed. +Startup explicitly calls the base method, so cannot invoke this halving +hook accidentally. This proves the invariant and exactly d-1 nodes. + +All accesses are local symbols, unit moves and fixed-role calls. The +subclass has no decoded precision, axis count, level or start and no +host sequence of nodes. The module factory fixes a provider class, not +runtime geometry. The inherited Python lease objects retain only the +current linear-use continuation; no unbounded stale-object history is +being compiled into constant space. + +## 4. Current source, exact precision and retired writes + +Every node uses the unchanged forward writer's full-source staging +protocol. While the lease is live, `stage` copies all source fields to +its separate role, replacing only the right coordinates by (3), and +returns the source, result, guide, axis and half heads. It does not write +the source. The lease then retires its numerical result, canonical input, +guide and guards, releases the physical bank, and advances topology. +Only after that close may `commit` copy the equal-length staged source +to the original backing and erase staging completely. + +Source headers, widths, moduli, record delimiters and logical extent are +unchanged, so the encoded topology's invariant is preserved by commit. +The next `NodeEntry` rereads coordinates from that actual source; it +caches neither old digits nor an earlier reconstructed left integer. +This applies after undoing the root as well as between lower nodes. The +last lease may clear all topology before commit because commit reads +only the staged word and source. The unchanged writer therefore needs +no reversal-specific cursor or cleanup change. + +For each new node, actual precision remains exactly P_G. With +m=min_i h_i>=2, all widths lie in [m,m+1]. An n-axis level has +P_G>=1+nm, while the next descending level has +P_G'<=1+(n/2)(m+1). Hence + + P_G - P_G' >= n(m-1)/2 > 0. (4) + +This is a decrease across a level boundary. There is **no** assertion +that successive precisions within a level decrease. Widths (2,2,3,3) +produce reverse precisions 11,5,7; the larger example includes +36,17,20,9,9,10,11. Thus the implementation must handle shrinkage followed +by regrowth on the same retained roles. + +The inherited guide and protected-word preparation uses the exact current +guide each time. The owner retires every previous live extent before a +new one is admitted, and all older cells beyond that extent are already +blank. A shorter current word therefore exposes no old data. A later +larger one reuses blank backing or extends it through local writes. The +eight guards have current RIGHT exactly at P_G+1; a historic root marker +cannot substitute for that delimiter. Full historical backing, including +the root's largest allocation, remains in the space invoice after erasure. + +Induction on the encoded schedule now establishes (2)-(3) from the actual +source left by all prior commits, preserves the physical source invariant, +and proves the complete inverse endpoint asserted in Section 1. + +## 5. Ownership and the failure boundary + +The same fixed inventory is used: 63 physical numerical-bank roles, +eight guards, seven topology roles and one full-source staging role. +The reverse bootstrap and halving reuse `depth`, `half` and `double`. +No new word, arena, Port or provider is acquired per level or node. + +The interface is the successful linear-use lifecycle of `step`/`run`. +Internal `stage` consumes this endpoint's current lease once; clients +must not bypass the endpoint, keep stale borrowed aliases or mutate its +ports between phases. A live result prohibits source commit. Each +successful step erases staging, numerical and guard roles, and the final +step additionally erases topology. Source head and all retired heads +return to one. None of those erasures shortens or forgets backing. + +For a fresh forward/inverse pair, retain the complete first inventory +while acquiring the second. The two inventories are disjoint and both +stay charged and blank at the final boundary. This gives 158 private +histories. A same-bank restart, arbitrary dirty-private-memory acquisition, +crash recovery and numerical-premise failure rollback are separate tasks. +The negative controls establish failure detection at named boundaries, +not a universal rollback or malformed-stream termination theorem. + +## 6. Complete source time and retained capacity + +All inherited costs remain charged: source scans, canonicalization, +exact-width guards, numerical production, output consumption, head +returns, owned erasure and bank release. The unchanged writer additionally +pays full-source staging, projection and same-source commit at every node. + +The inverse numerical seam uses an already proved operation. The pinned +#5053 numerical proof bounds **both** modular addition and subtraction by +2048(P+2) source operations, including their initialization and erasure. +Its slot schedule allows at most 24 newly live words plus eight borrowed +words. The changed line fits that same operation and two-temporary-word +envelope. There is no new arithmetic loop, additional axis pass, larger +word or new output field. Consequently the structural numerical proof +continues to apply; (1) conservatively allows twice its 2^20(P+2)^4 +bound. Entry still contributes 2^16(P+2)^2, and the physical owner still +contributes 4096 initially and per node. + +The reverse bootstrap doubles half sizes 1,2,...,d/4, whose sum is less +than d/2. Descending transitions halve d/2,d/4,...,2, whose sum is less +than d. The displayed unary loops use a fixed number of scans, copies, +rewinds and erasures per processed token. Bounding this extra work by +1024(d+2) raw Port actions leaves ample slack inside 2^19(M+2)^2 after +the forward writer/frontend's 2^18(M+2)^2 envelope. Reverse node order +does not change the multiset of selected groups or paid source scans. + +For completeness, the writer's per-node raw bill is at most + + 2048[M+n_G(P_G+2)] + 32, (5) + +where n_G is its number of axes. It includes source copying, skipped +offset bits, full updated-field validation, width manufacture/erasure, +all cursor/guide/result returns, source writing and staging erasure. Over +all balanced groups, + + sum_G M = (d-1)M, + sum_G n_G(P_G+2) = 3d log2(d) + 2A(d-1). + +Thus this entire added copying cost is O(A^2), not one uncharged copy at +the endpoints. All variable controller loops read a local symbol; their +role selectors, parity flags, phase state and call depth are fixed. +Expanding the fixed control supplies C_inv in (1). This is a fixed-alphabet +source tariff, not a count of Python instructions or binary-TM transitions. + +The numerical sum is O(A^4) uniformly in the admitted widths. At an +n-axis level there are d/n groups. With m=min_i h_i>=2, +P_G+2<=n(m+1)+3<=3nm for n>=2, and A>=dm. Therefore + + sum_G (P_G+2)^4 + <= 81 d m^4 sum_(n=2,4,...,d) n^3 + < (648/7) d^4 m^4 <= (648/7) A^4. (6) + +The analogous squared sum is O(A^2); M=O(A) because d<=A/2. This proves +the full asymptotic bound, including the helper work, under the stated +source-model premises. It does not improve a multiplication recurrence. + +The inherited numerical history envelope at P*=A+1 is + + B_num = (P*+1) + 2(2A+2d+2) + 57(P*+2) + + 3[d(P*+2)+2]. + +Let + + D = B_num + 8(P*+2) + 6(d+2) + (A+2) + M. (7) + +The retained-backing bound for one invocation is K_source+D. The seven +topology terms cover six count/position roles and the reused width role. +The reverse temporary never exceeds the already allowed d+2. Staging +retains exactly its at-most-M backing cells. Appending or erasing its +last delimiter can visit head index M, so a literal visited-span invoice +uses M+1 for that role instead; the other terms keep their predecessor's +declared backing model. This is not a literal binary space certificate. + +Every term is a maximum for one physical role over its whole history. +Shrinking a current word and erasing old bytes subtract nothing from (7). +A fresh two-invocation round trip has K_source+2D, with the source counted +once and all 158 private histories counted. Even though its endpoint +restores the initial coordinates, its source time is the sum of both +invocation bills, including both shape constructions and cleanups. + +## 7. Executed evidence and limits + +`verify.py` authenticates nine exports and the exact one-line producer +change. The runtime frontend, inverse adapter and unchanged writer have +host geometry/decode names poisoned. After initial fixed acquisition, +constructors for Ports, numerical Words and Arenas are sealed, and runtime +`Word.inspect` is prohibited. These controls accompany the written +finite-control argument; name poisoning alone is not a compiler proof. + +The main fixed domain has 53 input fixtures: all 32 padded pairs for +moduli (3,5), fifteen four-axis cases for (2,3,5,7), four composite-modulus +cases for (4,9), and two eight-axis mixed-width cases. Each fixture runs +both F^-1(F(x)) and F(F^-1(x)) with fresh real inventories: 380 actual +numerical nodes. Nonblank source tails of lengths 17,23,31 and 97 remain +intact. At each node an independent exhaustive congruence oracle computes +the current-left integer and offset, without supplying a runtime value. +The complete endpoint also agrees with the pinned `balanced(reverse=True)` +oracle. Every source mutation, head, role identity, historical length, +exact current guard extent and final cleanup is checked. + +A separate three-node test calls `endpoint.run()` without any supplied +iteration count or node schedule, while the same constructor/decode seals +remain active. It returns (0,1,0,0) from (0,1,2,1) and retires all 79 roles. +This makes explicit that observer-side loops in the main tests do not +perform production traversal. + +Eleven controls reject forward level order with subtraction, addition in +inverse nodes, stale pre-root left data, old root precision at a smaller +node, nonblank older guard tails, a hidden fresh Port, doubling instead +of halving, silently shortened backing, current coordinates misread as +original digits, a global-invalid identity shortcut, and source commit +before numerical retirement. The stale-left mutant still runs the actual +encoded numerical producer on a deliberately wrong borrowed descriptor; +it is not replaced by an oracle that manufactures the expected failure. + +Finite cases and AI cross-review corroborate this source-relative proof; +they do not establish independent human or proof-kernel acceptance. The +five foundational assumptions, selected certificate and complete kappa +are unchanged. No analytic accuracy, integer recovery theorem, payload +transport or all-size compiler theorem follows solely from this package. + +## Open next questions + +1. Bind one actual exceptional-key caller to this admitted source encoding, + paying source production, representation conversion, return transport + and its raw compact macro costs. This is required before a selected + caller can use the helper; generic inverse endpoint equality is not + that interface proof. +2. Prove a persistent restart interface that reinitializes the existing + 79 retired roles, including all prior backing, rather than acquiring a + second fresh inventory. The present complete round trip charges 158. +3. Supply synchronized encoded numerical row/target/header schedules for + the actual balanced payload caller. The #4024 triangular converter is + a different admitted path; address-state evaluation is not payload + routing and does not erase that cost. +4. Lower the complete actual provider closure to a common literal binary + program/tariff, including clean private acquisition. Source-operation + O(A^4) and retained backing O(A^2) do not discharge that obligation. + +## Credit + +Prepared for Jerry Chen / @CubeJerry with substantial OpenAI assistance. +Retain the published forward writer and #7154/#7152 work prepared for +CubeJerry; JoyboyBrian's #5053/#5219/#5505 numerical, entry and persistent +owner contracts; Ali Romman's #5353 axis encoding and #5625 retired-write +boundary; Cinna Davis's #4100 balanced algebra; Hiroki KUMAZAKI's padded +mixed-width/current-state and raw inverse work; Tekalign's #4024 encoded +bidirectional converter; ToikY's arena lineage; commdata2338's storage +accounting; and every notice in the unchanged source exports. The CRT +inverse identities are known predecessor results. The claimed contribution +is this exact encoded reverse consumer, source-preserving lifecycle and +complete source budget on the forward endpoint's physical interface. diff --git a/research/encoded-balanced-crt-inverse/README.md b/research/encoded-balanced-crt-inverse/README.md new file mode 100644 index 0000000000..82ab7df581 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/README.md @@ -0,0 +1,145 @@ +# Drive the padded balanced CRT inverse from encoded source with 79 retained roles + +This completes the reverse schedule and subtractive whole-node consumer +left open by the [published forward endpoint](https://github.com/CubeJerry/integer-mult-bounds/tree/532b60ac427f47191175aba2e1317db0f3508d51/research/encoded-balanced-crt-endpoint). +It evaluates the inverse of that same balanced CRT **address-state** map +on the same actual padded source. Runtime receives no decoded node start, +level, width, precision, coordinate or traversal list. Both composition +orders are identity on the entire admitted padded rectangle. The proof +is relative to explicitly pinned source contracts. **No new kappa.** + +The new [inverse_frontend.py](inverse_frontend.py) bootstraps the unary +half-size from the encoded depth and halves it between descending levels. +The new [inverse_producer.py](inverse_producer.py) has exactly one scientific +line changed from the current-coordinate producer: modular subtraction +replaces modular addition in its whole-node updated field. The forward +source writer is byte-for-byte unchanged. It stages the result, closes +the numerical lease, then commits the owned source at the same extent. +[SEAMS.json](SEAMS.json) records the precise seams; the replay authenticates +the one-line producer replacement and all nine source exports. + +The complete source cost is O(A^4), where A is the sum of declared widths, +and retained backing is K_source+O(A^2). All source reads, staging, writing, +head returns, precision preparation, lease retirement and cleanup are paid. +One invocation owns 79 roles. A fresh forward/inverse round trip retains +both inventories, **158 histories**, and charges both complete invocation +bills. Source acquisition in the admitted format and clean private backing +remain explicit premises. No same-bank restart is claimed. + +## What is new and what remains open + +The balanced inverse algebra and logical padded callers were already supplied +by [#4100](https://github.com/CrocSwap/integer-mult-bounds/pull/4100) and +[#4195](https://github.com/CrocSwap/integer-mult-bounds/pull/4195). +[#7152](https://github.com/CrocSwap/integer-mult-bounds/pull/7152) already +implements physical forward/reverse source-state trees at compiled geometry; +[#7154](https://github.com/CrocSwap/integer-mult-bounds/pull/7154) supplies +the encoded forward numerical iterator. [#5053](https://github.com/CrocSwap/integer-mult-bounds/pull/5053) +already proves the arithmetic and current-left reconstruction used here. +The contribution is their exact encoded reverse consumer join on the +forward writer's physical interface, with a complete current-state, +precision and retained-history argument. + +[#4024](https://github.com/CrocSwap/integer-mult-bounds/pull/4024) already +supplies an encoded bidirectional triangular payload converter, consumed +after integer recovery by [#5095](https://github.com/CrocSwap/integer-mult-bounds/pull/5095). +That different format and routing contract is not replaced by this one-vector +helper. Likewise, the raw compact macro inverse in +[#4169](https://github.com/CrocSwap/integer-mult-bounds/pull/4169) is not +implemented by this package. No first CRT inverse, payload permutation, +exceptional-key epoch or selected outer caller is claimed. + +The five selected foundational assumptions remain conditional. The complete +selected conditional kappa remains 0.00363005817. The source proof does not +certify the numerical value of its fixed finite-control refinement constant, +literal binary lowering, analytic error bounds or integer recovery. + +## Reproduce and review + +[PROOF.md](PROOF.md) gives the quantified claim, exact predecessor boundary, +all-size argument and complete cost ledger. With Python 3.12 and its standard +library, from this directory: + +```sh +python3.12 -I -W error -B verify.py +python3.12 -I -O -W error -B verify.py +``` + +Both executed modes print: + +```text +PASS_ENCODED_BALANCED_CRT_INVERSE cases=53 nodes=380 roles=79/158 controls=11 +``` + +The main fixed family runs both composition orders on all 32 padded pairs +for moduli (3,5), fifteen four-axis cases, four composite-modulus cases and +two eight-axis cases. Its 380 actual numerical nodes use 85,291,890 measured +source actions; these are finite observations, not the asymptotic proof. +A separate three-node `run()` test supplies no iteration count or schedule. +The main oracle independently solves each current-left congruence system +by exhaustive search. The complete endpoints also match the source-pinned +balanced forward/reverse oracle; observer results never enter runtime. + +Negative controls detect wrong level order, the wrong arithmetic sign, +stale pre-root left data, hidden current precision, nonblank older guard +tails, an extra physical role, wrong unary transition, forgotten retained +backing, current coordinates misread as original digits, a global-invalid +identity shortcut and source commit before retirement. Host geometry/decode +names are poisoned and physical constructors sealed after initial acquisition. +Failure detection is not an arbitrary error-rollback theorem. + +Actual precision is read from each current selected node. It decreases +between levels but can increase within a level: (2,2,3,3) declared widths +give inverse precisions **11,5,7**. The checks preserve all old backing and +require exact current guard extents plus blank older tails. Source metadata, +inaccessible nonblank history, extent, backing identity and heads are checked +after every node. Both fresh invocation inventories remain charged and blank +after each full-source round trip. + +[INPUT-PINS.json](INPUT-PINS.json) records exact repository, commit, byte hash +and Git-blob pins. Direct replay is offline and Git-free. The canonical base +is `e54523517d0f03e58352e647c403a5af3e525a57`, the frontend head is +`cc35ecedce6f208d5056fab6d17c58555affc73c`, and the unchanged forward writer +is at `532b60ac427f47191175aba2e1317db0f3508d51`. The pending dependencies +are preserved as exact package-local source, rather than inferred from a +moving branch or PR title. + +## Open next questions + +The structured first steps and blockers are in [TASK.json](TASK.json). +An actual exceptional-key caller needs paid source production, conversion +and return transport plus its separate raw compact macro contract. A restart +theorem could reuse the same 79 histories; this package charges 158 for two +fresh invocations. The balanced payload caller still needs its synchronized +encoded row/target/header schedules. The full provider closure and clean +private acquisition also need a common literal binary program and tariff. + +Prepared for Jerry Chen / @CubeJerry with substantial OpenAI assistance; +Apache-2.0. Retain JoyboyBrian's numerical/entry/owner work; Ali Romman's +encoding and retired-write boundary; Cinna Davis, Hiroki KUMAZAKI, Tekalign, +ToikY, commdata2338 and every notice in the unchanged exports. Full credit +is in PROOF.md. AI cross-review is not independent human or formal-kernel +acceptance. + +## Independent acceptance checks + +The orchestrator's [REVIEW.md](REVIEW.md) and separate +[PEER-REVIEW.md](PEER-REVIEW.md) accept the frozen source-relative theorem. +The peer authenticated all nine exports and independently checked reverse +control, current-left reconstruction, retirement, precision regrowth and +complete cost/history sums without rerunning the author verifier. + +A separate CRT-idempotent and global mixed-radix inverse oracle passes 20 +cases and 52 actual nodes, including padded axes, eight-axis cases, widths +up to nine bits, historical tails, the 11,5,7 precision sequence and a rejected +stale-coordinate mutation. Its portable command is: + +```sh +python3 -I -W error -B research/encoded-balanced-crt-inverse/independent_check.py +``` + +`INDEPENDENT-RESULT.json` records the full domain and exact code hashes. +The author normal and optimized replays also pass from this final packaged +directory with identical output. These are independent AI checks; no human +or formal-kernel acceptance is claimed. The full proposed PR description +is committed in `PR-DESCRIPTION.md`. diff --git a/research/encoded-balanced-crt-inverse/RESULT.json b/research/encoded-balanced-crt-inverse/RESULT.json new file mode 100644 index 0000000000..9201e2b52b --- /dev/null +++ b/research/encoded-balanced-crt-inverse/RESULT.json @@ -0,0 +1,4199 @@ +{ + "actual_numerical_nodes": 380, + "cases": [ + { + "input": [ + 0, + 0 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 59872, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 690, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 59880, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 690, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1338, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 59880, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 690, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 59872, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 690, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1338, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 0, + 1 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 59867, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 690, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 59875, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 690, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1338, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 59875, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 690, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 59867, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 690, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1338, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 0, + 2 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 59875, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 59883, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1340, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 59883, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 59875, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1340, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 0, + 3 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 59875, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 59883, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1340, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 59883, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 59875, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1340, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 0, + 4 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 59883, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 59891, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 59891, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 59883, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 0, + 5 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 57863, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 57871, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 57871, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 57863, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 0, + 6 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 57863, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 57871, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 57871, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 57863, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 0, + 7 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 57863, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 57871, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 57871, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 57863, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 1, + 0 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 60066, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 690, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 60077, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1339, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 60273, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 690, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 60268, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1339, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 1, + 1 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 60061, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 690, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 60077, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1339, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 60268, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 690, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 60276, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1340, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 1, + 2 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 60069, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 60085, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1341, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 60077, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 60066, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 690, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1339, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 1, + 3 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 60268, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 60273, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 690, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1339, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 60077, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 60061, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 690, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1339, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 1, + 4 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 60276, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 60268, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 690, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1340, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 60085, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 60069, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1341, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 1, + 5 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 58057, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 58065, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 58065, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 58057, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 1, + 6 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 58057, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 58065, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 58065, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 58057, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 1, + 7 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 58057, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 58065, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 58065, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 58057, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 2, + 0 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 60074, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 60093, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 60281, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 60268, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1340, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 2, + 1 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 60268, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 60281, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1340, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 60276, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 60276, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1341, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 2, + 2 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 60276, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 60276, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1341, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 60284, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 60276, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 2, + 3 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 60276, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 60284, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 60284, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 60284, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1343, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 2, + 4 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 60284, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 60284, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1343, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 60093, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 60074, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 2, + 5 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 58065, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 58073, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1344, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 58073, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 58065, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1344, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 2, + 6 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 58065, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 58073, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1344, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 58073, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 58065, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1344, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 2, + 7 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 58065, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 58073, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1344, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 58073, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 58065, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1344, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 3, + 0 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 60178, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 60186, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1340, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 60186, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 60178, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1340, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 3, + 1 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 60173, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 60181, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1340, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 60181, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 691, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 60173, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 691, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1340, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 3, + 2 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 60181, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 60189, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 60189, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 60181, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 3, + 3 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 60181, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 60189, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 60189, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 692, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 60181, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 692, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1342, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 3, + 4 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 60189, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 60197, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1344, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 60197, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 60189, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1344, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 3, + 5 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 58169, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 58177, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1344, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 58177, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 58169, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1344, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 3, + 6 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 58169, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 58177, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1344, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 58177, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 58169, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1344, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 3, + 7 + ], + "moduli": [ + 3, + 5 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 58169, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + }, + { + "actions": 58177, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1380, + "joint_retained": 1344, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 58177, + "precisions": [ + 6 + ], + "raw_bound": 8976343040, + "retained": 693, + "retained_bound": 711, + "reverse": true + }, + { + "actions": 58169, + "precisions": [ + 6 + ], + "raw_bound": 4681375744, + "retained": 693, + "retained_bound": 711, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1380, + "joint_retained": 1344, + "owned_roles": 158 + } + ], + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "input": [ + 0, + 0, + 0, + 0 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 357448, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1212, + "retained_bound": 1254, + "reverse": false + }, + { + "actions": 357537, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1212, + "retained_bound": 1254, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 2429, + "joint_retained": 2345, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 357537, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1212, + "retained_bound": 1254, + "reverse": true + }, + { + "actions": 357448, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1212, + "retained_bound": 1254, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 2429, + "joint_retained": 2345, + "owned_roles": 158 + } + ], + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "input": [ + 1, + 2, + 4, + 6 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 360506, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1216, + "retained_bound": 1254, + "reverse": false + }, + { + "actions": 360579, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1215, + "retained_bound": 1254, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 2429, + "joint_retained": 2352, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 358745, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1217, + "retained_bound": 1254, + "reverse": true + }, + { + "actions": 358634, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1215, + "retained_bound": 1254, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 2429, + "joint_retained": 2353, + "owned_roles": 158 + } + ], + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "input": [ + 1, + 1, + 1, + 1 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 359669, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1214, + "retained_bound": 1254, + "reverse": false + }, + { + "actions": 359787, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1215, + "retained_bound": 1254, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 2429, + "joint_retained": 2350, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 360305, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1212, + "retained_bound": 1254, + "reverse": true + }, + { + "actions": 360240, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1213, + "retained_bound": 1254, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 2429, + "joint_retained": 2346, + "owned_roles": 158 + } + ], + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "input": [ + 3, + 2, + 4, + 6 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 359345, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1218, + "retained_bound": 1254, + "reverse": false + }, + { + "actions": 359434, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1218, + "retained_bound": 1254, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 2429, + "joint_retained": 2357, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 359208, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1218, + "retained_bound": 1254, + "reverse": true + }, + { + "actions": 359103, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1218, + "retained_bound": 1254, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 2429, + "joint_retained": 2357, + "owned_roles": 158 + } + ], + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "input": [ + 1, + 3, + 4, + 6 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 358305, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1217, + "retained_bound": 1254, + "reverse": false + }, + { + "actions": 358394, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1217, + "retained_bound": 1254, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 2429, + "joint_retained": 2355, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 358168, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1217, + "retained_bound": 1254, + "reverse": true + }, + { + "actions": 358063, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1217, + "retained_bound": 1254, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 2429, + "joint_retained": 2355, + "owned_roles": 158 + } + ], + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "input": [ + 1, + 2, + 7, + 6 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 355033, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1216, + "retained_bound": 1254, + "reverse": false + }, + { + "actions": 355114, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1216, + "retained_bound": 1254, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 2429, + "joint_retained": 2353, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 353280, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1217, + "retained_bound": 1254, + "reverse": true + }, + { + "actions": 353180, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1216, + "retained_bound": 1254, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 2429, + "joint_retained": 2354, + "owned_roles": 158 + } + ], + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "input": [ + 1, + 2, + 4, + 7 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 352020, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1216, + "retained_bound": 1254, + "reverse": false + }, + { + "actions": 352101, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1216, + "retained_bound": 1254, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 2429, + "joint_retained": 2353, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 350827, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1217, + "retained_bound": 1254, + "reverse": true + }, + { + "actions": 350727, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1216, + "retained_bound": 1254, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 2429, + "joint_retained": 2354, + "owned_roles": 158 + } + ], + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "input": [ + 3, + 3, + 7, + 7 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 345405, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1218, + "retained_bound": 1254, + "reverse": false + }, + { + "actions": 345494, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1218, + "retained_bound": 1254, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 2429, + "joint_retained": 2357, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 345494, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1218, + "retained_bound": 1254, + "reverse": true + }, + { + "actions": 345405, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1218, + "retained_bound": 1254, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 2429, + "joint_retained": 2357, + "owned_roles": 158 + } + ], + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "input": [ + 0, + 2, + 1, + 5 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 358904, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1213, + "retained_bound": 1254, + "reverse": false + }, + { + "actions": 358990, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1214, + "retained_bound": 1254, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 2429, + "joint_retained": 2348, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 359009, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1215, + "retained_bound": 1254, + "reverse": true + }, + { + "actions": 358928, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1215, + "retained_bound": 1254, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 2429, + "joint_retained": 2351, + "owned_roles": 158 + } + ], + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "input": [ + 1, + 0, + 3, + 2 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 358979, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1216, + "retained_bound": 1254, + "reverse": false + }, + { + "actions": 359071, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1215, + "retained_bound": 1254, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 2429, + "joint_retained": 2352, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 359558, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1214, + "retained_bound": 1254, + "reverse": true + }, + { + "actions": 359469, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1214, + "retained_bound": 1254, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 2429, + "joint_retained": 2349, + "owned_roles": 158 + } + ], + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "input": [ + 0, + 0, + 7, + 7 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 344771, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1216, + "retained_bound": 1254, + "reverse": false + }, + { + "actions": 344860, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1216, + "retained_bound": 1254, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 2429, + "joint_retained": 2353, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 344860, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1216, + "retained_bound": 1254, + "reverse": true + }, + { + "actions": 344771, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1216, + "retained_bound": 1254, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 2429, + "joint_retained": 2353, + "owned_roles": 158 + } + ], + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "input": [ + 1, + 1, + 0, + 0 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 359113, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1212, + "retained_bound": 1254, + "reverse": false + }, + { + "actions": 359221, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1215, + "retained_bound": 1254, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 2429, + "joint_retained": 2348, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 359860, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1212, + "retained_bound": 1254, + "reverse": true + }, + { + "actions": 359774, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1212, + "retained_bound": 1254, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 2429, + "joint_retained": 2345, + "owned_roles": 158 + } + ], + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "input": [ + 0, + 1, + 0, + 0 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 358106, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1212, + "retained_bound": 1254, + "reverse": false + }, + { + "actions": 358193, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1213, + "retained_bound": 1254, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 2429, + "joint_retained": 2346, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 359555, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1212, + "retained_bound": 1254, + "reverse": true + }, + { + "actions": 359480, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1215, + "retained_bound": 1254, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 2429, + "joint_retained": 2348, + "owned_roles": 158 + } + ], + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "input": [ + 0, + 1, + 2, + 1 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 358559, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1213, + "retained_bound": 1254, + "reverse": false + }, + { + "actions": 358656, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1214, + "retained_bound": 1254, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 2429, + "joint_retained": 2348, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 358193, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1213, + "retained_bound": 1254, + "reverse": true + }, + { + "actions": 358106, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1212, + "retained_bound": 1254, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 2429, + "joint_retained": 2346, + "owned_roles": 158 + } + ], + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "input": [ + 1, + 3, + 1, + 1 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 357805, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1215, + "retained_bound": 1254, + "reverse": false + }, + { + "actions": 357910, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1215, + "retained_bound": 1254, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 2429, + "joint_retained": 2351, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 358104, + "precisions": [ + 11, + 5, + 7 + ], + "raw_bound": 80021766144, + "retained": 1213, + "retained_bound": 1254, + "reverse": true + }, + { + "actions": 358031, + "precisions": [ + 5, + 7, + 11 + ], + "raw_bound": 40676048896, + "retained": 1213, + "retained_bound": 1254, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 2429, + "joint_retained": 2347, + "owned_roles": 158 + } + ], + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "input": [ + 3, + 8 + ], + "moduli": [ + 4, + 9 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 81020, + "precisions": [ + 8 + ], + "raw_bound": 11063271424, + "retained": 859, + "retained_bound": 883, + "reverse": false + }, + { + "actions": 81012, + "precisions": [ + 8 + ], + "raw_bound": 21549031424, + "retained": 857, + "retained_bound": 883, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1712, + "joint_retained": 1662, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 80775, + "precisions": [ + 8 + ], + "raw_bound": 21549031424, + "retained": 859, + "retained_bound": 883, + "reverse": true + }, + { + "actions": 80759, + "precisions": [ + 8 + ], + "raw_bound": 11063271424, + "retained": 858, + "retained_bound": 883, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1712, + "joint_retained": 1663, + "owned_roles": 158 + } + ], + "source_tail": 23, + "widths": [ + 3, + 4 + ] + }, + { + "input": [ + 7, + 15 + ], + "moduli": [ + 4, + 9 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 77741, + "precisions": [ + 8 + ], + "raw_bound": 11063271424, + "retained": 860, + "retained_bound": 883, + "reverse": false + }, + { + "actions": 77749, + "precisions": [ + 8 + ], + "raw_bound": 21549031424, + "retained": 860, + "retained_bound": 883, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1712, + "joint_retained": 1666, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 77749, + "precisions": [ + 8 + ], + "raw_bound": 21549031424, + "retained": 860, + "retained_bound": 883, + "reverse": true + }, + { + "actions": 77741, + "precisions": [ + 8 + ], + "raw_bound": 11063271424, + "retained": 860, + "retained_bound": 883, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1712, + "joint_retained": 1666, + "owned_roles": 158 + } + ], + "source_tail": 23, + "widths": [ + 3, + 4 + ] + }, + { + "input": [ + 4, + 1 + ], + "moduli": [ + 4, + 9 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 80377, + "precisions": [ + 8 + ], + "raw_bound": 11063271424, + "retained": 857, + "retained_bound": 883, + "reverse": false + }, + { + "actions": 80385, + "precisions": [ + 8 + ], + "raw_bound": 21549031424, + "retained": 857, + "retained_bound": 883, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1712, + "joint_retained": 1660, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 80385, + "precisions": [ + 8 + ], + "raw_bound": 21549031424, + "retained": 857, + "retained_bound": 883, + "reverse": true + }, + { + "actions": 80377, + "precisions": [ + 8 + ], + "raw_bound": 11063271424, + "retained": 857, + "retained_bound": 883, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1712, + "joint_retained": 1660, + "owned_roles": 158 + } + ], + "source_tail": 23, + "widths": [ + 3, + 4 + ] + }, + { + "input": [ + 1, + 9 + ], + "moduli": [ + 4, + 9 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 77087, + "precisions": [ + 8 + ], + "raw_bound": 11063271424, + "retained": 858, + "retained_bound": 883, + "reverse": false + }, + { + "actions": 77095, + "precisions": [ + 8 + ], + "raw_bound": 21549031424, + "retained": 858, + "retained_bound": 883, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 1712, + "joint_retained": 1662, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 77095, + "precisions": [ + 8 + ], + "raw_bound": 21549031424, + "retained": 858, + "retained_bound": 883, + "reverse": true + }, + { + "actions": 77087, + "precisions": [ + 8 + ], + "raw_bound": 11063271424, + "retained": 858, + "retained_bound": 883, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 1712, + "joint_retained": 1662, + "owned_roles": 158 + } + ], + "source_tail": 23, + "widths": [ + 3, + 4 + ] + }, + { + "input": [ + 2, + 4, + 6, + 10, + 12, + 16, + 18, + 22 + ], + "moduli": [ + 3, + 5, + 7, + 11, + 13, + 17, + 19, + 23 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 6934507, + "precisions": [ + 9, + 9, + 10, + 11, + 17, + 20, + 36 + ], + "raw_bound": 2661716099072, + "retained": 3941, + "retained_bound": 4073, + "reverse": false + }, + { + "actions": 6934637, + "precisions": [ + 36, + 17, + 20, + 9, + 9, + 10, + 11 + ], + "raw_bound": 5312822411264, + "retained": 3937, + "retained_bound": 4073, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 7910, + "joint_retained": 7642, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 6923150, + "precisions": [ + 36, + 17, + 20, + 9, + 9, + 10, + 11 + ], + "raw_bound": 5312822411264, + "retained": 3946, + "retained_bound": 4073, + "reverse": true + }, + { + "actions": 6922873, + "precisions": [ + 9, + 9, + 10, + 11, + 17, + 20, + 36 + ], + "raw_bound": 2661716099072, + "retained": 3942, + "retained_bound": 4073, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 7910, + "joint_retained": 7652, + "owned_roles": 158 + } + ], + "source_tail": 97, + "widths": [ + 4, + 4, + 4, + 4, + 4, + 5, + 5, + 5 + ] + }, + { + "input": [ + 7, + 4, + 6, + 10, + 12, + 16, + 18, + 31 + ], + "moduli": [ + 3, + 5, + 7, + 11, + 13, + 17, + 19, + 23 + ], + "round_trips": [ + { + "calls": [ + { + "actions": 6838868, + "precisions": [ + 9, + 9, + 10, + 11, + 17, + 20, + 36 + ], + "raw_bound": 2661716099072, + "retained": 3943, + "retained_bound": 4073, + "reverse": false + }, + { + "actions": 6839038, + "precisions": [ + 36, + 17, + 20, + 9, + 9, + 10, + 11 + ], + "raw_bound": 5312822411264, + "retained": 3943, + "retained_bound": 4073, + "reverse": true + } + ], + "first_reverse": false, + "joint_bound": 7910, + "joint_retained": 7650, + "owned_roles": 158 + }, + { + "calls": [ + { + "actions": 6833059, + "precisions": [ + 36, + 17, + 20, + 9, + 9, + 10, + 11 + ], + "raw_bound": 5312822411264, + "retained": 3947, + "retained_bound": 4073, + "reverse": true + }, + { + "actions": 6832825, + "precisions": [ + 9, + 9, + 10, + 11, + 17, + 20, + 36 + ], + "raw_bound": 2661716099072, + "retained": 3947, + "retained_bound": 4073, + "reverse": false + } + ], + "first_reverse": true, + "joint_bound": 7910, + "joint_retained": 7658, + "owned_roles": 158 + } + ], + "source_tail": 97, + "widths": [ + 4, + 4, + 4, + 4, + 4, + 5, + 5, + 5 + ] + } + ], + "cases_count": 53, + "complete_run_driver": { + "actual_numerical_nodes": 3, + "output": [ + 0, + 1, + 0, + 0 + ], + "owned_roles": 79, + "verifier_schedule_supplied": false + }, + "controls": [ + "forward_level_order_with_subtraction", + "addition_in_inverse_nodes", + "stale_current_left_from_before_root", + "old_root_precision_reused_at_smaller_child", + "nonblank_old_tail_past_shorter_current_guard", + "hidden_new_role_at_reverse_level_transition", + "doubling_instead_of_reverse_halving", + "silently_shortened_historical_backing", + "current_child_misread_as_original_digits", + "global_invalid_identity_shortcut", + "source_write_before_inverse_result_retirement" + ], + "new_kappa": null, + "owned_roles_per_fresh_round_trip": 158, + "owned_roles_per_invocation": 79, + "scope": "one balanced address-state inverse; no payload or raw compact inverse", + "source_count": 9, + "status": "PASS_ENCODED_BALANCED_CRT_INVERSE" +} diff --git a/research/encoded-balanced-crt-inverse/REVIEW.md b/research/encoded-balanced-crt-inverse/REVIEW.md new file mode 100644 index 0000000000..6e4dc9a5c5 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/REVIEW.md @@ -0,0 +1,80 @@ +# Orchestrator acceptance and independent inverse oracle + +Prepared for @CubeJerry with substantial OpenAI assistance. Scientific base: +`e54523517d0f03e58352e647c403a5af3e525a57`. + +## Verdict + +Accepted at the stated encoded source-model boundary. This is an inverse of +the padded balanced CRT address-state endpoint, using the unchanged physical +writer and its retired-lease commit order. It is not a payload converter, a +literal emitted binary machine, or an admission into the selected outer caller. +The five selected assumptions and the conditional kappa remain unchanged. + +The root read the complete proof, reverse frontend, subtraction seam and +writer lifecycle, independently checked the geometric cost sums, and reviewed +the separate proof/control/cost assessment in `PEER-REVIEW.md`. That reviewer +authenticated all nine exported inputs and did not use author-test execution +as proof. Neither review found a blocking defect or requested a core change. + +## Independent executable method + +`independent_check.py` adapts the separately authored forward-endpoint review +checker from published commit `532b60ac427f47191175aba2e1317db0f3508d51`. +It constructs expected inverse nodes using direct CRT idempotents, rather +than the producer's digit-by-digit reconstruction, and subtracts the expected +rotation. For all-valid global fixtures it separately reconstructs the single +CRT integer from the transformed residues and extracts its mixed-radix digits. +It imports the actual production modules, but not the author's verifier. + +The fixed independent domain has 20 cases and 52 actual nodes. It includes +padding at different coordinates, eight axes, nine-bit words, near-equal +mixed widths, the precision sequence 11,5,7, and opaque historical source +tails. It checks current source coordinates after each node, all 79 private +histories at complete return, guide/head restoration, source object and +backing preservation, and the stated measured operation/space envelopes. +A stale-coordinate commit mutant is rejected by the independent numerical +oracle. Finite cases corroborate the universal argument; they do not establish +the theorem by extrapolation. + +```sh +python3 -I -W error -B research/encoded-balanced-crt-inverse/independent_check.py +``` + +Expected summary fields are `status: PASS`, `cases: 20`, `nodes: 52` and +`stale-coordinate commit rejected`. The full receipt is `INDEPENDENT-RESULT.json`. + +## Critical proof boundaries + +At each inverse node, the current left coordinates determine the same fixed +rotation that the forward node used. Subtraction inverts that rotation on +valid right values; padded right values remain unchanged. Invalid left values +set that node's controlling integer to zero. This does not imply a globally +invalid padded vector is fixed by every lower node. Disjoint nodes within a +level commute, so reverse level order suffices for both composition identities. + +Every invocation rebuilds its guide and guards at its current precision. +Retirement erases that interval; previously erased suffixes remain blank. +This invariant permits both shrinkage and later regrowth without scanning +the full maximum history at every small node. Historical backing is still +charged: 79 roles belong to one invocation, and two fresh forward/inverse +invocations retain 158 histories. Same-bank restarting is not proved. + +The extra reverse bootstrap and halving work is linear in the total unary +lengths. Complete source staging and commits remain quadratic in source +length. Summing the quartic numerical budgets gives the claimed O(A^4) +source time and O(A^2) extra retained backing. The finite refinement constant +`C_inv`, ownership/source contracts and the allocated-versus-visited-space +qualification remain explicit. Source-model checks do not replace a literal +machine refinement theorem. + +## Frozen scientific snapshot + +| File | SHA256 | +| --- | --- | +| `inverse_frontend.py` | `0e5f4c9450372c90000f5ebf3c22dfbe7241dd53da9ae9bcce310af859b009ef` | +| `inverse_producer.py` | `6acdebee7134fbc8e2d121060286bd05e7282900da8a28a78c80937dde7ea178` | +| `PROOF.md` | `edbeb16bd8d088ab75b73b22adf5fc8aeef1ec93e8333bf74d4ad8e7f2f3d51f` | + +This is independent AI mathematical and implementation review, not independent +human acceptance or formal-kernel certification. diff --git a/research/encoded-balanced-crt-inverse/SEAMS.json b/research/encoded-balanced-crt-inverse/SEAMS.json new file mode 100644 index 0000000000..c8d55740f8 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/SEAMS.json @@ -0,0 +1,20 @@ +{ + "producer": { + "source": "source/research/encoded-current-crt/producer.py", + "prefix": "# Inverse specialization for CubeJerry with OpenAI assistance. Apache-2.0.\n# Exactly one scientific line differs from the pinned #5053 producer.\n", + "before": "updated = a.add(canonical, offset, modulus)", + "after": "updated = a.subtract(canonical, offset, modulus)", + "occurrences": 1 + }, + "frontend": { + "source": "source/research/encoded-balanced-crt-entry/frontend.py", + "changes": [ + "Bootstrap encoded half size from 1 to d/2 by scanning depth tokens and invoking the unchanged doubling method.", + "Override the inherited _double_half level-transition hook with paid unary halving; every other frontend method is inherited unchanged." + ] + }, + "writer": { + "source": "source/research/encoded-balanced-crt-endpoint/endpoint.py", + "changes": [] + } +} diff --git a/research/encoded-balanced-crt-inverse/SOURCES.json b/research/encoded-balanced-crt-inverse/SOURCES.json new file mode 100644 index 0000000000..eecb107169 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/SOURCES.json @@ -0,0 +1,61 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "research/r437-preparation-composition/predecessor4025/source/words.py", + "usage": "provenance", + "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50", + "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9" + }, + { + "path": "research/r437-preparation-composition/predecessor4025/source/records.py", + "usage": "provenance", + "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3", + "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372" + }, + { + "path": "research/encoded-crt-entry-lifecycle/entry.py", + "usage": "provenance", + "git_blob": "1fa2b0cb88320d4f5b623554bb0fc6de332b773c", + "sha256": "0537ec98f306270c8ff6a424841886cf53f675d9947029347090c7dc779616d7" + }, + { + "path": "research/encoded-current-crt/producer.py", + "usage": "provenance", + "git_blob": "a327b0161eca57a1cc44ec2aa8e3defed2167ddc", + "sha256": "88dab4ca02a92164a67826db361214fa1405e4b4a588f8c4279a21bcee95ab76" + }, + { + "path": "research/crt-persistent-numerical-owner/owner.py", + "usage": "provenance", + "git_blob": "20ef3519b6fef691ec92b7315e320b5e8ce9bf18", + "sha256": "1d73f432f8de9c791260c43335eb207d82bbb3f5b190cc76d0d914a4db076f41" + }, + { + "path": "research/crt-mixed-row-entry/bridge.py", + "usage": "provenance", + "git_blob": "57f6853e262a6136bc616f1e47a31d0ace28495c", + "sha256": "89c38638c0d66da731566c903c32e7fa1ad31088d29cfd2634fce823dd07c1f9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e", + "usage": "provenance" + } + ], + "export_note": "All runtime imports and the verifier-only canonical balanced oracle are package-local exact byte exports authenticated by INPUT-PINS.json. Pending #7154 and the published forward writer at 532b60ac427f47191175aba2e1317db0f3508d51 are retained by explicit repository/commit/blob/hash pins; no nonancestor fetch is needed for replay." +} diff --git a/research/encoded-balanced-crt-inverse/TASK.json b/research/encoded-balanced-crt-inverse/TASK.json new file mode 100644 index 0000000000..37698991c2 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose 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.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Uniform encoded reverse balanced levels and subtractive whole-node current-coordinate consumer on the exact published forward padded owned-source interface; 79 roles per invocation and 158 retained histories for fresh round trips.", + "scope_change_reason": "The published forward endpoint leaves encoded reverse traversal open. Existing logical/compiled balanced inverses and the encoded triangular payload converter have different uniformity or caller interfaces; a bounded source-pinned feasibility audit distinguished them before allocation.", + "bottleneck_link": "Source-specific uniform encoded inverse and ownership/precision progress; it does not discharge any of the five selected assumptions or improve complete kappa.", + "budget_minutes": 60, + "stop_rule": "Stop on exact same-interface predecessor overlap, host geometry/traversal history, unretired source mutation, more than 79 roles, or failure of the complete O(A^4) source-time and K_source+O(A^2) history bill. No payload or raw compact inverse expansion.", + "outcome": "independently_reviewed_scoped_source_model_result", + "evidence": "PROOF.md; exact INPUT-PINS and SEAMS; author strict normal/optimized replays; REVIEW.md and PEER-REVIEW.md; independent 20-case/52-node inverse oracle.", + "author": "Jerry Chen / CubeJerry", + "ai_assistance": "Substantial OpenAI assistance; independent AI source/proof review, not human or proof-kernel acceptance", + "open_questions": [ + { + "question": "Can one actual exceptional-key caller admit this encoded inverse?", + "why_it_matters": "The source helper is not the raw compact macro inverse or full selected caller.", + "first_step": "Pin the caller input and output frames and charge source production, conversion, return transport and separate raw macro work.", + "blocked_by": "No caller-specific representation or three-epoch join is supplied." + }, + { + "question": "Can the same 79 historical roles restart for another invocation?", + "why_it_matters": "Fresh forward/inverse composition currently retains 158 histories and pays two complete acquisitions.", + "first_step": "Prove encoded shape reinitialization and ownership/precision reentry from every retired history.", + "blocked_by": "No persistent Endpoint restart API or proof is included." + }, + { + "question": "Can encoded balanced row/target/header production drive the payload caller?", + "why_it_matters": "An address-state inverse does not route all indexed payloads.", + "first_step": "Pin one actual synchronized row boundary and derive its geometry and fields from owned physical source.", + "blocked_by": "The existing triangular payload converter has a different interface and does not establish this balanced join." + }, + { + "question": "Can the complete source provider closure be lowered to one literal binary tariff?", + "why_it_matters": "O(A^4) source operations and O(A^2) backing are not a full compiler or multiplication theorem.", + "first_step": "Lower the fixed controllers together with actual arithmetic, entry, owner and clean-acquisition contracts.", + "blocked_by": "The exact control refinement constant and binary compiler remain uncertified." + } + ] +} diff --git a/research/encoded-balanced-crt-inverse/VALIDATION.json b/research/encoded-balanced-crt-inverse/VALIDATION.json new file mode 100644 index 0000000000..8a30755d2f --- /dev/null +++ b/research/encoded-balanced-crt-inverse/VALIDATION.json @@ -0,0 +1,50 @@ +{ + "status": "PASS", + "author_normal_optimized_equal": true, + "author_stdout": "PASS_ENCODED_BALANCED_CRT_INVERSE cases=53 nodes=380 roles=79/158 controls=11", + "independent_cases": 20, + "independent_nodes": 52, + "independent_method": "subtractive CRT idempotents plus independent global inverse reconstruction", + "independent_negative_controls": [ + "stale-coordinate commit rejected" + ], + "reviews": [ + "REVIEW.md", + "PEER-REVIEW.md" + ], + "limitations": [ + "Source-model refinement constant retained", + "79 histories per invocation; 158 for two fresh invocations", + "No selected caller or payload implementation", + "No new kappa or foundational assumption discharge" + ], + "sha256": { + "CHECKPOINT.json": "2eb8d21b9a2b1c8eaf841d13accbdf588f0fbe84ae85c1ad9910edef1a671917", + "INDEPENDENT-RESULT.json": "f2d2f7bf4c539672499c4d85f0face870b496b58af31c493f15d102261a8444a", + "INPUT-PINS.json": "eb9d2159d9a0a8d66470544fd9ec5bfa91898220f00139fb1bf5be80983a7646", + "PEER-REVIEW.md": "ed9b335a795481e2f6ec63be7af246dd3ca28b56536abd8f9f6774fa5d3a1fa0", + "PR-DESCRIPTION.md": "0f803c59319cf0c336bd22f42cacecb794287eb650361196e3c041512122d96a", + "PR-TITLE.txt": "7b695bfb438f8d216f4e4b67d8dd553c775df31595ec480228ab6dbd864d2c63", + "PROOF.md": "edbeb16bd8d088ab75b73b22adf5fc8aeef1ec93e8333bf74d4ad8e7f2f3d51f", + "README.md": "7634a9bf06c7a04870e1737e877956ce834df0a75b181965fd587e83d1b4451b", + "RESULT.json": "da72e6b1660c514459e12ebf4013a41ef38855fcc9679aff6911d6f1d42c44ce", + "REVIEW.md": "640242a47ad54ff00d20df6a9b2ac56b0f9fa1af52b88f5d64d63f0838603e58", + "SEAMS.json": "3a942dc7e32f898037362c00def8abddcfd41cf0ec3cb66899dd66c5380a9e97", + "SOURCES.json": "83d08cde522eb91c9c859c58f3bdb5523c4087dea7b31e96f015ded859e0b9c4", + "TASK.json": "f671c39bb1ded5c7de1b9b5738d3823ee330709bb87b0f4cacf833b7bc346a96", + "VERIFY.json": "9d2ef9c83ef1de6a011cb3d38ab69d85e4a8406d6f8be2d6d929cdc3eb92c3cf", + "independent_check.py": "2db9feb63c21257fc36d1db428d66f3ebf48c0c15fd6d689020b026627ea91ad", + "inverse_frontend.py": "0e5f4c9450372c90000f5ebf3c22dfbe7241dd53da9ae9bcce310af859b009ef", + "inverse_producer.py": "6acdebee7134fbc8e2d121060286bd05e7282900da8a28a78c80937dde7ea178", + "source/research/crt-mixed-row-entry/bridge.py": "89c38638c0d66da731566c903c32e7fa1ad31088d29cfd2634fce823dd07c1f9", + "source/research/crt-persistent-numerical-owner/owner.py": "1d73f432f8de9c791260c43335eb207d82bbb3f5b190cc76d0d914a4db076f41", + "source/research/encoded-balanced-crt-endpoint/endpoint.py": "c24ae2c90d175d276120438809e7c7401b8a8c04dec139f1b7345e9778984ced", + "source/research/encoded-balanced-crt-entry/frontend.py": "6ec9aab626a9d7a229b6f13ce6863e1ca77fa30ef65a4a66ae03a6ffaf2ee78c", + "source/research/encoded-crt-entry-lifecycle/entry.py": "0537ec98f306270c8ff6a424841886cf53f675d9947029347090c7dc779616d7", + "source/research/encoded-current-crt/producer.py": "88dab4ca02a92164a67826db361214fa1405e4b4a588f8c4279a21bcee95ab76", + "source/research/r437-preparation-composition/predecessor4025/source/records.py": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372", + "source/research/r437-preparation-composition/predecessor4025/source/words.py": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9", + "source/research/unconditional-batched-crt/check_batched_crt.py": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e", + "verify.py": "8ca14c361bd32666e6f94b8f5827b43879ecfc6b90fc56eff5ceaf77612c902d" + } +} diff --git a/research/encoded-balanced-crt-inverse/VERIFY.json b/research/encoded-balanced-crt-inverse/VERIFY.json new file mode 100644 index 0000000000..cd175f6c53 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/VERIFY.json @@ -0,0 +1,46 @@ +{ + "schema_version": 1, + "status": "independently_reviewed", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Nine exact exports and one-line producer seam; 53 padded fixtures in both composition orders, 380 actual numerical nodes, independent current-state congruence oracle, 79/158 histories, 11 controls and separate unscheduled 3-node run." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Repeat all explicit checks under optimized Python and compare the same exact frozen receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 180, + "checks": "Separate CRT-idempotent/global inverse oracle: 20 cases, 52 nodes and stale-coordinate mutant rejection." + } + ] +} diff --git a/research/encoded-balanced-crt-inverse/independent_check.py b/research/encoded-balanced-crt-inverse/independent_check.py new file mode 100644 index 0000000000..9944460718 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/independent_check.py @@ -0,0 +1,257 @@ +"""Independent review of the inverse join, not its author verifier. + +Adapted by the root from the separately authored forward reviewer at published +commit 532b60ac427f47191175aba2e1317db0f3508d51; direct CRT idempotent +oracles and physical-history checks are retained with inverse algebra. + +The oracle uses direct CRT idempotents, unlike the encoded mixed-radix +reconstruction. Observer-only integers/snapshots never enter runtime control. +Run: python3 -I -W error -B independent_check.py [package-directory] +Prepared for CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from hashlib import sha256 +from importlib.util import module_from_spec, spec_from_file_location +from pathlib import Path +from types import ModuleType +import json +import math +import sys + + +PKG = Path(sys.argv[1]).resolve() if len(sys.argv)>1 else Path(__file__).resolve().parent + + +def require(ok, why): + if not ok: + raise AssertionError(why) + + +def load(name, relative): + spec = spec_from_file_location(name, PKG / relative) + module = module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +w = load("words", "source/research/r437-preparation-composition/predecessor4025/source/words.py") +r = load("peer_records", "source/research/r437-preparation-composition/predecessor4025/source/records.py") +e = load("peer_entry", "source/research/encoded-crt-entry-lifecycle/entry.py") +n = load("peer_inverse_numeric", "inverse_producer.py") +o = load("peer_owner", "source/research/crt-persistent-numerical-owner/owner.py") +c = load("peer_canonical", "source/research/crt-mixed-row-entry/bridge.py") +forward_f = load("peer_frontend", "source/research/encoded-balanced-crt-entry/frontend.py") +f = load("peer_inverse_frontend", "inverse_frontend.py").bind(forward_f) +endpoint = load("peer_endpoint", "source/research/encoded-balanced-crt-endpoint/endpoint.py") + + +def fixture(moduli, widths, coords): + tape = e.Port(w) + fields = [] + for modulus, width, coordinate in zip(moduli, widths, coords): + tape.append(r.ROOT) + for _ in range(width): + tape.append(w.ONE) + tape.append(r.WORD_END) + for value, end in ((modulus, r.WORD_END), (coordinate, r.RECORD_END)): + positions = [] + for b in range(width): + positions.append(tape.head) + tape.append((value >> b) & 1) + tape.append(end) + fields.append(positions) + tape.append(w.RIGHT) + tape.rewind() + # Deliberately hostile inaccessible tail: includes a second LEFT/RIGHT. + tape.cells.extend([r.PAIR, w.LEFT, w.RIGHT, w.ONE, w.BLANK, r.ROOT]) + return tape, fields + + +def decode(tape, fields): + return tuple(sum(tape.cells[position] << b for b, position in enumerate(field)) + for field in fields) + + +def node_math(moduli, current, start, half): + result = list(current) + selected = moduli[start:start+half] + total = math.prod(selected) + lower = 0 + if all(current[i] < moduli[i] for i in range(start, start+half)): + prefix = 1 + # CRT idempotent formula, independent of digit-by-digit reconstruction. + for i in range(start, start+half): + modulus = moduli[i] + residue = (current[i] * prefix) % modulus + cofactor = total // modulus + lower += residue * cofactor * pow(cofactor, -1, modulus) + prefix *= modulus + lower %= total + prefix = total + for i in range(start+half, start+2*half): + if current[i] < moduli[i]: + result[i] = (current[i] - lower * pow(prefix, -1, moduli[i])) % moduli[i] + prefix *= moduli[i] + return tuple(result) + + +def port_actions(ports): + return sum(p.meter.reads+p.meter.writes+p.meter.moves for p in ports) + + +def run_case(moduli, widths, original, implementation=endpoint): + require(len(moduli) >= 2 and len(moduli) & (len(moduli)-1) == 0, "fixture dyadic") + require(max(widths)-min(widths) <= 1, "fixture near-equal widths") + require(all(2 <= s < 2**h and 0 <= x < 2**h + for s, h, x in zip(moduli, widths, original)), "fixture domain") + require(all(math.gcd(s,t)==1 for i,s in enumerate(moduli) for t in moduli[:i]), + "fixture pairwise coprime") + source, fields = fixture(moduli, widths, original) + initial = bytes(source.cells) + coordinates = set(sum(fields, [])) + state = implementation.Endpoint(f, w, r, e, n, o, c, source) + it = state.iterator + private = (*it.bank.ports, *it.guards, *it.counters.values(), state.staging) + all_ports = (source, *private) + identities = tuple(id(port.cells) for port in all_ports) + require(len(private) == 79 and len(set(identities)) == 80, "fixed disjoint role inventory") + A, d = sum(widths), len(widths) + M = 2+3*A+4*d + expected = tuple(original) + node_count = 0 + adapter_actions = 0 + numeric_actions = 0 + max_stage_head = 1 + old_step = e.Port.step + + def observing_step(port, direction): + nonlocal max_stage_head + old_step(port, direction) + if port is state.staging: + max_stage_head = max(max_stage_head, port.head) + + e.Port.step = observing_step + try: + half = d//2 + while half: + for start in range(0, d, 2*half): + node_count += 1 + lease = it.next() + require(lease is not None, "exact node count lower bound") + require(bytes(source.cells)==initial or decode(source,fields)==expected, + "source supplied current state") + require(source.head == 1, "source restored after fresh projection") + P = 1+sum(widths[start:start+2*half]) + guide = lease.actual.guide + require(list(guide.cells[:P+1]) == [w.LEFT]+[w.ONE]*P, + "guide reflects preserved widths at actual node") + require(guide.head==1, "guide handoff head") + axis = it.counters['axis'] + require(axis.cells[start+1]==r.STEP, "encoded start agrees with independent schedule") + if start+2*half < d: + require(axis.cells[start+2*half+1]==r.VALUE, "encoded next-node marker") + topologies = {key:(bytes(port.cells),port.head) + for key,port in it.counters.items() if key!='width'} + before = bytes(source.cells),source.head + raw = port_actions(all_ports) + state.stage(lease) + require((bytes(source.cells),source.head)==before, + "source immutable throughout live numerical lease") + require(all((bytes(it.counters[key].cells),it.counters[key].head)==snapshot + for key,snapshot in topologies.items()), "staging restores topology") + require(it.counters['width'].head==1 and + all(x==w.BLANK for x in it.counters['width'].cells[1:]), + "width role completely erased after full scan") + stage_actions = port_actions(all_ports)-raw + lease.close() + meter = lease.actual.context.arena.meter + numeric_actions += meter.reads+meter.writes+meter.moves + require(not it.live and not it.bank.busy, "close releases numerical lease") + raw = port_actions(all_ports) + state.commit() + actions = stage_actions+port_actions(all_ports)-raw + require(actions <= 2048*(M+2*half*(P+2))+32, + "full stage/commit raw tariff") + adapter_actions += actions + expected = node_math(moduli,expected,start,half) + require(decode(source,fields)==expected, "direct CRT node endpoint") + require(source.head==1 and tuple(id(port.cells) for port in all_ports)==identities, + "physical identity and source entry head") + require(len(source.cells)==len(initial) and + all(source.cells[i]==initial[i] for i in range(len(initial)) + if i not in coordinates), "source metadata and hostile old tail") + require(all(port.head==1 and all(x==w.BLANK for x in port.cells) + for port in (*it.bank.ports,*it.guards,state.staging)), + "every numerical/guard/staging history fully retired") + half //= 2 + require(it.closed and it.next() is None, "exact terminal boundary") + require(all(port.head==1 and all(x==w.BLANK for x in port.cells) + for port in private), "all 79 histories blank at termination") + require(len(state.staging.cells)==M and max_stage_head==M, + "M retained staging cells and M+1 visited span") + if all(x 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-balanced-crt-inverse/source/research/crt-mixed-row-entry/bridge.py b/research/encoded-balanced-crt-inverse/source/research/crt-mixed-row-entry/bridge.py new file mode 100644 index 0000000000..57f6853e26 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/source/research/crt-mixed-row-entry/bridge.py @@ -0,0 +1,93 @@ +"""Produce CRT entry streams from declared padded axis records. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" + + +def canonical_end(target, words, records): + """Remove high zero bits by local moves. Keep one bit for zero.""" + target.step(-1) + while target.read() == words.ZERO: + target.write(words.BLANK) + target.step(-1) + if target.read() in (records.ROOT, records.WORD_END): + target.step(1) + target.append(words.ZERO) + else: + words.need(target.read() == words.ONE, 'last nonzero bit') + target.step(1) + target.append(records.WORD_END) + + +class RowEntry: + """The topology is compile-time data. Axis fields stay on tapes.""" + + def __init__(self, words, records, entry, producer, source, dirty, + widths, ell, level, start, global_row): + w, r = words, records + d = len(widths) + w.need(d >= 2 and d & (d - 1) == 0, 'power-of-two axis count') + w.need(type(ell) is int and ell >= 2, 'compiled ell') + w.need(all(type(h) is int and h in (ell - 1, ell) for h in widths), + 'compiled width family') + w.need(type(level) is int and 1 <= level < d.bit_length(), 'compiled level') + size = 1 << level + w.need(type(start) is int and 0 <= start <= d - size and start % size == 0, + 'compiled tree node') + w.need(type(global_row) is int and 0 <= global_row < 2 * ell - 1, + 'compiled global row') + middle, stop = start + size // 2, start + size + self.active = tuple(i for i in range(middle, stop) + if widths[i] == ell or global_row not in (ell - 1, ell)) + w.need(len(dirty) == 8 and len({id(x) for x in (source, *dirty)}) == 9, + 'distinct source and dirty roles') + self.w, self.r = w, r + self.context, self.result, self.inputs = None, None, () + if not self.active: + return + self.guide, self.left, self.right = (entry.Port(w) for _ in range(3)) + self.inputs = (self.guide, self.left, self.right) + for axis, h in enumerate(widths): + selected = start <= axis < stop + target = self.left if axis < middle else self.right + w.need(source.read() == r.ROOT, 'axis record tag') + source.step(1) + if selected: + target.append(r.ROOT) + for _ in range(h): + w.need(source.read() == w.ONE, 'declared unary width') + source.step(1) + if selected: + self.guide.append(w.ONE) + w.need(source.read() == r.WORD_END, 'width delimiter') + source.step(1) + for delimiter in (r.WORD_END, r.RECORD_END): + for _ in range(h): + bit = source.read() + w.need(bit in (w.ZERO, w.ONE), 'declared padded field') + source.step(1) + if selected: + target.append(bit) + w.need(source.read() == delimiter, 'axis field delimiter') + source.step(1) + if selected: + canonical_end(target, w, r) + if selected: + target.append(r.RECORD_END) + w.need(source.read() == w.RIGHT, 'complete axis stream') + source.rewind() + self.guide.append(w.ONE) + self.guide.rewind() + for target in (self.left, self.right): + target.append(w.RIGHT) + target.rewind() + self.context = entry.Entry(w, r, self.guide, dirty) + self.result = self.context.invoke(producer, self.left, self.right) + + def close(self): + if self.context is None: + return + self.context.consume(self.result) + self.context.close() + for port in self.inputs: + port.retire() diff --git a/research/encoded-balanced-crt-inverse/source/research/crt-persistent-numerical-owner/owner.py b/research/encoded-balanced-crt-inverse/source/research/crt-persistent-numerical-owner/owner.py new file mode 100644 index 0000000000..20ef3519b6 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/source/research/crt-persistent-numerical-owner/owner.py @@ -0,0 +1,77 @@ +"""One physical63-role owner for the unchanged numerical CRT RowEntry. +JoyboyBrian, substantial OpenAI Codex assistance. Apache-2.0. +""" +from types import SimpleNamespace + + +class Bank: + def __init__(self, words, entry, ports=None): + self.w, self.entry = words, entry + # Physical allocation belongs only to initial owner acquisition. + if ports is None: + ports = [entry.Port(words) for _ in range(63)] + for port in ports: + port.retire() + words.need(len(ports) == 63 and len({id(p.cells) for p in ports}) == 63, + '63 distinct owned backing roles') + self.ports = tuple(ports) + self.busy = False + self.cursor = 0 + + def take(self, words): + words.need(words is self.w and self.busy and self.cursor < 63, + 'fixed live owner role') + port = self.ports[self.cursor] + self.cursor += 1 + words.need(port.head == 1 and port.read() == words.BLANK, + 'retired role head and body') + port.step(-1) + words.need(port.read() == words.BLANK, 'retired marker') + port.write(words.LEFT) + port.step(1) + return port + + def open(self, records, producer, bridge, source, dirty, + widths, ell, level, start, row): + self.w.need(not self.busy, 'previous result must retire first') + self.w.need(not ({id(p.cells) for p in self.ports} & + {id(p.cells) for p in (source, *dirty)}), + 'borrowed backing disjoint from owner') + self.busy, self.cursor = True, 0 + bank = self + + class Reentry(self.entry.Entry): + def new_port(self): + port = bank.take(self.w) + self.owned.append(port) + self.control += 1 + return port + + adapter = SimpleNamespace(Port=self.take, Entry=Reentry) + actual = bridge.RowEntry(self.w, records, adapter, producer, source, + dirty, widths, ell, level, start, row) + self.w.need(self.cursor == (63 if actual.active else 0), + 'complete fixed role acquisition') + return Lease(self, actual) + + def release(self): + self.w.need(self.busy, 'live bank') + # Fixed-role checks are paid local observations, never tail truncation. + for port in self.ports[:self.cursor]: + self.w.need(port.head == 1 and port.read() == self.w.BLANK, + 'retired numerical body') + port.step(-1) + self.w.need(port.read() == self.w.BLANK, 'retired owned marker') + port.step(1) + self.busy = False + + +class Lease: + def __init__(self, bank, actual): + self.bank, self.actual, self.closed = bank, actual, False + + def close(self): + self.bank.w.need(not self.closed, 'single row result retirement') + self.actual.close() + self.bank.release() + self.closed = True diff --git a/research/encoded-balanced-crt-inverse/source/research/encoded-balanced-crt-endpoint/endpoint.py b/research/encoded-balanced-crt-inverse/source/research/encoded-balanced-crt-endpoint/endpoint.py new file mode 100644 index 0000000000..b084d893bd --- /dev/null +++ b/research/encoded-balanced-crt-inverse/source/research/encoded-balanced-crt-endpoint/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-balanced-crt-inverse/source/research/encoded-balanced-crt-entry/frontend.py b/research/encoded-balanced-crt-inverse/source/research/encoded-balanced-crt-entry/frontend.py new file mode 100644 index 0000000000..8adbe2cfef --- /dev/null +++ b/research/encoded-balanced-crt-inverse/source/research/encoded-balanced-crt-entry/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-balanced-crt-inverse/source/research/encoded-crt-entry-lifecycle/entry.py b/research/encoded-balanced-crt-inverse/source/research/encoded-crt-entry-lifecycle/entry.py new file mode 100644 index 0000000000..1fa2b0cb88 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/source/research/encoded-crt-entry-lifecycle/entry.py @@ -0,0 +1,117 @@ +"""Guide-driven CRT numerical entry; no host width or bulk word constructor. +JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. +""" +from types import SimpleNamespace + +class Port: + def __init__(self,w): + self.w=w;self.cells=bytearray([w.BLANK]);self.head=0;self.meter=w.Meter() + self.write(w.LEFT);self.step(1) + def read(self): + self.meter.reads+=1 + return self.cells[self.head] if self.head=0,'unit local movement') + self.head+=d;self.meter.moves+=1 + def append(self,v): + self.w.need(self.read()==self.w.BLANK,'append blank');self.write(v);self.step(1) + def rewind(self): + self.step(-1) + while self.read()!=self.w.LEFT:self.step(-1) + self.step(1) + def clear(self): + self.rewind() + while self.read()!=self.w.BLANK:self.write(self.w.BLANK);self.step(1) + self.rewind() + def retire(self): + self.clear();self.step(-1);self.write(self.w.BLANK);self.step(1) + +class Extent: + """An encoded width value. Only the source's literal >=4 observation exists.""" + def __init__(self,guide,w):self.guide,self.w=guide,w + def __ge__(self,constant): + self.w.need(type(constant) is int and constant==4,'audited width observation') + good=True;g=self.guide + for _ in range(4): + if g.read()!=self.w.ONE:good=False;break + g.step(1) + g.rewind();return good + def __int__(self):raise ValueError('runtime width decode forbidden') + +class Entry: + def __init__(self,w,r,guide,dirty): + w.need(len(dirty)==8 and len({id(x) for x in [guide,*dirty]})==9,'eight distinct dirty ports') + self.w,self.r,self.guide,self.dirty=w,r,guide,tuple(dirty);self.owned=[];self.control=0;self.closed=False + width=Extent(guide,w);w.need(width>=4,'encoded width at least four') + a=object.__new__(w.Arena);a.bits=width;a.capacity=64;a.meter=w.Meter() + a.words=[];a.available=list(reversed(range(8,64)));a.live=set(range(8));self.arena=a + class HostedWord(w.Word): + @property + def cells(self):return self.port.cells + @property + def head(self):return self.port.head + @head.setter + def head(self,value):self.port.head=value + def wrap(port,slot): + word=object.__new__(HostedWord);word.arena=a;word.slot=slot;word.port=port;return word + for slot in range(64): + self.control+=1 + if slot<8:port=dirty[slot] + else:port=self.word_storage(False) + a.words.append(wrap(port,slot)) + a.template=wrap(self.word_storage(True),-1) + self.left,self.right,self.output=(self.new_port() for _ in range(3));self.output_taken=False + def new_port(self): + p=Port(self.w);self.owned.append(p);self.control+=1;return p + def word_storage(self,template): + p=self.new_port();g=self.guide;w=self.w + while g.read()==w.ONE:p.write(w.ZERO if template else w.BLANK);p.step(1);g.step(1) + w.need(g.read()==w.BLANK,'unary width guide');g.rewind() + p.write(w.RIGHT if template else w.BLANK);p.rewind();return p + def pad(self,source,target): + w,r,g=self.w,self.r,self.guide + while source.read()!=w.RIGHT: + w.need(source.read()==r.ROOT,'paired canonical tag');target.append(r.ROOT);source.step(1) + for _ in range(2): + seen=False;many=False;last=w.ZERO;ended=False + while g.read()==w.ONE: + if source.read()==r.WORD_END:ended=True + if ended:target.append(w.ZERO) + else: + bit=source.read();w.need(bit in (w.ZERO,w.ONE),'canonical bit') + many=seen;seen=True;last=bit;target.append(bit);source.step(1) + g.step(1) + w.need(g.read()==w.BLANK,'unary guide');g.rewind() + w.need(source.read()==r.WORD_END and seen and (last==w.ONE or not many),'canonical word fits width') + source.step(1);target.append(r.WORD_END) + w.need(source.read()==r.RECORD_END,'paired canonical end');source.step(1);target.append(r.RECORD_END) + target.append(w.RIGHT);target.rewind();source.rewind() + def output_factory(self): + self.w.need(not self.output_taken,'one output stream role');self.output_taken=True;return self.output + def invoke(self,producer,left,right): + self.w.need(not self.closed,'live context');self.pad(left,self.left);self.pad(right,self.right) + proxy=SimpleNamespace(**{n:getattr(self.r,n) for n in ('ROOT','RECORD_END','WORD_END','read_word','append_word')},Tape=self.output_factory) + old=self.w.Word.__init__;old_arena=self.w.Arena.__init__;inspect=self.w.Word.inspect + def forbidden(*args,**kwargs):raise ValueError('scientific host constructor/decode forbidden') + self.w.Word.__init__=forbidden;self.w.Arena.__init__=forbidden;self.w.Word.inspect=forbidden + try:return producer.produce(self.arena,self.left,self.right,self.w,proxy) + finally:self.w.Word.__init__=old;self.w.Arena.__init__=old_arena;self.w.Word.inspect=inspect + def consume(self,result): + self.arena.free_many(result['lower'],result['product']);result['stream'].clear() + self.left.clear();self.right.clear();self.output_taken=False + def close(self): + w=self.w;w.need(not self.closed and self.arena.live==set(range(8)),'terminal numerical owners') + # Retained private word backing is blank after free; remove its marker. + for word in self.arena.words[8:]: + word.rewind();w.need(word.read()==w.BLANK,'retired word body');word.step(-1) + # Word.write forbids LEFT/marker changes: the owned setup port performs this paid write. + port=word.port;port.write(w.BLANK);port.step(1) + self.arena.template.erase() + template=self.arena.template.port + template.step(-1);template.write(w.BLANK);template.step(1) + for p in (self.left,self.right,self.output):p.retire() + self.closed=True diff --git a/research/encoded-balanced-crt-inverse/source/research/encoded-current-crt/producer.py b/research/encoded-balanced-crt-inverse/source/research/encoded-current-crt/producer.py new file mode 100644 index 0000000000..a327b0161e --- /dev/null +++ b/research/encoded-balanced-crt-inverse/source/research/encoded-current-crt/producer.py @@ -0,0 +1,172 @@ +"""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.add(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-balanced-crt-inverse/source/research/r437-preparation-composition/predecessor4025/source/records.py b/research/encoded-balanced-crt-inverse/source/research/r437-preparation-composition/predecessor4025/source/records.py new file mode 100644 index 0000000000..4f00467a0f --- /dev/null +++ b/research/encoded-balanced-crt-inverse/source/research/r437-preparation-composition/predecessor4025/source/records.py @@ -0,0 +1,271 @@ +"""Sequential binary program/field records and typed continuation stacks. + +Runtime numerical words copy between tapes. Only tags, source codes, ranks +and row labels enter fixed finite control. Fixture encoding is separate. +""" +from words import BLANK, LEFT, ONE, RIGHT, ZERO, Meter, Unsigned, need + +WORD_END, RECORD_END = 5, 6 +ROOT, STEP, VALUE, CONSTANT, MULTIPLY, PAIR, RETURN = range(7, 14) +FINITE_BITS = 16 # Fixed vocabulary width for this compiled source instance. + + +class Tape: + def __init__(self): + self.cells = bytearray([LEFT]) + self.head = 1 + self.meter = Meter() + + def read(self): + self.meter.reads += 1 + return self.cells[self.head] if self.head < len(self.cells) else BLANK + + def write(self, symbol): + need(ZERO <= symbol <= RETURN, "fixed record alphabet") + self.meter.writes += 1 + if self.head >= len(self.cells): + self.cells.extend([BLANK]*(self.head+1-len(self.cells))) + self.cells[self.head] = symbol + + def step(self, direction): + need(direction in (-1, 1), "unit record-head move") + self.head += direction + need(self.head >= 0, "local record boundary") + self.meter.moves += 1 + + def append(self, symbol): + need(self.read() == BLANK, "append at record blank") + self.write(symbol) + self.step(1) + + def rewind(self): + self.step(-1) + while self.read() != LEFT: + self.step(-1) + self.step(1) + + def clear(self): + self.rewind() + while self.read() != BLANK: + self.write(BLANK) + self.step(1) + self.rewind() + + +def append_word(tape, word): + word.rewind() + while word.read() != RIGHT: + tape.append(word.read()) + word.step(1) + tape.append(WORD_END) + word.rewind() + + +def read_word(tape, arena): + out = arena.zero() + while tape.read() != WORD_END: + bit = tape.read() + need(bit in (ZERO, ONE) and out.read() != RIGHT, "encoded word extent") + out.write(bit) + out.step(1) + tape.step(1) + need(out.read() == RIGHT, "complete encoded word") + tape.step(1) + out.rewind() + return out + + +def append_finite(tape, value, bits=FINITE_BITS): + """Compile-time finite source/operation tag encoding.""" + need(0 <= value < 1 << bits, "compiled finite vocabulary") + for bit in range(bits): + tape.append((value >> bit) & 1) + tape.append(WORD_END) + + +def read_finite(tape, bits=FINITE_BITS): + # The accumulator ranges over a fixed finite set, independent of e/w/h. + state = 0 + for bit in range(bits): + value = tape.read() + need(value in (ZERO, ONE), "finite label bit") + state |= value << bit + tape.step(1) + need(tape.read() == WORD_END, "finite label delimiter") + tape.step(1) + return state + + +def seek_record(tape, index): + machine, arena = Unsigned(index.arena), index.arena + remaining, one = arena.copy(index), arena.literal(1) + tape.rewind() + while not remaining.zero(): + while tape.read() != RECORD_END: + need(tape.read() != BLANK, "record exists at global slot") + tape.step(1) + tape.step(1) + after = machine.subtract_exact(remaining, one) + arena.free(remaining) + remaining = after + arena.free_many(remaining, one) + + +class Stack: + def __init__(self, index_arena, residue_arena): + self.index_arena, self.residue_arena = index_arena, residue_arena + self.tape, self.reverse = Tape(), Tape() + + def empty(self): + self.tape.step(-1) + result = self.tape.read() == LEFT + self.tape.step(1) + return result + + def push(self, tag, *words): + need(tag in (VALUE, CONSTANT, MULTIPLY, PAIR, RETURN), "continuation kind") + need(len(words) == (2 if tag == VALUE else 1), "continuation arity") + self.tape.append(tag) + for word in words: + append_word(self.tape, word) + self.tape.append(RECORD_END) + + def pop(self): + need(not self.empty(), "nonempty continuation stack") + tape, reverse = self.tape, self.reverse + tape.step(-1) + need(tape.read() == RECORD_END, "continuation top delimiter") + tape.write(BLANK) + tape.step(-1) + while tape.read() not in (LEFT, RECORD_END): + reverse.append(tape.read()) + tape.write(BLANK) + tape.step(-1) + tape.step(1) + reverse.step(-1) + tag = reverse.read() + need(tag in (VALUE, CONSTANT, MULTIPLY, PAIR, RETURN), "encoded continuation kind") + reverse.write(BLANK) + reverse.step(-1) + arenas = (self.index_arena, self.index_arena) if tag == VALUE else (self.residue_arena,) + words = [] + for arena in arenas: + out = arena.zero() + while reverse.read() != WORD_END: + bit = reverse.read() + need(bit in (ZERO, ONE) and out.read() != RIGHT, "continuation binary word") + out.write(bit) + out.step(1) + reverse.write(BLANK) + reverse.step(-1) + need(out.read() == RIGHT, "complete continuation operand") + reverse.write(BLANK) + reverse.step(-1) + out.rewind() + words.append(out) + need(reverse.read() == LEFT, "complete continuation record") + reverse.step(1) + return tag, tuple(words) + + +class Program: + """Encoded root and admitted chronological steps; numerical fields are words.""" + def __init__(self, index_arena, residue_arena, code_bits=FINITE_BITS): + self.index_arena, self.residue_arena = index_arena, residue_arena + self.code_bits = code_bits + self.tape = Tape() + + def root(self): + self.tape.rewind() + need(self.tape.read() == ROOT, "root record") + self.tape.step(1) + size = read_word(self.tape, self.index_arena) + unit = read_word(self.tape, self.residue_arena) + depth = read_word(self.tape, self.index_arena) + need(self.tape.read() == RECORD_END, "root record end") + self.tape.rewind() + return size, unit, depth + + def step(self, level): + need(not level.zero(), "positive step level") + seek_record(self.tape, level) + need(self.tape.read() == STEP, "step record") + self.tape.step(1) + metadata = tuple(read_finite(self.tape, self.code_bits if field == 1 else FINITE_BITS) + for field in range(6)) + parent = read_word(self.tape, self.index_arena) + child = read_word(self.tape, self.index_arena) + need(self.tape.read() == RECORD_END, "step record end") + self.tape.rewind() + return metadata, parent, child + + @classmethod + def fixture(cls, index_arena, residue_arena, root_size, root_unit, events, code_bits=FINITE_BITS): + """Fixture-only serialization; runtime computes and validates extents.""" + out = cls(index_arena, residue_arena, code_bits) + out.tape.append(ROOT) + for arena, value in ((index_arena, root_size), (residue_arena, root_unit), (index_arena, len(events))): + word = arena.input(value) + append_word(out.tape, word) + arena.free(word) + out.tape.append(RECORD_END) + size = root_size + for kind, code, rank, field, reverse, half in events: + f = size//64 + child = rank*f if kind == 0 else f//2 if half else f + out.tape.append(STEP) + for field_index, label in enumerate((kind, code, rank, field, int(reverse), int(half))): + append_finite(out.tape, label, code_bits if field_index == 1 else FINITE_BITS) + for value in (size, child): + word = index_arena.input(value) + append_word(out.tape, word) + index_arena.free(word) + out.tape.append(RECORD_END) + size = child + out.tape.rewind() + return out + + +class Fields: + def __init__(self, index_arena, residue_arena, code_bits=FINITE_BITS): + self.index_arena, self.residue_arena = index_arena, residue_arena + self.code_bits = code_bits + self.tape = Tape() + + def check_code(self, slot, code): + seek_record(self.tape, slot) + observed = read_finite(self.tape, self.code_bits) + self.tape.rewind() + need(observed == code, "original global raw-field code") + + def end(self, after): + seek_record(self.tape, after) + complete = self.tape.read() == BLANK + self.tape.rewind() + need(complete, "exact frozen/current field prefix") + + def read(self, slot, code, depth): + need(Unsigned(self.index_arena).compare(slot, depth) < 0, "frozen field excludes current/future slot") + seek_record(self.tape, slot) + observed = read_finite(self.tape, self.code_bits) + need(observed == code, "exact encoded raw-field specification") + out = [[read_word(self.tape, self.residue_arena) for _ in range(64)] for _ in range(64)] + need(self.tape.read() == RECORD_END, "complete 64-dimensional raw high field") + self.tape.rewind() + return out + + @classmethod + def fixture(cls, index_arena, residue_arena, fields, code_bits=FINITE_BITS): + """Load canonical raw-field fixture data before measured execution.""" + out = cls(index_arena, residue_arena, code_bits) + for code, high in fields: + append_finite(out.tape, code, code_bits) + need(len(high) == 64 and all(len(row) == 64 for row in high), "field fixture shape") + for row in high: + for value in row: + word = residue_arena.input(value) + append_word(out.tape, word) + residue_arena.free(word) + out.tape.append(RECORD_END) + out.tape.rewind() + return out diff --git a/research/encoded-balanced-crt-inverse/source/research/r437-preparation-composition/predecessor4025/source/words.py b/research/encoded-balanced-crt-inverse/source/research/r437-preparation-composition/predecessor4025/source/words.py new file mode 100644 index 0000000000..8d4ba37e27 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/source/research/r437-preparation-composition/predecessor4025/source/words.py @@ -0,0 +1,415 @@ +"""Binary word tapes; unbounded numerical values stay in tape cells. + +Only zero/one carry states and fixed register/operation tags enter Python +control. Fixture loading/inspection methods are outside measured execution. +The arena bounds the tape inventory by a compile-time register capacity. +""" +ZERO, ONE, LEFT, RIGHT, BLANK = range(5) + + +def need(test, message): + if not test: + raise ValueError(message) + + +class Meter: + __slots__ = ("reads", "writes", "moves", "peak_live", "allocations") + + def __init__(self): + self.reads = self.writes = self.moves = self.peak_live = self.allocations = 0 + + def record(self): + return {name: getattr(self, name) for name in self.__slots__} + + +class Word: + __slots__ = ("arena", "slot", "cells", "head") + + def __init__(self, arena, slot): + self.arena, self.slot = arena, slot + self.cells = bytearray([LEFT] + [BLANK]*(arena.bits+1)) + self.head = 1 + + def read(self): + self.arena.meter.reads += 1 + return self.cells[self.head] + + def write(self, symbol): + need(symbol in (ZERO, ONE, RIGHT, BLANK), "word tape alphabet") + self.arena.meter.writes += 1 + self.cells[self.head] = symbol + + def step(self, direction): + need(direction in (-1, 1), "unit word-head movement") + self.head += direction + need(0 <= self.head < len(self.cells), "local word boundary") + self.arena.meter.moves += 1 + + def rewind(self): + self.step(-1) + while self.read() != LEFT: + self.step(-1) + self.step(1) + + def msb(self): + self.rewind() + while self.read() != RIGHT: + self.step(1) + self.step(-1) + + def zero(self): + self.rewind() + nonzero = False + while True: + bit = self.read() + if bit == RIGHT: + break + need(bit in (ZERO, ONE), "complete binary word") + nonzero = nonzero or bit == ONE + self.step(1) + self.rewind() + return not nonzero + + def erase(self): + self.rewind() + while self.read() != RIGHT: + self.write(BLANK) + self.step(1) + self.write(BLANK) + self.rewind() + + def inspect(self): + """Checker-only decoding; arithmetic code must not call this.""" + need(self.head == 1 and self.cells[-1] == RIGHT, "inspect a restored word") + return sum(bit << i for i, bit in enumerate(self.cells[1:-1])) + + +class Arena: + def __init__(self, bits, capacity=65536): + need(bits >= 2 and capacity > 0, "fixed word context") + self.bits, self.capacity = bits, capacity + self.meter = Meter() + self.words, self.available, self.live = [], [], set() + self.template = Word(self, -1) + self.template.cells[1:-1] = bytes([ZERO])*bits + self.template.cells[-1] = RIGHT + + def zero(self): + if self.available: + slot = self.available.pop() + out = self.words[slot] + else: + slot = len(self.words) + need(slot < self.capacity, "fixed register inventory") + out = Word(self, slot) + self.words.append(out) + need(slot not in self.live, "fresh numerical register") + self.live.add(slot) + self.meter.allocations += 1 + self.meter.peak_live = max(self.meter.peak_live, len(self.live)) + source = self.template + source.rewind() + while source.read() != RIGHT: + need(out.read() == BLANK, "erased register before reuse") + out.write(ZERO) + out.step(1) + source.step(1) + need(out.read() == BLANK, "erased right delimiter cell") + out.write(RIGHT) + out.rewind() + source.rewind() + return out + + def literal(self, value): + """Compile-time literal only; never decode a runtime word here.""" + need(isinstance(value, int) and value >= 0, "unsigned literal") + out = self.zero() + for bit in tuple((value >> i) & 1 for i in range(value.bit_length())): + need(out.read() != RIGHT, "literal fits the fixed word") + out.write(bit) + out.step(1) + out.rewind() + return out + + def input(self, value): + """Fixture-only loading of an encoded input word.""" + return self.literal(value) + + def copy(self, source): + need(source.arena is self, "one word extent") + out = self.zero() + source.rewind() + while source.read() != RIGHT: + out.write(source.read()) + source.step(1) + out.step(1) + out.rewind() + source.rewind() + return out + + def free(self, word): + need(word.arena is self and word.slot in self.live, "owned numerical register") + word.erase() + self.live.remove(word.slot) + self.available.append(word.slot) + + def free_many(self, *words): + for word in words: + self.free(word) + + def rollback(self, protected): + """Erase owned temporary roles on a rejecting path; capacity is fixed.""" + for slot in tuple(self.live): + if slot not in protected: + self.free(self.words[slot]) + for slot in protected: + self.words[slot].rewind() + + +class Unsigned: + def __init__(self, arena): + self.arena = arena + + def compare(self, a, b): + need(a.arena is b.arena is self.arena, "comparison word context") + if a is b: + return 0 + a.rewind() + b.rewind() + state = 0 + while a.read() != RIGHT: + x, y = a.read(), b.read() + need(x in (ZERO, ONE) and y in (ZERO, ONE), "comparison binary digits") + if x != y: + state = 1 if x == ONE else -1 + a.step(1) + b.step(1) + need(b.read() == RIGHT, "equal comparison extents") + a.rewind() + b.rewind() + return state + + def add(self, a, b): + out = self.arena.zero() + a.rewind() + b.rewind() + carry = 0 + while a.read() != RIGHT: + x, y = a.read(), b.read() + total = x+y+carry # Four finite carry states, not word arithmetic. + out.write(total & 1) + carry = total >> 1 + a.step(1) + if b is not a: + b.step(1) + out.step(1) + need(b.read() == RIGHT, "equal addition extents") + a.rewind() + b.rewind() + out.rewind() + return out, carry + + def subtract(self, a, b): + out = self.arena.zero() + a.rewind() + b.rewind() + borrow = 0 + while a.read() != RIGHT: + x, y = a.read(), b.read() + digit = x-y-borrow # One finite borrow bit. + out.write(digit & 1) + borrow = int(digit < 0) + a.step(1) + if b is not a: + b.step(1) + out.step(1) + need(b.read() == RIGHT, "equal subtraction extents") + a.rewind() + b.rewind() + out.rewind() + return out, borrow + + def subtract_exact(self, a, b): + out, borrow = self.subtract(a, b) + need(not borrow, "unsigned subtraction precondition") + return out + + def shift_add_bit(self, a, bit): + need(bit in (ZERO, ONE), "one incoming bit") + out = self.arena.zero() + a.rewind() + carry = bit + while a.read() != RIGHT: + previous = a.read() + out.write(carry) + carry = previous + a.step(1) + out.step(1) + a.rewind() + out.rewind() + need(not carry, "reserved high-bit margin") + return out + + def divmod(self, numerator, denominator): + need(not denominator.zero(), "nonzero binary divisor") + # A zero high bit leaves room for 2*remainder+bit. + denominator.msb() + margin = denominator.read() + denominator.rewind() + need(margin == ZERO, "binary divisor has the high-bit margin") + scan = self.arena.copy(numerator) + quotient, remainder = self.arena.zero(), self.arena.zero() + scan.msb() + quotient.msb() + while scan.read() != LEFT: + shifted = self.shift_add_bit(remainder, scan.read()) + self.arena.free(remainder) + if self.compare(shifted, denominator) >= 0: + remainder = self.subtract_exact(shifted, denominator) + self.arena.free(shifted) + quotient.write(ONE) + else: + remainder = shifted + quotient.write(ZERO) + scan.step(-1) + quotient.step(-1) + scan.step(1) + quotient.step(1) + self.arena.free(scan) + return quotient, remainder + + def times_small(self, a, constant): + """Multiply by a fixed finite matrix/rank label; preserve the word margin.""" + need(0 <= constant <= 128, "finite index multiplier") + result = self.arena.zero() + for bit in tuple((constant >> i) & 1 for i in range(constant.bit_length()-1, -1, -1)): + doubled, carry = self.add(result, result) + need(not carry, "index multiplication margin") + self.arena.free(result) + if bit: + result, carry = self.add(doubled, a) + need(not carry, "index multiplication extent") + self.arena.free(doubled) + else: + result = doubled + return result + + def increment_in_place(self, word): + """Ripple increment for a bounded address counter; restore its head.""" + word.rewind() + while word.read() == ONE: + word.write(ZERO) + word.step(1) + need(word.read() == ZERO, "ripple increment has space") + word.write(ONE) + word.rewind() + + +class Ring: + """Canonical residues modulo an encoded M>1 with one leading zero bit.""" + def __init__(self, modulus): + self.modulus, self.arena = modulus, modulus.arena + self.raw = Unsigned(self.arena) + self.one = self.arena.literal(1) + try: + need(self.raw.compare(modulus, self.one) > 0, "modulus exceeds one") + modulus.msb() + margin = modulus.read() + modulus.step(-1) + significant = modulus.read() + modulus.rewind() + need(margin == ZERO and significant == ONE, "canonical modulus word with one high-bit margin") + except ValueError: + self.arena.free(self.one) + raise + + def close(self): + self.arena.free(self.one) + + def add(self, a, b): + total, carry = self.raw.add(a, b) + need(not carry, "canonical modular addition margin") + if self.raw.compare(total, self.modulus) >= 0: + out = self.raw.subtract_exact(total, self.modulus) + self.arena.free(total) + return out + return total + + def subtract(self, a, b): + if self.raw.compare(a, b) >= 0: + return self.raw.subtract_exact(a, b) + larger, carry = self.raw.add(a, self.modulus) + need(not carry, "canonical modular subtraction margin") + out = self.raw.subtract_exact(larger, b) + self.arena.free(larger) + return out + + def negate(self, a): + zero = self.arena.zero() + out = self.subtract(zero, a) + self.arena.free(zero) + return out + + def multiply(self, a, b): + if a.zero() or b.zero(): + return self.arena.zero() + if self.raw.compare(a, self.one) == 0: + return self.arena.copy(b) + if self.raw.compare(b, self.one) == 0: + return self.arena.copy(a) + scan = self.arena.copy(b) + result = self.arena.zero() + scan.msb() + while scan.read() != LEFT: + doubled = self.add(result, result) + self.arena.free(result) + if scan.read() == ONE: + result = self.add(doubled, a) + self.arena.free(doubled) + else: + result = doubled + scan.step(-1) + scan.step(1) + self.arena.free(scan) + return result + + def inverse(self, a): + """Euclid, with Bezout coefficients reduced modulo M; None for nonunits.""" + r0, r1 = self.arena.copy(self.modulus), self.arena.copy(a) + t0, t1 = self.arena.zero(), self.arena.copy(self.one) + while not r1.zero(): + quotient, r2 = self.raw.divmod(r0, r1) + if self.raw.compare(quotient, self.modulus) >= 0: + reduced = self.raw.subtract_exact(quotient, self.modulus) + self.arena.free(quotient) + quotient = reduced + product = self.multiply(quotient, t1) + t2 = self.subtract(t0, product) + self.arena.free_many(quotient, 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 literal(self, constant): + """Compile a fixed signed integer through binary modular operations.""" + negative = constant < 0 + magnitude = abs(constant) + result = self.arena.zero() + instructions = tuple((magnitude >> i) & 1 for i in range(magnitude.bit_length()-1, -1, -1)) + for bit in instructions: + doubled = self.add(result, result) + self.arena.free(result) + if bit: + result = self.add(doubled, self.one) + self.arena.free(doubled) + else: + result = doubled + if negative: + out = self.negate(result) + self.arena.free(result) + result = out + return result diff --git a/research/encoded-balanced-crt-inverse/source/research/unconditional-batched-crt/check_batched_crt.py b/research/encoded-balanced-crt-inverse/source/research/unconditional-batched-crt/check_batched_crt.py new file mode 100644 index 0000000000..1cf78abccd --- /dev/null +++ b/research/encoded-balanced-crt-inverse/source/research/unconditional-batched-crt/check_batched_crt.py @@ -0,0 +1,265 @@ +"""Exact finite controls for the draft; not a machine-cost certificate.""" +import itertools +import json +import math + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def benes(permutation): + """Return (bit, switch table) layers on precisely len(permutation) wires.""" + size = len(permutation) + need(size >= 2 and size & (size - 1) == 0, "dyadic network size") + need(sorted(permutation) == list(range(size)), "permutation") + if size == 2: + return [(0, (permutation[0],) * 2)] + inverse = [0] * size + for x, y in enumerate(permutation): + inverse[y] = x + color = [-1] * size + for initial in range(size): + if color[initial] >= 0: + continue + color[initial] = 0 + stack = [initial] + while stack: + x = stack.pop() + for other in (x ^ 1, inverse[permutation[x] ^ 1]): + if color[other] < 0: + color[other] = color[x] ^ 1 + stack.append(other) + need(color[other] == color[x] ^ 1, "even cycle coloring") + first = tuple(color[x] ^ (x & 1) for x in range(size)) + last = tuple(color[inverse[y]] ^ (y & 1) for y in range(size)) + children = [] + for c in (0, 1): + child = [None] * (size // 2) + for x in range(size): + if color[x] == c: + child[x // 2] = permutation[x] // 2 + children.append(benes(child)) + result = [(0, first)] + for left, right in zip(*children): + need(left[0] == right[0], "common network schedule") + table = tuple((left, right)[x & 1][1][x // 2] for x in range(size)) + result.append((left[0] + 1, table)) + result.append((0, last)) + return result + + +def run_network(layers, value): + for bit, table in layers: + value ^= table[value] << bit + return value + + +def rotation(size, modulus, offset): + return tuple((x + offset) % modulus if x < modulus else x for x in range(size)) + + +def decode_group(values, moduli): + """Recover the integer from locally scaled CRT residues.""" + product = math.prod(moduli) + answer = 0 + prefix = 1 + for value, modulus in zip(values, moduli): + complement = product // modulus + residue = value * prefix % modulus + answer += residue * complement * pow(complement, -1, modulus) + prefix *= modulus + return answer % product + + +def balanced(values, moduli, reverse=False, compiled=False): + count = len(moduli) + need(count > 0 and count & (count - 1) == 0, "power-of-two axis count") + state = list(values) + levels = list(range(1, count.bit_length())) + for level in reversed(levels) if reverse else levels: + width = 1 << level + half = width // 2 + for start in range(0, count, width): + middle = start + half + valid = all(state[i] < moduli[i] for i in range(start, middle)) + lower = decode_group(state[start:middle], moduli[start:middle]) if valid else 0 + prefix = math.prod(moduli[start:middle]) + for i in range(middle, start + width): + offset = lower * pow(prefix, -1, moduli[i]) % moduli[i] + if reverse: + offset = -offset % moduli[i] + if compiled: + size = 1 << (moduli[i] - 1).bit_length() + state[i] = run_network(benes(rotation(size, moduli[i], offset)), state[i]) + elif state[i] < moduli[i]: + state[i] = (state[i] + offset) % moduli[i] + prefix *= moduli[i] + return tuple(state) + + +def direct(values, moduli): + prefix = 1 + integer = 0 + prefixes = [] + for value, modulus in zip(values, moduli): + prefixes.append(prefix) + integer += value * prefix + prefix *= modulus + return tuple(integer * pow(prefix, -1, modulus) % modulus + for prefix, modulus in zip(prefixes, moduli)) + + +def primitive_f(u, t, y, bits, positions, ybits, control_bits): + radix = 1 << bits + control_mask = (1 << control_bits) - 1 + ymask = (1 << ybits) - 1 + z = [(u >> (bits * i)) & 1 for i in range(len(positions))] + digits = [(t >> (bits * i)) & (radix - 1) for i in range(len(positions))] + y = (y + sum(2 * bit * digit * (1 << pos) + for bit, digit, pos in zip(z, digits, positions))) & ymask + t = (t + sum(((y >> pos) & 1) << (bits * i) + for i, pos in enumerate(positions))) & control_mask + digits = [(t >> (bits * i)) & (radix - 1) for i in range(len(positions))] + y = (y + sum(bit * (1 - 2 * digit) * (1 << pos) + for bit, digit, pos in zip(z, digits, positions))) & ymask + t = (t - sum((((y >> pos) & 1) ^ z[i]) << (bits * i) + for i, pos in enumerate(positions))) & control_mask + return u, t, y + + +def compact(u, t, y, source, bits=2, positions=(0,), ybits=6, control_bits=2): + need(control_bits >= bits * len(positions), "control field capacity") + mask = (1 << control_bits) - 1 + u, t, y = primitive_f(u, t, y, bits, positions, ybits, control_bits) + u = (u + sum(value << (bits * i) for i, value in enumerate(source(y)))) & mask + u, t, y = primitive_f(u, t, y, bits, positions, ybits, control_bits) + u = (u - sum(value << (bits * i) for i, value in enumerate(source(y)))) & mask + return u, t, y + + +def good(u, t, y, bits=2, positions=(0,), guard=6): + radix = 1 << bits + return all(((u >> (bits * i)) & (radix - 1)) != radix - 1 + and ((t >> (bits * i)) & (radix - 1)) != radix - 1 + and 2 * radix <= ((y >> (pos + 1)) & ((1 << (guard - 1)) - 1)) + < (1 << (guard - 1)) - 2 * radix + for i, pos in enumerate(positions)) + + +def linear_guard(u, t, y, bits=2, positions=(0,), guard=6, + control_bits=2, ybits=6): + """Bit-by-bit guard predicate; source functions are never evaluated.""" + steps = 0 + accepted = True + for word in (u, t): + for digit in range(len(positions)): + all_ones = True + for bit in range(bits): + all_ones = all_ones and bool((word >> (digit * bits + bit)) & 1) + steps += 1 + accepted = accepted and not all_ones + for pos in positions: + lower = 2 * (1 << bits) + upper = (1 << (guard - 1)) - lower + comparison = [0, 0] + for bit in range(guard - 2, -1, -1): + value = (y >> (pos + 1 + bit)) & 1 + for index, bound in enumerate((lower, upper)): + if comparison[index] == 0: + comparison[index] = value - ((bound >> bit) & 1) + steps += 2 + accepted = accepted and comparison[0] >= 0 and comparison[1] < 0 + need(steps <= 2 * control_bits + 2 * ybits, "linear tested-bit budget") + return accepted + + +def check(): + network_count = address_count = 0 + for bits in range(1, 7): + size = 1 << bits + for modulus in range(max(2, size // 2), size): + for offset in range(modulus): + permutation = rotation(size, modulus, offset) + layers = benes(permutation) + need(len(layers) == 2 * bits - 1, "network depth") + for bit, table in layers: + need(all(table[x] == table[x ^ (1 << bit)] for x in range(size)), + "switch control omits its target bit") + need(tuple(run_network(layers, x) for x in range(size)) == permutation, + "all-column modular rotation") + network_count += 1 + address_count += size + crt_addresses = valid_addresses = 0 + for moduli in ((3,), (3, 5), (3, 5, 7, 11)): + sizes = [1 << (s - 1).bit_length() for s in moduli] + seen = set() + for source in itertools.product(*(range(size) for size in sizes)): + target = balanced(source, moduli) + need(target not in seen, "padded CRT injection") + seen.add(target) + need(balanced(target, moduli, reverse=True) == source, "padded CRT inverse") + valid = all(x < s for x, s in zip(source, moduli)) + need(valid == all(x < s for x, s in zip(target, moduli)), "padding invariance") + if valid: + need(target == direct(source, moduli), "scaled CRT endpoint") + valid_addresses += 1 + need(balanced(source, moduli, compiled=True) == target, "compiled CRT endpoint") + crt_addresses += 1 + compact_cases = good_cases = repair_cases = 0 + functions = [lambda y: (0,), lambda y: (1,), lambda y: ((y >> 2) & 1,), + lambda y: ((y >> 1).bit_count() & 1,), + lambda y: ((((y >> 1) & 1) & ((y >> 4) & 1)),)] + for source_function, control_bits in itertools.product(functions, (2, 4)): + actual = {} + ideal = {} + for u, t, y in itertools.product(range(1 << control_bits), + range(1 << control_bits), range(64)): + start = (u, t, y) + end = compact(*start, source_function, control_bits=control_bits) + wanted = (u, t, y ^ source_function(y)[0]) + need(end not in actual, "actual gadget bijection") + need(wanted not in ideal, "ideal switch bijection") + actual[end] = start + ideal[wanted] = start + is_good = good(*start) + need(linear_guard(*start, control_bits=control_bits) == is_good, + "linear guard agrees with interval predicate") + need(good(*end) == is_good and good(*wanted) == is_good, "good/bad invariance") + if is_good: + need(end == wanted, "compact endpoint on good addresses") + good_cases += 1 + compact_cases += 1 + # Each arbitrary dirty input column follows S, then T S^-1 on bad holes. + for end, start in actual.items(): + u, t, y = start + repaired = (u, t, y ^ source_function(y)[0]) if not good(*end) else end + need(ideal[repaired] == start, "sparse correction column") + repair_cases += not good(*end) + multi_cases = 0 + def source_pair(y): + return (y >> 3) & 1, (y & ~65).bit_count() & 1 + for u, t in ((0, 0), (0, 15), (5, 5), (10, 10), (15, 0), (15, 15)): + for y in range(1 << 12): + start = (u, t, y) + end = compact(*start, source_pair, positions=(0, 6), ybits=12, control_bits=4) + f0, f1 = source_pair(y) + wanted = (u, t, y ^ f0 ^ (f1 << 6)) + is_good = good(*start, positions=(0, 6)) + need(linear_guard(*start, positions=(0, 6), control_bits=4, ybits=12) == is_good, + "two-target linear guard") + need(good(*end, positions=(0, 6)) == is_good, "two-target guard invariance") + if is_good: + need(end == wanted, "two-target compact endpoint") + multi_cases += 1 + return dict(status="PASS_FINITE_BATCHED_CRT_CONTROLS", network_count=network_count, + network_addresses=address_count, crt_addresses=crt_addresses, + valid_crt_addresses=valid_addresses, compact_addresses=compact_cases, + good_addresses=good_cases, repaired_bad_addresses=repair_cases, + two_target_addresses=multi_cases, linear_guard_verified=True, + machine_cost_verified=False, multiplication_kappa_claimed=False) + + +if __name__ == "__main__": + print(json.dumps(check(), sort_keys=True, indent=2)) diff --git a/research/encoded-balanced-crt-inverse/verify.py b/research/encoded-balanced-crt-inverse/verify.py new file mode 100644 index 0000000000..23887190e6 --- /dev/null +++ b/research/encoded-balanced-crt-inverse/verify.py @@ -0,0 +1,429 @@ +"""Source-pinned two-sided inverse tests and independent current-state oracle. + +All host integers, lists, decoding and snapshots here are observers. They +never supply a production coordinate, arithmetic result or runtime geometry. +Prepared for CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from contextlib import contextmanager +from hashlib import sha1, sha256 +from itertools import product +from math import prod +from pathlib import Path +from types import ModuleType, SimpleNamespace +import json +import sys + +HERE = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load(name, relative): + path = HERE/relative + module = ModuleType(name) + module.__file__ = str(path) + sys.modules[name] = module + exec(compile(path.read_bytes(), str(path), 'exec'), module.__dict__) + return module + + +def authenticate(): + pins = json.loads((HERE/'INPUT-PINS.json').read_text()) + for pin in pins: + raw = (HERE/pin['export_path']).read_bytes() + need(sha256(raw).hexdigest() == pin['sha256'], 'source SHA256') + need(sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() + == pin['git_blob'], 'source Git blob') + seam = json.loads((HERE/'SEAMS.json').read_text())['producer'] + base = (HERE/seam['source']).read_bytes() + before, after = seam['before'].encode(), seam['after'].encode() + need(base.count(before) == 1, 'unique subtractive producer seam') + expected = seam['prefix'].encode()+base.replace(before,after) + need((HERE/'inverse_producer.py').read_bytes() == expected, 'exact one-line specialization') + return len(pins) + + +def modules(): + root = 'source/research/' + w = load('words', root+'r437-preparation-composition/predecessor4025/source/words.py') + r = load('inverse_records', root+'r437-preparation-composition/predecessor4025/source/records.py') + e = load('inverse_entry', root+'encoded-crt-entry-lifecycle/entry.py') + n = load('forward_numeric', root+'encoded-current-crt/producer.py') + o = load('inverse_owner', root+'crt-persistent-numerical-owner/owner.py') + c = load('inverse_canonical', root+'crt-mixed-row-entry/bridge.py') + f = load('base_frontend', root+'encoded-balanced-crt-entry/frontend.py') + writer = load('unchanged_writer', root+'encoded-balanced-crt-endpoint/endpoint.py') + inverse = load('inverse_frontend', 'inverse_frontend.py') + subtractive = load('subtractive_numeric', 'inverse_producer.py') + oracle = load('pinned_balanced_oracle', root+'unconditional-batched-crt/check_batched_crt.py') + return SimpleNamespace(w=w, r=r, e=e, n=n, o=o, c=c, f=f, writer=writer, + inverse=inverse, subtractive=subtractive, oracle=oracle) + + +def fixture(m, moduli, widths, values, tail=0): + source, fields = m.e.Port(m.w), [] + for s, h, x in zip(moduli, widths, values, strict=True): + source.append(m.r.ROOT) + for _ in range(h): + source.append(m.w.ONE) + source.append(m.r.WORD_END) + for value, delimiter in ((s,m.r.WORD_END), (x,m.r.RECORD_END)): + begin = source.head + for bit in range(h): + source.append((value >> bit) & 1) + if delimiter == m.r.RECORD_END: + fields.append(tuple(range(begin, source.head))) + source.append(delimiter) + source.append(m.w.RIGHT) + source.rewind() + source.cells.extend((m.w.ONE,m.w.ZERO,m.w.BLANK)[j % 3] for j in range(tail)) + return source, fields + + +def values(source, fields): + return tuple(sum(source.cells[at] << j for j, at in enumerate(field)) + for field in fields) + + +def node_oracle(moduli, current, start, half, reverse): + left = moduli[start:start+half] + xs = current[start:start+half] + residues, prefix = [], 1 + for s, x in zip(left, xs): + residues.append(x*prefix % s) + prefix *= s + lower = 0 + if all(x < s for x, s in zip(xs, left)): + lower = next(k for k in range(prod(left)) + if all(k % s == y for s, y in zip(left, residues))) + result = list(current) + for i in range(start+half, start+2*half): + s, x = moduli[i], current[i] + offset = next(c for c in range(s) if (prefix*c-lower) % s == 0) + result[i] = (x-offset if reverse else x+offset) % s if x < s else x + prefix *= s + return tuple(result) + + +def poison(module): + def denied(*_args, **_kwargs): + raise ValueError('forbidden host geometry/decode') + for name in ('int','float','len','range','sum','min','max','enumerate','pow','sorted','zip'): + module.__dict__[name] = denied + + +@contextmanager +def sealed(m): + old = m.e.Port.__init__, m.w.Word.__init__, m.w.Arena.__init__, m.w.Word.inspect + def denied(*_args, **_kwargs): + raise ValueError('forbidden new physical role or host decode') + m.e.Port.__init__ = m.w.Word.__init__ = m.w.Arena.__init__ = m.w.Word.inspect = denied + try: + yield + finally: + m.e.Port.__init__, m.w.Word.__init__, m.w.Arena.__init__, m.w.Word.inspect = old + + +def blank(m, ports): + return all(p.head == 1 and all(x == m.w.BLANK for x in p.cells) for p in ports) + + +def actions(ports): + return sum(p.meter.reads+p.meter.writes+p.meter.moves for p in ports) + + +def owned(endpoint): + it = endpoint.iterator + return (*it.bank.ports, *it.guards, *it.counters.values(), endpoint.staging) + + +def handoff(m, endpoint, lease, precision, half): + it, w = endpoint.iterator, m.w + guide = lease.actual.guide + need(guide.cells[1:precision+1] == bytearray([w.ONE])*precision, + 'exact current precision tokens') + need(len(guide.cells) == precision+1 or guide.cells[precision+1] == w.BLANK, + 'current precision terminator') + for port in it.guards: + need(port.cells[:precision+2] == bytearray([w.LEFT]+[w.ZERO]*precision+[w.RIGHT]), + 'exact current protected width') + need(all(x == w.BLANK for x in port.cells[precision+2:]), 'blank old protected tail') + counter = it.counters['half'] + need(counter.cells[:half+2] == bytearray([w.LEFT]+[w.ONE]*half+[w.RIGHT]), + 'actual encoded node half size') + need(all(x == w.BLANK for x in counter.cells[half+2:]), 'blank old half-size tail') + + +def bounds(widths, trace, source_capacity, reverse): + a, d = sum(widths), len(widths) + length, pstar = 2+3*a+4*d, a+1 + numerical = (pstar+1)+2*(2*a+2*d+2)+57*(pstar+2)+3*(d*(pstar+2)+2) + space = numerical+8*(pstar+2)+6*(d+2)+(a+2)+length + cost = 2**19*(length+2)**2+4096 + coefficient = 2**21 if reverse else 2**20 + cost += sum(coefficient*(p+2)**4+2**16*(p+2)**2+4096 for p in trace) + return cost, source_capacity+space + + +def run_direction(m, source, fields, moduli, widths, reverse, + frontend=None, numeric=None): + initial = values(source, fields) + snapshot, source_id = bytes(source.cells), id(source.cells) + changed = set().union(*map(set, fields)) + before = actions([source]) + front = frontend or (m.inverse.bind(m.f) if reverse else m.f) + producer = numeric or (m.subtractive if reverse else m.n) + endpoint = m.writer.Endpoint(front,m.w,m.r,m.e,producer,m.o,m.c,source) + ports = owned(endpoint) + identities = tuple(id(p.cells) for p in ports) + need(len(ports) == 79 and len(set(identities)) == 79, '79 fixed owned roles') + stage, meters, precisions = endpoint.stage, [], [] + historical_lengths = [len(p.cells) for p in ports] + expected_precision = expected_half = None + def observed_stage(lease): + handoff(m,endpoint,lease,expected_precision,expected_half) + before_stage = bytes(source.cells), source.head + stage(lease) + need((bytes(source.cells),source.head) == before_stage, 'read-only numerical lease') + need(lease.actual.guide.head == 1 and lease.actual.result['stream'].head == 1, + 'consumed result heads returned') + need(endpoint.iterator.counters['axis'].head == 1 and + endpoint.iterator.counters['half'].head == 1, 'topology heads returned') + for i, port in enumerate(ports): + historical_lengths[i] = max(historical_lengths[i],len(port.cells)) + meters.append(lease.actual.context.arena.meter) + endpoint.stage = observed_stage + levels = tuple(range(1,len(moduli).bit_length())) + current = initial + with sealed(m): + for level in reversed(levels) if reverse else levels: + expected_half = 1 << (level-1) + for start in range(0,len(moduli),2*expected_half): + expected_precision = 1+sum(widths[start:start+2*expected_half]) + current = node_oracle(moduli,current,start,expected_half,reverse) + need(endpoint.step(), 'every current node executes') + need(values(source,fields) == current, 'independent current-node endpoint') + need(source.head == 1 and id(source.cells) == source_id, + 'actual source and head restored') + need(len(source.cells) == len(snapshot) and + all(source.cells[i] == x for i,x in enumerate(snapshot) if i not in changed), + 'metadata and old source tail preserved') + need(tuple(id(p.cells) for p in ports) == identities, 'stable complete history') + need(all(len(p.cells) >= size for p,size in zip(ports,historical_lengths)), + 'retained histories never shortened') + it = endpoint.iterator + need(blank(m,(*it.bank.ports,*it.guards,endpoint.staging)), + 'all current numerical/staging histories retired') + precisions.append(expected_precision) + need(not endpoint.step() and endpoint.iterator.closed, 'exact inverse termination') + need(current == m.oracle.balanced(initial,moduli,reverse=reverse), 'pinned full endpoint') + need(blank(m,ports), 'all 79 role histories blank') + work = actions([source,*ports])-before+sum(x.reads+x.writes+x.moves for x in meters) + time_bound, space_bound = bounds(widths,precisions,len(snapshot),reverse) + retained = len(source.cells)+sum(len(p.cells) for p in ports) + need(work <= time_bound and retained <= space_bound, 'complete source envelopes') + return endpoint, {'reverse':reverse, 'precisions':precisions,'actions':work, + 'raw_bound':time_bound,'retained':retained,'retained_bound':space_bound} + + +def round_trip(m, moduli, widths, original, tail): + result = [] + for first_reverse in (False,True): + source, fields = fixture(m,moduli,widths,original,tail) + snapshot = bytes(source.cells), source.head + first, one = run_direction(m,source,fields,moduli,widths,first_reverse) + second, two = run_direction(m,source,fields,moduli,widths,not first_reverse) + histories = (*owned(first),*owned(second)) + need(len(histories) == 158 and len({id(p.cells) for p in histories}) == 158, + 'two fresh invocations retain all 158 distinct histories') + need(blank(m,histories) and (bytes(source.cells),source.head) == snapshot, + 'two-sided exact full-source restoration') + joint = len(source.cells)+sum(len(p.cells) for p in histories) + bound = one['retained_bound']+two['retained_bound']-len(source.cells) + need(joint <= bound, 'both retained inventories charged') + result.append({'first_reverse':first_reverse,'calls':[one,two], + 'joint_retained':joint,'joint_bound':bound,'owned_roles':158}) + return {'moduli':list(moduli),'widths':list(widths),'input':list(original), + 'source_tail':tail,'round_trips':result} + + +def inverse_case(m, original=(0,1,2,1), frontend=None, numeric=None): + moduli, widths = (2,3,5,7), (2,2,3,3) + source, fields = fixture(m,moduli,widths,original,29) + answer = run_direction(m,source,fields,moduli,widths,True,frontend,numeric) + return source, fields, answer + + +def stale_provider(m): + """Bounded fault: third call rereads the old right-child left value 2. + + The real caller has restored that value to zero at the root. Only the + lower descriptor bit is temporarily altered; actual encoded arithmetic + then runs and the borrowed descriptor is restored. No production hook + or numerical replacement oracle is introduced. + """ + calls = 0 + def produce(arena, left, right, words, records): + nonlocal calls + calls += 1 + if calls != 3: + return m.subtractive.produce(arena,left,right,words,records) + for _ in range(10): + left.step(1) + old = left.read() + need(old == words.ZERO, 'fixture actual current-left bit is zero') + left.write(words.ONE) + left.rewind() + result = m.subtractive.produce(arena,left,right,words,records) + for _ in range(10): + left.step(1) + left.write(old) + left.rewind() + return result + return SimpleNamespace(produce=produce) + + +def bad_guards(m, dirty_tail): + base = m.inverse.bind(m.f).Iterator + class Iterator(base): + count = 0 + def _prepare_guards(self, guide): + super()._prepare_guards(guide) + self.count += 1 + if self.count != 2: + return + port = self.guards[0] + if dirty_tail: + for _ in range(11): + port.step(1) + port.write(self.w.ONE) + else: + for _ in range(5): + port.step(1) + for _ in range(6): + port.write(self.w.ZERO) + port.step(1) + port.write(self.w.RIGHT) + port.rewind() + return SimpleNamespace(Iterator=Iterator) + + +def controls(m): + labels = [] + def rejects(label, operation, message): + try: + operation() + except ValueError as error: + need(message in str(error), 'specific rejection for '+label+': '+str(error)) + labels.append(label) + else: + raise ValueError('undetected negative control: '+label) + rejects('forward_level_order_with_subtraction', + lambda: inverse_case(m,frontend=m.f), 'exact current precision tokens') + rejects('addition_in_inverse_nodes', lambda: inverse_case(m,numeric=m.n), + 'independent current-node endpoint') + rejects('stale_current_left_from_before_root', + lambda: inverse_case(m,numeric=stale_provider(m)), 'independent current-node endpoint') + rejects('old_root_precision_reused_at_smaller_child', + lambda: inverse_case(m,frontend=bad_guards(m,False)), 'exact current protected width') + rejects('nonblank_old_tail_past_shorter_current_guard', + lambda: inverse_case(m,frontend=bad_guards(m,True)), 'blank old protected tail') + base = m.inverse.bind(m.f).Iterator + class FreshRole(base): + def _double_half(self): + self.e.Port(self.w) + super()._double_half() + rejects('hidden_new_role_at_reverse_level_transition', + lambda: inverse_case(m,frontend=SimpleNamespace(Iterator=FreshRole)), + 'forbidden new physical role') + class Doubled(base): + def _double_half(self): + m.f.Iterator._double_half(self) + rejects('doubling_instead_of_reverse_halving', + lambda: inverse_case(m,frontend=SimpleNamespace(Iterator=Doubled)), + 'complete selected node') + class Shortened(base): + def _double_half(self): + super()._double_half() + self.counters['half'].cells.pop() + rejects('silently_shortened_historical_backing', + lambda: inverse_case(m,frontend=SimpleNamespace(Iterator=Shortened)), + 'retained histories never shortened') + wrong = SimpleNamespace(produce=lambda a,l,r,w,rec: + m.subtractive.produce(a,l,r,w,rec,fault='treat_current_as_original')) + rejects('current_child_misread_as_original_digits', + lambda: inverse_case(m,(1,1,1,1),numeric=wrong), 'independent current-node endpoint') + source, fields, _ = inverse_case(m,(1,3,1,1)) + need(values(source,fields) == (1,3,1,5), 'actual globally invalid inverse witness') + rejects('global_invalid_identity_shortcut', + lambda: need(values(source,fields) == (1,3,1,1),'invalid rectangle is not pointwise fixed'), + 'not pointwise fixed') + source, fields = fixture(m,(2,3,5,7),(2,2,3,3),(0,1,2,1)) + endpoint = m.writer.Endpoint(m.inverse.bind(m.f),m.w,m.r,m.e,m.subtractive,m.o,m.c,source) + before = bytes(source.cells), source.head + lease = endpoint.iterator.next() + endpoint.stage(lease) + rejects('source_write_before_inverse_result_retirement',endpoint.commit, + 'follows numerical retirement') + need((bytes(source.cells),source.head) == before, 'rejected write preserves source') + lease.close() + endpoint.commit() + endpoint.iterator.close() + need(blank(m,owned(endpoint)), 'paid early-close cleanup') + return labels + + +def complete_run_driver(m): + source, fields = fixture(m,(2,3,5,7),(2,2,3,3),(0,1,2,1),47) + calls = 0 + def observed_produce(*args): + nonlocal calls + calls += 1 + return m.subtractive.produce(*args) + endpoint = m.writer.Endpoint(m.inverse.bind(m.f),m.w,m.r,m.e, + SimpleNamespace(produce=observed_produce),m.o,m.c,source) + with sealed(m): + endpoint.run() # No verifier-supplied iteration count or schedule. + need(calls == 3 and values(source,fields) == (0,1,0,0), 'complete encoded run driver') + need(source.head == 1 and blank(m,owned(endpoint)), 'complete run ownership') + return {'actual_numerical_nodes':calls,'owned_roles':79, + 'verifier_schedule_supplied':False,'output':list(values(source,fields))} + + +def main(): + count = authenticate() + m = modules() + for module in (m.f,m.writer,m.inverse): + poison(module) + cases = [round_trip(m,(3,5),(2,3),x,17) for x in product(range(4),range(8))] + four = ((0,0,0,0),(1,2,4,6),(1,1,1,1),(3,2,4,6),(1,3,4,6), + (1,2,7,6),(1,2,4,7),(3,3,7,7),(0,2,1,5),(1,0,3,2), + (0,0,7,7),(1,1,0,0),(0,1,0,0),(0,1,2,1),(1,3,1,1)) + cases += [round_trip(m,(2,3,5,7),(2,2,3,3),x,31) for x in four] + cases += [round_trip(m,(4,9),(3,4),x,23) + for x in ((3,8),(7,15),(4,1),(1,9))] + for x in ((2,4,6,10,12,16,18,22),(7,4,6,10,12,16,18,31)): + cases.append(round_trip(m,(3,5,7,11,13,17,19,23), + (4,4,4,4,4,5,5,5),x,97)) + result = {'status':'PASS_ENCODED_BALANCED_CRT_INVERSE','source_count':count, + 'cases':cases,'cases_count':len(cases),'owned_roles_per_invocation':79, + 'owned_roles_per_fresh_round_trip':158, + 'actual_numerical_nodes':sum(len(call['precisions']) for case in cases + for trip in case['round_trips'] for call in trip['calls']), + 'controls':controls(m),'complete_run_driver':complete_run_driver(m),'new_kappa':None, + 'scope':'one balanced address-state inverse; no payload or raw compact inverse'} + rendered = json.dumps(result,sort_keys=True,indent=2)+'\n' + if '--write-result' in sys.argv: + (HERE/'RESULT.json').write_text(rendered) + else: + need(rendered == (HERE/'RESULT.json').read_text(), 'frozen exact receipt') + print(result['status'],'cases='+str(len(cases)), + 'nodes='+str(result['actual_numerical_nodes']), + 'roles=79/158','controls='+str(len(result['controls']))) + + +if __name__ == '__main__': + main() From 8c0e55c9ba25ff2c8199b01539a4d56ae71a1473 Mon Sep 17 00:00:00 2001 From: Jerry Jiaheng Chen <80299683+CubeJerry@users.noreply.github.com> Date: Wed, 11 Nov 2026 22:53:19 +0800 Subject: [PATCH 2/2] Use the repository's accepted replay metadata values; preserve reviewed scientific bytes --- research/encoded-balanced-crt-inverse/TASK.json | 2 +- research/encoded-balanced-crt-inverse/VALIDATION.json | 7 ++++--- research/encoded-balanced-crt-inverse/VERIFY.json | 2 +- 3 files changed, 6 insertions(+), 5 deletions(-) diff --git a/research/encoded-balanced-crt-inverse/TASK.json b/research/encoded-balanced-crt-inverse/TASK.json index 37698991c2..9278a6a5b3 100644 --- a/research/encoded-balanced-crt-inverse/TASK.json +++ b/research/encoded-balanced-crt-inverse/TASK.json @@ -68,7 +68,7 @@ "bottleneck_link": "Source-specific uniform encoded inverse and ownership/precision progress; it does not discharge any of the five selected assumptions or improve complete kappa.", "budget_minutes": 60, "stop_rule": "Stop on exact same-interface predecessor overlap, host geometry/traversal history, unretired source mutation, more than 79 roles, or failure of the complete O(A^4) source-time and K_source+O(A^2) history bill. No payload or raw compact inverse expansion.", - "outcome": "independently_reviewed_scoped_source_model_result", + "outcome": "completed", "evidence": "PROOF.md; exact INPUT-PINS and SEAMS; author strict normal/optimized replays; REVIEW.md and PEER-REVIEW.md; independent 20-case/52-node inverse oracle.", "author": "Jerry Chen / CubeJerry", "ai_assistance": "Substantial OpenAI assistance; independent AI source/proof review, not human or proof-kernel acceptance", diff --git a/research/encoded-balanced-crt-inverse/VALIDATION.json b/research/encoded-balanced-crt-inverse/VALIDATION.json index 8a30755d2f..7e47741135 100644 --- a/research/encoded-balanced-crt-inverse/VALIDATION.json +++ b/research/encoded-balanced-crt-inverse/VALIDATION.json @@ -31,8 +31,8 @@ "REVIEW.md": "640242a47ad54ff00d20df6a9b2ac56b0f9fa1af52b88f5d64d63f0838603e58", "SEAMS.json": "3a942dc7e32f898037362c00def8abddcfd41cf0ec3cb66899dd66c5380a9e97", "SOURCES.json": "83d08cde522eb91c9c859c58f3bdb5523c4087dea7b31e96f015ded859e0b9c4", - "TASK.json": "f671c39bb1ded5c7de1b9b5738d3823ee330709bb87b0f4cacf833b7bc346a96", - "VERIFY.json": "9d2ef9c83ef1de6a011cb3d38ab69d85e4a8406d6f8be2d6d929cdc3eb92c3cf", + "TASK.json": "10d915cf9122becf0cdf57361dc14636c1129ed912cd06da4656ee664bd1e6a2", + "VERIFY.json": "f2853a880802021dec61d9ba45c9220e9102fee8da8687ccad7f10aae9713d53", "independent_check.py": "2db9feb63c21257fc36d1db428d66f3ebf48c0c15fd6d689020b026627ea91ad", "inverse_frontend.py": "0e5f4c9450372c90000f5ebf3c22dfbe7241dd53da9ae9bcce310af859b009ef", "inverse_producer.py": "6acdebee7134fbc8e2d121060286bd05e7282900da8a28a78c80937dde7ea178", @@ -46,5 +46,6 @@ "source/research/r437-preparation-composition/predecessor4025/source/words.py": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9", "source/research/unconditional-batched-crt/check_batched_crt.py": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e", "verify.py": "8ca14c361bd32666e6f94b8f5827b43879ecfc6b90fc56eff5ceaf77612c902d" - } + }, + "metadata_note": "VERIFY.json uses required ready and TASK.json uses required completed; detailed independent acceptance remains in review and validation files." } diff --git a/research/encoded-balanced-crt-inverse/VERIFY.json b/research/encoded-balanced-crt-inverse/VERIFY.json index cd175f6c53..1ccff63d3b 100644 --- a/research/encoded-balanced-crt-inverse/VERIFY.json +++ b/research/encoded-balanced-crt-inverse/VERIFY.json @@ -1,6 +1,6 @@ { "schema_version": 1, - "status": "independently_reviewed", + "status": "ready", "python": "3.12", "requirements": [], "inputs": [],