diff --git a/research/word-ram-transfer/.gitattributes b/research/word-ram-transfer/.gitattributes new file mode 100644 index 0000000000..fa1385d99a --- /dev/null +++ b/research/word-ram-transfer/.gitattributes @@ -0,0 +1 @@ +* -text diff --git a/research/word-ram-transfer/CONTENT-HASHES.json b/research/word-ram-transfer/CONTENT-HASHES.json new file mode 100644 index 0000000000..9503eadacf --- /dev/null +++ b/research/word-ram-transfer/CONTENT-HASHES.json @@ -0,0 +1,38 @@ +{ + ".gitattributes": "705fd4d6451a31d36b3df7de96f83f30ac976c9b4a6d1e51671d8e2f33e2d0da", + "compiler/CHECKS.json": "a4c2a1cb86fa8d14b169b1dd47e54bfb27dd8a73fca6132836bdfab528b73849", + "compiler/OVERLAP.md": "91486eff77f1a79bcb25ec0cc47f1c3dcd17b33a76a624130d57182c86e7c5cc", + "compiler/SOURCES.json": "1090c437e66722ab5253f97fb5678ed08beeaaf790c3ffc58eb86d1adbd227a1", + "compiler/TM-TO-WORD-RAM.md": "b5d444b83a7b276ee02f1317a30e7b67f9a0bc1fa14be503716ee8fa1822f2f7", + "compiler/tm_to_ramstd.py": "dc405afa466191117c72bf92878b4eed687a0e3e29329fccd140bd69da9f78c3", + "cost/COST-RESULT.json": "3457f019b630f82cd84d61f3ed32f1e378a00281daee0193db4bdd8f79f64335", + "cost/COST-THEOREMS.md": "79eef859eb2ae32a66879f294d626c3947bcfe55434b4a38a296d271b3aa9675", + "cost/monomial_metadata.py": "a539a148a58e5b9850b6d52cc2467ced32eac3b99a3bfd8a0344a224d3dc88db", + "cost/quadratic_phase.py": "bdc0bcc5a8c96cd9f09d6985d7c9ac2870a2c2ed11fcbe347011d1374d32f882", + "cost/SOURCE-HASHES.json": "7787b4b28b3650dc14149b71e1427502410b8df24f7152d853a014ee599efb05", + "cost/streaming_affine.py": "89b668be21b9ee67b46b5448a7d2c4de372521ead8112f42d1217811702d2b79", + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "machine/AUDIT.json": "c546ef5ba34d17916a8120ef6207445ec3bcf61c61f6b35a13e5c8dedbbeda2d", + "machine/DEPENDENCIES.json": "8bf3635fbef878201d7dc3a253e033b8539aa3e828f266d174104ac7fc56117c", + "machine/INDEPENDENT-AUDIT.json": "6e9c73c01b64c40502ede07c9530be0ae87eeec02c1d5d2f293fe788e983f5a5", + "machine/MACHINE-INTERFACE.md": "923d902b3b0f6e4d7b661fd9b133f2964d08ed1b4488ea6c594b420aa34fa9d6", + "machine/REPRODUCE.md": "0f5ab02838f09ae03a83d2cc0e4c1dafc595ab8b9619341678ef3a79d07b1904", + "machine/SOURCE-MAP.json": "256b9c73419f564d10405a554d97ec6efeea43c0850060dc09972367e4ccc405", + "machine/sources/Mathproof/Meta/Problem18RAMLax13ProofsBounds20261001.lean": "16ca19d477c17805abecb3ca265e4b2b7ca0c17011ca884161f1a59a541e52e2", + "machine/sources/Mathproof/Meta/Problem18RAMLax13ProofsCompile20261001.lean": "bc2237188b9b7c6f4d5524bad17d353bab873ab693ddb2e947574739dc2aae2c", + "machine/sources/Mathproof/Meta/Problem18RAMLax13ProofsImp20261001.lean": "cf6303e7ef49ed47d0f2c396d074c194c30673482ef4e44f5dff1ada06f68c6c", + "machine/sources/Mathproof/Meta/Problem18RAMLax13ProofsMachine20261001.lean": "82bbeff85aebddd2740f28476f3b602a8593358bd509ac9a75944610f06fb3e8", + "machine/sources/Mathproof/Meta/Problem18RAMLax13ProofsSimulation20261001.lean": "2db5af757e7808c62ac1b578a26e198532c24b17388a06719c127f08de23811c", + "machine/sources/Mathproof/Meta/Problem18RAMLax13Ram20261001.lean": "b95844098a3c402ec895c542d07a4b60354455cf66fe77bad1050d15583ec948", + "machine/sources/Mathproof/Meta/Problem18RAMLax51BinaryWordEncoding20261001.lean": "d0f28fb10d6b09de7fb8888ddb0fe9a45a414ab9a8f1d90cef4e5c8e3bf4fe2d", + "machine/sources/Mathproof/Meta/Problem18RAMLax51RamPolytime20261001.lean": "370a943f3e4b0ec7fb536ac5c4c4cc0ebbc7b55a52706863a1d5379aa53e3836", + "machine/sources/Mathproof/Meta/RamStd20261007.lean": "7c9263a14360b7fe485a753bda9c35c408b768612538d092f0dff217aa4f597e", + "machine/WordRAMLogWidthTransfer20261022.lean": "e1849b658e0278181b41beb3572af26bceb035fa5c02c260993e9f34f21361c3", + "PACKED-TAPES.md": "27a1c874f2eae10f3f70758f6f2e5e221e505ec3d5b9fb847f7c5ca3cbe4f10c", + "packed_tape.py": "5a4eca73b6043b3b6a2785fd475491a4960caa40b426a5cd0a237434cd295020", + "README.md": "4160d820310fb9bcebc359e7108146ea2e1ca9713277feaa4636e820211fabef", + "SOURCES.json": "57f78e056178dcb5eb8b4438df7dfa560e209cc21f7236e81be3853f9a62a4cf", + "TASK.json": "d15103c4312faf7af1f8daefe355c82dd53418d20b21a58fda2c45ddef4186d2", + "VERIFY.json": "5699bc0079b6b72a94e83b2e452ca1761e02ae54ac5112c8ecd5c074379f3bc7", + "verify.py": "8af9fa54081c3cce91dc7672db63b97c3182a4a10574d4685845701618573a55" +} diff --git a/research/word-ram-transfer/LICENSE b/research/word-ram-transfer/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/word-ram-transfer/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/word-ram-transfer/PACKED-TAPES.md b/research/word-ram-transfer/PACKED-TAPES.md new file mode 100644 index 0000000000..9137c0370a --- /dev/null +++ b/research/word-ram-transfer/PACKED-TAPES.md @@ -0,0 +1,43 @@ +# Uniform packed tape kernels + +## Representation theorem + +Fix k tapes and a fixed alphabet with blank 0, represented by c-bit fields, where c is a fixed power of two and the alphabet has at most 2^c symbols. Fix H = 2^h >= 2k. Registers below 64 and packed storage beginning at address 128 are disjoint. The RAM has w-bit modular values and addresses, Boolean operations, shifts, addition, natural monus subtraction, indirect loads/stores and branches. No multiplication or division is used. + +For input bit length n, set lambda = floor(log2(n+2)), q = floor(lambda/(8c)), and let B be the largest power of two at most q, or 1 when q = 0. INIT in packed_tape.py computes log2(B) and B-1 using the same finite program at every input length and word width. The fixed program depends on c, not on n, w or a time-horizon advice string. + +Map tape i and signed coordinate z to tag = 2i + [z < 0], and u = z for z >= 0 or -z-1 otherwise. Write u = Bt+j with 0 <= j < B. Store the symbol in field j of word address + + 128 + Ht + tag, + +at bit offset cj. For valid parameters and nonwrapping addresses, GET returns that symbol in exactly 13 successful RAM instructions, and SET writes a supplied c-bit symbol in exactly 17 successful RAM instructions. SET preserves every other field, every unused high bit of that word, and every other data word. Scratch registers are explicitly clobbered. Halt is terminal and is not counted as a successful transition. + +### Proof + +INIT repeatedly right-shifts n+2 until it is less than 2, incrementing lambda once per shift. Dividing lambda by 8c is a fixed right shift because c is a power of two. Repeated doubling then selects B and computes B-1. Since B is a power of two, t = u >> log2(B) and j = u AND (B-1). Both computations take one instruction. The address is formed by shifting t left by h, adding the tag and adding 128. + +Addresses of different blocks or tags cannot coincide: equality modulo no wrap reduces to H(t-t') = tag'-tag, and the right side has magnitude below H. Hence t=t' and tag=tag'. The two sign banks partition integer coordinates without losing coordinate -1 or 0. The c-bit fields at offsets cj do not overlap. GET shifts the selected word right and ANDs with 2^c-1. SET constructs mask (2^c-1) << cj, clears precisely that mask, shifts the supplied symbol into it, and ORs the result. These Boolean identities prove the result even with arbitrary values in neighboring fields or high padding. Counting the displayed address macro's 9 instructions and the respective 4 or 8 field instructions proves the exact costs. + +For width safety, let S >= max(n,N+T+m+2), where N is the physical input size, T the number of TM steps, and m the requested output window. All touched head magnitudes and output positions are below S. A sufficient condition is + + w >= max(10, c, ceil(log2(256 + H(S+1)))). + +Then n+2, all indices, masks, effective addresses and scratch addresses fit. If B=1, cB=c<=w. Otherwise cB<=lambda/8<=w/8. Thus the final field ends by bit cB<=w; left shifts cannot discard any field. INIT's doubled trial value also fits. Standard modular arithmetic consequently agrees with the natural address calculations just proved. + +The active data footprint is at most 2k ceil(S/B) words, plus constant scratch; this is a word-count upper bound, not the numeric address span. For fixed c and sufficiently large n, B is between lambda/(16c) and lambda/(8c), up to the harmless small-input cutoff. It is therefore Theta(log n). Combined with a known polynomial bound on S, the sufficient word width is O(log(n+2)). This width is an external machine parameter satisfying a proved lower bound; the program neither obtains nor assumes a time horizon as input. + +## Use in the compiler migration + +For a fixed TM, replace each tape read/write by the displayed macros, and maintain each head's sign and magnitude with bounded additions, subtraction and branching. The fixed transition dispatcher reads all k symbols before performing writes, as in compiler/TM-TO-WORD-RAM.md. These operations require O(1) instructions per TM transition for fixed machine and alphabet. Physical input initialization and output serialization still cost O(N+m). Packed storage does not prove a T/w execution speedup. + +For a complete backend with many reserved head/control cells, use a fixed machine-dependent base R >= 128 above all those cells. The emitters accept this base as a literal parameter. Replace 128 by R in the address and 256 by 2R in the sufficient width bound; the same proof and 13/17 counts apply. This prevents large fixed-k control storage from overlapping the packed data. Replay includes bases 256, 1024 and 4096 with 128 tape tags. + +This is a constructive representation and macro theorem, with an informal universal proof and exact finite replay. The complete packed finite-control backend has not been emitted or Lean-verified. The separate unpacked compiler is the executable end-to-end semantic baseline. + +Zero-initialized RAM fields represent initially blank tape cells. A caller that reuses dirty memory must initialize the fields it will read; arbitrary dirty unvisited fields are allowed only if never read as blanks. The field-preservation theorem permits arbitrary dirty neighboring fields without asserting they are blank. Initializing N input symbols takes O(N) SET calls. No uncharged conversion from arbitrary symbol words into densely packed bit input is assumed. + +## Evidence + +The optimized isolated replay covers 15,360 traces, tape counts 1, 2, 4 and 8, field widths 1, 2 and 4 bits, and word widths 10, 16, 32, 64 and 128. It checks retained writes across banks and signs, exact instruction counts, dirty-padding preservation and an intentionally wrong-bank control. These finite checks support the implementation; the representation proof above supplies the universal argument. + +Prepared by Dugongue with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/word-ram-transfer/README.md b/research/word-ram-transfer/README.md new file mode 100644 index 0000000000..18d6f2682f --- /dev/null +++ b/research/word-ram-transfer/README.md @@ -0,0 +1,50 @@ +# Bounded-word RAM transfer and native kernels + +This package starts the requested migration from multitape Turing machines to a concrete Word RAM. It supplies an executable finite TM compiler, a freshly kernel-checked logarithmic-word bridge using the actual Problem 1.8 compiler, packed-tape access kernels, and constructive RAM-native algorithms for affine permutations and quadratic Gaussian phases. It does not claim an improved kappa or a fully rewritten native multiplication algorithm. + +## Results and review order + +1. [Machine interface and checked bridge](machine/MACHINE-INTERFACE.md): for an actual bounded IMP execution of k steps whose values and indices are polynomially bounded in n, the existing fixed compiled program runs in at most 10k successful RAM instructions at logarithmic word width. The new explicit input-domain interface fixes a quantifier mismatch in the unrestricted list-of-naturals logarithmic-width wrapper. This reuses the implemented Problem 1.8 machine and compiler; the new Lean appendix has five checked theorems. +2. [Finite TM compiler](compiler/TM-TO-WORD-RAM.md): an actual emitter for a fixed finite-alphabet multitape machine, with signed heads, polynomial-envelope logarithmic word width, genuine halt and fixed-length LSB output adaptation. Its sufficient simulation theorem transfers any complete fixed-machine multiplication theorem at constant step overhead. This is a classical model conversion, not a new multiplication exponent. The emitter and simulation proof are not Lean-formalized. +3. [Packed storage](PACKED-TAPES.md): uniform n-dependent packing with 13-instruction reads and 17-instruction writes, preserving neighboring fields and high padding. This reduces storage words while retaining constant simulation overhead. It does not imply a word-factor time saving. +4. [RAM-native layout algorithms](cost/COST-THEOREMS.md): affine record permutations in at most 8NL + 40N + 8 instructions; quadratic Z/4 phases in O(N+r); exact monomial action on modular limb records in O(NL+N+r). An explicit X/S/Z/CNOT/SWAP/CZ metadata compiler costs O((m+1)(r+1)^2). These are candidate replacements for paid tape routing and monomial segments. Hadamards, arbitrary phase roots and ADD crossings are excluded from this local normal form. + +The target is finite bounded-word memory with logarithmic word width, not unit-cost exact-complex cells or one unit-cost multiplication on an entire n-bit input. The new TM compiler, packed-access kernels and native layout constructions use no word multiplication or division. The general IMP bridge preserves the source command's operations and may use those instructions; it does not lower arbitrary IMP multiplication or division to additive operations. Every full buffer, table, register region and effective address must fit below 2^w. + +## Why this is a useful first migration step + +The universal compiler separates correctness transfer from native optimization: mathematical identities, precision/recovery proofs and conditional recurrence hypotheses remain available, while tape-specific routing can be replaced one subroutine at a time. The native kernels identify actual blocks that can be replaced with finite-word algorithms and complete local costs. No term is deleted from an existing multiplication invoice merely because random access is available. + +A model comparison is essential. Fuerer's [2014 log-RAM paper](https://arxiv.org/abs/1402.1811) already gives linear-time integer multiplication with unit-cost logarithmic-word multiplication. Thus preserving a TM bound on that stronger model is a baseline, not a best-known RAM complexity claim. The present restricted additive/Boolean compiler is also not asserted to be a new complexity record. + +## Reproduce + +From the repository root, with Python 3.12 and no third-party packages: + +```sh +python3 scripts/research_package.py --package research/word-ram-transfer --check-only +python3 scripts/research_package.py --package research/word-ram-transfer +``` + +A Git-free extracted package can instead run `python3 -I -O -B verify.py` from its own directory. The verifier authenticates every package byte listed in CONTENT-HASHES.json before executing any local checker. It launches isolated optimized Python subprocesses; no result depends on enabled assert statements. The Python command checks finite implementations and proof-source integrity, not the universal claims or Lean compilation. + +The [Lean reproduction instructions](machine/REPRODUCE.md) pin Lean 4.33.0 and Mathlib db584cd6d46c92f209a44c0f1c829460d327499d. Nine dependency source files are included, unchanged. [INDEPENDENT-AUDIT.json](machine/INDEPENDENT-AUDIT.json) records a second fresh audit of all five new theorems using existing pinned canonical import artifacts: only propext, Classical.choice and Quot.sound occur. An isolated rebuild of all frozen dependencies is not claimed. Publication snapshots are not an additional active DAG. + +## Scope, overlap and provenance + +The assigned task is a model migration, explicitly replacing the usual kappa hill-climb objective. TASK.json preserves the nearest historical card and marks this changed scope. Main was refreshed at f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc. Selected-frontier files and prior research are unchanged. [Overlap and credit](compiler/OVERLAP.md) compares actual pinned proof sources from PRs #956 and #647, which already construct exact scalar RAM providers in their declared models. Their bit-lowering obligations must not be silently treated as bounded-word operations. + +Retrieval covered the federated source catalog and canonical Lean tree, with sixteen selected machine precedents plus cost and compiler source pins. It returned 153 Problem18RAM modules and nine Lax13 modules, but missed some newer on-disk RamStd/RAMRoot identities and exact typed queries returned no records. This is substantial source retrieval, not a claim to have read or rechecked every registered theorem. SOURCE-MAP.json and the component manifests state that coverage. + +## Open next questions + +- **First native caller:** choose one pinned admitted multiplication caller and replace a fully specified monomial/layout segment, preserving its actual observation boundary, input/output order, precision and aliasing contract. First step: identify the exact executable segment and pay metadata, copying and serialization in its whole-call invoice. Blocker: these local kernels have not yet been wired into that caller. +- **Complete packed backend:** emit head updates, dispatcher and IO around the packed macros, then compare the resulting actual finite program with the existing unpacked reference. First step: a one-transition invariant with all reads before writes. Blocker: only the access macros currently have emitted code and finite checks. +- **Formal compiler refinement:** prove the new emitter against RamStd.step and the explicit input-domain contract. First step: fixed-bank non-aliasing and one finite dispatcher transition. Blocker: the five checked Lean theorems concern the pre-existing IMP compiler, not this new TM emitter. +- **Precision and full cost:** connect the native modular-limb representation to each chosen transform's signed headroom and rounding/recovery estimates. First step: instantiate the existing Problem 1.8 limb/gather contracts at the selected precision. Blocker: Gaussian-unit phase correctness alone does not prove arbitrary transform accuracy or complete multiplication cost. + +## Credit + +Prepared for Dugongue by OpenAI Codex with three parallel agents and substantial AI assistance. Existing Problem 1.8 formalizations supply the RAM, bounded IMP semantics, physical layout, compiler, simulation and limb/gather precedents. Szymon Torunczyk and GPT's compositional-polytime implementation is retained through the structured-TM precedent. The tensor/symplectic and frame/normal-form precedents motivate the restricted monomial segments without asserting that arbitrary Clifford circuits are free. + +Retain the upstream lineage detailed in compiler/OVERLAP.md, including Dugongue's #390, Jacob Sussman's frame/bank/RAM/Fourier and P193 contributions, the bridge/normalization/audit chain, native/controller work by zxv, Jacob Alan Sussman's mixed-target recursion, Cinna Davis's query/helper work, and all physical, precision, prime, tape and outer-analysis suppliers. New material is Apache-2.0; existing source headers are preserved. No independent human peer review is claimed. diff --git a/research/word-ram-transfer/SOURCES.json b/research/word-ram-transfer/SOURCES.json new file mode 100644 index 0000000000..18b51b4e95 --- /dev/null +++ b/research/word-ram-transfer/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + } + ] +} diff --git a/research/word-ram-transfer/TASK.json b/research/word-ram-transfer/TASK.json new file mode 100644 index 0000000000..96b96a9a5b --- /dev/null +++ b/research/word-ram-transfer/TASK.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Construct bounded-word machine contracts, an executable finite TM compiler and positive RAM-native replacements using Problem 1.8 and federated proof precedents.", + "scope_change_reason": "Explicit user assignment to migrate the complete multiplication route to Word RAM, instead of another register-model or kappa hill climb; the nearest historical model-change card is retained only as provenance.", + "bottleneck_link": "Side result supporting a requested model migration: removes a semantic transfer obstacle and supplies concrete replacements for paid tape layout, without changing the selected frontier.", + "budget_minutes": 60, + "stop_rule": "Stop after positive universal component proofs, fresh bridge audit and isolated finite implementation checks; do not claim full native multiplication or new kappa.", + "outcome": "partial", + "evidence": "Five fresh Lean bridge theorems, independent standard-axiom audit, finite TM emitter, packed access kernels and exact native-layout checks.", + "author": "Dugongue", + "ai_assistance": "OpenAI Codex root plus three parallel agents; no human peer review claimed.", + "open_questions": [ + { + "question": "Which complete multiplication caller should receive the first native monomial/layout replacement?", + "why_it_matters": "Converts local RAM primitives into actual whole-call savings.", + "first_step": "Freeze one executable segment and include descriptor, buffer and IO costs.", + "blocked_by": "No caller integration yet." + }, + { + "question": "Can the packed macros be assembled into a complete emitted TM backend?", + "why_it_matters": "Retains the current semantic reference while reducing memory words.", + "first_step": "Implement head-update and dispatcher glue with one-step invariants.", + "blocked_by": "Only packed access macros emitted so far." + }, + { + "question": "Can the finite TM emitter be refined against RamStd.step in Lean?", + "why_it_matters": "Extends checked quantitative transfer beyond the existing IMP compiler.", + "first_step": "Prove finite bank non-aliasing and all-reads-before-writes transition correctness.", + "blocked_by": "New emitter has informal proof and finite replay only." + } + ] +} diff --git a/research/word-ram-transfer/VERIFY.json b/research/word-ram-transfer/VERIFY.json new file mode 100644 index 0000000000..6f70de67c9 --- /dev/null +++ b/research/word-ram-transfer/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "SHA256 binding of all package bytes; actual finite TM execution and five injected faults; output orientation; packed bank/frame and exact instruction counts; affine, phase and metadata identities; existing fresh Lean receipt, not recompilation." + } + ] +} diff --git a/research/word-ram-transfer/compiler/CHECKS.json b/research/word-ram-transfer/compiler/CHECKS.json new file mode 100644 index 0000000000..02dc412f85 --- /dev/null +++ b/research/word-ram-transfer/compiler/CHECKS.json @@ -0,0 +1,30 @@ +{ + "cases": 246, + "checker_sha256": "dc405afa466191117c72bf92878b4eed687a0e3e29329fccd140bd69da9f78c3", + "emitted_code_faults_rejected": [ + "stride", + "head_unit", + "store", + "halt", + "output" + ], + "formal_lean_verification": false, + "halting_cases": 158, + "lsb_emitter": { + "cases": 9762, + "dirty_post_terminator_tested": true, + "full_width_no_terminator_tested": true, + "leading_zero_tested": true, + "microinstructions": 3146059, + "product_pairs": 1364, + "small_word_boundary_tested": true, + "wrong_direction_code_rejected": true, + "wrong_msb_append_detected": true + }, + "macro_boundaries": 4794, + "microinstructions": 156594, + "nonhalting_prefix_cases": 88, + "schema": "tm-to-ramstd-finite-check-v1", + "small_word_rejections": 1, + "uses_multiplication_or_division": false +} diff --git a/research/word-ram-transfer/compiler/OVERLAP.md b/research/word-ram-transfer/compiler/OVERLAP.md new file mode 100644 index 0000000000..95e574e241 --- /dev/null +++ b/research/word-ram-transfer/compiler/OVERLAP.md @@ -0,0 +1,89 @@ +# Provenance and overlap for the finite compiler + +This simulation is classical. Its useful local contribution is an actual +finite-program construction against the existing Problem 1.8 `RamStd` semantics, +a complete logarithmic-word sufficient theorem with signed head positions and +no supplied time horizon, and an executable semantic comparison. It claims no +new multiplication exponent or first-ever RAM realization. + +## Existing local proofs reused as precedents + +The target machine is the house standard `RamStd20261007.lean`, built on the +Problem 1.8 `Lax13.Ram` definitions. It has shared register/data memory, modular +addresses and values, and natural monus subtraction. We inspected source bytes; +we have not freshly checked those files or this new compiler in Lean. Exact +source hashes are in `SOURCES.json`. + +`Problem18StructuredTMCompiler20260930.lean` explicitly retains Szymon Torunczyk +and GPT's compositional-polytime proof implementation at +`7fadbfd005b359a66ccc1165b2d1becddb2906b8`, Apache-2.0. It treats finite local +operations, finite-control loops and actual contract implementations; a mere +iteration bound is not an implementation. Our theorem follows the same +principle by emitting actual finite target instructions, rather than placing +a whole TM step inside one unexplained unit-cost operation. + +`Problem18TM2OperationalBridge20260930.lean` has exact deterministic terminal-run +transfer lemmas (`deterministic_reaches_terminal`, `deterministic_outputs`). Its +scope distinguishes terminal semantics from arbitrary totalized iteration. Our +compiler analogously reaches an actual `halt`, rather than just stabilizing +under a totalized transition. We do not import that module or assert its theorem +instantiates this separate compiler automatically. + +`MultitapeFrameRule20261014.lean` supplies bounded-footprint lockstep and terminal +preservation principles (`step_lockstep`, `FootprintedRuns.completed_lockstep`, +`completed_runs_finite_frame`). They support the finite-envelope invariant used +here: only visited and requested output cells need representation; no injection +of all integers into finite-word memory is asserted. Again this is a conceptual +reuse of source-inspected proved statements, not a new kernel derivation. + +## Public exact-RAM work already exists + +We fetched and inspected the following actual proof files at pinned public heads, +not just their PR titles. Digests are in `SOURCES.json`. + +- [PR #956 proof](https://github.com/CrocSwap/integer-mult-bounds/blob/fa4df77c9dfdbac93368d95dcb361e69b3b65464/research/pr390-heterogeneous-provider-closure/PROOF.md), + especially its model section and Section 5, already gives constructive native + Gaussian/Walsh realization and charged recurrence in an exact scalar/index + RAM. Its scalar heights are explicitly unrestricted. This is stronger than + a pseudocode-only provider in its declared model, but not a bounded-word bit + RAM multiplication theorem. Credit Dugongue's PR #390 and retained lineage, + Jacob Sussman's frame/bank/RAM/Fourier formalizations and P193 supplier, + PR #363/#373/#375/#377/#381/#397 bridge work, PR #401 normalization and + PR #430's interface audit, together with the OpenAI/math transfer sources. +- [PR #647 provider proof](https://github.com/CrocSwap/integer-mult-bounds/blob/3b3fda9c602fbe4b45d02d1ead0b757b3c94f52c/research/e8-paid-copy-ram-20261013/PROVIDER-PROOF.md), + especially Section 10, already constructs uniform exact-arithmetic RAM + programs, charges address maps and tables, and proves recursive private + workspace separation. It uses exact complex cells and explicitly leaves + finite-alphabet/bit multiplication outside the model. Its companion cyclic + corollary uses separately credited transfer machinery; the provider proof's + earlier scope paragraph must not be used to deny that companion result. + Preserve its Pro provider attribution, Sussman/P193 and E8 antecedents, + dirty-response and bridge contributors, imported OpenAI compiler sources, + and substantial OpenAI Pro/Codex assistance. + +These packages address native scalar realization. The present compiler instead +starts from a fixed finite-alphabet multitape machine and preserves its bit +execution at bounded logarithmic word width. The approaches are complementary. +We do not silently turn their exact-complex primitives into constant-time +bounded-word operations, and do not claim those prior packages are erroneous +merely because they intentionally use a different model. + +## Frontier provenance + +Canonical main was refreshed and pinned at +`f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc`. Its selected record still identifies +conditional kappa 23/10000 from PR #4359; merged PR #4470 gives a stronger +conditional claim 0.00302015 with joint helper boundaries. At this inspection +PR #4535 newly claims 0.003020165 through critical-root transfer. This package +neither adjudicates that pending claim nor changes any selected-result pointer. +Its transfer corollary quantifies over every complete conditional fixed-machine +multiplication theorem, so no numerical frontier assertion is required. + +For every application, preserve the full pinned antecedent's source manifest +and author notices, including native/controller work by zxv, Jacob Alan Sussman's +mixed-target recursion, Cinna Davis's query/helper improvements and all retained +physical, precision, prime, tape and outer-analysis suppliers. Passing our finite +compiler checks does not independently validate any of those upstream claims. + +Prepared by Dugongue with substantial OpenAI Codex assistance. New material is +Apache-2.0. No independent human peer review or Lean certification is claimed. diff --git a/research/word-ram-transfer/compiler/SOURCES.json b/research/word-ram-transfer/compiler/SOURCES.json new file mode 100644 index 0000000000..2c7c0def29 --- /dev/null +++ b/research/word-ram-transfer/compiler/SOURCES.json @@ -0,0 +1,36 @@ +[ + { + "pr": 956, + "commit": "fa4df77c9dfdbac93368d95dcb361e69b3b65464", + "path": "research/pr390-heterogeneous-provider-closure/PROOF.md", + "sha256": "33949793c1044204fec332174071714bb085f32054062fcfb3d56fb84dd0a8d9", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/fa4df77c9dfdbac93368d95dcb361e69b3b65464/research/pr390-heterogeneous-provider-closure/PROOF.md" + }, + { + "pr": 647, + "commit": "3b3fda9c602fbe4b45d02d1ead0b757b3c94f52c", + "path": "research/e8-paid-copy-ram-20261013/PROVIDER-PROOF.md", + "sha256": "cdc496acb844de3b3bcf03f811d1bd345e476b40f0b1cb7c866066612770e834", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/3b3fda9c602fbe4b45d02d1ead0b757b3c94f52c/research/e8-paid-copy-ram-20261013/PROVIDER-PROOF.md" + }, + { + "local_source": "RamStd20261007.lean", + "sha256": "7c9263a14360b7fe485a753bda9c35c408b768612538d092f0dff217aa4f597e", + "evidence": "source inspection only; no new kernel check" + }, + { + "local_source": "Problem18StructuredTMCompiler20260930.lean", + "sha256": "c6f4e59f434f2a041bc1f602cc89846088261220e526cc307cd2f4f14f6e490c", + "evidence": "source inspection only; no new kernel check" + }, + { + "local_source": "Problem18TM2OperationalBridge20260930.lean", + "sha256": "9d4b46d0d787e7fd75e8ad9bf5ac9c12e1457b86a3a9b55f6409e8ef9a2a545c", + "evidence": "source inspection only; no new kernel check" + }, + { + "local_source": "MultitapeFrameRule20261014.lean", + "sha256": "e5aa9ec056340c67bc6e382eee0a859e6903d9944d3a0e021f2a24a12459cb66", + "evidence": "source inspection only; no new kernel check" + } +] diff --git a/research/word-ram-transfer/compiler/TM-TO-WORD-RAM.md b/research/word-ram-transfer/compiler/TM-TO-WORD-RAM.md new file mode 100644 index 0000000000..1cac8e84d2 --- /dev/null +++ b/research/word-ram-transfer/compiler/TM-TO-WORD-RAM.md @@ -0,0 +1,343 @@ +# A constructive multitape-to-Word-RAM transfer + +Prepared by Dugongue with substantial OpenAI Codex assistance. Apache-2.0. + +## Exact scope + +This is a classical simulation argument specialized to the project's actual +`RamStd` semantics, with an executable finite-program compiler and an independent +multitape interpreter. It is not a new RAM multiplication record. It transfers a +complete conditional multitape multiplication theorem, with all of its assumptions, +to a restricted logarithmic-word RAM. It does not discharge any missing theorem +in that antecedent or introduce unit-cost multiplication of arbitrary integers. +No Lean verification of this compiler is claimed. + +The target is `Mathproof/Meta/RamStd20261007.lean`: +SHA-256 `7c9263a14360b7fe485a753bda9c35c408b768612538d092f0dff217aa4f597e`. +Memory includes register cells, starts identically zero, and all written values +and memory addresses are reduced modulo 2^w. `sub` is natural truncated +subtraction. A program is a fixed finite list; labels/program counters are +natural numbers, not memory words. `read` at EOF and `halt` return `none`; +`write` appends one word. Every successful instruction costs one word operation. +The executable compiler uses exactly this subset: + + set load store add sub and jlt jzero jump read write halt + +It uses no multiply, divide, remainder, high product, wrapping subtraction, +randomness, hash table, unit-cost arbitrary-precision field element or oracle. +It even avoids shifts. The parent package separately considers packed tapes. + +## Theorem 1: uniform finite compiler, arbitrary tapes and both directions + +Fix positive integers k, A and Q. Let M be a deterministic k-tape machine with +alphabet {0,...,A-1}, blank 0, states {0,...,Q-1}, initial state 0, and a partial +transition table + + delta : (state, k read symbols) -> (next state, k write symbols, k moves), + +where each move is -1, 0 or +1. A missing transition means genuine halt without +changing the configuration. Tape cells are indexed by all integers. Initially +all heads are 0, tape i has a supplied finite word t_i at nonnegative positions, +and all other cells are blank. Choose an output tape o in {0,...,k-1}; the output +protocol requests positions 0,...,m-1 of that tape at halt. + +There is an explicitly computable fixed finite `RamStd.Program` P_M, independent +of the input lengths, time bound, actual execution and word length. Write +N = sum_i |t_i| and let T be the number of actual M transitions before halt. +Let R be the least power of two strictly larger than 8+3k, and set + + B = 2R + 4(k+1)(N + T + m + A + 2), + C = 100(k+1)(A^k + 1) + 20(k+1)^2. + +For every word length w with 2^w > B, P_M halts with exactly the m output +symbols in at most + + C(T+1) + 10(N+m+k+1) + +successful instructions. All accessed addresses are below B; at most B memory +words are used. More sharply, its live tape-address envelope is +R + 2k(N+T+m+2)+k and its register region has 8+3k words. For every nonhalting +run, every finite prefix that satisfies the same address bound is simulated +faithfully; the compiler does not introduce a spontaneous halt. + +Input ABI: the usual outer list-length header, followed by + + [m, |t_0|, t_0..., |t_1|, t_1..., ..., |t_(k-1)|, t_(k-1)...]. + +Each header and symbol fits under the displayed bound. The program consumes +exactly this valid prefix and never attempts an EOF read. An external caller may +omit the outer header with a fixed one-instruction prelude change. + +### Construction and proof + +Let pi(z)=2z for z>=0 and pi(z)=-2z-1 for z<0. This is a bijection Z -> N. +Store tape i cell z at the address + + addr(i,z) = R + i + k*pi(z). + +Different tape/cell pairs are disjoint: reduction modulo the positive integer k +recovers i, and then injectivity of pi recovers z. All such addresses are at +least R, whereas every register address is below R. Computing this address +requires setting R+i and adding the head-index register to it k times; k is a +fixed machine constant. There is no multiplication instruction. + +Store u_i=pi(head_i) in register 8+i; use the next k registers for addresses, +the next k for read symbols, and registers 0,...,7 for zero, one, two, one +scratch value, a counter, stride 2k, output length m, and parity. Zero and all +heads are initially available from the specified zero-initialized memory. + +The input loop places t_i[j] at R+i+2kj, using a stride register initialized to +2k. A guarded counter guarantees that each input symbol is consumed and stored +once. No clearing pass over untouched cells is necessary: the actual target +machine starts with zero memory, agreeing with blank 0. This is a stated +machine property, not uncharged initialization of arbitrary dirty scratch. + +At each state-labelled code block the compiler computes all k current addresses +and loads all k read symbols before writing any tape. It dispatches over the +finite alphabet tuples. Equality of x to a constant s is tested by setting a +scratch word to s and rejecting if x=2 | u+2 | u-2 | +| u odd, u=1 | 0 | 3 | +| u odd, u>=3 | u-2 | u+2 | + +They follow by substituting z in the definition of pi, separately for z>=0 +and z<0. All subtractions are guarded by positivity and therefore coincide +with natural `sub`; no unsigned underflow occurs. A stationary head changes +nothing. In particular neither negative head positions nor a crossing of zero +requires a supplied origin offset or a time horizon. + +The loop invariant at a state label q is: + +1. the label is precisely M's state q; +2. each head register equals pi of the corresponding signed TM head; +3. for every i and every z in the finite proof envelope |z| <= N+T+m+1, the RAM tape cell at addr(i,z) equals the TM tape symbol; +4. all symbols and live registers are below 2^w; register and tape cells are + disjoint, so temporary register changes do not alter any tape symbol. + +The address bound below ensures injectivity after modular reduction on this finite envelope. No claim of an injective embedding of all of Z into finite-word RAM is made. The input loops establish the invariant. The all-reads-before-writes discipline, +the dispatched literal table entry and the head formulas preserve it for one +complete macro step. Induction proves it for every finite transition prefix. +The missing-table branch occurs exactly when M has no successor. The output +loop reads the requested m positions with stride 2k, appends them in order, +and reaches a real `halt` instruction. This proves exact output and genuine +halting. A malformed ABI is outside the theorem; no correctness guarantee is +claimed for a missing header or invalid symbol code. + +At prefix time t<=T, every visited head satisfies |head|<=t. Initial occupied +coordinates are below N, and output coordinates are below m. Consequently all +needed addresses, including the loops' one-past-end pointers, are bounded by +the stated envelope. Each intermediate address is a monotone sum toward that +bound. Symbol values are =1 and a>=1, + + T(N) + m(N) + N + A + 2 <= a (N+2)^d. + +There is a fixed integer c depending only on M,a,d for which the compiler is +correct for every w >= c(floor(log2(N+2))+1), with the time bound of Theorem 1. + +Proof: put L=floor(log2(N+2))+1, so N+2<2^L and L>=1. Then +B <= [2R+4(k+1)a] 2^(dL). Choose an integer e with +2R+4(k+1)a < 2^e and let c=d+e+1. For w>=cL we have +2^w >= 2^((d+e+1)L) > [2R+4(k+1)a]2^(dL) >= B. +The program neither receives a, d, T nor a guessed horizon. They appear only +in the sufficient word-size contract. A finite set of exceptional small input +sizes can be handled by fixed lookup code, or absorbed by a larger constant a +when their halting times are finite. No online word widening/restart is needed. + +**Predicate warning.** The current unrestricted `RamStd.LogWordTime` definition +quantifies over all natural-number lists, including one-element lists containing +arbitrarily large values. Its separate per-entry fit requirement makes it the +wrong direct wrapper for arbitrary-value lists at logarithmic word length. +Use an explicit admissible binary/fixed-alphabet input predicate and the same +`RamStd.step` semantics, or prove a suitable encoded-input wrapper. Do not claim +that this theorem establishes that unrestricted definition for arbitrary lists. +The symbols, length headers and output words in the present ABI do satisfy the +word-fit contract. Input bit size is Theta(N+log(N+2)) for fixed nonempty tape +count and fixed-alphabet symbols under the usual at-least-one-bit-per-symbol +encoding, so replacing N by encoded bit size changes only constants. + +## Corollary 3: whole-solution transfer, preserving every conditional kappa + +Let H denote the explicitly retained analytic, native physical, exact recovery, +precision, scheduling, prime and uniformity premises of one pinned integer +multiplication theorem. Suppose H implies the existence of a single fixed +multitape machine multiplying two n-bit integers, emitting its usual nonnegative product as an MSB-first binary word of at most +2n digits at a known output-tape origin, followed by a blank or explicit +end marker, in + + O(n (log(n+2))^(1-kappa)) + +bit/tape steps, for 0= n, the O(n) overhead is absorbed. The compiler uses +no result of the multiplication it computes. It preserves the same kappa, +not a stronger one. + +### Explicit fixed-width LSB output posttransducer + +Define the new binary-word output ABI to be exactly 2n logical bits, least +significant first; its represented integer is sum_j b_j 2^j. The zero product +may have the usual one-digit representation `0` or an empty canonical +representation, provided the antecedent specifies which. Both are handled. +Assume the antecedent's conventional result prefix begins at position 0 of +its designated output tape. Its machine head at halt may be anywhere: the +RAM wrapper uses explicit simulated addresses and does not move that head. +Let the requested output width m=2n be retained in register M. Let a be an +address register, L a fresh/reused count register, S the constant stride 2k, +one the constant 1 register, z the constant 0 register, and x a scratch word. +The following finite labelled instruction sequence replaces the generic +output emitter; all operations are actual members of the displayed whitelist. + + set L 0 + set a (R+o) + scan: + jlt L M probe + jump reverse + probe: + load x a + jzero x reverse + add L L one + add a a S + jump scan + reverse: + jzero L pad + sub a a S + load x a + sub x x one + write x + sub L L one + sub M M one + jump reverse + pad: + jzero M halt + write z + sub M M one + jump pad + halt: + halt + +For an explicit nonzero end marker, put one additional constant equality test +before the three `probe` updates; its cost is constant per scanned symbol. +For the blank-terminated form displayed above the successful instruction count +is at most 14m+7. Scanning is bounded by m even when the actual result has m +bits and the terminating blank lies just beyond the scanned interval. + +At the beginning of `reverse`, L is exactly the number ell of payload bits, +0<=ell<=m, and a=R+o+2k*ell. Every preceding payload symbol is 1 or 2. Thus +`sub a a S` addresses the preceding valid cell while L>0, and `sub x x one` +decodes exactly the logical bit. The reverse loop emits the MSB word in reverse +order: the genuine LSB-first payload. It decrements M once for each bit emitted; +its value on entering `pad` is m-ell. The pad loop emits exactly that many +logical zero words at the high-order end of the LSB representation. Therefore +it preserves the represented integer and emits exactly 2n logical bits. +The registers used here can be the original emitter's no-longer-live counters +and scratch registers, or a fixed number of additional reserved cells. All +pointers stay within the same finite tape envelope. This gives a concrete +linear posttransducer even if unused cells after the first terminator are dirty: +they are not read. It does require the predecessor's actual output prefix/ +termination contract; an unspecified output encoding cannot be silently +interpreted. + +The wrapper above is implemented by `compile_tm(..., output_mode="fixed_lsb")`. +The default mode and its raw-symbol ABI are unchanged. Its separate replay +checks 9,762 emitter cases against ordinary represented-integer semantics, +including 1,364 product pairs, zero/one/two/three, empty and leading-zero payloads, +full-width payloads without an end blank inside the cap, dirty cells after an +earlier terminator, and a word-size boundary fixture. A corrupted reversal +direction in the actual emitted program rejects; the wrong MSB-append +normalization also fails the integer-value check. This emitter emits bounded +binary words, and no multiplication instruction is introduced by these tests. +The displayed loop invariant is still the all-input proof, distinct from its +finite corroboration. + +This is an implication from the complete fixed-machine theorem. A finite +native tableau replay, exact recurrence certificate or source-level pseudocode +alone is not such a theorem. For the selected and pending project claims, keep +all their existing conditional assumptions: this transfer does not magically +supply a missing finite-state implementation or validate their full analytic +argument. Uniform tables/setups that have already been paid as part of the +antecedent machine are simulated like every other step, not assumed free. + +The entire old tape machine can therefore serve as a correct reference backend +for a new RAM implementation. A future RAM-native rewrite can replace a tape +subroutine once it proves its input/output/refinement contract and includes its +word costs; it need not redesign the algebraic recurrence simultaneously. + +## Dependency disposition + +- Finite native operator identities, residual/precision estimates, mixed-child + inequalities, prime existence and exact recovery statements are mathematical + propositions; their truth does not depend on a tape or RAM execution model. +- Tape movement/routing/stock schedules are executable-cost premises. The + compiler transfers their actual tape execution unchanged at constant overhead. + It does not grant random access for free inside a tape-derived invoice. +- A RAM-native replacement may eliminate scans, routing, transpositions or + sequential descriptor work. Each such saving needs a new complete RAM invoice; + it cannot be credited by deleting old terms from the scalar recurrence. +- Arbitrary-height exact scalar RAM providers are distinct from bounded-word + bit RAM. Their coefficients and arithmetic must be bit-lowered or bounded + before they can replace a subroutine in this restricted compiler. + +## Finite verification + +Run `python3 -I -O -B tm_to_ramstd.py`. The checker constructs actual finite +programs, interprets individual target instructions, and compares state, signed +heads and every relevant tape cell with a separately written signed-coordinate +TM interpreter at each macro boundary. Random cases include k=1,2,3, three +symbols, three states, partial transition tables, arbitrary source contents and +stationary/negative/positive moves. Directed tests cover both zero crossings, +long one-sided walks, empty-transition immediate halting, and multiple word +lengths. A too-small word contract rejects. Nonhalting finite prefixes are +checked without labelling them as halting computations. Tests do not establish +the universal theorem; the written invariant argument does. + +## Open next questions + +1. Prove the compiler invariant and finite-table code generation in Lean against + actual `RamStd.step`, using admissible-input predicates rather than the + unrestricted logarithmic word wrapper. First milestone: one transition with + all k reads saved before the writes and modular-address non-aliasing. +2. Replace the one-cell-per-word representation with the parent packed-tape + theorem; compare actual memory words and IO contracts, retaining this simple + backend as an independent semantic reference. +3. Select one fully costed native project subroutine and implement its random + access RAM version. First compare descriptor generation, precision and data + motion in a complete invoice; only then optimize the global recurrence. + diff --git a/research/word-ram-transfer/compiler/tm_to_ramstd.py b/research/word-ram-transfer/compiler/tm_to_ramstd.py new file mode 100644 index 0000000000..690e550d27 --- /dev/null +++ b/research/word-ram-transfer/compiler/tm_to_ramstd.py @@ -0,0 +1,323 @@ +"""Executable finite TM to RamStd-subset compiler; no multiplication primitive. + +Apache-2.0. Prepared by Dugongue with substantial OpenAI Codex assistance. +Finite tests corroborate the separate universal proof; this is not Lean verification. +""" +from itertools import product +import json +import random + +OPS = frozenset(('set','load','store','add','sub','and','jlt','jzero','jump','read','write','halt')) + +class Assembler: + def __init__(self): + self.code = [] + self.labels = {} + def mark(self, label): + if label in self.labels: + raise ValueError('duplicate label') + self.labels[label] = len(self.code) + def emit(self, op, *args): + if op not in OPS: + raise ValueError('forbidden opcode') + self.code.append((op,) + args) + +def compile_tm(k, alphabet, states, delta, output_tape=0, output_mode="raw"): + """Transition (q, read tuple) -> (q', write tuple, moves tuple), else halt. + + Input x (before house-standard list-length prefix) is + [m,n_0,tape_0...,n_1,tape_1...,...]. All heads initially 0. + Default output is the m raw symbols at positions 0,...,m-1. + fixed_lsb decodes the MSB prefix of bit codes 1,2 before blank 0, + reverses it and pads to exactly m logical bits (prefix length <= m). + Symbol 0 is blank. A missing transition halts genuinely. + """ + if output_mode not in ('raw','fixed_lsb'): + raise ValueError('unknown output mode') + if output_mode=='fixed_lsb' and alphabet<3: + raise ValueError('fixed_lsb requires blank 0 and bit codes 1,2') + if k < 1 or alphabet < 1 or states < 1 or not 0 <= output_tape < k: + raise ValueError('invalid finite machine shape') + for (q,read), (nq,write,moves) in delta.items(): + if not (0<=q=0, and -2z-1 for z<0. + # A crossing of zero is the only exceptional case. + end=('moveend',q,serial,i) + special=('special',q,serial,i) + a.emit('and',PARITY,HEAD[i],ONE) + a.emit('jzero',PARITY,('even',q,serial,i)) + # Odd u: right subtracts 2 except u=1 -> 0; left adds 2. + if d==1: + a.emit('jlt',HEAD[i],TWO,special) + a.emit('sub',HEAD[i],HEAD[i],TWO); a.emit('jump',end) + a.mark(special); a.emit('set',HEAD[i],0) + else: a.emit('add',HEAD[i],HEAD[i],TWO) + a.emit('jump',end) + a.mark(('even',q,serial,i)) + if d==1: a.emit('add',HEAD[i],HEAD[i],TWO) + else: + a.emit('jzero',HEAD[i],('zero',q,serial,i)) + a.emit('sub',HEAD[i],HEAD[i],TWO); a.emit('jump',end) + a.mark(('zero',q,serial,i)); a.emit('set',HEAD[i],1) + a.mark(end) + a.emit('jump',('state',nq)) + a.mark(skip) + # Alphabet validity invariant makes this defensive path unreachable. + a.emit('jump','output') + a.mark('output'); a.emit('set',ADDRESS[0],BASE+output_tape) + if output_mode=='raw': + a.mark('outloop'); a.emit('jzero',M,'halt') + a.emit('load',TMP,ADDRESS[0]); a.emit('write',TMP) + a.emit('add',ADDRESS[0],ADDRESS[0],STRIDE) + a.emit('sub',M,M,ONE); a.emit('jump','outloop') + else: + # Fixed-width LSB output from the usual blank-terminated MSB bit prefix. + # COUNT is no longer live after input initialization; M is remaining width. + a.emit('set',COUNT,0) + a.mark('scan'); a.emit('jlt',COUNT,M,'probe'); a.emit('jump','reverse') + a.mark('probe'); a.emit('load',TMP,ADDRESS[0]); a.emit('jzero',TMP,'reverse') + a.emit('add',COUNT,COUNT,ONE); a.emit('add',ADDRESS[0],ADDRESS[0],STRIDE) + a.emit('jump','scan') + a.mark('reverse'); a.emit('jzero',COUNT,'pad') + a.emit('sub',ADDRESS[0],ADDRESS[0],STRIDE); a.emit('load',TMP,ADDRESS[0]) + a.emit('sub',TMP,TMP,ONE); a.emit('write',TMP) + a.emit('sub',COUNT,COUNT,ONE); a.emit('sub',M,M,ONE); a.emit('jump','reverse') + a.mark('pad'); a.emit('jzero',M,'halt'); a.emit('write',ZERO) + a.emit('sub',M,M,ONE); a.emit('jump','pad') + a.mark('halt'); a.emit('halt') + # labels may be tuples as well as strings. + code=[] + for ins in a.code: + code.append((ins[0],)+tuple(a.labels[v] if isinstance(v,(str,tuple)) and v in a.labels else v for v in ins[1:])) + return code,dict(base=BASE,head=HEAD,states={a.labels[('state',q)]:q for q in range(states)},labels=a.labels) + +class VM: + def __init__(self,w,code,inp): + self.mod=1<=0 else -2*z-1 + +def reference_step(q,heads,tapes,delta): + read=tuple(tapes[i].get(h,0) for i,h in enumerate(heads)) + t=delta.get((q,read)) + if t is None: return None + nq,writes,moves=t + for i,h in enumerate(heads): tapes[i][h]=writes[i] + return nq,[h+d for h,d in zip(heads,moves)] + +def check_case(k,A,Q,delta,tapes,m,width=16,max_macro=40): + code,meta=compile_tm(k,A,Q,delta) + if (1<bound: raise AssertionError('advertised instruction envelope failed') + if any(i[0] not in OPS for i in code): raise AssertionError('forbidden primitive') + return dict(macros=macros,steps=v.steps,halted=halted,program_instructions=len(code)) + +def check_lsb_emitters(): + rng=random.Random(2235); cases=0; product_cases=0; total_steps=0 + fixtures=[] + for m in range(13): + for bits in product((0,1),repeat=m): + fixtures.append((m,list(bits))) + for n in range(1,6): + for left in range(1<>j)&1 for j in range(m)] + if vm.out!=expected: raise AssertionError('LSB emitter numeric mismatch') + if before is None or vm.steps-before>14*m+7: + raise AssertionError('LSB emitter cost envelope failed') + if max(vm.mem,default=0)>meta['base']+2*k*(sum(map(len,tapes))+m+2)+k: + raise AssertionError('LSB emitter finite memory envelope failed') + if any(ins[0] not in OPS for ins in code): raise AssertionError('LSB forbidden opcode') + cases+=1; total_steps+=vm.steps + # Wrongly appending blanks/zeros to MSB "11" at width 4 represents 12, + # whereas the specified LSB normalization must represent the original 3. + wrong_msb_append=int('1100',2) + if wrong_msb_append==3: raise AssertionError('MSB append negative control invalid') + # Actually corrupt the reversal direction; independent numeric semantics rejects. + code,meta=compile_tm(1,3,1,{},output_mode='fixed_lsb') + code=[('add',*ins[1:]) if ins[0]=='sub' and ins[1]==9 else ins for ins in code] + x=[4,5,2,2,0,1,2] + broken=VM(12,code,[len(x),*x]) + while broken.steps<10000 and broken.step(): pass + if broken.out==[1,1,0,0]: raise AssertionError('Wrong-direction emitted-code mutation escaped') + return dict(cases=cases,product_pairs=product_cases,microinstructions=total_steps, + wrong_direction_code_rejected=True,small_word_boundary_tested=True, + wrong_msb_append_detected=True,full_width_no_terminator_tested=True, + dirty_post_terminator_tested=True,leading_zero_tested=True) + +def run_checks(): + rng=random.Random(20261022); results=[] + for k in (1,2,3): + for case in range(80): + A=3; Q=3; delta={} + for q in range(Q): + for read in product(range(A),repeat=k): + if rng.randrange(8)==0: continue + delta[q,read]=(rng.randrange(Q),tuple(rng.randrange(A) for _ in range(k)),tuple(rng.choice((-1,0,1)) for _ in range(k))) + tapes=[[rng.randrange(A) for _ in range(rng.randrange(9))] for _ in range(k)] + results.append(check_case(k,A,Q,delta,tapes,rng.randrange(10))) + # Sweep both zero crossings and long negative/positive prefixes deliberately. + for d in (-1,1): + delta={(0,(s,)):(0,(s,),(d,)) for s in range(3)} + results.append(check_case(1,3,1,delta,[[1,2,1]],5,max_macro=200)) + # The generic theorem is valid at every larger word length, not only its minimum. + for w in (12,16,31,64): + results.append(check_case(1,3,1,{},[[1,2]],4,width=w)) + rejected=0 + try: check_case(1,3,1,{},[[1,2]],4,width=3) + except ValueError: rejected+=1 + if rejected!=1: raise AssertionError('small-word negative control accepted') + # Actual emitted-code faults must be caught by the independent semantic check. + global compile_tm + good_compiler=compile_tm + faults=('stride','head_unit','store','halt','output') + caught=[] + for fault in faults: + def faulty(*args, _fault=fault, **kwargs): + code,meta=good_compiler(*args,**kwargs) + if _fault=='stride': + at=next(i for i,x in enumerate(code) if x[0]=='set' and x[1]==5) + code[at]=('set',5,1) + elif _fault=='head_unit': + code[1]=('set',2,1) + elif _fault=='store': + code=[('load',*x[1:]) if x[0]=='store' else x for x in code] + elif _fault=='halt': + code[-1]=('jump',next(iter(meta['states']))) + elif _fault=='output': + code=[('write',0) if x[0]=='write' else x for x in code] + return code,meta + compile_tm=faulty + try: + delta={(0,(s,)):(1,(1,),(1,)) for s in range(3)} + check_case(1,3,2,delta,[[2,2,2]],3) + except AssertionError: + caught.append(fault) + finally: + compile_tm=good_compiler + if caught!=list(faults): raise AssertionError('emitted-code negative control escaped') + lsb=check_lsb_emitters() + out=dict(lsb_emitter=lsb,schema='tm-to-ramstd-finite-check-v1',cases=len(results),macro_boundaries=sum(r['macros']+1 for r in results),microinstructions=sum(r['steps'] for r in results),halting_cases=sum(r['halted'] for r in results),nonhalting_prefix_cases=sum(not r['halted'] for r in results),small_word_rejections=rejected,emitted_code_faults_rejected=caught,uses_multiplication_or_division=False,formal_lean_verification=False) + print(json.dumps(out,indent=2,sort_keys=True)) + return out + +if __name__=='__main__': run_checks() + diff --git a/research/word-ram-transfer/cost/COST-RESULT.json b/research/word-ram-transfer/cost/COST-RESULT.json new file mode 100644 index 0000000000..704ed896b0 --- /dev/null +++ b/research/word-ram-transfer/cost/COST-RESULT.json @@ -0,0 +1,35 @@ +{ + "streaming_affine": { + "status": "PASS", + "program_macro_instructions": 30, + "permutation_cases": 5554, + "negative_controls": { + "singular_rejections": 355, + "address_or_column_rejections": 3 + }, + "max_observed_bound_ratio": 0.9184540001394992, + "scope": "exact portable finite replay, not kernel proof or new kappa" + }, + "quadratic_phase": { + "status": "PASS", + "phase_cases": 17073, + "modular_negation_cases": 4226, + "scope": "exact portable finite replay, not kernel proof or new kappa" + }, + "monomial_metadata": { + "status": "PASS", + "gate_words": 11015, + "basis_state_comparisons": 122956, + "rejected_nonmonomial_gate": true, + "retained_global_phase": true, + "scope": "exact portable finite replay, not kernel proof or new kappa" + }, + "evidence": "Isolated optimized Python finite exact replays; informal universal proofs; no Lean kernel check; no new kappa.", + "file_hashes": { + "COST-THEOREMS.md": "79eef859eb2ae32a66879f294d626c3947bcfe55434b4a38a296d271b3aa9675", + "monomial_metadata.py": "a539a148a58e5b9850b6d52cc2467ced32eac3b99a3bfd8a0344a224d3dc88db", + "quadratic_phase.py": "bdc0bcc5a8c96cd9f09d6985d7c9ac2870a2c2ed11fcbe347011d1374d32f882", + "SOURCE-HASHES.json": "7787b4b28b3650dc14149b71e1427502410b8df24f7152d853a014ee599efb05", + "streaming_affine.py": "89b668be21b9ee67b46b5448a7d2c4de372521ead8112f42d1217811702d2b79" + } +} diff --git a/research/word-ram-transfer/cost/COST-THEOREMS.md b/research/word-ram-transfer/cost/COST-THEOREMS.md new file mode 100644 index 0000000000..a5d940b205 --- /dev/null +++ b/research/word-ram-transfer/cost/COST-THEOREMS.md @@ -0,0 +1,259 @@ +# Streaming Word RAM costs for the native layout layer + +These are constructive sufficient results for a Word RAM port. They establish +primitive semantics and costs. They do not establish a new multiplication bound, +a new κ, or a complete port of the analytic/recursion/compiler chain. + +## Model and representation + +The baseline instruction set has bounded-word ADD, truncated SUB, AND, NOT, +left shift, indirect LOAD/STORE, conditional/unconditional jumps, and literals. +Words and addresses have w bits, with w >= 6 so the fixed program and registers fit. Multiplication and division of words are not +used by the constructions below. They remain legitimate optional instructions +in the richer `Lax13.Ram` model; an n-bit input-sized unit multiplication is not +being introduced. XOR and MOV are macros taking at most 4 and 2 instructions +respectively in that existing model. JNZ expands to at most 2 instructions. + +A record consists of L >= 1 arbitrary words, stored at stride K = 2^s, where +L <= K < 2L. Let N = 2^r and r <= w. The two record buffers, the column tables, +and a constant register/scratch region are disjoint and lie strictly below +2^w. This is stronger than r <= w; in particular r = w cannot fit these two buffers. No address calculation wraps. Initial values outside the +written payload cells are arbitrary. The source is preserved. + +The supplied affine map has columns c_0,...,c_(r-1) in F_2^r, assumed linearly +independent, and offset b in F_2^r. Preparing/checking supplied metadata is a +separate caller action, not an uncharged gate-list compiler. Invertibility can +be checked by ordinary word-packed elimination in O(r^2) word operations. +A straightforward gate-word metadata compiler may instead cost O(m r^2) for m +gates; no bound on that cost is hidden in the streaming theorem. + +## Theorem 1: affine permutation with a linear word count + +There is one fixed program that, from the above data, writes + + destination[(A x XOR b)*K + j] = source[x*K+j] + +for every 0 <= x < N and 0 <= j < L, preserves every source/table cell and every +untouched destination padding cell, and uses at most + + 8 N L + 40 N + 8 + +expanded instructions. This count starts from preloaded buffers and parameters; +input deserialization and final output serialization are caller costs. + +Proof. Start with x = 0 and y = b. Copy the L-word payload to destination record +y. To advance x, visit exactly the bit positions flipped by binary increment, +XORing c_j into y for every flipped bit j. Thus the invariant y = A x XOR b +holds initially and after every increment, by linearity over F_2. Invertibility +makes the N destination indices distinct, so every destination payload is +written exactly once. The buffers are disjoint, so no source read is invalidated. +No instruction writes a source, table, or padding address. + +For each bit j, binary increment between 0 and N-1 flips that bit exactly +N/2^j - 1 times. The total number of flips is therefore + + T = sum_(j=0)^(r-1) (N/2^j - 1) = 2N - r - 2, + +including r = 0, when T = 0. The displayed fixed program has 30 macro +instructions, with loops but no instruction depending on r, L, or the input +values. Its charged expansion count is + + 8 N L + 9 N + 11 T + 3 + = 8 N L + 31 N - 11 r - 19 + <= 8 N L + 40 N + 8. + +The r = 0 case costs 8L + 12 and satisfies the same formulas. Destination base +addresses use y << s; multiplication is unnecessary. All masks, counters, +indices, payload values, and effective addresses fit in a word by the stated +bounds. This proves both semantics and the instruction bound. ∎ + +`streaming_affine.py` is an executable fixed-program model. Its macro costs are +upper bounds on `Lax13.Ram` expansions, rather than a claim that Python runtime +measures Word RAM time. The model is not itself a Lean proof or a complete +emitted `Lax13.Ram.Program`; resolving macro labels in such a compiler remains +an integration task. + +## Theorem 2: all quadratic Gaussian phases in linear streaming time + +Let a_j be in Z/4, and let B be a symmetric binary r-by-r matrix with zero +diagonal. Define + + q(x) = sum_j a_j x_j + 2 sum_(j= 3. There are T < 2N bit flips by Theorem 1, and the +metadata initialization takes O(r) instructions. The phase and gradient +invariants therefore prove the result. ∎ + +## Theorem 3: exact monomial Clifford action on limb records + +Let each coefficient be a pair of integers (u_x,v_x), represented modulo +2^(kL) by L little-endian limbs of k bits, where 1 <= k <= w-2. For invertible +A, offset b, and q as above, the map + + (u+iv)_x -> i^q(x) (u+iv)_x at index A x XOR b + +can be evaluated by a uniform additive/Boolean Word RAM in O(NL + N + r) +operations, preserving the source, using two disjoint padded output buffers +and O(r) metadata words. All real/imaginary source and destination buffers and scratch cells must fit together below 2^w. This statement uses precomputed A,b,a,B metadata. + +Proof. Theorems 1 and 2 maintain the destination index and phase in constant +amortized work per coefficient. Multiplication by i^q uses only a swap of the +real/imaginary destinations and zero, one, or two integer negations: + + q=0: (u,v); q=1: (-v,u); q=2: (-u,-v); q=3: (v,-u). + +To negate an L-limb residue, complement each digit within base beta = 2^k and +add a carry initially equal to 1. At digit a, form beta-1-a+carry; store its +residue modulo beta and set the carry to 1 exactly when this value is beta. +Every temporary is at most beta, hence fits in a word; each digit takes +constant-many instructions. The standard radix identity proves this is +negation modulo beta^L. Copying, swapping destinations, and up to two such +negations take O(L) instructions per coefficient. The disjoint-buffer argument +from Theorem 1 proves the frame property. ∎ + +The residue width here is exactly kL bits: no unmasked partial top limb is permitted. If a caller starts with B bits not divisible by k, it must pad to kL and establish the signed interpretation at that full width, or supply a separately proved top-mask operation. + +If the intended coefficients are signed integers strictly between +-2^(kL-1) and 2^(kL-1), interpret the residues by signed decoding. Negation and +Gaussian-unit phases then agree with ordinary integer arithmetic, provided the +endpoint excluded above does not occur. In fact, an absolute-value headroom +bound is invariant under these phases. This does not justify arbitrary +finite-precision rounding or multiplication by roots other than Gaussian units. + +## Theorem 4: uniform metadata compiler, with global phase retained + +For a word of m gates from X_j, S_j, Z_j, CNOT_(j,k), SWAP_(j,k), and CZ_(j,k), +there is an exact uniform metadata constructor using O((m+1)(r+1)^2) Word RAM +operations and O(r) words of live metadata. It returns A,b,c,a,B such that + + literal_word |x> = i^(c+q(x)) |A x XOR b>. + +The exponent c is retained modulo 4, including global phase; it is not discarded +as physically irrelevant. The combined metadata compiler and streaming evaluator +therefore costs O((m+1)(r+1)^2 + NL). This is a fully specified sufficient +construction for monomial segments, not an assumed metadata oracle. + +Proof. Initially A is identity, b=0, c=0, a=0, and B=0. Maintain the stated +identity after every appended gate. X_j toggles bit j of b. CNOT_(j,k) toggles +bit k in every affine column whose bit j is set, and does the same to b. SWAP +swaps those bits in every column and in b. These update the output affine map +without changing the phase polynomial. + +For phase gates, write output coordinate j as b_j XOR u dot x, with u the +j-th row of A. Its value modulo 4 is + + b_j + (1-2*b_j) sum_l u_l*x_l + + 2 sum_(l>j)&1 for v in A] + def toggle_edge(j,k): + B[j]^=1<>j)&1 + c=(c+bj)&3 + for l in range(r): a[l]=(a[l]+(1-2*bj)*u[l])&3 + for l in range(r): + for k in range(l+1,r): + if u[l]&u[k]: toggle_edge(l,k) + elif op=='Z': + u=row(j) + c=(c+2*((b>>j)&1))&3 + for l in range(r): a[l]=(a[l]+2*u[l])&3 + elif op in ('CNOT','SWAP','CZ'): + if len(rest)!=1 or not (0<=rest[0]>j)&1)<>j)&1)<>j)^(v>>k))&1 + return v^(d<>j)&1,(b>>k)&1 + c=(c+2*(bj&bk))&3 + for l in range(r): + lin=(bj&v[l])^(bk&u[l])^(u[l]&v[l]) + a[l]=(a[l]+2*lin)&3 + for l in range(r): + for t in range(l+1,r): + if (u[l]&v[t])^(u[t]&v[l]): toggle_edge(l,t) + else: raise ValueError('nonmonomial or unknown gate: '+op) + return dict(columns=A,bias=b,constant=c,linear=a,quadratic=B) + + +def evaluate(m,x): + r=len(m['columns']) + y=m['bias'] + q=m['constant'] + for j in range(r): + if (x>>j)&1: + y^=m['columns'][j] + q+=m['linear'][j] + for k in range(j+1,r): q+=2*((m['quadratic'][j]>>k)&1)*((x>>k)&1) + return y,q&3 + + +def literal(gates,x): + q=0 + for gate in gates: + op,j,*rest=gate + if op=='X': x^=1<>j)&1 + elif op=='Z': q+=2*((x>>j)&1) + elif op=='CZ': q+=2*((x>>j)&1)*((x>>rest[0])&1) + elif op=='CNOT': x^=((x>>j)&1)<>j)^(x>>k))&1 + x^=(d<> j & 1)) + for j in range(r): + for k in range(j + 1, r): + z += 2 * (cols[j] >> k & 1) * (x >> j & 1) * (x >> k & 1) + return z & 3 + +def stream(a, cols): + r = len(a) + if not len(cols) == r: + raise AssertionError('exact check failed') + if not all((0 <= c < 1 << r for c in cols)): + raise AssertionError('exact check failed') + if not all((not cols[j] >> j & 1 for j in range(r))): + raise AssertionError('exact check failed') + if not all((cols[j] >> k & 1 == cols[k] >> j & 1 for j in range(r) for k in range(r))): + raise AssertionError('exact check failed') + q, gradient, x = (0, 0, 0) + result, flips = ([], 0) + for target in range(1 << r): + if not target == x: + raise AssertionError('exact check failed') + result.append(q) + if target + 1 == 1 << r: + break + j, mask = (0, 1) + while True: + old = bool(x & mask) + delta = a[j] + (2 if gradient & mask else 0) & 3 + q = (q + 4 - delta if old else q + delta) & 3 + gradient ^= cols[j] + flips += 1 + if not old: + break + j += 1 + mask <<= 1 + x += 1 + if not flips == 2 * (1 << r) - r - 2: + raise AssertionError('exact check failed') + return result + +def columns_from_edges(r, edge_bits): + cols = [0] * r + for bit, (j, k) in enumerate(itertools.combinations(range(r), 2)): + if edge_bits >> bit & 1: + cols[j] |= 1 << k + cols[k] |= 1 << j + return cols + +def negate_limbs(words, k): + beta = 1 << k + carry = 1 + out = [] + for a in words: + z = beta - 1 - a + carry + carry = int(z == beta) + out.append(z - beta if carry else z) + return out + +def value(words, k): + return sum((a << j * k for j, a in enumerate(words))) + +def verify(): + phase_cases = 0 + for r in range(5): + for a in itertools.product(range(4), repeat=r): + for e in range(1 << r * (r - 1) // 2): + cols = columns_from_edges(r, e) + if not stream(a, cols) == [quadratic(a, cols, x) for x in range(1 << r)]: + raise AssertionError('exact check failed') + phase_cases += 1 + rng = random.Random(20261022) + for r in range(5, 12): + for _ in range(20): + a = [rng.randrange(4) for j in range(r)] + cols = columns_from_edges(r, rng.getrandbits(r * (r - 1) // 2)) + if not stream(a, cols) == [quadratic(a, cols, x) for x in range(1 << r)]: + raise AssertionError('exact check failed') + phase_cases += 1 + neg_cases = 0 + for k in range(1, 5): + for L in range(1, 5): + limit = 1 << k * L + xs = range(limit) if limit <= 1024 else [rng.randrange(limit) for _ in range(1000)] + for x in xs: + words = [x >> k * j & (1 << k) - 1 for j in range(L)] + got = negate_limbs(words, k) + if not all((0 <= z < 1 << k for z in got)): + raise AssertionError('exact check failed') + if not value(got, k) == -x % limit: + raise AssertionError('exact check failed') + neg_cases += 1 + return dict(status='PASS', phase_cases=phase_cases, modular_negation_cases=neg_cases, scope='exact portable finite replay, not kernel proof or new kappa') +if __name__ == '__main__': + print(json.dumps(verify(), indent=2)) diff --git a/research/word-ram-transfer/cost/streaming_affine.py b/research/word-ram-transfer/cost/streaming_affine.py new file mode 100644 index 0000000000..3b0bd0cd54 --- /dev/null +++ b/research/word-ram-transfer/cost/streaming_affine.py @@ -0,0 +1,190 @@ +"""Portable exact model for the streaming affine-layout Word RAM lemma. +The interpreter is evidence about the displayed fixed program; the universal +invariant proof is in COST-THEOREMS.md. This is not a Lean certificate. +""" +from collections import Counter +import itertools +import json +import random +from pathlib import Path +COST = {'mov': 2, 'xor': 4, 'jnz': 2} + +def program(): + code, labels = ([], {}) + + def label(s): + labels[s] = len(code) + + def emit(*s): + code.append(s) + emit('set', 'x', 0) + emit('mov', 'y', 'bias') + emit('mov', 'sp', 'src') + label('outer') + emit('shl', 'dp', 'y', 's') + emit('add', 'dp', 'dp', 'dst') + emit('set', 'j', 0) + label('copy') + emit('add', 'tmp', 'sp', 'j') + emit('load', 'v', 'tmp') + emit('add', 'tmp', 'dp', 'j') + emit('store', 'tmp', 'v') + emit('add', 'j', 'j', 'one') + emit('sub', 'tmp', 'L', 'j') + emit('jnz', 'tmp', 'copy') + emit('add', 'xn', 'x', 'one') + emit('sub', 'tmp', 'N', 'xn') + emit('jzero', 'tmp', 'end') + emit('set', 'k', 0) + emit('set', 'mask', 1) + label('toggle') + emit('add', 'tmp', 'columns', 'k') + emit('load', 'col', 'tmp') + emit('xor', 'y', 'y', 'col') + emit('and', 'bit', 'x', 'mask') + emit('jzero', 'bit', 'last') + emit('shl', 'mask', 'mask', 'one') + emit('add', 'k', 'k', 'one') + emit('jump', 'toggle') + label('last') + emit('mov', 'x', 'xn') + emit('add', 'sp', 'sp', 'K') + emit('jump', 'outer') + label('end') + emit('halt') + return [(i[0], *(labels.get(v, v) if i[0] in ('jump', 'jzero', 'jnz') and j == len(i) - 2 else v for j, v in enumerate(i[1:]))) for i in code] +CODE = program() + +def run(w, registers, memory): + mask = (1 << w) - 1 + regs = dict(registers) + mem = dict(memory) + pc, ops, counts = (0, 0, Counter()) + while True: + ins = CODE[pc] + op, a = ins[:2] if len(ins) > 1 else (ins[0], None) + counts[op] += 1 + ops += COST.get(op, 1) + pc += 1 + if op == 'halt': + break + if op == 'jump': + pc = a + continue + if op in ('jzero', 'jnz'): + if (regs[a] == 0) == (op == 'jzero'): + pc = ins[2] + continue + if op == 'store': + mem[regs[a] & mask] = regs[ins[2]] + continue + if op == 'set': + value = ins[2] + elif op == 'mov': + value = regs[ins[2]] + elif op == 'load': + value = mem.get(regs[ins[2]] & mask, 0) + else: + b, c = (regs[ins[2]], regs[ins[3]]) + if op == 'add': + value = b + c + elif op == 'sub': + value = max(0, b - c) + elif op == 'and': + value = b & c + elif op == 'xor': + value = b ^ c + elif op == 'shl': + value = 0 if c >= w else b << c + else: + raise ValueError(op) + regs[a] = value & mask + return (mem, ops, counts) + +def linear(columns, x): + result = 0 + for j, column in enumerate(columns): + if x & 1 << j: + result ^= column + return result + +def independent(columns): + return len({linear(columns, x) for x in range(1 << len(columns))}) == 1 << len(columns) + +def instance(columns, bias, L, w=16): + r, N = (len(columns), 1 << len(columns)) + if not all(0 <= c < N for c in columns): + raise ValueError('column outside F2^r') + if not independent(columns): + raise ValueError('Singular matrix is not a permutation') + if not (0 <= bias < N and L >= 1): + raise ValueError('bad parameters') + s = (L - 1).bit_length() + K = 1 << s + src, dst, table = (64, 64 + N * K, 64 + 2 * N * K) + if table + r + 32 >= 1 << w: + raise ValueError('address space insufficient') + words = {src + x * K + j: ((x + 1) * 257 + j * 13) % (1 << w) for x in range(N) for j in range(L)} + words.update({table + j: c for j, c in enumerate(columns)}) + for x in range(N): + for j in range(L, K): + words[dst + x * K + j] = (1 << w) - 1 + reg = dict(N=N, L=L, K=K, s=s, src=src, dst=dst, columns=table, bias=bias, one=1) + result, ops, counts = run(w, reg, words) + for x in range(N): + y = linear(columns, x) ^ bias + for j in range(L): + if not result[dst + y * K + j] == words[src + x * K + j]: + raise AssertionError('exact check failed') + if not all((result[a] == v for a, v in words.items())): + raise AssertionError('exact check failed') + toggles = 2 * N - r - 2 if r else 0 + if not counts['xor'] == toggles: + raise AssertionError('exact check failed') + if not counts['store'] == N * L: + raise AssertionError('exact check failed') + if not ops <= 8 * N * L + 40 * N + 8: + raise AssertionError('exact check failed') + return dict(r=r, records=N, limbs=L, expanded_cost=ops, bound=8 * N * L + 40 * N + 8, toggles=toggles) + +def verify(): + tests, max_ratio = (0, 0) + checks = Counter() + for r in range(4): + N = 1 << r + for columns in itertools.product(range(N), repeat=r): + if not independent(columns): + checks['singular_rejections'] += 1 + try: + instance(columns, 0, 1) + except ValueError: + pass + else: + raise AssertionError('singular accepted') + continue + for bias in range(N): + for L in (1, 2, 3, 5): + z = instance(columns, bias, L) + tests += 1 + max_ratio = max(max_ratio, z['expanded_cost'] / z['bound']) + rng = random.Random(20261022) + for r in range(4, 11): + for _ in range(10): + columns = [1 << j for j in range(r)] + for _ in range(5 * r): + a, b = rng.sample(range(r), 2) + columns[a] ^= columns[b] + z = instance(columns, rng.randrange(1 << r), rng.choice((1, 3, 7, 9))) + tests += 1 + max_ratio = max(max_ratio, z['expanded_cost'] / z['bound']) + for columns,bias,L,w in (([1],0,1,1), ([1,2],0,1,2), ([1<<8],0,1,16)): + try: + instance(columns,bias,L,w) + except ValueError: + checks['address_or_column_rejections'] += 1 + else: + raise AssertionError('invalid instance accepted') + report = dict(status='PASS', program_macro_instructions=len(CODE), permutation_cases=tests, negative_controls=dict(checks), max_observed_bound_ratio=max_ratio, scope='exact portable finite replay, not kernel proof or new kappa') + return report +if __name__ == '__main__': + print(json.dumps(verify(), indent=2)) diff --git a/research/word-ram-transfer/machine/AUDIT.json b/research/word-ram-transfer/machine/AUDIT.json new file mode 100644 index 0000000000..1a4698fb92 --- /dev/null +++ b/research/word-ram-transfer/machine/AUDIT.json @@ -0,0 +1,17 @@ +{ + "source_sha256": "e1849b658e0278181b41beb3572af26bceb035fa5c02c260993e9f34f21361c3", + "audit_source_sha256": "817f5735a3d814f7f69a61919a0413776062ecc66f471903f8b9b4290f11216c", + "source_unchanged": true, + "exit_code": 0, + "timed_out": false, + "seconds": 19.875, + "lean_version": "4.33.0", + "maximum_concurrent_audit_processes": 1, + "theorems": [ + "computesIn_on", + "computesInOn_mono", + "computesInOn_ofLax13", + "polynomial_fitsWords", + "compiled_polynomial_run" + ] +} diff --git a/research/word-ram-transfer/machine/DEPENDENCIES.json b/research/word-ram-transfer/machine/DEPENDENCIES.json new file mode 100644 index 0000000000..7b896c202c --- /dev/null +++ b/research/word-ram-transfer/machine/DEPENDENCIES.json @@ -0,0 +1,113 @@ +{ + "role": "Frozen publication dependency snapshot, not an active module tree and not DAG-indexed.", + "toolchain": "leanprover/lean4:v4.33.0", + "mathlib_manifest_entry": [ + { + "url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "db584cd6d46c92f209a44c0f1c829460d327499d", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0", + "inherited": false, + "configFile": "lakefile.lean" + } + ], + "files": [ + { + "relative_path": "Mathproof/Meta/Problem18RAMLax13ProofsSimulation20261001.lean", + "sha256": "2db5af757e7808c62ac1b578a26e198532c24b17388a06719c127f08de23811c", + "bytes": 51699, + "imports": [ + "Mathproof.Meta.Problem18RAMLax13ProofsCompile20261001", + "Mathproof.Meta.Problem18RAMLax13ProofsMachine20261001" + ] + }, + { + "relative_path": "Mathproof/Meta/Problem18RAMLax13ProofsMachine20261001.lean", + "sha256": "82bbeff85aebddd2740f28476f3b602a8593358bd509ac9a75944610f06fb3e8", + "bytes": 17767, + "imports": [ + "Mathproof.Meta.Problem18RAMLax13Ram20261001", + "Mathlib.Tactic" + ] + }, + { + "relative_path": "Mathproof/Meta/Problem18RAMLax13Ram20261001.lean", + "sha256": "b95844098a3c402ec895c542d07a4b60354455cf66fe77bad1050d15583ec948", + "bytes": 13687, + "imports": [ + "Mathlib.Data.List.Basic" + ] + }, + { + "relative_path": "Mathproof/Meta/Problem18RAMLax13ProofsCompile20261001.lean", + "sha256": "bc2237188b9b7c6f4d5524bad17d353bab873ab693ddb2e947574739dc2aae2c", + "bytes": 22016, + "imports": [ + "Mathproof.Meta.Problem18RAMLax13Ram20261001", + "Mathproof.Meta.Problem18RAMLax13ProofsBounds20261001" + ] + }, + { + "relative_path": "Mathproof/Meta/Problem18RAMLax13ProofsBounds20261001.lean", + "sha256": "16ca19d477c17805abecb3ca265e4b2b7ca0c17011ca884161f1a59a541e52e2", + "bytes": 10404, + "imports": [ + "Mathproof.Meta.Problem18RAMLax13ProofsImp20261001" + ] + }, + { + "relative_path": "Mathproof/Meta/Problem18RAMLax13ProofsImp20261001.lean", + "sha256": "cf6303e7ef49ed47d0f2c396d074c194c30673482ef4e44f5dff1ada06f68c6c", + "bytes": 15213, + "imports": [ + "Mathlib.Tactic" + ] + }, + { + "relative_path": "Mathproof/Meta/RamStd20261007.lean", + "sha256": "7c9263a14360b7fe485a753bda9c35c408b768612538d092f0dff217aa4f597e", + "bytes": 14098, + "imports": [ + "Mathproof.Meta.Problem18RAMLax51RamPolytime20261001", + "Mathlib.Tactic.Ring", + "Mathlib.Tactic.Linarith" + ] + }, + { + "relative_path": "Mathproof/Meta/Problem18RAMLax51RamPolytime20261001.lean", + "sha256": "370a943f3e4b0ec7fb536ac5c4c4cc0ebbc7b55a52706863a1d5379aa53e3836", + "bytes": 2535, + "imports": [ + "Mathproof.Meta.Problem18RAMLax13Ram20261001", + "Mathproof.Meta.Problem18RAMLax51BinaryWordEncoding20261001", + "Mathlib.Algebra.Polynomial.Eval.Defs" + ] + }, + { + "relative_path": "Mathproof/Meta/Problem18RAMLax51BinaryWordEncoding20261001.lean", + "sha256": "d0f28fb10d6b09de7fb8888ddb0fe9a45a414ab9a8f1d90cef4e5c8e3bf4fe2d", + "bytes": 1551, + "imports": [ + "Mathlib.Data.Nat.Bits", + "Mathlib.Data.Fintype.Basic", + "Mathlib.Tactic.DeriveFintype" + ] + } + ], + "external_imports": [ + "Mathlib.Algebra.Polynomial.Eval.Defs", + "Mathlib.Data.Fintype.Basic", + "Mathlib.Data.List.Basic", + "Mathlib.Data.Nat.Bits", + "Mathlib.Tactic", + "Mathlib.Tactic.DeriveFintype", + "Mathlib.Tactic.Linarith", + "Mathlib.Tactic.Ring" + ], + "total_files": 9, + "total_bytes": 148970 +} diff --git a/research/word-ram-transfer/machine/INDEPENDENT-AUDIT.json b/research/word-ram-transfer/machine/INDEPENDENT-AUDIT.json new file mode 100644 index 0000000000..33d4e27efa --- /dev/null +++ b/research/word-ram-transfer/machine/INDEPENDENT-AUDIT.json @@ -0,0 +1,55 @@ +{ + "status": "VERIFIED", + "sha256": "e1849b658e0278181b41beb3572af26bceb035fa5c02c260993e9f34f21361c3", + "theorems": [ + { + "axioms": [ + "propext", + "Quot.sound" + ], + "theorem": "Mathproof.WordRAMLogWidthTransfer20261022.computesIn_on" + }, + { + "axioms": [ + "propext", + "Quot.sound" + ], + "theorem": "Mathproof.WordRAMLogWidthTransfer20261022.computesInOn_mono" + }, + { + "axioms": [ + "propext", + "Quot.sound" + ], + "theorem": "Mathproof.WordRAMLogWidthTransfer20261022.computesInOn_ofLax13" + }, + { + "axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "theorem": "Mathproof.WordRAMLogWidthTransfer20261022.polynomial_fitsWords" + }, + { + "axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "theorem": "Mathproof.WordRAMLogWidthTransfer20261022.compiled_polynomial_run" + } + ], + "allowed_axioms": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "error": null, + "max_heartbeats": null, + "seconds": 60.953, + "toolchain": "leanprover/lean4:v4.33.0", + "source": "machine/WordRAMLogWidthTransfer20261022.lean", + "method": "Fresh independent Lean subprocess using existing pinned canonical import artifacts; no isolated source rebuild claimed.", + "mathlib": "db584cd6d46c92f209a44c0f1c829460d327499d" +} diff --git a/research/word-ram-transfer/machine/MACHINE-INTERFACE.md b/research/word-ram-transfer/machine/MACHINE-INTERFACE.md new file mode 100644 index 0000000000..bfdef63475 --- /dev/null +++ b/research/word-ram-transfer/machine/MACHINE-INTERFACE.md @@ -0,0 +1,62 @@ +# A concrete logarithmic-word interface from the Problem 1.8 compiler + +This packet reuses the actual Problem 1.8 word RAM and proves a sufficient bridge from bounded numerical IMP computations to logarithmic-width executions of a fixed finite RAM program. It does not assert that the complete multiplication algorithm has already been rebuilt or that κ improves. + +## The actual machine + +The implementation is `Lax13.Ram` in `Problem18RAMLax13Ram20261001.lean`, extended conservatively by `RamStd20261007.lean`. Memory and register cells start at zero. A finite program is fixed before the input and word width. Every produced value and every memory address is reduced modulo $2^w$. Each direct or indirect access costs one instruction. Input and output are word streams; reading exhausted input halts, and writing appends one word. + +The extension adds wrapping subtraction, high-word multiplication, remainder, OR, XOR, right shift and strict comparison. Its `runsTo_ofLax13` theorem preserves exact successful-step counts, output and halting. Multiplication of an entire unbounded input is not primitive: permitted word multiplication has operands of only $w=\Theta(\log n)$ bits. The elementary TM simulator needs only an explicit smaller instruction whitelist. Existing `basicOps` and `noMulOps` exclude Boolean operations and shifts, so those predicates should not be misused as the desired whitelist. + +## An admissible input interface + +Existing `RamStd.ComputesIn` quantifies over all lists of natural numbers and requires every input entry to fit at the prescribed width. This is appropriate in the polynomial-width regime. Its `LogWordTime` specialization cannot be used unchanged for arbitrary lists: the single item $2^m$ has encoded size proportional to $m$ and does not fit in $c\log m$ bits for fixed $c$. + +The supplied `ComputesInOn D f p W T` restricts the quantifier to an explicit input predicate $D(x)$ while keeping precisely the same RAM. It requires fitting of the input length prefix, all input items and all output items, then correctness at every word width at least $W(\operatorname{bitSize}(x))$. `BinaryWords` is the one-bit-per-item admissibility predicate. Packed inputs can supply a digit-width predicate; their representation must be specified independently of an unbounded input-sized word primitive. + +`LogWordTimeOn` uses $c(\lfloor\log_2(n+2)\rfloor+1)$. The appendix includes conservative restriction, input-domain monotonicity and exact base-machine transfer lemmas. It changes neither the machine nor any instruction cost. + +## A positive compilation theorem + +Fix an IMP command $c$ and a well-formed layout $L$. Put +$$ +A=L.\mathrm{temps}+2+|L.\mathrm{scalars}|,\qquad q=|L.\mathrm{arrays}|. +$$ +The existing compiler places array $j$ at index $i$ in memory cell $A+j+qi$. This interleaving is independent of input size, array capacity, numerical bound and word width. The address span for indices below $B$ is $A+qB$. The implemented compiler constant is exactly $10$. + +**Theorem.** Let `BigStepB B c (initEnv ext x) s k` be an actual bounded IMP execution, with a well-formed command, all input values below $B$, and fixed constants $d,a$ satisfying +$$ +1