From 532b60ac427f47191175aba2e1317db0f3508d51 Mon Sep 17 00:00:00 2001 From: Jerry Jiaheng Chen <80299683+CubeJerry@users.noreply.github.com> Date: Wed, 11 Nov 2026 21:53:16 +0800 Subject: [PATCH 1/2] Execute encoded balanced CRT source-state commits with a paid owned lifecycle --- .../CHECKPOINT.json | 23 + .../INDEPENDENT-RESULT.json | 468 +++++++ .../INPUT-PINS.json | 65 + .../PR-DESCRIPTION.md | 88 ++ .../PR-TITLE.txt | 1 + .../encoded-balanced-crt-endpoint/PROOF.md | 347 +++++ .../encoded-balanced-crt-endpoint/README.md | 92 ++ .../encoded-balanced-crt-endpoint/RESULT.json | 1223 +++++++++++++++++ .../encoded-balanced-crt-endpoint/REVIEW.md | 150 ++ .../SOURCES.json | 55 + .../encoded-balanced-crt-endpoint/TASK.json | 101 ++ .../encoded-balanced-crt-endpoint/VERIFY.json | 47 + .../encoded-balanced-crt-endpoint/endpoint.py | 157 +++ .../independent_check.py | 248 ++++ .../research/crt-mixed-row-entry/bridge.py | 93 ++ .../crt-persistent-numerical-owner/owner.py | 77 ++ .../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 ++++++ .../encoded-balanced-crt-endpoint/verify.py | 299 ++++ 22 files changed, 4786 insertions(+) create mode 100644 research/encoded-balanced-crt-endpoint/CHECKPOINT.json create mode 100644 research/encoded-balanced-crt-endpoint/INDEPENDENT-RESULT.json create mode 100644 research/encoded-balanced-crt-endpoint/INPUT-PINS.json create mode 100644 research/encoded-balanced-crt-endpoint/PR-DESCRIPTION.md create mode 100644 research/encoded-balanced-crt-endpoint/PR-TITLE.txt create mode 100644 research/encoded-balanced-crt-endpoint/PROOF.md create mode 100644 research/encoded-balanced-crt-endpoint/README.md create mode 100644 research/encoded-balanced-crt-endpoint/RESULT.json create mode 100644 research/encoded-balanced-crt-endpoint/REVIEW.md create mode 100644 research/encoded-balanced-crt-endpoint/SOURCES.json create mode 100644 research/encoded-balanced-crt-endpoint/TASK.json create mode 100644 research/encoded-balanced-crt-endpoint/VERIFY.json create mode 100644 research/encoded-balanced-crt-endpoint/endpoint.py create mode 100644 research/encoded-balanced-crt-endpoint/independent_check.py create mode 100644 research/encoded-balanced-crt-endpoint/source/research/crt-mixed-row-entry/bridge.py create mode 100644 research/encoded-balanced-crt-endpoint/source/research/crt-persistent-numerical-owner/owner.py create mode 100644 research/encoded-balanced-crt-endpoint/source/research/encoded-balanced-crt-entry/frontend.py create mode 100644 research/encoded-balanced-crt-endpoint/source/research/encoded-crt-entry-lifecycle/entry.py create mode 100644 research/encoded-balanced-crt-endpoint/source/research/encoded-current-crt/producer.py create mode 100644 research/encoded-balanced-crt-endpoint/source/research/r437-preparation-composition/predecessor4025/source/records.py create mode 100644 research/encoded-balanced-crt-endpoint/source/research/r437-preparation-composition/predecessor4025/source/words.py create mode 100644 research/encoded-balanced-crt-endpoint/verify.py diff --git a/research/encoded-balanced-crt-endpoint/CHECKPOINT.json b/research/encoded-balanced-crt-endpoint/CHECKPOINT.json new file mode 100644 index 0000000000..4fd4efb842 --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/CHECKPOINT.json @@ -0,0 +1,23 @@ +{ + "base": "e54523517d0f03e58352e647c403a5af3e525a57", + "status": "complete; independent source/proof review and final strict reproduction passed", + "package": "research/encoded-balanced-crt-endpoint", + "core_sha256": { + "endpoint.py": "c24ae2c90d175d276120438809e7c7401b8a8c04dec139f1b7345e9778984ced", + "verify.py": "19954541b1677d926c7a0f0e7466d437ecd6eef0cde2c03a0ab71ad168a48c87", + "PROOF.md": "a20c90aada4ea2d9141a465b10bd1d54a1047b52608bb19c88efa7fd98eeacf3", + "INPUT-PINS.json": "d7749cb00e6c86b42fd21f0263051c2d8eb2d752c2bd29fc261b2a2da03801fc", + "RESULT.json": "2d75ea3687028911e523fff368eb7699b9dc194c757e6ba6e4a9444c00bcd2ed" + }, + "checks": [ + "Python 3.12.14 strict normal verifier PASS 45 cases / 75 nodes / 79 owned roles / 8 controls", + "Python 3.12.14 strict optimized verifier PASS; same frozen RESULT", + "Independent source/proof review PASS; 18 cases / 46 nodes; source contract and scope retained", + "Root reran strict normal and optimized author verifier and independent checker from final self-contained package; PASS" + ], + "next": [ + "Reproduce commands in VERIFY.json from this package", + "Inspect remote committed tree and source pins after publication", + "Select a separately claimed next obligation; do not infer assumption discharge" + ] +} diff --git a/research/encoded-balanced-crt-endpoint/INDEPENDENT-RESULT.json b/research/encoded-balanced-crt-endpoint/INDEPENDENT-RESULT.json new file mode 100644 index 0000000000..9a84e936d4 --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/INDEPENDENT-RESULT.json @@ -0,0 +1,468 @@ +{ + "status": "PASS", + "method": "direct CRT idempotents plus independent global closed form", + "cases": 18, + "nodes": 46, + "negative_controls": [ + "stale-coordinate commit rejected" + ], + "rows": [ + { + "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, + 1 + ], + "adapter_actions": 771, + "numeric_actions": 34754, + "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, + 4 + ], + "adapter_actions": 1080, + "numeric_actions": 80685, + "staging_backing": 31, + "staging_visited": 32 + }, + { + "axes": 2, + "widths": [ + 9, + 9 + ], + "nodes": 1, + "original": [ + 16, + 256 + ], + "result": [ + 16, + 136 + ], + "adapter_actions": 2213, + "numeric_actions": 345844, + "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, + 1, + 4, + 3 + ], + "adapter_actions": 6219, + "numeric_actions": 532086, + "staging_backing": 60, + "staging_visited": 61 + }, + { + "axes": 4, + "widths": [ + 3, + 4, + 3, + 4 + ], + "nodes": 3, + "original": [ + 2, + 1, + 4, + 6 + ], + "result": [ + 2, + 1, + 4, + 4 + ], + "adapter_actions": 6219, + "numeric_actions": 530278, + "staging_backing": 60, + "staging_visited": 61 + }, + { + "axes": 4, + "widths": [ + 3, + 4, + 3, + 4 + ], + "nodes": 3, + "original": [ + 1, + 3, + 4, + 6 + ], + "result": [ + 1, + 3, + 4, + 4 + ], + "adapter_actions": 6219, + "numeric_actions": 528013, + "staging_backing": 60, + "staging_visited": 61 + }, + { + "axes": 4, + "widths": [ + 3, + 4, + 3, + 4 + ], + "nodes": 3, + "original": [ + 1, + 2, + 5, + 6 + ], + "result": [ + 1, + 1, + 5, + 5 + ], + "adapter_actions": 6219, + "numeric_actions": 522519, + "staging_backing": 60, + "staging_visited": 61 + }, + { + "axes": 4, + "widths": [ + 3, + 4, + 3, + 4 + ], + "nodes": 3, + "original": [ + 1, + 2, + 4, + 7 + ], + "result": [ + 1, + 1, + 4, + 7 + ], + "adapter_actions": 6219, + "numeric_actions": 519032, + "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, + 2, + 2 + ], + "adapter_actions": 6219, + "numeric_actions": 530507, + "staging_backing": 60, + "staging_visited": 61 + }, + { + "axes": 4, + "widths": [ + 4, + 3, + 4, + 3 + ], + "nodes": 3, + "original": [ + 1, + 0, + 2, + 4 + ], + "result": [ + 1, + 2, + 3, + 0 + ], + "adapter_actions": 6219, + "numeric_actions": 529812, + "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, + 1, + 4, + 3, + 10, + 10, + 2, + 1 + ], + "adapter_actions": 34085, + "numeric_actions": 6015165, + "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, + 4, + 10, + 15, + 16, + 31 + ], + "adapter_actions": 34085, + "numeric_actions": 5870278, + "staging_backing": 142, + "staging_visited": 143 + } + ], + "pins": { + "endpoint.py": "c24ae2c90d175d276120438809e7c7401b8a8c04dec139f1b7345e9778984ced", + "independent_check.py": "b1d22ea3c046f77e88fd30c3233a9974a0150189ca598f81825776a81b5a9ff5", + "source/research/crt-mixed-row-entry/bridge.py": "89c38638c0d66da731566c903c32e7fa1ad31088d29cfd2634fce823dd07c1f9", + "source/research/crt-persistent-numerical-owner/owner.py": "1d73f432f8de9c791260c43335eb207d82bbb3f5b190cc76d0d914a4db076f41", + "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", + "verify.py": "19954541b1677d926c7a0f0e7466d437ecd6eef0cde2c03a0ab71ad168a48c87" + }, + "proof_sha256": "a20c90aada4ea2d9141a465b10bd1d54a1047b52608bb19c88efa7fd98eeacf3" +} diff --git a/research/encoded-balanced-crt-endpoint/INPUT-PINS.json b/research/encoded-balanced-crt-endpoint/INPUT-PINS.json new file mode 100644 index 0000000000..bda585dc26 --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/INPUT-PINS.json @@ -0,0 +1,65 @@ +[ + { + "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" + } +] diff --git a/research/encoded-balanced-crt-endpoint/PR-DESCRIPTION.md b/research/encoded-balanced-crt-endpoint/PR-DESCRIPTION.md new file mode 100644 index 0000000000..c99d9f96da --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/PR-DESCRIPTION.md @@ -0,0 +1,88 @@ +## Result + +This closes one changing-source consumer boundary after #7154: its actual +encoded balanced-node iterator now feeds a paid whole-node result projection +and same-source commit, producing the complete forward balanced CRT +address-state endpoint without host node/width/precision/coordinate arguments. +The source-relative proof uses **79 stable owned roles**, O(p^4) complete +source-model time and K_source + O(p^2) historical backing. **No new kappa.** + +The consumer stages the full framed source while the numerical result is +live, copies whole-node updated-coordinate fields, validates every high bit +beyond its destination width, retires the lease, and commits to the same +owned source. Preserved metadata reestablishes the encoded iterator invariant, +so the next node reads the actual newly committed coordinates. + +## Novelty and predecessor work + +#7154 supplies the physical numerical-node iterator and leaves its source +read-only. #7152 supplies the full source-state tree at compiled micro-row +geometry. #5053 already supplies whole-node updated coordinates; #5496 +correctly discards those values when building a single micro-row. #5625 +supplies the earlier retire-before-source-write principle. This contribution +is the exact uniform consumer join, heterogeneous-width projection, encoded +topology preservation lemma, and its complete occurrence/history budget. +It does not claim new CRT identities or generic disjoint-support commutation. + +## Source pins and checks + +Canonical base: `e54523517d0f03e58352e647c403a5af3e525a57`. +Runtime frontend #7154: `cc35ecedce6f208d5056fab6d17c58555affc73c`. +Endpoint-comparison #7152: `66adbede4bd4ab603ba3e0a7f6708403905b753c`. +All seven runtime inputs are unchanged byte-pinned exports inside this package; +direct replay requires no network or nonancestor Git object. + +From `research/encoded-balanced-crt-endpoint`, Python 3.12: + +```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_ENDPOINT cases=45 nodes=75 owned_roles=79 controls=8 +``` + +The family includes all 32 padded pairs for (3,5), twelve four-axis states, +and one eight-axis tree. Independent congruence enumeration checks each node; +a different global mixed-radix formula checks valid endpoints. The tests +authenticate source bytes and inspect all 79 role histories, source metadata, +nonblank old tails, stable backing identities, boundary heads and cleanup. +Eight negative controls exercise stale/wrong projection, overflow, lifecycle +ordering and erasure. Runtime geometry/decode functions are poisoned and +constructors sealed after fixed-role acquisition. Full evidence is in +PROOF.md, RESULT.json, INPUT-PINS.json, TASK.json and VERIFY.json. + +A separate reviewer read the complete source chain and proof. Its own checker, +which does not invoke the author verifier, uses CRT idempotent sums and passes +18 cases / 46 nodes, including padded-invalid axes, mixed widths, changing +precision and hostile source tails; a stale-coordinate mutant is rejected. +Reproduce with `python3.12 -I -W error -B independent_check.py .`. +See REVIEW.md and INDEPENDENT-RESULT.json for the independent receipt. + +## Limitations and open obligations + +This is one address-state evaluator. It does not move a payload indexed by +all addresses, produce encoded micro-row/ROM selections, implement inverse +traversal or the complete three-epoch key, or lower the providers to a +bit-Turing-machine program. The source-operation theorem retains an +unspecified fixed finite-control refinement constant. Allocated backing and +visited positions are distinguished: the staging role retains M cells but +transiently visits index M, so a visited-span caller pays M+1. Predecessor +numerical/frontend contracts remain premises. Malformed-provider detection +does not establish arbitrary error rollback or dirty-memory allocation. + +All five selected foundational assumptions remain conditional. The selected +complete bound remains at kappa 0.00363005817; this is an enabling lemma, +not supplier admission or an unconditional multiplication theorem. + +## Credit + +Prepared for Jerry Chen / @CubeJerry with substantial OpenAI assistance. +Credit #7154/#7152; JoyboyBrian's #5053/#5219/#5505/#5496 numerical, entry, +owner and query work; Ali Romman's #5353/#5625 source/retirement work; +Cinna Davis's #4100 CRT/Beneš construction; Hiroki KUMAZAKI, ToikY, +commdata2338 and all unchanged source notices. Separate AI cross-review is +distinct from independent human or formal-kernel acceptance. Apache-2.0. diff --git a/research/encoded-balanced-crt-endpoint/PR-TITLE.txt b/research/encoded-balanced-crt-endpoint/PR-TITLE.txt new file mode 100644 index 0000000000..c673234b80 --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/PR-TITLE.txt @@ -0,0 +1 @@ +Execute the complete balanced CRT address-state endpoint from encoded source with a paid 79-role commit lifecycle (no new kappa) diff --git a/research/encoded-balanced-crt-endpoint/PROOF.md b/research/encoded-balanced-crt-endpoint/PROOF.md new file mode 100644 index 0000000000..d3b9ce4fae --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/PROOF.md @@ -0,0 +1,347 @@ +# Uniform balanced CRT address-state evaluation through a paid source commit + +Prepared for Jerry Chen / @CubeJerry with substantial OpenAI assistance. +Apache-2.0. Canonical base: `e54523517d0f03e58352e647c403a5af3e525a57`. +This is a source-relative enabling construction, **no new kappa**. + +## 1. Exact claim and predecessor boundary + +Supply the physical padded axis stream admitted by #5353 and #7154. There +are d >= 2 axes, with d a power of two, declared widths h_i in {ell-1,ell}, +ell >= 2, pairwise coprime moduli 2 <= s_i < 2^h_i, and arbitrary padded +coordinates 0 <= x_i < 2^h_i. All admitted h_i are consequently at least +two. Each record is ROOT, h_i unary ONE symbols, WORD_END, h_i modulus bits, +WORD_END, h_i coordinate bits, RECORD_END. LEFT is at cell zero and RIGHT +terminates the logical source. Its head enters at one. Write + + A = sum_i h_i, M = 2 + 3A + 4d, P_G = 1 + sum_(i in G) h_i. + +The supplied source has historical capacity K_source >= M. Its inaccessible +tail after RIGHT is retained and charged, including any old data there. +The source is owned by this enclosing evaluator. It is borrowed read-only +by each individual numerical invocation. + +**Theorem (relative to the pinned numerical and frontend source contracts).** +The fixed finite-symbol program `endpoint.Endpoint.run`, receiving only +that source and its fixed provider modules, computes the complete forward +balanced CRT *address-state* endpoint on that same source. It enumerates +each aligned node exactly once, in increasing level and start order, +using the unchanged #7154 encoded iterator. Each node reads the actual +coordinates left by all earlier commits. There are no runtime host integers +for coordinates, moduli, widths, precision, level, node start or axis count. + +Only coordinate bits may change in the final source. Every other cell, +including the source's historical tail, is preserved, its backing object +and capacity are unchanged, and its head returns to one. There are exactly +79 owned roles: the predecessor's 78 roles and one full-source staging +role. Upon successful completion every owned historical cell is blank and +every owned head is one. One lifecycle is claimed; no persistent restart +or arbitrary dirty-backing allocator is supplied. + +The complete source-operation cost has the form + + C_state (M+2)^2 + 4096 + + sum_G [2^20(P_G+2)^4 + 2^16(P_G+2)^2 + 4096], (1) + +where C_state is one fixed input-independent finite-control refinement +constant. The raw reads/writes/unit-moves of the frontend and this adapter +fit 2^18(M+2)^2. The separate inherited numerical bounds are added in (1). +The exact complete-control value of C_state is not certified, as in #7154. +For A <= p this is O(p^4) time and K_source + O(p^2) retained cells. + +This evaluates one address-state vector. It does not move a payload indexed +by all addresses, produce or select Beneš micro-rows, implement inverse +traversal, or prove a bit-Turing-machine compiler. The source arithmetic, +entry, physical owner and encoded-iterator contracts remain explicit +premises. All five selected foundational assumptions remain conditional. + +### Exact pins and novelty + +The runtime frontend is #7154 at +`cc35ecedce6f208d5056fab6d17c58555affc73c`, unchanged blob +`8adbe2cfef74da9854ed0b70b6c221f5746efa9f`. The six unchanged numerical, +entry, owner, word, record and canonicalization sources come from canonical +base `e54523517d0f03e58352e647c403a5af3e525a57`. +`INPUT-PINS.json` authenticates all seven exact byte exports by SHA256 and +Git blob. Their copyright and assistance notices are retained. + +#7154 supplies a numerical-node iterator and leaves its whole source +read-only. #7152, head `66adbede4bd4ab603ba3e0a7f6708403905b753c`, supplies +the complete actual source-state transform through paid micro-row queries +at compiled geometry. #5053 already supplies each whole-node updated +coordinate, and #5496 explicitly discards that field while building a +single micro-row. None of those predecessor results is claimed anew. + +The new implication is that #7154's physical iterator remains correct when +the enclosing owner commits precisely the emitted whole-node coordinate +fields between leases. The accompanying paid projection/commit code proves +that implication on actual streams, with exact extent and lifetime checks. +It bypasses ROM construction only for this one-vector endpoint consumer. +It supplies neither the encoded row scheduler left open by #7154 nor the +payload implementation left open by #7152. + +## 2. What one whole-node result means + +For a node G = [a,a+2H), let its left child be A_G and right child B_G. +The #5053 numerical contract reconstructs k_A from the *current* left +coordinates, not from their original mixed-radix interpretation. If a +left coordinate is invalid padding, it sets k_A = 0. Otherwise k_A is the +unique integer in [0,S_A), S_A = product_(i in A_G) s_i, satisfying + + k_A = x_i product_(a <= j < i) s_j (mod s_i), i in A_G. + +For each right axis i in order it returns a P_G-bit pair (c_i, y_i), where + + c_i = k_A [product_(a <= j < i) s_j]^-1 mod s_i, + y_i = (x_i + c_i) mod s_i if x_i < s_i, + y_i = x_i if x_i >= s_i. (2) + +Pairwise coprimality guarantees each inverse. The prefix includes all +earlier right moduli, even when an earlier right coordinate is padded. +The output is a sequential ROOT/pair/RECORD_END stream. The numerical +producer, and its proof of (2), are unchanged premises of this package. + +For either branch of (2), 0 <= y_i < 2^h_i. Therefore every bit above the +destination's declared width h_i is zero. This is the precise implication +needed to project the common-precision result to the source's heterogeneous +physical fields. `_updated` consumes the offset word by a paid P_G-bit +scan, copies exactly h_i low bits from the updated word, and checks every +remaining high bit is zero before consuming its delimiters. A malformed +or overflowing field cannot be silently truncated. The offset field is +never mistaken for the updated coordinate. + +## 3. Snapshot before retirement, commit after retirement + +At node handoff, #7154 leaves the source, axis cursor and unary half-size +counter at head one. STEP marks the current node's first axis; VALUE, +when present, marks the following node. The width counter is blank at +head one and may be reused after canonical input construction. + +`stage` reinstates LEFT on the sole retired staging role. It scans source +records and the existing axis cursor together up to STEP, copying every +record unchanged. It then takes one unary-half pass over the left group, +also unchanged, and one over the right group using `_updated`. It copies +the remaining suffix unchanged, verifies that source and axis terminate +together, appends RIGHT, and returns all borrowed heads locally. + +Each `_record` copies the original unary header and manufactures its width +counter from that header. The modulus field is copied in full. The original +coordinate is either copied or replaced with exactly as many low result +bits as the width counter contains. Thus each record retains exactly its +original extent and all tags. The width counter is cleared after every +record. Source validation and copying use only fixed-alphabet reads, +writes, append operations and unit moves; no width is decoded. + +Induction on the scan establishes the exact staged word: it equals the +current complete source outside the right-coordinate fields of G and +contains (2) in those fields. It has the same logical length M. In this +entire phase the actual source is read-only. All source and numeric result +heads return to one before retirement. Staging is an owned independent +copy, not an alias of numerical output or source backing. + +`lease.close()` next consumes the numerical output, clears its canonical +input and guide roles, retires the exact-width protected words, releases +the 63-role bank, and advances the encoded topology. The staged word +survives this close in its separate role. Only then may `commit` write +the source. Its guard requires a pending staged word, no live iterator +result and a released bank. It copies cells from staging to the same +source positions until the staged RIGHT and verifies the original source +RIGHT at precisely that position. The final RIGHT need not be rewritten. +It returns the source head and physically retires staging, including LEFT +and RIGHT. No backing is replaced, shrunk or forgotten. + +The last node is included: the iterator may retire all topology counters +inside `lease.close`, because commit needs only the already completed +staged word and the source. No dead cursor or retired guide is read during +commit. This is why copying the full framed source is useful at this seam. + +## 4. Coordinate-only mutation preserves the encoded iterator + +The original #7154 whole-lifecycle source-preservation assertion is not +invoked for a changing source. Instead, use the following explicit extension +of its local state invariant. + +At a retired node boundary, allow the enclosing owner to change coordinate +bits while preserving every record header, width, modulus, delimiter, +logical extent and entry head. The encoded axis count, depth, current STEP, +pending-marker discipline and unary half-size are consequently unchanged. +They depend only on the preserved shape and the number of completed nodes. +The next `_record` reads the newly supplied coordinate bits afresh; no +coordinate or arithmetic result is cached in the topology state. The +numerical bank and guards are already blank before the source update. +All next-entry premises therefore hold with the new coordinates. + +The projection/commit lemma proves exactly these conditions. In particular +the high-bit check ensures that each new coordinate fits its physical field; +the copied moduli preserve coprimality and the complete-product capacity +margin. The source head returns to one, and mutation does not touch the +encoded next-node cursor. Inducting across all d-1 nodes proves both the +correct schedule and that each node sees the actual state left by its +predecessors, including children before their parent. + +The controlled public operation is `step` (or repeated `run`), whose phases +are retired, result-live, staged, numerical-retired, committed. Internal +`stage` receives this evaluator's current lease exactly once; clients must +not bypass that protocol by calling the child iterator directly or retaining +stale lease aliases. This is the predecessor's linear-use interface, not a +general token-authentication or arbitrary consumer-mutation API. + +## 5. Equality with the complete balanced CRT endpoint + +At one node, every micro-row changes only right coordinates. Its controls +are determined by the unchanged left coordinates and fixed modulus +prefixes. The retained Beneš theorem says the complete micro-row sequence +implements exactly (2), including the padded-wire identity endpoint. +This package evaluates that endpoint directly; it does not suppress a +micro-row based on a padded intermediate, nor assert that the intermediate +states agree with the numerical output. + +Distinct nodes at a common level act on disjoint coordinate groups and +read controls only within their own groups. Their micro-row maps commute. +Thus the compiled level/row/node order in #7152 and the level/node order +of complete node endpoints here have the same composed endpoint. Earlier +levels finish before later levels in both schedules. Together with Section +4, this proves the complete forward source-state equality for every +admitted padded input. It transfers no micro-row time, payload map, +physical routing or exception-repair theorem to this implementation. + +On fully valid initial coordinates there is an additional independent +closed-form characterization. Put K = sum_i x_i product_(j=2, +A>=2d, log2(d)<=d-1 and M=2+3A+4d imply each of these two sums is at +most dM<=M^2. Adding (4), initial staging acquisition/retirement and the +predecessor 2^16(M+2)^2 raw frontend envelope fits 2^18(M+2)^2. + +All variable adapter loops perform at least one local observation per +iteration; the only unobserved role iteration is the fixed two-child loop. +The symbols, finite phases, role selectors and call depth are fixed. +Expanding this fixed control supplies an input-independent multiplier, +giving C_state in (1). Its numerical value is deliberately not claimed. +The unchanged near-equal-width geometric sums from #7154 bound the fourth +power numerical terms by O(A^4) and the quadratic terms by O(A^2). + +Let P*=A+1. The unchanged numerical bank has the rolewise history envelope + + B_num = (P*+1) + 2(2A+2d+2) + 57(P*+2) + + 3[d(P*+2)+2]. + +The seven topology roles and eight guards retain the predecessor bounds. +The new staging role retains backing of at most M cells, and writes every +data cell only inside that extent. Appending or clearing the final RIGHT +transiently visits head index M, so literal visited-position accounting +charges M+1 cells. The list backing is never shortened. The retained-backing +envelope measured by the executable is + + K_source + B_num + 8(P*+2) + 6(d+2) + (A+2) + M. (5) + +For a caller charging the staging role's full visited span, replace the +last M in (5) by M+1. The other role terms retain the predecessor's declared +backing model; no literal binary space bound is inferred here. +This sums a maximum for each physical role across its whole history. +Erasure never subtracts capacity, and the source's old tail is counted +as K_source. Reusing the width counter for full-source copying does not +increase its existing A+2 envelope. Initial clean private backing and +the already encoded source remain explicit acquisition premises. + +## 7. Evidence, failure boundary and unresolved obligations + +`verify.py` authenticates exact source bytes, poisons host geometry/decode +names in both new adapter and frontend, and seals Port, Word and Arena +constructors after the 79 fixed roles are acquired. It executes the actual +providers, not a replacement numerical oracle. At every node an independent +integer search solves the defining CRT congruences. Fully valid inputs are +also checked by (3), independently of any tree recurrence. + +The fixed finite family consists of all 32 padded coordinate pairs for +moduli (3,5), twelve four-axis states at (2,3,5,7), and one eight-axis tree. +It includes invalid left coordinates, padded right coordinates, mixed +declared widths, nonzero node starts, changing precision and retained +source tails. This is 45 cases and 75 actual numerical nodes. Runtime +values and decisions never come from the verifier. Histories, source +metadata, actual source object identity, extent, every boundary head, +complete private cleanup and the conservative cost envelopes are checked. + +Negative controls reject writes before numerical retirement, advancing +before pending commit, double commit, unchanged stale coordinates in place +of emitted values, missing staging erasure, reversed close/write order, +projection into the wrong half, and a nonzero discarded high bit. The +high-bit control deliberately violates the trusted numerical-provider +postcondition. It demonstrates rejection before source data writes; it +does not establish cleanup or head rollback after that failure. + +The successful theorem is not arbitrary malformed-input rollback, crash +recovery, dirty-memory acquisition or unbounded stale-handle validation. +Numerical-provider correctness, per-call entry retirement and #7154's +encoded schedule are inherited source hypotheses. Finite execution and +AI cross-review are not independent human or formal-kernel acceptance. + +## Open next questions + +1. Supply a reverse encoded node schedule and an actual subtractive + whole-node numerical consumer. First pin an inverse caller and preserve + the same current-state and retired-write boundary. This package supplies + only forward evaluation; reversing the Python node list would reintroduce + an external schedule and is not an implemented solution. +2. Bind this forward evaluator to an actual exceptional-key epoch whose + input is already in the admitted axis encoding. Charge both representation + conversion and the return to that caller's source frame. Generic endpoint + equality does not establish the three-epoch key contract. +3. Complete encoded micro-row/target/header production for payload routing + separately. The numerical endpoint shortcut applies to one address vector; + it cannot replace the synchronized physical payload permutation. +4. Lower the complete fixed-alphabet controls and all providers to a literal + binary program with a common tariff. (1) is a source-model bound; no + selected compiler, precision, native-column or analytic-recovery + obligation is discharged by relabeling it. + +## Credit + +#7154 and #7152 were prepared for Jerry Chen / CubeJerry with OpenAI +assistance. JoyboyBrian supplies #5053, #5219, #5505 and the #5496 numerical, +entry, owner and current-row contracts. Ali Romman supplies #5353's physical +axis encoding and #5625's retire-before-source-write predecessor. Retain +Cinna Davis's #4100 balanced CRT/Beneš construction, Hiroki KUMAZAKI's +current-coordinate/mixed-width work, ToikY's arena lineage, commdata2338's +storage accounting, and every notice in the unchanged source exports. +The elementary CRT identities and disjoint-support commutation are used +as known facts; the claimed contribution is the exact encoded consumer +join and its ownership, shape-preservation and complete source budget. diff --git a/research/encoded-balanced-crt-endpoint/README.md b/research/encoded-balanced-crt-endpoint/README.md new file mode 100644 index 0000000000..2df34a868c --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/README.md @@ -0,0 +1,92 @@ +# Commit whole-node CRT results into the encoded balanced source on 79 owned roles + +This supplies a paid changing-source consumer for the physical balanced-node +iterator in [#7154](https://github.com/CrocSwap/integer-mult-bounds/pull/7154). +The complete forward balanced CRT **address-state endpoint** now executes on +the actual source tape without supplying node indices, widths, precision or +coordinate values as host integers. The proof is relative to the pinned +numerical, entry, owner and frontend contracts. **No new kappa.** + +The consumer stages each whole-node updated-coordinate field in a same-length +source copy, checks discarded high bits, retires the numerical result, and +then writes the owned source. Preserved metadata and widths reestablish the +encoded iterator's next-node invariant. The complete source-model time is +O(p^4), for p bounding the sum of declared widths; historical backing is +K_source + O(p^2). All copying, writing, head returns and erasure are paid. +The one new staging role retains M allocated cells; visited-position +accounting adds one for its transient head at index M. + +#7154 supplies the read-only numerical iterator; this adds its actual +changing-source commit. [#7152](https://github.com/CrocSwap/integer-mult-bounds/pull/7152) +already supplies the same endpoint at compiled micro-row geometry. +[#5053](https://github.com/CrocSwap/integer-mult-bounds/pull/5053) already +computes whole-node values, which [#5496](https://github.com/CrocSwap/integer-mult-bounds/pull/5496) +correctly discards when building an individual micro-row. Those are credited +premises. The new claim is the exact encoded consumer join and its preservation, +ownership and cost proof. + +This evaluates one address vector. Encoded micro-row selection, physical +payload permutation, the three-epoch key, inverse traversal, binary lowering +and all five selected framework assumptions remain open. The complete selected +conditional kappa remains 0.00363005817. The numerical value of the fixed +finite-control refinement constant is not certified; an explicit raw-action +envelope is given separately. + +## Reproduction and evidence + +[PROOF.md](PROOF.md) gives the quantified statement and full ledger. +[endpoint.py](endpoint.py) is the adapter; [verify.py](verify.py) executes the +unchanged seven byte-pinned sources. From this directory, Python 3.12: + +```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_ENDPOINT cases=45 nodes=75 owned_roles=79 controls=8 +``` + +The family covers all 32 padded coordinate pairs for moduli (3,5), twelve +four-axis states and one eight-axis tree. Independent congruence enumeration +checks every node; a separate global mixed-radix formula checks fully valid +endpoints. The actual runs total 13,102,659 source actions. The eight-axis +fixture retains 3,941 cells within a 4,073-cell backing envelope. These are +finite corroborating checks, not a universal proof by enumeration. + +Eight controls detect premature writing/advancement, double commit, stale +coordinate copying, missing erasure, reversed close/write order, wrong-half +projection and a nonzero discarded high bit. Source metadata, inaccessible +nonblank old tails, boundary heads, stable identities and successful cleanup +are checked. Geometry/decode functions are poisoned and physical constructors +sealed after initial acquisition. Failure detection is not a rollback theorem. + +[INPUT-PINS.json](INPUT-PINS.json) records original repositories, commits, +Git blobs, SHA256 values and package-local export paths. Runtime #7154 is +frozen at `cc35ecedce6f208d5056fab6d17c58555affc73c`; canonical sources are at +`e54523517d0f03e58352e647c403a5af3e525a57`; comparison #7152 is frozen at +`66adbede4bd4ab603ba3e0a7f6708403905b753c`. A direct cold replay needs only +this package and Python's standard library, without network or an unmerged +Git object. Standard source provenance is recorded separately in SOURCES.json. + +## Open next questions + +[TASK.json](TASK.json) records structured first steps and blockers. An inverse +evaluator needs an encoded reverse schedule and subtractive consumer. An +actual exceptional-key epoch needs charged representation conversion and +restoration. Payload routing still needs encoded row/target/header selection. +A complete binary program and common tariff remain separate obligations; +unimplemented restarts and arbitrary dirty-memory acquisition are excluded. + +Prepared for Jerry Chen / @CubeJerry with substantial OpenAI assistance. +Retain JoyboyBrian's numerical/entry/owner/query work; Ali Romman's source +encoding and retire-before-write work; Cinna Davis, Hiroki KUMAZAKI, ToikY, +commdata2338 and all unchanged notices. See PROOF.md for full attribution. +Separate AI cross-review is not independent human or formal-kernel acceptance. +Apache-2.0. + +## Independent review + +[REVIEW.md](REVIEW.md) records a separate source and proof review. The independent checker does not call the author verifier and uses CRT idempotent sums as its node oracle. Run `python3.12 -I -W error -B independent_check.py .`; its JSON report records 18 cases, 46 nodes and a rejected stale-coordinate mutant. The executed receipt is [INDEPENDENT-RESULT.json](INDEPENDENT-RESULT.json). diff --git a/research/encoded-balanced-crt-endpoint/RESULT.json b/research/encoded-balanced-crt-endpoint/RESULT.json new file mode 100644 index 0000000000..b12a86f2fb --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/RESULT.json @@ -0,0 +1,1223 @@ +{ + "cases": [ + { + "actions": 59872, + "input": [ + 0, + 0 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 0, + 0 + ], + "raw_bound": 4490272768, + "retained": 690, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 59867, + "input": [ + 0, + 1 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 0, + 1 + ], + "raw_bound": 4490272768, + "retained": 690, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 59875, + "input": [ + 0, + 2 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 0, + 2 + ], + "raw_bound": 4490272768, + "retained": 691, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 59875, + "input": [ + 0, + 3 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 0, + 3 + ], + "raw_bound": 4490272768, + "retained": 691, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 59883, + "input": [ + 0, + 4 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 0, + 4 + ], + "raw_bound": 4490272768, + "retained": 692, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 57863, + "input": [ + 0, + 5 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 0, + 5 + ], + "raw_bound": 4490272768, + "retained": 692, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 57863, + "input": [ + 0, + 6 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 0, + 6 + ], + "raw_bound": 4490272768, + "retained": 692, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 57863, + "input": [ + 0, + 7 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 0, + 7 + ], + "raw_bound": 4490272768, + "retained": 692, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 60066, + "input": [ + 1, + 0 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 1, + 2 + ], + "raw_bound": 4490272768, + "retained": 690, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 60061, + "input": [ + 1, + 1 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 1, + 3 + ], + "raw_bound": 4490272768, + "retained": 690, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 60069, + "input": [ + 1, + 2 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 1, + 4 + ], + "raw_bound": 4490272768, + "retained": 691, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 60268, + "input": [ + 1, + 3 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 1, + 0 + ], + "raw_bound": 4490272768, + "retained": 691, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 60276, + "input": [ + 1, + 4 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 1, + 1 + ], + "raw_bound": 4490272768, + "retained": 692, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 58057, + "input": [ + 1, + 5 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 1, + 5 + ], + "raw_bound": 4490272768, + "retained": 692, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 58057, + "input": [ + 1, + 6 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 1, + 6 + ], + "raw_bound": 4490272768, + "retained": 692, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 58057, + "input": [ + 1, + 7 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 1, + 7 + ], + "raw_bound": 4490272768, + "retained": 692, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 60074, + "input": [ + 2, + 0 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 2, + 4 + ], + "raw_bound": 4490272768, + "retained": 691, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 60268, + "input": [ + 2, + 1 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 2, + 0 + ], + "raw_bound": 4490272768, + "retained": 691, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 60276, + "input": [ + 2, + 2 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 2, + 1 + ], + "raw_bound": 4490272768, + "retained": 692, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 60276, + "input": [ + 2, + 3 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 2, + 2 + ], + "raw_bound": 4490272768, + "retained": 692, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 60284, + "input": [ + 2, + 4 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 2, + 3 + ], + "raw_bound": 4490272768, + "retained": 693, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 58065, + "input": [ + 2, + 5 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 2, + 5 + ], + "raw_bound": 4490272768, + "retained": 693, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 58065, + "input": [ + 2, + 6 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 2, + 6 + ], + "raw_bound": 4490272768, + "retained": 693, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 58065, + "input": [ + 2, + 7 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 2, + 7 + ], + "raw_bound": 4490272768, + "retained": 693, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 60178, + "input": [ + 3, + 0 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 3, + 0 + ], + "raw_bound": 4490272768, + "retained": 691, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 60173, + "input": [ + 3, + 1 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 3, + 1 + ], + "raw_bound": 4490272768, + "retained": 691, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 60181, + "input": [ + 3, + 2 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 3, + 2 + ], + "raw_bound": 4490272768, + "retained": 692, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 60181, + "input": [ + 3, + 3 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 3, + 3 + ], + "raw_bound": 4490272768, + "retained": 692, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 60189, + "input": [ + 3, + 4 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 3, + 4 + ], + "raw_bound": 4490272768, + "retained": 693, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 58169, + "input": [ + 3, + 5 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 3, + 5 + ], + "raw_bound": 4490272768, + "retained": 693, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 58169, + "input": [ + 3, + 6 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 3, + 6 + ], + "raw_bound": 4490272768, + "retained": 693, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 58169, + "input": [ + 3, + 7 + ], + "moduli": [ + 3, + 5 + ], + "nodes": 1, + "output": [ + 3, + 7 + ], + "raw_bound": 4490272768, + "retained": 693, + "retained_bound": 711, + "source_tail": 17, + "widths": [ + 2, + 3 + ] + }, + { + "actions": 357448, + "input": [ + 0, + 0, + 0, + 0 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "nodes": 3, + "output": [ + 0, + 0, + 0, + 0 + ], + "raw_bound": 40020688896, + "retained": 1212, + "retained_bound": 1254, + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "actions": 360506, + "input": [ + 1, + 2, + 4, + 6 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "nodes": 3, + "output": [ + 1, + 1, + 4, + 3 + ], + "raw_bound": 40020688896, + "retained": 1216, + "retained_bound": 1254, + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "actions": 359669, + "input": [ + 1, + 1, + 1, + 1 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "nodes": 3, + "output": [ + 1, + 0, + 4, + 2 + ], + "raw_bound": 40020688896, + "retained": 1214, + "retained_bound": 1254, + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "actions": 359345, + "input": [ + 3, + 2, + 4, + 6 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "nodes": 3, + "output": [ + 3, + 2, + 4, + 4 + ], + "raw_bound": 40020688896, + "retained": 1218, + "retained_bound": 1254, + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "actions": 358305, + "input": [ + 1, + 3, + 4, + 6 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "nodes": 3, + "output": [ + 1, + 3, + 4, + 4 + ], + "raw_bound": 40020688896, + "retained": 1217, + "retained_bound": 1254, + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "actions": 355033, + "input": [ + 1, + 2, + 7, + 6 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "nodes": 3, + "output": [ + 1, + 1, + 7, + 5 + ], + "raw_bound": 40020688896, + "retained": 1216, + "retained_bound": 1254, + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "actions": 352020, + "input": [ + 1, + 2, + 4, + 7 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "nodes": 3, + "output": [ + 1, + 1, + 4, + 7 + ], + "raw_bound": 40020688896, + "retained": 1216, + "retained_bound": 1254, + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "actions": 345405, + "input": [ + 3, + 3, + 7, + 7 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "nodes": 3, + "output": [ + 3, + 3, + 7, + 7 + ], + "raw_bound": 40020688896, + "retained": 1218, + "retained_bound": 1254, + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "actions": 358904, + "input": [ + 0, + 2, + 1, + 5 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "nodes": 3, + "output": [ + 0, + 2, + 0, + 3 + ], + "raw_bound": 40020688896, + "retained": 1213, + "retained_bound": 1254, + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "actions": 358979, + "input": [ + 1, + 0, + 3, + 2 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "nodes": 3, + "output": [ + 1, + 2, + 4, + 1 + ], + "raw_bound": 40020688896, + "retained": 1216, + "retained_bound": 1254, + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "actions": 344771, + "input": [ + 0, + 0, + 7, + 7 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "nodes": 3, + "output": [ + 0, + 0, + 7, + 7 + ], + "raw_bound": 40020688896, + "retained": 1216, + "retained_bound": 1254, + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "actions": 359113, + "input": [ + 1, + 1, + 0, + 0 + ], + "moduli": [ + 2, + 3, + 5, + 7 + ], + "nodes": 3, + "output": [ + 1, + 0, + 3, + 5 + ], + "raw_bound": 40020688896, + "retained": 1212, + "retained_bound": 1254, + "source_tail": 31, + "widths": [ + 2, + 2, + 3, + 3 + ] + }, + { + "actions": 6934507, + "input": [ + 2, + 4, + 6, + 10, + 12, + 16, + 18, + 22 + ], + "moduli": [ + 3, + 5, + 7, + 11, + 13, + 17, + 19, + 23 + ], + "nodes": 7, + "output": [ + 2, + 3, + 6, + 9, + 7, + 4, + 2, + 6 + ], + "raw_bound": 2656504414208, + "retained": 3941, + "retained_bound": 4073, + "source_tail": 97, + "widths": [ + 4, + 4, + 4, + 4, + 4, + 5, + 5, + 5 + ] + } + ], + "cases_count": 45, + "controls": [ + "write_before_numerical_retirement", + "advance_with_uncommitted_staging", + "recommit_retired_staging", + "stale_original_coordinate", + "retained_staging", + "actual_order_mutation", + "wrong_half_projection", + "nonzero_discarded_high_bit" + ], + "new_kappa": null, + "nodes": 75, + "owned_roles": 79, + "runtime_constructors_sealed": true, + "runtime_geometry_poisoned": true, + "scope": "source-model forward address-state endpoint; no payload routing", + "source_count": 7, + "status": "PASS_ENCODED_BALANCED_CRT_ENDPOINT" +} diff --git a/research/encoded-balanced-crt-endpoint/REVIEW.md b/research/encoded-balanced-crt-endpoint/REVIEW.md new file mode 100644 index 0000000000..c2a53dfa10 --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/REVIEW.md @@ -0,0 +1,150 @@ +# Independent review of the encoded CRT endpoint join + +**Outcome: PASS for the declared source-model, one-lifecycle address-state +theorem.** No substantive defect was found. This does not discharge +`analytic_recovery`, certify payload routing, or certify a complete binary +machine tariff. It establishes no new kappa. + +Reviewer: compiler/source-index worker, independently of the CRT package +author. Prepared for Jerry Chen / @CubeJerry with substantial OpenAI +assistance. Canonical base is +`e54523517d0f03e58352e647c403a5af3e525a57`. + +## Reviewed bytes and dependencies + +- `endpoint.py`: SHA256 + `c24ae2c90d175d276120438809e7c7401b8a8c04dec139f1b7345e9778984ced`. +- Updated `PROOF.md`: SHA256 + `a20c90aada4ea2d9141a465b10bd1d54a1047b52608bb19c88efa7fd98eeacf3`. +- Read the complete new endpoint, numerical producer, persistent bank, + guide-driven numerical entry, frontend iterator and its node/lease + classes. Also read the source-model word/record APIs and relevant + predecessor iterator and whole-state composition proofs. +- All seven source files independently matched both SHA256 and Git blob + pins in `INPUT-PINS.json`. The frontend dependency is the explicit + CubeJerry fork commit `cc35ecedce6f208d5056fab6d17c58555affc73c`, blob + `8adbe2cfef74da9854ed0b70b6c221f5746efa9f`; it is a pending contribution, + not silently treated as merged canonical code. + +No author files were edited during this review. The proof hash differs +from the initial review assignment because its author clarified the +staging boundary-cell accounting before the final review snapshot. + +## Mathematical assessment + +### 1. Source mutation is compatible with the iterator + +The persistent topology contains the axis count, balanced level, half-size, +current STEP and pending VALUE markers. These are derived from record +framing and never from coordinate values. The numerical precision is +manufactured afresh by scanning unary width headers in the selected node. +The commit preserves all such headers, moduli, delimiters, record count, +logical length and historical backing. Therefore none of the iterator's +cached topological facts is invalidated. Each subsequent node projection +reads the updated coordinate bits from the actual source rather than +reusing old arithmetic payload. + +At a handoff the width counter is clean at head one, so staging can reuse +it. Its full-source pass restores axis, half-size, source, guide and result +heads before close. Closing is permitted to advance or entirely retire +the topology: commit subsequently uses only source and staging. The final +node is thus covered without trying to read a retired cursor. + +### 2. Numerical projection and padded inputs + +For a valid left child, the independent defining residues are +`x_i * product_(a<=j independent-result.json +``` + +The checker imports the pinned implementation modules directly; it does +not import, invoke or copy the author's `verify.py`. Its numerical oracle +uses the CRT idempotent sum, a different arithmetic route from the +producer's digit reconstruction. On globally valid inputs it also checks +the independent full mixed-radix closed form, which uses no tree updates. + +Observed result: **18 cases, 46 numerical nodes, PASS**. Cases include +2-, 4- and 8-axis trees; widths through 9; alternating declared widths; +each possible invalid axis position in four-axis examples; multiple +simultaneous invalid fields; and an inaccessible tail containing hostile +LEFT/RIGHT/record symbols. Every node checks the actual precision guide, +STEP/VALUE location, topology restoration, source bytes outside coordinate +fields, bank/guard/staging retirement and the per-node adapter action bill. +At termination it checks all 79 owned histories blank at head one. A +mutation committing stale coordinate bits fails the independent endpoint +comparison. Complete tested source hashes and per-case measurements are +in `INDEPENDENT-RESULT.json`. + +These finite tests detect implementation failures and reinforce the +symbolic argument; they are not the universal proof or an asymptotic +experiment. The universal claims depend on the stated source contracts. + +## Residual obligations + +The package is a useful uniform endpoint composition. Its declared scope +still excludes the actual caller's encoded source production, payload +routing/micro-row selection, reverse scheduling and the complete binary +machine refinement. The pending frontend dependency and inherited +numerical/rotation contracts must remain explicit in publication. + +## Root integration review + +The orchestrator independently read the complete adapter, author verifier, proof and this review. The staging boundary-cell clarification was accepted before freezing the core. Publication changes only packaging, the independent checker's default path and documentation; the reviewed endpoint and proof bytes remain unchanged. Strict author and independent checks were rerun from this self-contained package. No complete selected-certificate replay is claimed or needed for this isolated enabling lemma. diff --git a/research/encoded-balanced-crt-endpoint/SOURCES.json b/research/encoded-balanced-crt-endpoint/SOURCES.json new file mode 100644 index 0000000000..887c183862 --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/SOURCES.json @@ -0,0 +1,55 @@ +{ + "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" + } + ], + "export_note": "Runtime imports are package-local exact exports authenticated by INPUT-PINS.json. The pending #7154 source is retained as bytes; replay does not fetch its nonancestor head." +} diff --git a/research/encoded-balanced-crt-endpoint/TASK.json b/research/encoded-balanced-crt-endpoint/TASK.json new file mode 100644 index 0000000000..af0821c529 --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/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": "Compose the encoded balanced-node iterator with paid whole-node coordinate projection, numerical retirement and same-source commit; complete forward address-state endpoint on 79 stable owned roles.", + "scope_change_reason": "The read-only numerical iterator of #7154 and compiled micro-row source mutation of #7152 leave this uniform whole-node consumer join open. Whole-node values are already supplied by #5053; this package does not construct row/ROM or payload schedules.", + "bottleneck_link": "Source-specific uniform control and preservation on the analytic_recovery track; all five selected assumptions and complete kappa remain unchanged.", + "budget_minutes": 90, + "stop_rule": "Only the actual numerical-result-to-same-source seam. Stop on host geometry decoding, unretired source writes, or exact predecessor overlap. Independent verification must cover topology preservation, endpoint equality and full cost.", + "outcome": "completed_independently_reviewed", + "evidence": "PROOF.md; source-authenticated RESULT.json; strict normal/optimized verify.py; REVIEW.md; independent_check.py and INDEPENDENT-RESULT.json.", + "author": "Jerry Chen / CubeJerry", + "ai_assistance": "Substantial OpenAI assistance; independent AI source/proof review, not human or proof-kernel acceptance", + "open_questions": [ + { + "question": "Can an encoded reverse schedule drive a subtractive whole-node consumer?", + "why_it_matters": "Inverse key boundaries require actual reverse evaluation.", + "first_step": "Pin a reverse caller and retain current-state and retired-write invariants.", + "blocked_by": "The iterator and producer here are forward only." + }, + { + "question": "Can this evaluator bind to an actual exceptional-key epoch?", + "why_it_matters": "Endpoint evaluation alone does not provide the complete three-epoch key.", + "first_step": "Charge one caller's source-frame conversion and restoration.", + "blocked_by": "No actual epoch source/transport contract is supplied." + }, + { + "question": "Can encoded synchronized row/target/header selection be supplied for the payload caller?", + "why_it_matters": "One-vector endpoint evaluation is not a physical payload permutation.", + "first_step": "Replace one compiled #5496 row/header input with encoded geometry.", + "blocked_by": "The ROM/micro-row path remains separate." + }, + { + "question": "What common binary tariff admits the complete program?", + "why_it_matters": "The source-model bound does not discharge compiler or analytic recovery assumptions.", + "first_step": "Lower actual providers and controller with source-production and ownership costs.", + "blocked_by": "Only fixed-alphabet source operations and inherited contracts are established." + } + ] +} diff --git a/research/encoded-balanced-crt-endpoint/VERIFY.json b/research/encoded-balanced-crt-endpoint/VERIFY.json new file mode 100644 index 0000000000..4d5c35f39a --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/VERIFY.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate seven exact exports; 45 complete source-state cases, 75 actual numerical nodes, independent congruence/global oracles, 79 role histories, eight controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat every explicit check under optimized Python and compare the same exact receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent_check.py", + "{package}" + ], + "timeout_seconds": 120, + "checks": "Independent direct CRT idempotent and global mixed-radix oracles: 18 cases, 46 nodes, retired history and stale-coordinate negative control." + } + ] +} diff --git a/research/encoded-balanced-crt-endpoint/endpoint.py b/research/encoded-balanced-crt-endpoint/endpoint.py new file mode 100644 index 0000000000..b084d893bd --- /dev/null +++ b/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-endpoint/independent_check.py b/research/encoded-balanced-crt-endpoint/independent_check.py new file mode 100644 index 0000000000..2d12f2a7f3 --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/independent_check.py @@ -0,0 +1,248 @@ +"""Independent review of the CRT endpoint join, not its author verifier. + +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_numeric", "source/research/encoded-current-crt/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") +f = load("peer_frontend", "source/research/encoded-balanced-crt-entry/frontend.py") +endpoint = load("peer_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 = 1 + while half < d: + 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= 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-endpoint/source/research/crt-persistent-numerical-owner/owner.py b/research/encoded-balanced-crt-endpoint/source/research/crt-persistent-numerical-owner/owner.py new file mode 100644 index 0000000000..20ef3519b6 --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/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-endpoint/source/research/encoded-balanced-crt-entry/frontend.py b/research/encoded-balanced-crt-endpoint/source/research/encoded-balanced-crt-entry/frontend.py new file mode 100644 index 0000000000..8adbe2cfef --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/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-endpoint/source/research/encoded-crt-entry-lifecycle/entry.py b/research/encoded-balanced-crt-endpoint/source/research/encoded-crt-entry-lifecycle/entry.py new file mode 100644 index 0000000000..1fa2b0cb88 --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/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-endpoint/source/research/encoded-current-crt/producer.py b/research/encoded-balanced-crt-endpoint/source/research/encoded-current-crt/producer.py new file mode 100644 index 0000000000..a327b0161e --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/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-endpoint/source/research/r437-preparation-composition/predecessor4025/source/records.py b/research/encoded-balanced-crt-endpoint/source/research/r437-preparation-composition/predecessor4025/source/records.py new file mode 100644 index 0000000000..4f00467a0f --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/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-endpoint/source/research/r437-preparation-composition/predecessor4025/source/words.py b/research/encoded-balanced-crt-endpoint/source/research/r437-preparation-composition/predecessor4025/source/words.py new file mode 100644 index 0000000000..8d4ba37e27 --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/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-endpoint/verify.py b/research/encoded-balanced-crt-endpoint/verify.py new file mode 100644 index 0000000000..680d185e54 --- /dev/null +++ b/research/encoded-balanced-crt-endpoint/verify.py @@ -0,0 +1,299 @@ +"""Independent integer oracles and physical lifecycle checks for the new join. + +Observer integers, enumeration and byte snapshots never enter runtime control. +Prepared for CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from contextlib import contextmanager +from hashlib import sha1, sha256 +from itertools import product +from pathlib import Path +from types import ModuleType +import json +import math +import sys + +P = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load(name, relative): + path = P/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 source_check(): + pins = json.loads((P/'INPUT-PINS.json').read_text()) + for pin in pins: + raw = (P/'source'/pin['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') + return len(pins) + + +def modules(): + root = 'source/research/' + w = load('words', root+'r437-preparation-composition/predecessor4025/source/words.py') + r = load('endpoint_records', root+'r437-preparation-composition/predecessor4025/source/records.py') + e = load('endpoint_entry', root+'encoded-crt-entry-lifecycle/entry.py') + n = load('endpoint_numeric', root+'encoded-current-crt/producer.py') + o = load('endpoint_owner', root+'crt-persistent-numerical-owner/owner.py') + c = load('endpoint_canonical', root+'crt-mixed-row-entry/bridge.py') + f = load('endpoint_frontend', root+'encoded-balanced-crt-entry/frontend.py') + return w, r, e, n, o, c, f + + +def fixture(m, moduli, widths, values, tail=0): + w, r, e, *_ = m + source = e.Port(w) + fields = [] + for s, h, x in zip(moduli, widths, values, strict=True): + source.append(r.ROOT) + for _ in range(h): + source.append(w.ONE) + source.append(r.WORD_END) + for value, delimiter in ((s, r.WORD_END), (x, r.RECORD_END)): + begin = source.head + for j in range(h): + source.append((value >> j) & 1) + if delimiter == r.RECORD_END: + fields.append(tuple(range(begin, source.head))) + source.append(delimiter) + source.append(w.RIGHT) + source.rewind() + # Observer-supplied old backing is intentionally not all blank. Runtime + # stops at RIGHT and must preserve these inaccessible historical cells. + source.cells.extend((w.ONE, w.ZERO, w.BLANK)[j % 3] for j in range(tail)) + return source, fields + + +def coordinates(source, fields): + return tuple(sum(source.cells[at] << j for j, at in enumerate(field)) + for field in fields) + + +def node_oracle(moduli, values, start, half): + """Exhaust defining CRT congruences, independent of the encoded recurrence.""" + left = moduli[start:start+half] + xs = values[start:start+half] + total = math.prod(left) + residues, prefix = [], 1 + for s, x in zip(left, xs): + residues.append(x*prefix % s) + prefix *= s + if all(x < s for x, s in zip(xs, left)): + lower = next(k for k in range(total) + if all(k % s == y for s, y in zip(left, residues))) + else: + lower = 0 + answer = list(values) + prefix = total + for i in range(start+half, start+2*half): + s, x = moduli[i], values[i] + shift = next(c for c in range(s) if (c*prefix-lower) % s == 0) + answer[i] = (x+shift) % s if x < s else x + prefix *= s + return tuple(answer) + + +def global_oracle(moduli, original): + """One mixed-radix integer; no tree, reconstruction, or node update.""" + integer, prefix = 0, 1 + for s, x in zip(moduli, original): + integer += x*prefix + prefix *= s + answer, prefix = [], 1 + for s in moduli: + answer.append(integer*pow(prefix, -1, s) % s) + prefix *= s + return tuple(answer) + + +def poison(module): + def denied(*_args, **_kwargs): + raise ValueError('forbidden runtime 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): + w, _, e, *_ = m + old = e.Port.__init__, w.Word.__init__, w.Arena.__init__, w.Word.inspect + def denied(*_args, **_kwargs): + raise ValueError('forbidden runtime allocation/decode') + e.Port.__init__ = w.Word.__init__ = w.Arena.__init__ = w.Word.inspect = denied + try: + yield + finally: + e.Port.__init__, w.Word.__init__, w.Arena.__init__, w.Word.inspect = old + + +def actions(ports): + return sum(p.meter.reads+p.meter.writes+p.meter.moves for p in ports) + + +def run_case(module, m, moduli, widths, original, tail=0): + w, r, e, n, o, c, f = m + source, fields = fixture(m, moduli, widths, original, tail) + before, source_id = bytes(source.cells), id(source.cells) + active_cells = set().union(*map(set, fields)) + initial_source_actions = actions([source]) + endpoint = module.Endpoint(f, w, r, e, n, o, c, source) + it = endpoint.iterator + ports = (*it.bank.ports, *it.guards, *it.counters.values(), endpoint.staging) + need(len(ports) == 79 and len({id(p.cells) for p in ports}) == 79, '79 owned roles') + identities = tuple(id(p.cells) for p in ports) + expected, meters, trace = tuple(original), [], [] + stage = endpoint.stage + def observed_stage(lease): + snapshot = bytes(source.cells), source.head + stage(lease) + need((bytes(source.cells), source.head) == snapshot, 'live lease leaves source unchanged') + need(lease.actual.guide.head == 1 and lease.actual.result['stream'].head == 1, + 'consumed numerical streams restore heads') + need(it.counters['axis'].head == 1 and it.counters['half'].head == 1, + 'borrowed topology heads restored') + need(it.counters['width'].head == 1 and + all(x == w.BLANK for x in it.counters['width'].cells[1:]), + 'reused width counter body blank') + meters.append(lease.actual.context.arena.meter) + endpoint.stage = observed_stage + with sealed(m): + for level in range(1, len(moduli).bit_length()): + half = 1 << (level-1) + for start in range(0, len(moduli), 2*half): + expected = node_oracle(moduli, expected, start, half) + need(endpoint.step(), 'every aligned node executes') + need(coordinates(source, fields) == expected, 'independent node endpoint') + need(source.head == 1 and id(source.cells) == source_id, 'actual source backing and head') + need(len(source.cells) == len(before), 'source historical extent unchanged') + need(all(v == source.cells[i] for i, v in enumerate(before) + if i not in active_cells), 'metadata and source tail unchanged') + need(tuple(id(p.cells) for p in ports) == identities, 'stable owned histories') + need(not it.live and not it.bank.busy and not endpoint.pending, 'node retirement boundary') + need(all(p.head == 1 and all(x == w.BLANK for x in p.cells) + for p in (*it.bank.ports, *it.guards)), 'numerical bank and guards retired') + need(all(x == w.BLANK for x in endpoint.staging.cells) + and endpoint.staging.head == 1, 'staging fully retired') + trace.append((level, start, 1+sum(widths[start:start+2*half]))) + need(not endpoint.step() and it.closed, 'exact termination') + if all(x < s for x, s in zip(original, moduli)): + need(expected == global_oracle(moduli, original), 'independent global mixed-radix endpoint') + need(all(p.head == 1 and all(x == w.BLANK for x in p.cells) for p in ports), 'all historical backing blank') + total = actions([source, *ports])-initial_source_actions + total += sum(x.reads+x.writes+x.moves for x in meters) + a, d = sum(widths), len(widths) + logical = 2+3*a+4*d + bound = 2**18*(logical+2)**2+4096 + bound += sum(2**20*(precision+2)**4+2**16*(precision+2)**2+4096 + for _, _, precision in trace) + need(total <= bound, 'raw source-action envelope') + pstar = a+1 + inherited = (pstar+1)+2*(2*a+2*d+2)+57*(pstar+2)+3*(d*(pstar+2)+2) + space = len(before)+inherited+8*(pstar+2)+6*(d+2)+(a+2)+logical + retained = len(source.cells)+sum(len(p.cells) for p in ports) + need(retained <= space, 'rolewise historical capacity envelope') + return {'moduli': list(moduli), 'widths': list(widths), 'input': list(original), + 'output': list(expected), 'nodes': len(trace), 'actions': total, + 'raw_bound': bound, 'retained': retained, 'retained_bound': space, + 'source_tail': tail} + + +def mutant(text, old, new): + need(text.count(old) == 1, 'unique mutation site') + module = ModuleType('endpoint_mutant') + exec(compile(text.replace(old, new), 'endpoint-mutant', 'exec'), module.__dict__) + poison(module) + return module + + +def controls(module, m): + w, r, e, n, o, c, f = m + labels = [] + def rejects(label, operation, message): + try: + operation() + except ValueError as error: + need(message in str(error), 'specific negative control: '+label) + labels.append(label) + else: + raise ValueError('undetected negative control: '+label) + source, _ = fixture(m, (3,5), (2,3), (1,1), 29) + endpoint = module.Endpoint(f, w, r, e, n, o, c, source) + snapshot = bytes(source.cells), source.head + lease = endpoint.iterator.next() + endpoint.stage(lease) + rejects('write_before_numerical_retirement', endpoint.commit, 'follows numerical retirement') + need((bytes(source.cells), source.head) == snapshot, 'premature update touches no source') + rejects('advance_with_uncommitted_staging', endpoint.step, 'must commit') + lease.close() + endpoint.commit() + rejects('recommit_retired_staging', endpoint.commit, 'follows numerical retirement') + text = (P/'endpoint.py').read_text() + wrong = mutant(text, 'self.staging.append(new)', 'self.staging.append(old)') + rejects('stale_original_coordinate', lambda: run_case(wrong, m, (2,3,5,7), + (2,2,3,3), (1,1,1,1)), 'independent node endpoint') + dirty = mutant(text, 'self.source.rewind()\n self.staging.retire()\n self.pending = False', + 'self.source.rewind()\n self.staging.rewind()\n self.pending = False') + rejects('retained_staging', lambda: run_case(dirty, m, (3,5), (2,3), (1,1)), + 'staging fully retired') + late = mutant(text, 'lease.close()\n self.commit()', 'self.commit()\n lease.close()') + rejects('actual_order_mutation', lambda: run_case(late, m, (3,5), (2,3), (1,1)), + 'follows numerical retirement') + shifted = mutant(text, 'for selected in (False, True):', 'for selected in (True, False):') + rejects('wrong_half_projection', lambda: run_case(shifted, m, (5,7), (3,3), (1,1)), + 'independent node endpoint') + source, _ = fixture(m, (3,5), (2,3), (1,1)) + original_source = bytes(source.cells) + endpoint = module.Endpoint(f, w, r, e, n, o, c, source) + lease = endpoint.iterator.next() + # Corrupt the first bit above the destination's h=3 low bits in the + # P=6 updated field. This tests failure detection, not error rollback. + lease.actual.result['stream'].cells[6+3+3] = w.ONE + rejects('nonzero_discarded_high_bit', lambda: endpoint.stage(lease), + 'fits declared width') + need(bytes(source.cells) == original_source, 'failed projection leaves source bytes') + return labels + + +def main(): + authenticated = source_check() + m = modules() + module = load('endpoint_join', 'endpoint.py') + poison(module) + poison(m[-1]) + cases = [run_case(module, m, (3,5), (2,3), values, tail=17) + for values in product(range(4), range(8))] + for values in ((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)): + cases.append(run_case(module, m, (2,3,5,7), (2,2,3,3), values, tail=31)) + cases.append(run_case(module, m, (3,5,7,11,13,17,19,23), + (4,4,4,4,4,5,5,5), (2,4,6,10,12,16,18,22), tail=97)) + result = {'status': 'PASS_ENCODED_BALANCED_CRT_ENDPOINT', 'source_count': authenticated, + 'cases': cases, 'cases_count': len(cases), 'nodes': sum(c['nodes'] for c in cases), + 'owned_roles': 79, 'controls': controls(module, m), + 'runtime_geometry_poisoned': True, 'runtime_constructors_sealed': True, + 'scope': 'source-model forward address-state endpoint; no payload routing', + 'new_kappa': None} + rendered = json.dumps(result, sort_keys=True, indent=2)+'\n' + if '--write-result' in sys.argv: + (P/'RESULT.json').write_text(rendered) + else: + need(rendered == (P/'RESULT.json').read_text(), 'frozen exact result') + print(result['status'], 'cases='+str(len(cases)), 'nodes='+str(result['nodes']), + 'owned_roles=79', 'controls='+str(len(result['controls']))) + + +if __name__ == '__main__': + main() From d2ed3959c30528b0b85fc6d815d4ad4f94f6be86 Mon Sep 17 00:00:00 2001 From: Jerry Jiaheng Chen <80299683+CubeJerry@users.noreply.github.com> Date: Wed, 11 Nov 2026 22:53:16 +0800 Subject: [PATCH 2/2] Use the repository's accepted replay metadata values; preserve reviewed scientific bytes --- research/encoded-balanced-crt-endpoint/TASK.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/research/encoded-balanced-crt-endpoint/TASK.json b/research/encoded-balanced-crt-endpoint/TASK.json index af0821c529..9401cddc0e 100644 --- a/research/encoded-balanced-crt-endpoint/TASK.json +++ b/research/encoded-balanced-crt-endpoint/TASK.json @@ -68,7 +68,7 @@ "bottleneck_link": "Source-specific uniform control and preservation on the analytic_recovery track; all five selected assumptions and complete kappa remain unchanged.", "budget_minutes": 90, "stop_rule": "Only the actual numerical-result-to-same-source seam. Stop on host geometry decoding, unretired source writes, or exact predecessor overlap. Independent verification must cover topology preservation, endpoint equality and full cost.", - "outcome": "completed_independently_reviewed", + "outcome": "completed", "evidence": "PROOF.md; source-authenticated RESULT.json; strict normal/optimized verify.py; REVIEW.md; independent_check.py and INDEPENDENT-RESULT.json.", "author": "Jerry Chen / CubeJerry", "ai_assistance": "Substantial OpenAI assistance; independent AI source/proof review, not human or proof-kernel acceptance",