diff --git a/research/crt-shared-row-banks/PROOF.md b/research/crt-shared-row-banks/PROOF.md new file mode 100644 index 0000000000..6450788848 --- /dev/null +++ b/research/crt-shared-row-banks/PROOF.md @@ -0,0 +1,181 @@ +# Cross-row ROM reentry with fixed historical extents + +## Statement and premises + +Fix an admitted node of the two-width CRT caller in PR #5625. Keep its axis +source, widths, moduli, eight protected numerical words, precision P and row +sequence. Supply one clean ROM bank with the 52 distinct role backings of +PR #5519, separate from source, protected words, numerical workspaces and staging. +Assume the source RowEntry, ROM producer, joined-query and paid source-update +theorems cited in PR #5625. This proof builds on them; it does not re-prove them. + +For any finite compiled row sequence with q >= 1 active rows, the changed +caller executes the same row permutations and returns each ROM role blank +across its entire allocated extent before the next row. It retains one ROM +bank instead of q distinct banks. Every other row workspace remains retained +and billed. Malformed executions and failure rollback are outside the theorem, +as in the predecessor. + +## The interface + +`adapt_source` makes five exact, guarded substitutions in the authenticated +joined-query source. They add a bank parameter and owner reference, acquire +that bank before constructing the four header wrappers, replace the fresh +service allocation, and release ownership after query retirement. Every +runtime tape read, write, move, producer instruction and source-update call is +unchanged. The original source files and their credit lines retain their bytes. + +`BankPool` is a model of supplied blank physical tapes with a single owner. +It rejects a simultaneous second lease and a release of a different bank. +The role map and wiring are compiled topology. Acquire and release touch only +fixed ownership metadata, with no tape-content scan, copy or erasure. Runtime +coordinates remain on the predecessor's tapes. The external verifier observes +blankness and physical identity; those observations provide no runtime values. + +The source's numerical workspaces, coordinate tape, countdown tape and result +tape are freshly constructed per query. The staging tape from PR #5625 remains +shared as before. The construction does not assert reuse of those other roles. + +## Historical-extent induction + +Use the credited role table in PR #5519, PROOF.md, section "Exact retained +footprint of this shared ROM bank". For N=2^H and +J=N(H^2+3H+1), preallocate: + +* 44 scalar roles and three ordinary headers, P+2 cells each; +* offset header, P+3 cells; +* arena, 5PJ+2 cells; +* spool, N(2H-1)+2 cells; +* complete layers, (N+1)(2H-1)+2 cells; +* selected ROM, N+2 cells. + +Here H is the largest active right-axis width in the compiled sequence. +The predecessor proves these per-role extents are nondecreasing in height, +are independent of runtime offset values, and bound every successful visited +cell. No successful path steps beyond the displayed right marker. Their sum is + + B(P,H) = 5P 2^H(H^2+3H+1) + 2^H(4H-1) + 48P + 2H + 104. + +This formula and its rolewise derivation are predecessor results. The new +use is to supply the same physical roles to the next RowQuery constructor. + +Initially all allocated cells are blank. Couple an invocation to the credited +fresh-bank execution by equal symbols and heads on each visited prefix. Extra +cells are blank and lie beyond that execution's maximal visited cell. Unit +reads, writes and moves therefore take the same branches and produce identical +outputs. The preallocated version never needs to extend a list. The inherited +producer retirement clears its used private prefixes; the joined caller erases +layers, ROM and all headers. Untouched suffixes remain blank. Query close then +retires the result and numerical Entry before releasing the bank lease. +Thus the entire historical extent, rather than just the latest prefix, is +blank at release. New header and observer wrappers begin at physical origin +zero, and producer execution initializes each role head at zero as before. +This is the entry contract for the next row. Induction proves reentry for every +finite compiled sequence. An idle row neither acquires nor changes the bank. + +The source-update consumer still copies the live output to separate staging, +closes the query, and then changes the owned source. Consequently bank reuse +does not extend the source borrow or erase a needed result. The credited +current-state composition theorem now applies row by row. A full level and its +reverse restore the same source and protected dirty words. + +## Complete retained-work accounting + +For a fixed admitted node, active H is the same for every active row. If any +right axis is long, it is active in every row and determines H. If all right +axes are short, they are either all idle or all active, and active H is their +common width. This uses the source two-width contract. + +Let E_j count row j's numerical owned backing, X_j its three non-bank joined +ports, and S the one staging extent. Count physical identities once, including +blank retired backing. For q >= 1 active rows, the distinct-bank contract uses + + S + sum_j (E_j + X_j + B(P,H)). + +The new interface uses + + S + sum_j (E_j + X_j) + B(P,H). + +The exact reduction is (q-1)B(P,H), positive for q >= 2. This is a statement +about the declared ROM change; it does not replace the sum of numerical +workspaces by a peak. Source backing, eight protected words and any exterior +reserve remain additional in both expressions. For an entirely idle sequence, +no bank is needed; the supplied-bank theorem above assumes an active row. + +Every tape instruction is preserved, so the predecessor's active-row time +allowance and source-update charges still apply. The bank is supplied already +blank and counted at its complete capacity. This is not a free dirty-allocation +or erasure algorithm. Fixed ownership control adds no tape actions. A full +binary transition compiler and its representation overhead remain unprovided. + +## Executed evidence and limits + +The main fixture is the two-target complete level with moduli (5,7,3,2), +widths (3,3,2,2), initial state (3,2,1,1), precision 11 and H=2. It executes +ten rows, six active rows and twelve physical producer calls. Each active bank +has 3,084 cells. Exact physical-identity accounting gives 8,894 retained work +cells; replacing the one bank by six distinct equal banks gives 24,314 cells. +The reduction is 5 times 3,084, or 15,420 cells. Both counts retain every +numerical query object and every other allocated work backing. + +The mixed-height control uses right widths (3,2) and two consecutive row-one +queries. Each query executes the long target and then the short target on the +same bank. The second query reuses the identical backing. It checks complete +source round-trip, all protected inputs, ownership, fixed capacities, all +numerical and joined retirement, and every historical blank suffix. Five +negative controls reject overlapping ownership, the wrong release object, a +nonblank arena-tail cell, a changed extent and a mismatched source seam. +RESULT.json is generated from these executions and binds the implementation +and input manifest by SHA256. It is not a handwritten receipt. + +This is a source-bound scoped construction and composition proof, supported by +finite execution. Initial clean supply, arbitrary dirty acquisition, shared +numerical banks, changing precision, whole-tree and exceptional-key execution, +binary lowering, full supplier admission and the five selected framework +assumptions remain separate. No new multiplication theorem or kappa is claimed. +No independent human or proof-kernel acceptance is claimed. + +## Implementation constraints + +All new functions are below 60 physical lines. New loops use the fixed 52-role +inventory, the five source substitutions, the bounded source manifest, or the +fixed 10-row/2-row fixtures. Source pins are checked before loading executable +premises. Failures propagate as ValueError; there is no recovery guarantee +for malformed production executions. + +Power-of-Ten rule 3 deviation: Python allocates managed objects while the +verifier runs. Physical bank capacity is fixed before execution at B(P,H), and +all other retained backing is enumerated by identity. The bounded fixture and +fixed role table bound live data; Python interpreter memory is outside the +finite-symbol cell claim. Follow-up is an explicit binary implementation before +using this result as a binary-space theorem. + +Power-of-Ten rules 8 and 9 deviation: the source-bound adapter compiles a +changed query module using the predecessor's module loader. There is no runtime +input interpolation. Only five fixed substitutions of SHA256-authenticated +source are allowed, each with exactly one occurrence. Source drift rejects. +The exact transformed source remains inspectable through `adapt_source`. +A future upstream constructor parameter could remove this scoped compilation; +predecessor code is immutable in this contribution. + +Diagnostics use Python warnings as errors in normal and optimized runs. The +registered source metadata, committed-byte and source-history checks remain +separate from the mathematical theorem premises. No repository-wide code +cleanup or predecessor replay is part of this contribution. + +## Related prior numerical owner + +JoyboyBrian's PR #5505 constructs reuse of the separate 63-role numerical +owner, including changing precision and paid marker reinstatement. It leaves +complete physical ROM/level integration open. This construction changes the +52-role ROM bank across paid source-update rows and does not compose that +numerical owner. The two results concern different role inventories and +lifecycle seams; no numerical reuse is claimed here. + +## Credit + +This contribution was produced by Nick Petalas. Credit Ali Romman, commdata2338, +JoyboyBrian, ToikY, Hiroki KUMAZAKI, Cinna Davis and all source notices and +retained predecessors as linked in PR #5625 and PR #5519. The bank formula, +rolewise maximum principle and original caller theorems are not claimed as new. +Apache-2.0. diff --git a/research/crt-shared-row-banks/README.md b/research/crt-shared-row-banks/README.md new file mode 100644 index 0000000000..99e57d6c7c --- /dev/null +++ b/research/crt-shared-row-banks/README.md @@ -0,0 +1,65 @@ +# Share the physical ROM bank across CRT rows + +A new explicit bank interface lets consecutive paid CRT row queries reuse the +same 52 physical ROM tapes. In the complete ten-row forward/reverse fixture, +retained owned work falls from the derived distinct-bank baseline of 24,314 +cells to 8,894 cells, saving 15,420 finite-symbol tape cells. Source and protected +input backing are additional in both counts. + +Claim type: a source-bound construction and scoped composition proof, with +finite executable evidence. This is a new reentry interface for the open shared +workspace question of Ali Romman's [PR #5625](https://github.com/CrocSwap/integer-mult-bounds/pull/5625). +Its source-update theorem and the numerical/ROM producer theorems are premises, +not audit targets. No new kappa or selected-assumption discharge is claimed. + +The 52-role inventory, componentwise extent formulas and within-row reuse +argument are credited to commdata2338's +[PR #5519](https://github.com/CrocSwap/integer-mult-bounds/pull/5519), including +its retained-backing predecessors. The new step is executable reuse across +separately constructed row queries, with exclusive leases and full historical +blank tails at each reentry. Numerical entry workspaces and the three other +joined ports remain distinct and fully charged. + +See [PROOF.md](PROOF.md), [shared.py](shared.py), [verify.py](verify.py) and the +generated, hash-bound [RESULT.json](RESULT.json). The verifier executes the +changed caller and uses the retained logical caller only as its endpoint oracle. +It does not run a predecessor scientific replay. An additional two-row control +uses a long target followed by a short target within each row. Every bank keeps +its preallocated extent, including blank tails. Five rejection controls cover +lease ownership, historical tails, extent changes and source drift. + +From the worktree root, reproduce with: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/crt-shared-row-banks +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/crt-shared-row-banks/verify.py +``` + +Both normal and optimized registered commands must print +`PASS_CRT_SHARED_ROW_BANKS`. Metadata, committed-byte checks and hosted CI are +separate from the mathematical premises. Python 3.12 and the standard library +suffice. No full selected replay, proof assistant or binary compiler is supplied. + +## Open next questions + +Can JoyboyBrian's [PR #5505](https://github.com/CrocSwap/integer-mult-bounds/pull/5505) +reusable 63-role numerical owner compose with this updated source and shared +ROM bank? That predecessor already constructs numerical-bank reuse across +changing precision, separately from physical ROM/level integration. Start by +binding its live-result lease and marker reinstatement to this query close. +The current construction keeps its numerical workspaces distinct and does not +claim this additional composition. + +Can a single bank cross a changing-precision node boundary? Start with the +actual protected-word conversion and source lifecycle at one adjacent pair of +nodes. Monotone bank capacities alone do not establish those caller contracts. + +How can the required clean reserve be acquired from arbitrary dirty backing? +Start with the source-owned erasure contract and charge the complete restoration +or allocation mechanism. This construction assumes supplied clean banks. + +This contribution was produced by Nick Petalas. Credit Ali Romman for paid CRT +source updates and row reentry; commdata2338 for the exact shared ROM footprint; +JoyboyBrian for the joined query and numerical/ROM lifecycle; ToikY for the +retained arena and caller; Hiroki KUMAZAKI and Cinna Davis for the CRT contracts. +All retained source notices and predecessor credit remain unchanged. Apache-2.0. diff --git a/research/crt-shared-row-banks/RESULT.json b/research/crt-shared-row-banks/RESULT.json new file mode 100644 index 0000000000..6860359a84 --- /dev/null +++ b/research/crt-shared-row-banks/RESULT.json @@ -0,0 +1,176 @@ +{ + "status": "PASS_CRT_SHARED_ROW_BANKS", + "claim_type": "scoped construction and composition proof", + "implementation_sha256": { + "shared.py": "058da49c5270076753953ba231e4a858d0981fa3b388e9183f62bb7eace5eb02", + "verify.py": "843f1e8dc11db825867b8927d64b2c558fabb768c79001036bb1b104552e3022", + "SOURCES.json": "95a9df81a00290e8dfe4369a0eeffcb1721887ae706f1a15ecfb892733e4b1d6" + }, + "case": { + "rows": 10, + "active_rows": 6, + "producer_calls": 12, + "precision": 11, + "height": 2, + "bank_roles": 52, + "bank_cells": 3084, + "distinct_bank_baseline_cells": 24314, + "shared_bank_cells": 8894, + "saved_cells": 15420, + "trace": [ + { + "row": 0, + "state": [ + 3, + 2, + 1, + 1 + ], + "producer_calls": 2, + "row_backing_cells": 4051 + }, + { + "row": 1, + "state": [ + 3, + 2, + 1, + 1 + ], + "producer_calls": 2, + "row_backing_cells": 4051 + }, + { + "row": 2, + "state": [ + 3, + 2, + 1, + 1 + ], + "producer_calls": 0, + "row_backing_cells": 0 + }, + { + "row": 3, + "state": [ + 3, + 2, + 1, + 1 + ], + "producer_calls": 0, + "row_backing_cells": 0 + }, + { + "row": 4, + "state": [ + 3, + 2, + 1, + 0 + ], + "producer_calls": 2, + "row_backing_cells": 4051 + }, + { + "row": 4, + "state": [ + 3, + 2, + 1, + 1 + ], + "producer_calls": 2, + "row_backing_cells": 4051 + }, + { + "row": 3, + "state": [ + 3, + 2, + 1, + 1 + ], + "producer_calls": 0, + "row_backing_cells": 0 + }, + { + "row": 2, + "state": [ + 3, + 2, + 1, + 1 + ], + "producer_calls": 0, + "row_backing_cells": 0 + }, + { + "row": 1, + "state": [ + 3, + 2, + 1, + 1 + ], + "producer_calls": 2, + "row_backing_cells": 4051 + }, + { + "row": 0, + "state": [ + 3, + 2, + 1, + 1 + ], + "producer_calls": 2, + "row_backing_cells": 4051 + } + ] + }, + "mixed_height_control": { + "rows": 2, + "active_rows": 2, + "producer_calls": 4, + "precision": 11, + "height": 3, + "bank_roles": 52, + "bank_cells": 9086, + "distinct_bank_baseline_cells": 20127, + "shared_bank_cells": 11041, + "saved_cells": 9086, + "trace": [ + { + "row": 1, + "state": [ + 1, + 4, + 7, + 3 + ], + "producer_calls": 2, + "row_backing_cells": 10059 + }, + { + "row": 1, + "state": [ + 1, + 4, + 7, + 3 + ], + "producer_calls": 2, + "row_backing_cells": 10059 + } + ] + }, + "controls": [ + "overlapping_lease", + "wrong_release", + "dirty_historical_tail", + "changed_extent", + "source_drift" + ] +} diff --git a/research/crt-shared-row-banks/SOURCES.json b/research/crt-shared-row-banks/SOURCES.json new file mode 100644 index 0000000000..8b4aaeb6e3 --- /dev/null +++ b/research/crt-shared-row-banks/SOURCES.json @@ -0,0 +1,234 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/crt-current-row-query/join.py", + "usage": "input", + "git_blob": "676582b4a376db375237ec52df84a3ddaf231827", + "sha256": "11c9ac1175a45edae80869b22c041e31a1b5cc75f4389ec2e073de37e547bf35" + }, + { + "path": "research/crt-paid-row-reentry/PROOF.md", + "usage": "input", + "git_blob": "eec7613f560e8c04b1c8c4d821660f912584e0b2", + "sha256": "3e87455e3f30af808c1aac199001b968a92ca087906eec7f227b9296a6e5b48e" + }, + { + "path": "research/crt-current-row-query/PROOF.md", + "usage": "input", + "git_blob": "0449d47c5027b4b5a6b6b5b2a87219069d4ad91c", + "sha256": "6aaa6253bf5f64f07cbfbf0a98a7c464e5a78cfa05c398f7eb41a27f03a7379c" + }, + { + "path": "research/crt-current-row-query/SOURCES.json", + "usage": "input", + "git_blob": "56ddb1dafd73ddac3e0a4f0a64f9e0455fad6f85", + "sha256": "39c9b9b9e530a93da6aaf7f02a6884882cdaca778767d9fa06c4a42d2cf6a47a" + }, + { + "path": "research/crt-dense-guard-scan/machine.py", + "usage": "input", + "git_blob": "ce763898bd7b4401bbab818c640a0593b65c9a82", + "sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7" + }, + { + "path": "research/crt-encoded-benes-rom-producer/PROOF.md", + "usage": "input", + "git_blob": "cdd530c668254558bb1ef8a6c6af9a5660f8f9c2", + "sha256": "93bd340ac9b77f8f781926aeb7327325789b331863b3088fed1809eefb789bd2" + }, + { + "path": "research/crt-encoded-benes-rom-producer/SOURCES.json", + "usage": "input", + "git_blob": "ea930342bb19c3f87839990d2e91ce6e4fb06654", + "sha256": "527b3a3a2996c24462b7f81f0e37c86fb315f8401026f2e19e46bb5bc55bffce" + }, + { + "path": "research/crt-encoded-benes-rom-producer/microcode.py", + "usage": "input", + "git_blob": "052b01a83bc910c176b83a012b9f46f0e9525b9d", + "sha256": "d4af5350854a87b67484840800b94e1e53cff82c78ec0f2a91753fed9ea70af7" + }, + { + "path": "research/crt-encoded-benes-rom-producer/vendor/pr4192-NOTICE.md", + "usage": "input", + "git_blob": "6ca47019de7e58edf93c4278a6a8251625d37477", + "sha256": "b886589be7c8b87bcf12b14ce4db6827299b7cec93836ed22cff81aed37623dc" + }, + { + "path": "research/crt-encoded-benes-rom-producer/vendor/pr4192-PROOF.md", + "usage": "input", + "git_blob": "af1ea10b9d2b117d150ec7bddfb81e681172cdb4", + "sha256": "c3eb4e14dc5ee0102cbf77c4a0e61db9989c2b8a0eaf7f0659a6e39373197474" + }, + { + "path": "research/crt-encoded-benes-rom-producer/vendor/pr4192-verify.py", + "usage": "input", + "git_blob": "e79a9ce3f38f78031310acd9e384fd4010ce8ca8", + "sha256": "e8ff7800ffa267d2825009656b78ab1613544b55301982744ec0d99f38800913" + }, + { + "path": "research/crt-mask-repair-bridge/key_subroutine.py", + "usage": "input", + "git_blob": "5771ae55626dbc2a32a95d8c098bdd03d820833c", + "sha256": "ffdbb610be71ae20bf974946dac66b6c1b4d43739cbc3b1eb81cbbeab8784b44" + }, + { + "path": "research/crt-mixed-row-entry/PROOF.md", + "usage": "input", + "git_blob": "76e75e002b5c5860a43b2fe6313ba4339efcc3ff", + "sha256": "8a529ece497c62d5225261cdacebfd88979322b3a8886d1a31eb6295f1989e4b" + }, + { + "path": "research/crt-mixed-row-entry/SOURCES.json", + "usage": "input", + "git_blob": "d6782e6fdb4600499843b932efa93a5700fe47bc", + "sha256": "aac37dac580b1c3b3b4b53220b76292519d3188da0384a728270b02119ea7d80" + }, + { + "path": "research/crt-mixed-row-entry/bridge.py", + "usage": "input", + "git_blob": "57f6853e262a6136bc616f1e47a31d0ace28495c", + "sha256": "89c38638c0d66da731566c903c32e7fa1ad31088d29cfd2634fce823dd07c1f9" + }, + { + "path": "research/crt-mixed-row-entry/verify.py", + "usage": "input", + "git_blob": "0ec8d2906fb0a07e0c2a34a43b260c742d0b148f", + "sha256": "b8695e19bbd597b61dd97379f3970b62f375719a10512dea77784e2ce3b71f2d" + }, + { + "path": "research/crt-mixed-width-caller/README.md", + "usage": "input", + "git_blob": "ff3b6d0708cd5296e71756a16b22167746ac1b24", + "sha256": "c5126d2e1f381fe5a34b8e3350799ac4c3a58fe2def590b12ad4354da7b01ebf" + }, + { + "path": "research/crt-mixed-width-caller/verify.py", + "usage": "input", + "git_blob": "7980582b86e8d20269ae32252ad03896eff1131b", + "sha256": "5e62787f3c4a8f1175ca7dea6c6b8ceff7863a3f879abd6245faf6aeb272fd45" + }, + { + "path": "research/crt-multitarget-row-audit/PROOF.md", + "usage": "input", + "git_blob": "77adf1bcd4d5da9035d400985638f13572055387", + "sha256": "607397886c41c0abe00969c5e1cd54f23c16a61e4fc34d3dc1eb8d47e8f97662" + }, + { + "path": "research/crt-multitarget-row-audit/README.md", + "usage": "input", + "git_blob": "fd052021bd66bba6e8a2ab6d1af8ee3c0240eadb", + "sha256": "5414c943d1ce540b84500a0a1960210640f287ab2ce5a4a91fc261d6109977ad" + }, + { + "path": "research/crt-paid-key-service/PROOF.md", + "usage": "input", + "git_blob": "a0b84e8d3bd80d760a1be9e801fc57939b6f24e9", + "sha256": "1a4ac02653eb6c1b20807033a910f27bf9484cc972bf2629941f589275a87325" + }, + { + "path": "research/crt-paid-key-service/service.py", + "usage": "input", + "git_blob": "726d9523ab7dd4a16697f9201b0224f2da1f2517", + "sha256": "ff06c6305c9f650a694e5c42baa4c7d841decf844a4f44f6776acc10a8400083" + }, + { + "path": "research/crt-paid-key-service/verify.py", + "usage": "input", + "git_blob": "9cd6b46a1ae52223ffe8de73c8e223e74f11ba4a", + "sha256": "fb02e2792cb07c52367c0a8c7087d54958bdf55214e51bc02f4e68dbf95547b1" + }, + { + "path": "research/crt-paid-row-reentry/SOURCES.json", + "usage": "input", + "git_blob": "8f77f1ca423df752272669bc7e71e8642b1c2f5b", + "sha256": "3b7107191656e0945c709364f2f5a0ca0161c92be368ca55f9f032f3e692a3ac" + }, + { + "path": "research/crt-paid-row-reentry/reentry.py", + "usage": "input", + "git_blob": "a0c99ee0b0012caabde48bc44d5b19befb59245f", + "sha256": "19b9ffa6d77547818d7e71980c29492c27f5d6fbd81e2cccac4ee752acadcf25" + }, + { + "path": "research/crt-paid-row-reentry/verify.py", + "usage": "input", + "git_blob": "f9054c051897c32864a6d63cab3031df87fdd775", + "sha256": "6a79ea51739a824647d7c3971135c4767336bcdc7c1b088b0f821177724f600d" + }, + { + "path": "research/crt-uniform-rom-query/PROOF.md", + "usage": "input", + "git_blob": "63b0551a7715b9b67f2b13510183254401eb082f", + "sha256": "736be5e1af590f2195e8b56b958258f0babe5cd6d2cf6f4f5023410112f4d870" + }, + { + "path": "research/crt-uniform-rom-query/machine.py", + "usage": "input", + "git_blob": "88292ce98d31d540c7dba6960bfe4c19f06a8077", + "sha256": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d" + }, + { + "path": "research/encoded-crt-entry-lifecycle/PROOF.md", + "usage": "input", + "git_blob": "8c9d971a3d3e5a75637e3279ed8f7f89b0c6a566", + "sha256": "a619be48c8c85749ea5411929aa6ff3986443b467133d32d19d543250b0054b0" + }, + { + "path": "research/encoded-crt-entry-lifecycle/entry.py", + "usage": "input", + "git_blob": "1fa2b0cb88320d4f5b623554bb0fc6de332b773c", + "sha256": "0537ec98f306270c8ff6a424841886cf53f675d9947029347090c7dc779616d7" + }, + { + "path": "research/encoded-current-crt/PROOF.md", + "usage": "input", + "git_blob": "286ab05ba7ab500e5b86268384545dcec8862d1c", + "sha256": "7da614e737414a373c8716158f2c02a52666620ea1f114fac7ca09b3b38489bc" + }, + { + "path": "research/encoded-current-crt/producer.py", + "usage": "input", + "git_blob": "a327b0161eca57a1cc44ec2aa8e3defed2167ddc", + "sha256": "88dab4ca02a92164a67826db361214fa1405e4b4a588f8c4279a21bcee95ab76" + }, + { + "path": "research/r437-preparation-composition/predecessor4025/source/records.py", + "usage": "input", + "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3", + "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372" + }, + { + "path": "research/r437-preparation-composition/predecessor4025/source/words.py", + "usage": "input", + "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50", + "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9" + }, + { + "path": "research/unconditional-batched-crt/NOTICE.md", + "usage": "input", + "git_blob": "886a8fdee275f01b459cbd68ae2815dc9269502f", + "sha256": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461" + }, + { + "path": "research/unconditional-batched-crt/check_batched_crt.py", + "usage": "input", + "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc", + "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e" + } + ] +} diff --git a/research/crt-shared-row-banks/TASK.json b/research/crt-shared-row-banks/TASK.json new file mode 100644 index 0000000000..2d57062a13 --- /dev/null +++ b/research/crt-shared-row-banks/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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": "changed", + "actual_scope": "Explicit shared physical ROM bank across separately constructed paid CRT row queries at a fixed admitted node.", + "scope_change_reason": "Take PR5625 Open next question 2, a scoped owned-erasure/reentry interface; do not audit the predecessor or claim the selected assumption in full.", + "bottleneck_link": "A source-bound reuse contract replaces a sum of retained ROM capacities by one bank while preserving dirty inputs and source updates. Supplier and whole-tree admission remain separate.", + "budget_minutes": 60, + "stop_rule": "Stop research at the first verified strict storage reduction; package the result and leave broader reuse open.", + "outcome": "completed", + "evidence": "PROOF.md; shared.py; verify.py; generated hash-bound RESULT.json", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can PR5505 reusable numerical ownership compose with this shared-ROM source-update caller?", + "why_it_matters": "Their capacities still sum across rows.", + "first_step": "Bind PR5505 live-result leases and marker reinstatement to this query close.", + "blocked_by": "The existing numerical-owner construction has not been composed with this physical ROM/level caller." + }, + { + "question": "Can the same bank cross changing-precision nodes?", + "why_it_matters": "Whole-tree storage needs actual boundary contracts.", + "first_step": "Bind protected-word conversion and source ownership at one adjacent node pair.", + "blocked_by": "Changing-precision caller composition remains open." + }, + { + "question": "How is clean bank capacity acquired from dirty backing?", + "why_it_matters": "The theorem assumes supplied clean tapes.", + "first_step": "Price one exact allocation or restored-erasure mechanism.", + "blocked_by": "No arbitrary-dirty acquisition algorithm is supplied." + } + ], + "environment": { + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "implementation": "CPython" + } +} diff --git a/research/crt-shared-row-banks/VERIFY.json b/research/crt-shared-row-banks/VERIFY.json new file mode 100644 index 0000000000..2e4655518d --- /dev/null +++ b/research/crt-shared-row-banks/VERIFY.json @@ -0,0 +1,69 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/crt-current-row-query/PROOF.md", + "research/crt-current-row-query/SOURCES.json", + "research/crt-current-row-query/join.py", + "research/crt-dense-guard-scan/machine.py", + "research/crt-encoded-benes-rom-producer/PROOF.md", + "research/crt-encoded-benes-rom-producer/SOURCES.json", + "research/crt-encoded-benes-rom-producer/microcode.py", + "research/crt-encoded-benes-rom-producer/vendor/pr4192-NOTICE.md", + "research/crt-encoded-benes-rom-producer/vendor/pr4192-PROOF.md", + "research/crt-encoded-benes-rom-producer/vendor/pr4192-verify.py", + "research/crt-mask-repair-bridge/key_subroutine.py", + "research/crt-mixed-row-entry/PROOF.md", + "research/crt-mixed-row-entry/SOURCES.json", + "research/crt-mixed-row-entry/bridge.py", + "research/crt-mixed-row-entry/verify.py", + "research/crt-mixed-width-caller/README.md", + "research/crt-mixed-width-caller/verify.py", + "research/crt-multitarget-row-audit/PROOF.md", + "research/crt-multitarget-row-audit/README.md", + "research/crt-paid-key-service/PROOF.md", + "research/crt-paid-key-service/service.py", + "research/crt-paid-key-service/verify.py", + "research/crt-paid-row-reentry/PROOF.md", + "research/crt-paid-row-reentry/SOURCES.json", + "research/crt-paid-row-reentry/reentry.py", + "research/crt-paid-row-reentry/verify.py", + "research/crt-uniform-rom-query/PROOF.md", + "research/crt-uniform-rom-query/machine.py", + "research/encoded-crt-entry-lifecycle/PROOF.md", + "research/encoded-crt-entry-lifecycle/entry.py", + "research/encoded-current-crt/PROOF.md", + "research/encoded-current-crt/producer.py", + "research/r437-preparation-composition/predecessor4025/source/records.py", + "research/r437-preparation-composition/predecessor4025/source/words.py", + "research/unconditional-batched-crt/NOTICE.md", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "New persistent 52-role bank on ten current-state rows, complete round trip, historical tails, exact retained-cell reduction and five rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "New persistent 52-role bank on ten current-state rows, complete round trip, historical tails, exact retained-cell reduction and five rejection controls." + } + ] +} diff --git a/research/crt-shared-row-banks/shared.py b/research/crt-shared-row-banks/shared.py new file mode 100644 index 0000000000..62eda05226 --- /dev/null +++ b/research/crt-shared-row-banks/shared.py @@ -0,0 +1,69 @@ +"""Persistent ROM backing for the source-bound CRT row query. + +New interface produced by Nick Petalas. Apache-2.0. +The source query and producer retain their original notices and credit. +""" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def capacities(registers, precision, height): + """PR5519's credited role extents, used as supplied blank capacities.""" + need(len(registers) == 44 and len(set(registers)) == 44, "44 scalar roles") + need(1 <= height < precision, "Compiled precision and height") + n = 1 << height + sizes = {name: precision + 2 for name in registers} + sizes.update(arena=5 * precision * n * (height**2 + 3 * height + 1) + 2, + spool=n * (2 * height - 1) + 2, + layers=(n + 1) * (2 * height - 1) + 2, rom=n + 2, + h=precision + 2, modulus=precision + 2, + selected_layer=precision + 2, offsets=precision + 3) + need(len(sizes) == 52, "52 distinct bank roles") + return sizes + + +class BankPool: + """A supplied clean bank, with a single compiled owner at a time. + + Allocation is fixture initialization. Runtime acquire/release only changes + ownership metadata; it never reads, clears, copies or resizes tape contents. + Blank reentry is a proved precondition, observed separately by the verifier. + """ + + def __init__(self, sizes): + need(len(sizes) == 52 and all(n > 0 for n in sizes.values()), "Bank shape") + self.cells = {name: ["_"] * size for name, size in sizes.items()} + self.leased = False + + def acquire(self): + need(not self.leased, "Bank already leased") + self.leased = True + return self.cells + + def release(self, cells): + need(self.leased and cells is self.cells, "Bank lease ownership") + self.leased = False + + +def adapt_source(source): + """Add one explicit bank parameter; retain every runtime tape instruction.""" + edits = ( + ("start, row, fault=None):", "start, row, banks, fault=None):"), + (" self.fault = fault", " self.fault = fault\n self.banks = banks"), + (" headers = {name: Tape() for name in names}", + " self.service = banks.acquire()\n" + " headers = {name: Tape(self.service[name]) for name in names}"), + (" self.service = {name: ['_'] for name in rom_module.REGS+('arena','spool','layers','rom')}\n" + " self.service.update({name: headers[name].cells for name in names})\n", ""), + (" self.entry.close()\n self.closed=True", + " self.entry.close()\n" + " if self.service is not None:self.banks.release(self.service)\n" + " self.closed=True"), + ) + for old, new in edits: + need(source.count(old) == 1, "Exact source-bound allocation seam") + source = source.replace(old, new, 1) + return source diff --git a/research/crt-shared-row-banks/verify.py b/research/crt-shared-row-banks/verify.py new file mode 100644 index 0000000000..3145272886 --- /dev/null +++ b/research/crt-shared-row-banks/verify.py @@ -0,0 +1,175 @@ +"""Execute the new cross-row bank interface, not a predecessor replay. + +Produced by Nick Petalas. Apache-2.0. +""" +from hashlib import sha256 +from pathlib import Path +import importlib.util +import json +import sys +import time + +P = Path(__file__).resolve().parent +ROOT = P.parents[1] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + need(spec is not None and spec.loader is not None, "Module specification") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def modules(): + pins = json.loads((P / "SOURCES.json").read_text())["files"] + for pin in pins: + if pin["usage"] == "input": + need(sha256((ROOT / pin["path"]).read_bytes()).hexdigest() == pin["sha256"], "Source bytes") + old = load("shared_row_fixture", ROOT / "research/crt-paid-row-reentry/verify.py") + mod = old.modules() + shared = load("shared_row_bank", P / "shared.py") + path = ROOT / "research/crt-current-row-query/join.py" + joined = old.load("shared_row_join", path, shared.adapt_source(path.read_text())) + return old, shared, joined, mod + + +def observe_bank(pool, sizes, identities): + need(not pool.leased, "Retired bank lease") + need({k: id(v) for k, v in pool.cells.items()} == identities, "Persistent physical identities") + need({k: len(v) for k, v in pool.cells.items()} == sizes, "Fixed historical extents") + need(all(all(x == "_" for x in v) for v in pool.cells.values()), "Full historical bank blank") + + +def new_query(mod, joined, pool, source, dirty, widths, ell, level, start, row): + helper, base, rom, _, _, program = mod + w, records, entry, numeric, _, _, row_module = base + return joined.RowQuery(w, records, entry, numeric, row_module, rom, program, + source, dirty, widths, ell, level, start, row, pool) + + +def finish_row(old, mod, query, staging, source, dirty, initial_dirty, widths, expected, level, start): + helper, base, _, _, adapter, _ = mod + w, records, *_ = base + owned = [] if query.output is None else [*query.entry.inputs, *query.entry.context.owned] + adapter.consume_into_source(query, staging, widths, level, start) + need(query.closed and source.head == 1, "Query closes before next row") + need(old.decode(source, widths, w, records) == expected, "Current-state row endpoint") + need(helper.snapshot(dirty) == initial_dirty, "Protected dirty bytes and heads") + need(staging.head == 0 and all(x == "_" for x in staging.cells), "Staging retired") + need(all(t.head == 1 and all(x == w.BLANK for x in t.cells) for t in owned), "Numerical retirement") + need(all(t.head == 0 and all(x == "_" for x in t.cells) for t in query.ports), "Joined retirement") + + +def run_case(old, shared, joined, mod, mixed=False): + helper, base, rom, _, _, _ = mod + w, records, entry, _, caller_module, crt, _ = base + moduli, widths, state = (5, 7, 3, 2), (3, 3, 2, 2), (3, 2, 1, 1) + if mixed: + moduli, widths, state = (2, 5, 7, 3), (2, 3, 3, 2), (1, 4, 7, 3) + ell, level, start = 3, 2, 0 + precision = 1 + sum(widths) + source = helper.axis_stream(w, records, entry, moduli, widths, state) + source_identity = id(source.cells) + original = bytes(source.cells) + dirty = [helper.port(w, entry, helper.bits(3 * i + 1, precision) + [w.RIGHT]) for i in range(8)] + for i, tape in enumerate(dirty): + for _ in range(i % 3): + tape.step(1) + initial_dirty = helper.snapshot(dirty) + staging = joined.Tape() + sizes = shared.capacities(rom.REGS, precision, max(widths[2:])) + pool = shared.BankPool(sizes) + identities = {k: id(v) for k, v in pool.cells.items()} + caller = caller_module.Caller(moduli, widths, ell, crt) + expected, retained_queries, backings, trace = state, [], {}, [] + schedule = tuple(range(2 * ell - 1)) + tuple(reversed(range(2 * ell - 1))) + if mixed: + schedule = (1, 1) # Same involutive row twice, with height 3 then 2 each time. + for row in schedule: + specs = [s for s in caller.row(expected, level, row) if 2 <= s[0] < 4] + expected = caller.apply(expected, specs) + before = bytes(source.cells), source.head + query = new_query(mod, joined, pool, source, dirty, widths, ell, level, start, row) + need((bytes(source.cells), source.head) == before, "Query borrows source unchanged") + row_backings, _ = old.footprint(query) + retained_queries.append(query) + finish_row(old, mod, query, staging, source, dirty, initial_dirty, widths, expected, level, start) + observe_bank(pool, sizes, identities) + need(id(source.cells) == source_identity, "Persistent owned source") + backings.update(row_backings) + trace.append(dict(row=row, state=list(expected), producer_calls=query.invocations, + row_backing_cells=sum(map(len, row_backings.values())))) + need(bytes(source.cells) == original and expected == state, "Complete forward/reverse endpoint") + bank_cells = sum(sizes.values()) + fresh_cells = sum(x["row_backing_cells"] for x in trace) + len(staging.cells) + shared_cells = sum(map(len, backings.values())) + len(staging.cells) + active = sum(q.output is not None for q in retained_queries) + need(shared_cells == fresh_cells - (active - 1) * bank_cells, "Exact retained storage reduction") + need(shared_cells < fresh_cells, "Strict storage improvement") + return dict(rows=len(schedule), active_rows=active, producer_calls=sum(q.invocations for q in retained_queries), + precision=precision, height=max(widths[2:]), bank_roles=len(sizes), bank_cells=bank_cells, + distinct_bank_baseline_cells=fresh_cells, shared_bank_cells=shared_cells, + saved_cells=fresh_cells - shared_cells, trace=trace) + + +def controls(shared, mod): + rom = mod[2] + sizes = shared.capacities(rom.REGS, 11, 3) + pool = shared.BankPool(sizes) + ids = {k: id(v) for k, v in pool.cells.items()} + rejected = [] + messages = {"overlapping_lease": "Bank already leased", "wrong_release": "Bank lease ownership", + "dirty_historical_tail": "Full historical bank blank", "changed_extent": "Fixed historical extents", + "source_drift": "Exact source-bound allocation seam"} + for label, message in messages.items(): + fresh = shared.BankPool(sizes) + try: + if label == "overlapping_lease": + fresh.acquire(); fresh.acquire() + elif label == "wrong_release": + fresh.acquire(); fresh.release({}) + elif label == "dirty_historical_tail": + pool.cells["arena"][-1] = "1" + observe_bank(pool, sizes, ids) + elif label == "changed_extent": + fresh.cells["rom"].append("_") + observe_bank(fresh, sizes, {k: id(v) for k, v in fresh.cells.items()}) + else: + shared.adapt_source("not the pinned query") + except ValueError as error: + need(str(error) == message, "Expected semantic rejection: " + label) + rejected.append(label) + else: + raise ValueError("Defective interface accepted: " + label) + if label == "dirty_historical_tail": + pool.cells["arena"][-1] = "_" + observe_bank(pool, sizes, ids) + return rejected + + +def main(): + start = time.monotonic() + old, shared, joined, mod = modules() + hashes = {name: sha256((P / name).read_bytes()).hexdigest() + for name in ("shared.py", "verify.py", "SOURCES.json")} + result = dict(status="PASS_CRT_SHARED_ROW_BANKS", claim_type="scoped construction and composition proof", + implementation_sha256=hashes, + case=run_case(old, shared, joined, mod), + mixed_height_control=run_case(old, shared, joined, mod, mixed=True), + controls=controls(shared, mod)) + if "--write" in sys.argv: + (P / "RESULT.json").write_text(json.dumps(result, indent=2) + "\n") + else: + need(result == json.loads((P / "RESULT.json").read_text()), "Generated receipt") + print(result["status"], json.dumps(result["case"], sort_keys=True), "controls=" + str(len(result["controls"]))) + print("elapsed_seconds=" + str(round(time.monotonic() - start, 3))) + + +if __name__ == "__main__": + main()