From 46ca24a88b5194725a82c02003aac8aea0c6f53a Mon Sep 17 00:00:00 2001 From: Dugongue <49054532+Dugongue@users.noreply.github.com> Date: Wed, 21 Oct 2026 22:22:10 -0700 Subject: [PATCH] Derive packed Word RAM transfer with logarithmic simulation speedup --- research/packed-ram-speedup/.gitattributes | 1 + research/packed-ram-speedup/CALLERS.json | 35 +++ .../packed-ram-speedup/CONTENT-HASHES.json | 21 ++ .../packed-ram-speedup/LEAN-PRECEDENTS.json | 113 +++++++ research/packed-ram-speedup/LICENSE | 201 ++++++++++++ .../packed-ram-speedup/OVERLAP-SOURCES.json | 222 ++++++++++++++ research/packed-ram-speedup/OVERLAP.md | 50 +++ research/packed-ram-speedup/PACKED-IO.md | 159 ++++++++++ research/packed-ram-speedup/PROOF.md | 112 +++++++ research/packed-ram-speedup/README.md | 51 +++ research/packed-ram-speedup/SOURCES.json | 18 ++ .../packed-ram-speedup/TABULATED-MULTIPLY.md | 44 +++ research/packed-ram-speedup/TASK.json | 76 +++++ research/packed-ram-speedup/VALIDATION.md | 16 + research/packed-ram-speedup/VERIFY.json | 20 ++ research/packed-ram-speedup/end_to_end.py | 99 ++++++ research/packed-ram-speedup/packed_codec.py | 151 +++++++++ .../packed-ram-speedup/tabulated_multiply.py | 77 +++++ research/packed-ram-speedup/tabulated_tm.py | 290 ++++++++++++++++++ research/packed-ram-speedup/verify.py | 25 ++ 20 files changed, 1781 insertions(+) create mode 100644 research/packed-ram-speedup/.gitattributes create mode 100644 research/packed-ram-speedup/CALLERS.json create mode 100644 research/packed-ram-speedup/CONTENT-HASHES.json create mode 100644 research/packed-ram-speedup/LEAN-PRECEDENTS.json create mode 100644 research/packed-ram-speedup/LICENSE create mode 100644 research/packed-ram-speedup/OVERLAP-SOURCES.json create mode 100644 research/packed-ram-speedup/OVERLAP.md create mode 100644 research/packed-ram-speedup/PACKED-IO.md create mode 100644 research/packed-ram-speedup/PROOF.md create mode 100644 research/packed-ram-speedup/README.md create mode 100644 research/packed-ram-speedup/SOURCES.json create mode 100644 research/packed-ram-speedup/TABULATED-MULTIPLY.md create mode 100644 research/packed-ram-speedup/TASK.json create mode 100644 research/packed-ram-speedup/VALIDATION.md create mode 100644 research/packed-ram-speedup/VERIFY.json create mode 100644 research/packed-ram-speedup/end_to_end.py create mode 100644 research/packed-ram-speedup/packed_codec.py create mode 100644 research/packed-ram-speedup/tabulated_multiply.py create mode 100644 research/packed-ram-speedup/tabulated_tm.py create mode 100644 research/packed-ram-speedup/verify.py diff --git a/research/packed-ram-speedup/.gitattributes b/research/packed-ram-speedup/.gitattributes new file mode 100644 index 0000000000..fa1385d99a --- /dev/null +++ b/research/packed-ram-speedup/.gitattributes @@ -0,0 +1 @@ +* -text diff --git a/research/packed-ram-speedup/CALLERS.json b/research/packed-ram-speedup/CALLERS.json new file mode 100644 index 0000000000..6d211b8a37 --- /dev/null +++ b/research/packed-ram-speedup/CALLERS.json @@ -0,0 +1,35 @@ +{ + "kind": "Reference provenance only, not executable or verified multiplication inputs", + "canonical_main": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "word_ram_predecessor": { + "pr": 4538, + "head": "dffc7939519e486ebeb97aff315ce01e067d4728", + "role": "Bounded-word model, explicit-domain interface and packed-tape refinement precedent" + }, + "selected_TM": { + "pr": 4359, + "conditional_kappa": "0.0023", + "role": "Selected conditional theorem; transfer preserves its complete antecedent" + }, + "strongest_inspected_pending_TM": { + "pr": 4535, + "head": "a6d7237f697185e857090e174c23c1cb22c6563c", + "conditional_kappa": "0.003020165", + "role": "Stronger pending conditional theorem; not independently validated by this package" + }, + "critical_root_predecessor": { + "pr": 4532, + "head": "644607ba59ebe401ac7ecd627ae7f331f924d1b0" + }, + "native_supplier": { + "pr": 4470, + "head": "b9a13c1673e0e9697de410de16e8bbf3207a7363" + }, + "independent_arithmetic": { + "pr": 4536, + "head": "26502792b9d46fc353fc7b092de070a675264fd8", + "scope": "Arithmetic only; excludes complete compiler/physical theorem" + }, + "frontier_change": false, + "new_TM_kappa": false +} diff --git a/research/packed-ram-speedup/CONTENT-HASHES.json b/research/packed-ram-speedup/CONTENT-HASHES.json new file mode 100644 index 0000000000..55ce52eb9c --- /dev/null +++ b/research/packed-ram-speedup/CONTENT-HASHES.json @@ -0,0 +1,21 @@ +{ + ".gitattributes": "705fd4d6451a31d36b3df7de96f83f30ac976c9b4a6d1e51671d8e2f33e2d0da", + "CALLERS.json": "c50b683515f33ddff7863653ebdca4eba6f43d01e5e02a4568c3d14f9b79a027", + "end_to_end.py": "e7c540dea7a8cc884aa63ea4ff25ac97fb7fdbb1fce8a31cd756feb418c9f5fe", + "LEAN-PRECEDENTS.json": "a9cd1737575f872b0e4b7dd32f01632cbd3cd9324718b4e491e83d80452a6dde", + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "OVERLAP-SOURCES.json": "7e0bb443a152b8c65f631b4a0495bdb351a7033c5f20941759668408c83b68af", + "OVERLAP.md": "d6c20147e749ee4bb5931413fe8bda56c8a8f6aa4d8681867c0c2ed0426047a5", + "PACKED-IO.md": "3197b3763d6c8ac7733ed128b4191b19ae0fd22a9d94d90cf80ca2a3b9459120", + "packed_codec.py": "2a45d3de4e9b1093129179a036d4f3165808c1744cf84190a9c6829714f6c789", + "PROOF.md": "788535dea58df897055de81175acdea9abb149604ad9bdf7ee36b6100982d541", + "README.md": "7d5226933a90c875ea217f1814c15bac1206da38abb5373e1a4583ea02d09f4f", + "SOURCES.json": "57f78e056178dcb5eb8b4438df7dfa560e209cc21f7236e81be3853f9a62a4cf", + "TABULATED-MULTIPLY.md": "653a050590f1514f594985265dadbc2a29d4e6cafaa2980fce29aa2fc20fc692", + "tabulated_multiply.py": "cdf4e671ca82c8f3cab8635354629f0b3630395f325e5e715f85edfaa590f8d2", + "tabulated_tm.py": "659e7fa8bd8bd6376760f7ffe1c26da56de9a80d84475bb1c7781177be18a152", + "TASK.json": "7d16977960f08b70c3f51c12d29e3458afafc5106476501f84f7aa11c362f55c", + "VALIDATION.md": "0986660d873e839bb3301b35bc2d0a6813cfa3eca2721b6888d46147673855cc", + "VERIFY.json": "791bc9fc978b593abe3b572876ef9130f7d06762afdf23a917d7d2b959ea15fa", + "verify.py": "e8dda0310634cd5f38e9c08021b9d70e03adddc1104e48d603089f46fee0d48f" +} diff --git a/research/packed-ram-speedup/LEAN-PRECEDENTS.json b/research/packed-ram-speedup/LEAN-PRECEDENTS.json new file mode 100644 index 0000000000..2b58c3baca --- /dev/null +++ b/research/packed-ram-speedup/LEAN-PRECEDENTS.json @@ -0,0 +1,113 @@ +{ + "scope": "Reused selected-source provenance from PR4538, not a fresh complete DAG or kernel check. The new construction is informal.", + "sources": [ + { + "module": "Mathproof.Meta.RamStd20261007", + "source_path": "canonical-project/Mathproof/Meta/RamStd20261007.lean", + "source_sha256": "7c9263a14360b7fe485a753bda9c35c408b768612538d092f0dff217aa4f597e", + "source_lines": 323, + "evidence": "Exact source inspected; artifact presence is historical evidence, not a fresh audit of source." + }, + { + "module": "Mathproof.Meta.Problem18RAMLax13Ram20261001", + "source_path": "canonical-project/Mathproof/Meta/Problem18RAMLax13Ram20261001.lean", + "source_sha256": "b95844098a3c402ec895c542d07a4b60354455cf66fe77bad1050d15583ec948", + "source_lines": 295, + "evidence": "Exact source inspected; artifact presence is historical evidence, not a fresh audit of source." + }, + { + "module": "Mathproof.Meta.Problem18RAMLax13ProofsImp20261001", + "source_path": "canonical-project/Mathproof/Meta/Problem18RAMLax13ProofsImp20261001.lean", + "source_sha256": "cf6303e7ef49ed47d0f2c396d074c194c30673482ef4e44f5dff1ada06f68c6c", + "source_lines": 325, + "evidence": "Exact source inspected; artifact presence is historical evidence, not a fresh audit of source." + }, + { + "module": "Mathproof.Meta.Problem18RAMLax13ProofsBounds20261001", + "source_path": "canonical-project/Mathproof/Meta/Problem18RAMLax13ProofsBounds20261001.lean", + "source_sha256": "16ca19d477c17805abecb3ca265e4b2b7ca0c17011ca884161f1a59a541e52e2", + "source_lines": 221, + "evidence": "Exact source inspected; artifact presence is historical evidence, not a fresh audit of source." + }, + { + "module": "Mathproof.Meta.Problem18RAMLax13ProofsCompile20261001", + "source_path": "canonical-project/Mathproof/Meta/Problem18RAMLax13ProofsCompile20261001.lean", + "source_sha256": "bc2237188b9b7c6f4d5524bad17d353bab873ab693ddb2e947574739dc2aae2c", + "source_lines": 496, + "evidence": "Exact source inspected; artifact presence is historical evidence, not a fresh audit of source." + }, + { + "module": "Mathproof.Meta.Problem18RAMLax13ProofsSimulation20261001", + "source_path": "canonical-project/Mathproof/Meta/Problem18RAMLax13ProofsSimulation20261001.lean", + "source_sha256": "2db5af757e7808c62ac1b578a26e198532c24b17388a06719c127f08de23811c", + "source_lines": 931, + "evidence": "Exact source inspected; artifact presence is historical evidence, not a fresh audit of source." + }, + { + "module": "Mathproof.Meta.Problem18RAMLax51RamPolytime20261001", + "source_path": "canonical-project/Mathproof/Meta/Problem18RAMLax51RamPolytime20261001.lean", + "source_sha256": "370a943f3e4b0ec7fb536ac5c4c4cc0ebbc7b55a52706863a1d5379aa53e3836", + "source_lines": 58, + "evidence": "Exact source inspected; artifact presence is historical evidence, not a fresh audit of source." + }, + { + "module": "Mathproof.Meta.Problem18RAMLax51TuringRamEquivalence20261001", + "source_path": "canonical-project/Mathproof/Meta/Problem18RAMLax51TuringRamEquivalence20261001.lean", + "source_sha256": "6b3f5decde11412c0737c5522a13c587fb40031614a9ffddba950bb4392716a7", + "source_lines": 54, + "evidence": "Exact source inspected; artifact presence is historical evidence, not a fresh audit of source." + }, + { + "module": "Mathproof.Meta.Problem18RAMRoot20261006", + "source_path": "canonical-project/Mathproof/Meta/Problem18RAMRoot20261006.lean", + "source_sha256": "88c0e0dfc5214faa7c1396f10787f2956a6639e6d979433fcc176bae13a247a0", + "source_lines": 495, + "evidence": "Exact source inspected; artifact presence is historical evidence, not a fresh audit of source." + }, + { + "module": "Mathproof.Meta.Problem18RAMRootLean20261007", + "source_path": "canonical-project/Mathproof/Meta/Problem18RAMRootLean20261007.lean", + "source_sha256": "b0471819ac3fb1e634709abaddfceabaa57a3b0af4176156645d66da10320a53", + "source_lines": 78, + "evidence": "Exact source inspected; artifact presence is historical evidence, not a fresh audit of source." + }, + { + "module": "Mathproof.Meta.Problem18RAMRootLog20261007", + "source_path": "canonical-project/Mathproof/Meta/Problem18RAMRootLog20261007.lean", + "source_sha256": "2189302e7a212da8520d046c0e00f2c661e40e98a66a22273be33f1e9786107e", + "source_lines": 173, + "evidence": "Exact source inspected; artifact presence is historical evidence, not a fresh audit of source." + }, + { + "module": "Mathproof.Meta.MpSparse20261007", + "source_path": "canonical-project/Mathproof/Meta/MpSparse20261007.lean", + "source_sha256": "16b861e3f381d5e02203ca71d905a1d16bacc2179e29ba6e25df52755153d180", + "source_lines": 944, + "evidence": "Exact source inspected; artifact presence is historical evidence, not a fresh audit of source." + }, + { + "module": "Mathproof.Meta.MpGlue20261007", + "source_path": "canonical-project/Mathproof/Meta/MpGlue20261007.lean", + "source_sha256": "3dd80f72059101310cc13c1278b0d2815ae02587192af2742535674b642ed84d", + "source_lines": 539, + "evidence": "Exact source inspected; artifact presence is historical evidence, not a fresh audit of source." + }, + { + "module": "Mathproof.Meta.MpLimbs20261007", + "source_path": "canonical-project/Mathproof/Meta/MpLimbs20261007.lean", + "source_sha256": "cbbb9b64e17dd9059378e92819c7da492a1643a6505ea35d24e486d8d6798600", + "source_lines": 3213, + "evidence": "Exact source inspected; artifact presence is historical evidence, not a fresh audit of source." + }, + { + "source_path": "research-archive/problem18-typed-20260930/reuse/RAM-TM/concepts/Lax51/TuringRamEquivalence.lean", + "source_sha256": "1708e355c07bbcf788a58af6d7ff764b925e5376da64df43a8d01593dbaf5ed0", + "evidence": "Historical source only. Concepts version includes an axiom; separate proof theorem not used by the new bridge." + }, + { + "source_path": "research-archive/problem18-typed-20260930/reuse/RAM-TM/proofs/Lax51Proofs/TuringRamEquivalence.lean", + "source_sha256": "70e4d7ee08eedbcc94536c3c6204d31c5e78d7c5f72780ff9b8b7e5d7a601816", + "evidence": "Historical source only. Concepts version includes an axiom; separate proof theorem not used by the new bridge." + } + ] +} diff --git a/research/packed-ram-speedup/LICENSE b/research/packed-ram-speedup/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/packed-ram-speedup/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/packed-ram-speedup/OVERLAP-SOURCES.json b/research/packed-ram-speedup/OVERLAP-SOURCES.json new file mode 100644 index 0000000000..a12afc7d48 --- /dev/null +++ b/research/packed-ram-speedup/OVERLAP-SOURCES.json @@ -0,0 +1,222 @@ +{ + "sources": [ + { + "title": "Hopcroft, Paul and Valiant (1975), On Time versus Space and Related Problems", + "url": "https://www-wjp.cs.uni-saarland.de/publikationen/HPV75.pdf", + "sha256": "4700da81799d5e8794d37c2fdcc43eb06c3ec252ed9b878ce56805df5f88e57c", + "relevant": "Section 4, Theorem 5 and Corollary 3, printed page 63; PDF page 7." + }, + { + "path": "upstream/build/sections/00-introduction.tex", + "url": "https://raw.githubusercontent.com/openai/math/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Integer-multiplication-below-n-log-n-September-23-2026/build/sections/00-introduction.tex", + "sha256": "98721f03682ccf1cc7d0850b07adabaa2d8f3afe552e3861753eba9d284d0da0" + }, + { + "path": "upstream/build/sections/01-history.tex", + "url": "https://raw.githubusercontent.com/openai/math/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Integer-multiplication-below-n-log-n-September-23-2026/build/sections/01-history.tex", + "sha256": "798956c8150c31e3e2f5f29c47110d25ce619faad1374f4d3a0f15fa3ee33ead" + }, + { + "path": "upstream/build/sections/02-streams.tex", + "url": "https://raw.githubusercontent.com/openai/math/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Integer-multiplication-below-n-log-n-September-23-2026/build/sections/02-streams.tex", + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab" + }, + { + "path": "upstream/build/sections/09-exact-arithmetic.tex", + "url": "https://raw.githubusercontent.com/openai/math/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Integer-multiplication-below-n-log-n-September-23-2026/build/sections/09-exact-arithmetic.tex", + "sha256": "5714e5d0656c78c6a1fde8d01fd11f1ba856a7ea94149b283bd9a50fdbf516c3" + } + ], + "queries": { + "repo:CrocSwap/integer-mult-bounds is:pr \"RAM\"": { + "total_count": 19, + "results": [ + { + "number": 956, + "title": "Research: close the PR390 heterogeneous physical provider in exact RAM", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/956" + }, + { + "number": 4538, + "title": "Word RAM transfer: finite TM compiler, checked logarithmic-width bridge and native kernels", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4538" + }, + { + "number": 647, + "title": "Research: paid-copy E8 exact-RAM realization with an attributed DFT corollary", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/647" + }, + { + "number": 2235, + "title": "Add verified multitape foundations, compilers, dirty-frame callers and quadratic multiplication output", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2235" + }, + { + "number": 697, + "title": "Research construction: direct-source E8 with 120 fewer helpers", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/697" + }, + { + "number": 209, + "title": "Parallel-effort entry: Lean proof of #130's frame lemma and check of #193's complex word, Fourier side (no \u03ba claim)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/209" + }, + { + "number": 2035, + "title": "Apply parallel worker memory budgets on Windows", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2035" + }, + { + "number": 721, + "title": "Tooling: reduce reconciliation replay peak RSS by 56% with exact streaming", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/721" + }, + { + "number": 3122, + "title": "Research: reduce batched lifting clean workspace with paid checkpoints", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3122" + }, + { + "number": 4242, + "title": "Replay pinned GL3 RUP certificates on another native platform", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4242" + }, + { + "number": 682, + "title": "Research audit: tensor E8 rate and finite-depth center-copy correction", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/682" + }, + { + "number": 4076, + "title": "Conditional \u03ba = 0.001730809033576552081734 (+1.458e-7 over #3945): three staged helper entries and an LP-exact T360 fill", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4076" + }, + { + "number": 3129, + "title": "Research: near-input clean workspace for batched lifting", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3129" + }, + { + "number": 765, + "title": "Scoped negative result: tensor E8 basis mixing cannot lower 72^d copy rank", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/765" + }, + { + "number": 514, + "title": "Conditional kappa 0.001391523459591829: partial-own factory, 92 pivots and asynchronous whole owners", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/514" + }, + { + "number": 2208, + "title": "Research: all-word dirty-connector bounds and signed triangle (no new \u03ba)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2208" + }, + { + "number": 1974, + "title": "Research: the 916 open mixed GL3 target pairs need exactly their direct cost (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1974" + }, + { + "number": 1175, + "title": "Conditional kappa 0.001675338871723469: whole-owner map at the packin\u2026", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1175" + }, + { + "number": 1101, + "title": "Tooling: overlap bit589 and complex741 in the #741 ancestry replay, 17% (50% with --complex-jobs 3) less wall time (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1101" + } + ] + }, + "repo:CrocSwap/integer-mult-bounds is:pr \"word-RAM\"": { + "total_count": 3, + "results": [ + { + "number": 4538, + "title": "Word RAM transfer: finite TM compiler, checked logarithmic-width bridge and native kernels", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4538" + }, + { + "number": 514, + "title": "Conditional kappa 0.001391523459591829: partial-own factory, 92 pivots and asynchronous whole owners", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/514" + }, + { + "number": 956, + "title": "Research: close the PR390 heterogeneous physical provider in exact RAM", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/956" + } + ] + }, + "repo:CrocSwap/integer-mult-bounds is:pr \"log-RAM\"": { + "total_count": 0, + "results": [] + }, + "repo:CrocSwap/integer-mult-bounds is:pr \"tabulation\"": { + "total_count": 1, + "results": [ + { + "number": 1790, + "title": "Selected PR1094: complete two-role whole-helper swap census (no improving swap)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1790" + } + ] + }, + "repo:CrocSwap/integer-mult-bounds is:pr \"Hopcroft\"": { + "total_count": 10, + "results": [ + { + "number": 364, + "title": "\u03ba = 8.04879370798932e-4: #362 with \u03ba-exact min-cost carrier matching in the base producer (+3.0e-8)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/364" + }, + { + "number": 167, + "title": "Open search tooling for paired-cube complex words (no \u03ba claim)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/167" + }, + { + "number": 181, + "title": "Shared-edge local circuit on PR168 v4 paired cubes (\u03ba = 6.59180578557293e-4)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/181" + }, + { + "number": 72, + "title": "Searched orders on PR #49's graphs: conditional \u03ba = 4.125007391e-5", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/72" + }, + { + "number": 182, + "title": "Shared-edge local circuit, refined bit frames and bit terminal sinks on PR168 v4 (\u03ba = 6.60216552061722e-4)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/182" + }, + { + "number": 189, + "title": "Shared-edge complex and face-diagonal bit local circuits on PR168 v4 (\u03ba = 6.61755179959122e-4)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/189" + }, + { + "number": 196, + "title": "Face-diagonal local circuits on both suppliers of PR168 v4 (\u03ba = 6.65046903615388e-4)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/196" + }, + { + "number": 325, + "title": "Conditional \u03ba = 7.696840393833340e-4: a stronger p = 10 bit word \u2014 re-annealed pair module, p = 10 local design, balanced cube orientation, tiered reuse matching (+0.71% over #315's word)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/325" + }, + { + "number": 200, + "title": "A stronger bit supplier: fixed-coordinate and face-diagonal bit local circuit on PR168 v4 (effective bit saving 6.7734e-4)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/200" + }, + { + "number": 276, + "title": "Conditional \u03ba = 7.22869827347495e-4: a new paired-cube bit word (arc-aware local circuit, centre-sharing pair module) in the five-stage completed banks", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/276" + } + ] + } + }, + "coverage": "Public GitHub PR title/body search, current open-PR listing, exact original OpenAI source inspection and selected existing exact-RAM proofs. This is not an exhaustive search of all PR code, comments or historical literature." +} diff --git a/research/packed-ram-speedup/OVERLAP.md b/research/packed-ram-speedup/OVERLAP.md new file mode 100644 index 0000000000..f88cf29130 --- /dev/null +++ b/research/packed-ram-speedup/OVERLAP.md @@ -0,0 +1,50 @@ +# Overlap: packed RAM corollary, original source and classical simulation + +## What the original manuscript states + +The retained OpenAI manuscript is pinned at openai/math commit adc7f1241b42e322a6451854ab7e4b4c146bf78a. Its introduction states the multiplication result on a single fixed finite-alphabet, fixed-tape-count TM, with the exact fixed-width MSB-first product. Its history section distinguishes storage-modification machines and Groff's RAM result with excluded preprocessing; its exact-DFT discussion uses unbounded exact complex scalars and explicitly separates bit complexity. No packed bounded-word multiplication corollary appears in those inspected passages. + +The current upstream path history returned only its initial commit. Four inspected source files match the pinned upstream manifest exactly. Their hashes and public original URLs are in OVERLAP-SOURCES.json. + +Relevant originals: +- Introduction, lines 13–29: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Integer-multiplication-below-n-log-n-September-23-2026/build/sections/00-introduction.tex +- History, lines 28–34 and 141–164: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Integer-multiplication-below-n-log-n-September-23-2026/build/sections/01-history.tex +- Fixed-tape model, Section 2: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Integer-multiplication-below-n-log-n-September-23-2026/build/sections/02-streams.tex + +## The classical simulation precedent + +Hopcroft, Paul and Valiant's *On Time versus Space and Related Problems* (FOCS 1975), Section 4, Theorem 5, gives a logarithmic RAM simulation speedup using precomputed bounded TM blocks. It explicitly assumes t(n)>=n log n and explains that its RAM needs n operations to examine the input. Corollary 3 applies this to multiplication, obtaining O(n log log n) from the then-available TM algorithm, while keeping numbers O(log n) bits long. + +Primary source: https://www-wjp.cs.uni-saarland.de/publikationen/HPV75.pdf , printed page 63 (PDF page 7). SHA-256: 4700da81799d5e8794d37c2fdcc43eb06c3ec252ed9b878ce56805df5f88e57c. + +Therefore the generic Four-Russians TM simulation is classical. The original theorem's stated t>=n log n hypothesis cannot simply be ignored when applying it to t=n(log n)^(1-kappa). A complete present proof must supply its packed-I/O variant, charge its preprocessing and establish bounded words and addresses. + +## What is different in the present application + +The proposed constructive variant uses Theta(log n)-step local windows and pays uniform sublinear table generation. With packed binary input/output and explicit codecs, its cost is +$$ +O\left(\frac{T(n)+n}{\log(n+2)} ++n^\epsilon\operatorname{polylog}(n)\right) +$$ +for a chosen fixed epsilon<1. At a fixed 0=2, a power of two, and r>=1, also a power of two. The simulated tape +alphabet uses blank symbol 0 and logical bit codes 1,2. Other symbols may exist +internally, but an output binary prefix contains only 1 and 2 before its first +blank. Let beta=2^r. An n-bit operand arrives in exactly ceil(n/r) little-endian +base-beta digit words; the final digit's unused high bits must be zero. The +length header n, table arenas, input/output arrays and all pointers fit in +bounded w-bit words. Require 2cr+8=8, d>=1 give + + T+n+m+16 <= 2^(a-4) (n+2)^d. + +The machine receives packed binary input in power-of-two chunks as specified below. Its conventional TM input protocol uses two nonblank bit symbols distinct from blank, at fixed tape origins; its output is an MSB-first binary word at a fixed origin, terminated by blank or occupying the whole m-cell cap. A fixed alphabet relabeling and ordinary linear-time TM protocol conversion can arrange this standard interface. Such conversion time is part of T, not an uncharged oracle. + +There is a uniform finite-program Word RAM algorithm, fixed before n and independent of actual T and physical word width, with word width w >= C_M (floor(log2(n+2))+1), that produces exactly the same integer output in fixed-width packed LSB form. It uses only literal assignment, indirect LOAD/STORE, ADD, natural SUB, Boolean operations, shifts, branches and word input/output. It uses no multiplication/division instruction, supplied lookup table, advice string, randomization or unit-cost exact complex cell. Its total cost is + + O_M((T+n+m)/log(n+2) + (n+2)^(1/16) log(n+2)). (1) + +All constants and the fixed program may depend on M and the chosen envelope constants a,d; the M subscript below includes those fixed constants. Every address and intermediate value fits in a word. A nonhalting TM computation is not converted to a halt by an artificial epoch boundary: every finite prefix within the same numerical envelope is simulated faithfully. The halting theorem itself assumes the stated finite T. + +The RAM memory starts identically zero, as in the actual Problem 1.8 RamStd model used in PR #4538. All newly allocated table, tape, IO, descriptor and scratch arenas are disjoint. The numeric span of memory is polynomial in n; zero initialization of that model is not a clearing algorithm for arbitrary dirty storage. + +## 1. Uniform parameter choice and complete setup + +Let lambda=floor(log2(n+2)), ell=lambda+1. Choose c, a fixed power of two, large enough to encode the fixed alphabet, and c>=2 so blank and the two bit codes fit. Let K be the least power of two at least k and s=max(1,ceil(log2 Q)). Define + + q = floor(lambda/(64 K c)); + r = largest power of two <= max(1,q); + B = 4r; L = 2r+1. + +Because 64Kc is a power of two, q is obtained by a right shift; r is obtained by a doubling loop. lambda is computed by repeatedly right-shifting n+2. This costs O(log(n+2)) word operations. r is Theta_M(log(n+2)), with the small-input cutoff absorbed in machine-dependent constants; in particular r >= lambda/(128Kc) when lambda>=1. + +The local table has one row for every bit pattern consisting of a state field and k windows of L consecutive c-bit symbols. Its key size is + + b = s + kc(2r+1). + +For lambda >= max(64Kc,64s), we have r>=1, 64kcr<=lambda and 64s<=lambda. Since 2r+1<=3r, + + 16b <= 16s + 48kcr <= lambda. + +Thus all 2^b rows, including invalid/unreachable state or symbol patterns, number at most (n+2)^(1/16). The finitely many smaller inputs have a fixed table-size bound depending only on M. No universal statement about an arbitrary Q is inferred from the Q=3 parameter tests; the state-bit cutoff is explicit. + +For each row, place each local head at offset r in its window and simulate up to r literal M transitions, stopping at the first missing transition. Save the terminal state, a true-halt flag, elapsed transition count, all k updated windows, and the k final local head offsets. Missing transitions on invalid patterns may be defined as halt; valid runs never use invalid encodings. Dispatch over the fixed finite transition table costs a machine-dependent constant per local step. Construction therefore costs O_M(r 2^b) operations. Store each row in a fixed power-of-two stride of at least 2k+3 words, so its address is formed by a shift and an addition. Every entry is generated during the run from M and r; no table is supplied for free. + +The binary codec tables in PACKED-IO.md contain O(2^r+2^(cr)) rows and take O(r 2^(cr)) setup. Their exponent is smaller than b, so they fit the same startup bound. This pays setup for every input, without amortizing over an unspecified batch of inputs. + +## 2. Ordinary coordinates, packed words and address safety + +Use a fixed polynomial origin + + H = 2^(a+d*ell). + +This is computed by a shift whose exponent uses fixed-constant repeated addition. The program knows a,d as machine constants; it does not receive T or a time-horizon advice string. A signed TM coordinate z is represented at nonnegative position H+z. The envelope implies H is more than sufficient for every visited position and the margin r; no truncating subtraction of a left window origin changes its intended value. + +A tape word stores B fields. Take a fixed power-of-two interleaving stride J>=k. Tape i, block u, is stored at + + dataBase + J*u + i. + +The table base is a fixed machine-dependent power of two above every reserved register/scratch cell (at least 512 in the model); the data base lies above all table and reserved cells. This remains valid for large fixed k, rather than assuming a 512-cell prefix suffices for every machine. Dividing a position by B and reducing it modulo B are right shift and AND because B is a power of two. Different tapes and blocks have different addresses; all metadata, rows, IO buffers and descriptors have separate arenas. + +A window of L<=B consecutive cells spans at most two packed words. If its first word supplies a fields, read its suffix and, only if needed, the low L-a fields of the next word. Shift, OR and mask these fields into one word. To write it back, clear only the corresponding field masks and OR in the two fragments. The Boolean identities prove preservation of every neighboring field and every unused high bit, with arbitrary dirty values there. This is a constant-size additive/Boolean operation sequence per tape, even when a window crosses a packed block boundary. The implementation provides generalized bounded-length chunks for input/output as well. + +This ordinary-coordinate representation matters: a signed interval is not a contiguous bitstring under the unpacked compiler's zigzag mapping. No strided gather, negative-bank reversal or arbitrary bit permutation is assumed to cost one operation. + +To see a logarithmic width suffices globally, note that key bits are at most s+3kc+lambda/32 for all inputs, table row size is fixed, H has a+d*ell+1 bits, and every visited coordinate lies within the supplied polynomial envelope. Multiplying a block index by the fixed interleaving stride is a shift. Adding all IO/descriptor arenas and margins still has polynomial numeric span. A sufficiently large fixed C_M bounds all these exponents and literals. For example, uniform_parameters in tabulated_tm.py uses the conservative coefficient a+d+s+rowLog+strideLog+4kc+32 for its table/tape envelope; a caller includes its fixed IO arena constants in C_M. Word width also exceeds 4cr+1, so masks, reservoirs and all shifted fields fit. At every greater physical word width, the same intended operations and output are obtained. This is bounded-word computation, not an unbounded-register simulation. + +## 3. One macro step and genuine halt + +Maintain the invariant: the saved state is M's state, head i is H plus its signed TM position, and every represented tape field equals its TM symbol. Initially encoded input fields establish the invariant, and every uninitialized field is blank because RAM memory is zero. + +At a macro boundary, fetch all k windows centered on the current heads before performing any tape writes. Form their concatenated key with the current state and fetch the generated row in O_M(1) word operations. Apply every updated window at its old position and set + + newHead_i = oldHead_i + savedLocalHead_i - r. + +All subtractions are safe under the polynomial-origin bound. During r TM transitions a head moves at most r, so it never reads or writes outside the supplied 2r+1-cell window; the final move may reach an endpoint, still inside the window. The local table's literal transition simulation and the all-reads-before-writes discipline therefore preserve the full invariant, including distinct tapes at coincident coordinates. Applying a returned complete window also preserves every cell outside it. + +If a missing transition is seen before r successful transitions, the true-halt flag is set and elapsed counts only actual transitions. If the r-th transition reaches a halting configuration, the next macro detects that missing transition with elapsed zero. Thus at most floor(T/r)+1 macro calls are needed for a halting run. An epoch completing r transitions without a flag does not itself halt. This proves both exact halting semantics and O_M(T/r+1) simulation cost. + +The operational model records its displayed primitive operations, not exact fully emitted RamStd instruction counts. All source loops are over fixed k or the explicit bounded table/epoch counters. Fixed-size dispatch, register assignment and branch lowering alter only machine-dependent constants. No local table lookup is counted as a whole TM step oracle: the complete table construction is explicit and charged above. + +## 4. Packed external ABI, including partial chunks + +Let each operand arrive as exactly ceil(length/r) little-endian r-bit digit words, with unused high bits zero; the logical lengths are supplied as bounded headers. The physical list-length prefix is also paid and fits in a word. For w=Theta(log n), this is an ordinary constant-density packing of the binary input. The format is determined by n, not by the unknown physical w, so it works at all sufficiently large word widths. Input bit length n is the declared padded binary length, not the number of list entries or the numerical value of an all-zero operand. + +The codec explicitly tabulates expansion from binary r-bit chunks into c-bit codes 1/2, and decoding from c-bit chunks to binary values with prefix lengths and validity. It handles reversed chunk order for MSB input and reversed output descriptors for fixed LSB output. Read, store, reverse and masked-insert O(n/r) chunks. Separate operands may use separate tapes. If they share a tape, use one continuous reservoir across operands and delimiters; concatenating separately padded partial chunks would insert blank cells and is incorrect. A fixed binary length header costs only O(log n) cells and fits the startup allowance. + +The output decoder reads at most ceil(m/r) coded chunks, stops at the first blank or cap, reverses the retained descriptors, writes exactly ceil(m/r) LSB digit words, and pads only high bits with zeros. This preserves the numeric value even for leading zeros, zero itself and a short terminated prefix. A full-width output need not expose its following terminator. No bit-by-bit external IO pass costing Theta(n) is hidden here. The detailed reservoir and first-blank proofs are in PACKED-IO.md. + +Counting generated setup, simulation, input and output now gives + + O_M(r 2^b + log(n+2) + T/r + (n+m)/r + 1), + +which implies (1). The total buffer footprint and the polynomial numeric address envelope were included above. Arbitrary dirty reuse would require separately paid initialization; the theorem does not silently change the zero-initialized RamStd model. + +## Corollary: the supplied multiplication bound + +Suppose a fixed deterministic multitape machine multiplies two padded n-bit integers in + + T(n) = O(n (log n)^(1-kappa)), 0=n log n because its input scan costs n. We use the method as precedent and supply the packed-input/packed-output construction explicitly for the sub-n-log-n regime; that theorem's original hypothesis is not simply dropped. PR #4538 supplies this project's exact bounded-word machine and packed-field refinement precedents. The current proof and code do not claim to have invented tabulation or established worldwide priority for the corollary. + +Sources and inspected overlap are recorded in OVERLAP.md and OVERLAP-SOURCES.json. The finite implementations check the displayed model; an emitted complete RamStd program, formal compiler refinement, isolated Linux execution and a new TM paid-profile witness are separate future work. They are not assumed as hidden mathematical gadgets in the algorithm above. diff --git a/research/packed-ram-speedup/README.md b/research/packed-ram-speedup/README.md new file mode 100644 index 0000000000..84d57c3372 --- /dev/null +++ b/research/packed-ram-speedup/README.md @@ -0,0 +1,51 @@ +# Packed Word RAM multiplication transfer + +**Positive result:** a complete fixed multitape algorithm taking T(n) steps has a uniform bounded-word RAM implementation taking + + O((T(n)+n+m)/log(n+2) + (n+2)^(1/16) log(n+2)) + +operations, with explicitly packed binary input, output cap m, paid generated lookup tables, sufficient logarithmic word width and a fixed polynomial address envelope. Thus a supplied conditional integer-multiplication theorem T(n)=O(n(log n)^(1-kappa)) gives **O(n/(log n)^kappa)** RAM operations, including setup and IO. This is a genuine asymptotic improvement over the constant-overhead RAM backend in PR #4538. + +**No improved TM kappa is claimed.** The exponent kappa is inherited from the supplied TM theorem; its assumptions are not discharged. The current selected value is 0.0023 (#4359). Pending #4535 claims 0.003020165 using #4532/#4470; its arithmetic audit #4536 is not a complete proof audit. Neither selected-result files nor their suppliers are changed. No best-known unconditional RAM record, practical speedup or historical priority is asserted. + +## What changed and why it matters + +The previous PR gave constant overhead per TM step and packed storage. This package tabulates Theta(log n) consecutive TM steps and applies each generated row to a constant number of packed words. Crucially, a second generated codec avoids losing that gain in a linear bit-per-word input/output scan. The full native multiplication algorithm can therefore be transferred as an entire fixed TM, rather than requiring every analytic or recursive component to be rewritten before any target-model time gain is available. + +The target is the Problem 1.8 RamStd instruction semantics used in #4538: finite bounded words and addresses, zero-initialized memory, shared register/data semantics and successful-instruction cost. Algorithms use ADD, monus SUB, Boolean operations, shifts, loads/stores, branches and word IO. Word multiplication/division and exact complex-cell arithmetic are not used. The methods and proof are informal; the operational models are not complete emitted RamStd programs or Lean formalizations. + +## Review and reproduce + +Start with [PROOF.md](PROOF.md) for the complete construction, hypotheses, address proof and multiplication corollary. [PACKED-IO.md](PACKED-IO.md) proves binary expansion, reversed/capped output and padding. [TABULATED-MULTIPLY.md](TABULATED-MULTIPLY.md) provides a supplementary constructive word-MUL elimination lemma; the main simulation does not rely on it. [OVERLAP.md](OVERLAP.md) compares actual primary and project sources. + +From the repository root, Python 3.12 and standard library only: + +```sh +python3 scripts/research_package.py --package research/packed-ram-speedup --check-only +python3 scripts/research_package.py --package research/packed-ram-speedup +``` + +A Git-free extracted package can run `python3 -I -O -B verify.py`. The verifier authenticates the exact package inventory and every listed source before launching isolated optimized checks. The composed fixture also authenticates and directly compiles dependency source bytes, avoiding cached bytecode. No network, GitHub access, native compiler, GPU or Lean installation is required for the finite replays. + +The generic `run_packed` entry point computes its epoch and polynomial origin from the declared total length, generates all tables anew, and composes the codecs with the TM simulation without any supplied runtime fuel. Its caller supplies a fixed machine and proves the stated polynomial envelope. The composed checker includes one fresh invocation of that generic runner. + +The main model actually constructs every row of each finite test table and compares macro state, signed heads and every potentially affected tape cell against a separate literal TM interpreter. Controls include early/epoch-boundary halt, nonhalting prefixes, arbitrary dirty window neighbors, corrupted table rows and insufficient width. The codec checks partial chunks, leading zeros, blank termination, dirty post-terminator cells and seven actual decoder mutations. The composed positive fixture is one fixed 144-state machine multiplying all pairs of 2-bit integers through the entire packed codec/window/table/output chain. It is **not an all-length multiplier** or a claim that the huge frontier TM has been materialized. + +## Frontier work and remaining scope + +Three workers and the root also investigated changed native contact graphs, general Clifford frames, whole-prefix retiming and deferred helper compensation. No completely paid cheaper Fourier-rank profile was obtained. A faster free monomial wrapper or an entrance-only deletion with unaccounted prefix contacts cannot justify a larger TM kappa. These local attempts are not packaged as the research result: the positive complete-model transfer above is the result. + +The implementation is a finite operational model with an informal universal proof, not a kernel certificate. Fully emitting and refining the parametric RamStd code remains a concrete implementation task. Literal primitive-operation counts in model reports are not exact emitted instruction counts. All standard fixed-loop/control lowering contributes only machine-dependent constants to the proved asymptotic bound. Tests ran on Windows with portable Python; Linux-hosted execution is not claimed. + +## Open next questions + +- **Emit the whole parametric backend.** Why: makes the complete all-length uniform RAM program executable against RamStd.step. First step: lower table generation and the two-word window merge to finite labels, preserving source hashes and the fixed polynomial origin. Blocker: current executable is the operational model, not a serialized full program. +- **Bind a published complete TM instance.** Why: turns the generic corollary into a fully source-bound application. First step: select either #4359's admitted conditional supplier or #4535's stronger pending supplier and carry its whole source/assumption manifest into the transfer. Blocker: their enormous algorithm-defined transition machine is not materialized here; finite arithmetic audits do not prove those antecedents. +- **Change an actually paid native profile.** Why: a better TM kappa requires a new productive/paid moment, beyond free-wrapper savings. First step: construct one exact all-input coupled-contact rewrite and serialize every owned transport and prefix observation before scoring it. Blocker: no such cheaper complete invoice was established in this session. +- **Measure crossover and practical memory.** Why: machine-dependent table constants can be enormous. First step: report table rows, setup, steady-state work and memory separately for a real bounded machine. Blocker: finite tiny fixtures do not predict a useful threshold for the theoretical multiplier. + +## Credit + +Prepared for Dugongue with substantial OpenAI Codex assistance and three parallel agents. The logarithmic simulation/tabulation method is classical: credit John Hopcroft, Wolfgang Paul and Leslie Valiant (1975), Section 4. Martin Fuerer's 2014 log-RAM model and linear-time multiplication results are model-comparison precedents, not displaced unconditional results. Preserve the existing Problem 1.8 RAM/IMP/compiler and tensor/frame source credits through #4538, and Szymon Torunczyk/GPT's compositional-polytime lineage. + +The conditional multiplication antecedent retains the original OpenAI manuscript, Dillon's #4532, hexapode's #4535, Cinna Davis's #4470 and native/controller lineage, zxv's compiler and flow work, Jacob Alan Sussman's mixed-target recursion, Ryanson Jonathan's mirror/audit work, Dugongue's compact consumer/Word RAM work, and all physical, precision, prime, analytic and recovery contributors. PRs #647/#956 already construct exact-scalar RAM providers in their own models; this package does not relabel them as finite-word bit algorithms. Source-specific notices remain authoritative. New work is Apache-2.0; no independent human peer review is claimed. diff --git a/research/packed-ram-speedup/SOURCES.json b/research/packed-ram-speedup/SOURCES.json new file mode 100644 index 0000000000..18b51b4e95 --- /dev/null +++ b/research/packed-ram-speedup/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/packed-ram-speedup/TABULATED-MULTIPLY.md b/research/packed-ram-speedup/TABULATED-MULTIPLY.md new file mode 100644 index 0000000000..61d0274add --- /dev/null +++ b/research/packed-ram-speedup/TABULATED-MULTIPLY.md @@ -0,0 +1,44 @@ +# Uniform removal of bounded-word multiplication + +This is a classical tabulation construction, supplied as a sufficient target-model result. It does not improve a multitape-Turing-machine κ and is not claimed to be historically new. + +## Exact model + +Fix a constant C. For input length n, let l=floor(log2(n+2))+1, and use virtual words of V=C*l bits, with actual RAM word width at least V and large enough for the disjoint input, working memory and table banks. The program is fixed before n and the actual width. Let b=floor(l/4), assuming l>=8; handle the finitely many smaller n by fixed code. Set B=2^b and K=8C, so K*b>=V. The target uses bounded ADD, natural SUB, Boolean operations, left/right shifts, branches and indirect memory. It does not use multiplication, division, population count or a supplied table. + +The richer RamStd shiftr instruction is permitted. If using only the narrower original Lax13 fragment, a separate right-shift macro without division is needed; the following theorem does not pretend its div-based macro meets a no-division whitelist. + +## Table construction + +Allocate B^2 product entries. In row a, start v=0, and for j=0,...,B-1: +- store v at address base+(a<=n operations has a uniform implementation without multiplication instructions in O(T(n)+sqrt(n)+log(n)) time, with the original memory plus O(sqrt(n)) table words. This statement preserves the original arithmetic and address widths; any virtual-width masking and bank relocation must be included in the caller's implementation. + +For a program also using division, this theorem alone is insufficient: division needs its own implementation or a proof that the selected algorithm does not use it. Fürer's 2014 Theorem 4.1(a) gives linear multiplication in the richer log-RAM model and analyzes short integer multiplications plus simple FFT operations; a fully pinned instruction-level instantiation still must account for its complete setup and operations. Do not cite this tabulation lemma alone as a new linear multiplication algorithm or an unconditional project frontier improvement. + +Primary precedent: Martin Fürer, *How Fast Can We Multiply Large Integers on an Actual Computer?*, arXiv:1402.1811v1, Section 2 and Theorem 4.1(a), https://arxiv.org/html/1402.1811v1 . The broader tabulation technique is standard; this note makes its uniform preprocessing, address footprint and bounded intermediates explicit for the RamStd migration. diff --git a/research/packed-ram-speedup/TASK.json b/research/packed-ram-speedup/TASK.json new file mode 100644 index 0000000000..c314dccdfe --- /dev/null +++ b/research/packed-ram-speedup/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": "Prove a complete O((T+n+m)/log n+n^(1/16)log n) packed bounded-word RAM transfer with paid tables, genuine halt and binary codecs; derive the supplied multiplication theorem as a conditional target-model consequence.", + "scope_change_reason": "Explicit user asks for real progress toward improved kappa using #4538. Changed native-profile search found no valid cheaper invoice; positive scope is a whole-algorithm asymptotic packed Word RAM transfer, rather than register-model card or a fabricated TM kappa.", + "bottleneck_link": "Supports requested Word RAM migration with an actual logarithmic time gain over constant-overhead simulation; does not change the TM rank-moment bottleneck or selected frontier.", + "budget_minutes": 60, + "stop_rule": "Require complete setup/IO/address/semantic assembly and isolated exact checks; reject unpaid native-profile savings and cross-model kappa relabeling.", + "outcome": "partial", + "evidence": "Informal universal construction; full finite local table generation, separate TM reference, packed IO and mutation controls; composed fixed multiplication machine; no new TM kappa or Lean formalization.", + "author": "Dugongue", + "ai_assistance": "OpenAI Codex root plus three parallel agents; substantial AI assistance and independent agent reviews, no human peer-review claim.", + "open_questions": [ + { + "question": "Can the entire parametric backend be emitted and refined against RamStd.step?", + "why_it_matters": "Turns the complete model construction into an executable formal target program.", + "first_step": "Emit full table generation and two-word masked window updates at fixed labels.", + "blocked_by": "Current source is a finite operational model." + }, + { + "question": "Which complete conditional TM supplier should be source-bound into an all-length multiplication application?", + "why_it_matters": "Preserves all exact antecedents while applying the generic transfer.", + "first_step": "Freeze the entire selected or strongest pending supplier manifest and its input/output protocol.", + "blocked_by": "No enormous frontier transition table is materialized here." + }, + { + "question": "Can an all-input coupled native rewrite lower the complete paid Fourier-rank moment?", + "why_it_matters": "Needed for an actual better TM kappa.", + "first_step": "Account for every helper prefix observation, owned edge and output compensation before computing a changed histogram.", + "blocked_by": "No valid cheaper full invoice found." + } + ] +} diff --git a/research/packed-ram-speedup/VALIDATION.md b/research/packed-ram-speedup/VALIDATION.md new file mode 100644 index 0000000000..2dae5b8b49 --- /dev/null +++ b/research/packed-ram-speedup/VALIDATION.md @@ -0,0 +1,16 @@ +# Validation scope + +The registered check authenticates all packaged bytes, then runs four exact finite components and one composed multiplication fixture under isolated optimized Python. It does not invoke Lean and does not verify a complete multiplication theorem or an improved TM kappa. + +- The macro model builds every local transition-table row, checks full affected tape ranges after each macro against a separate signed-coordinate TM reference, retains nonhalting prefixes and checks table/address rejection controls. Uniform parameter tests are separate from tiny finite simulation fixtures. +- The codec checks genuine bit spreading/gathering through generated tables; it includes MSB/LSB direction, partial chunks, zero, leading zeros, cap boundaries, dirty post-terminator data and corrupted decoder rows. +- The finite composed fixture executes one fixed 144-state single-tape machine that multiplies all 16 pairs of 2-bit operands. Python multiplication appears in its fixed truth-table constructor and independent oracle, not in runtime RAM operations. This does not provide an all-length multiplier. One extra invocation of the generic supplied-machine runner recomputes all parameters and setup for a fresh input, rather than reusing the fixture table. +- The short-product supplement checks radix reconstruction, low/high products and a carry mutation. It does not remove arbitrary division or instantiate an entire richer-RAM multiplier by assumption. + +The universal claims have informal proofs and independent agent review. The operational model's counters record displayed arithmetic/memory primitives and annotated control, not every instruction of a fully emitted RamStd program. The proof pays a fixed factor for finite control lowering. No microbenchmark is used as an asymptotic proof. + +New TM profile candidates were tested before scoring. Generalizing a single geodesic contact to arbitrary Clifford labels did not supply a changed paid graph. Deferring a helper's initial correction also required additional prefix contacts and output Fourier compensation; no entrance-only saving was admitted. A further chronological X/Y shared-qubit scan tested 7,140 two/three-stage gauge assignments under the noncommuting-stage certificate; none improved the complete profile. These are bounded local observations, not a universal no-improvement theorem. + +The historical key-budget ResearchRoute ledger is scoped only to its numerical table-size sublemma. An observed finite experiment there is not a kernel proof or an audit of this complete informal construction. No new Lean theorem is claimed by this package. + +The frozen base is f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc. Public source pins and overlap are in SOURCES.json and OVERLAP-SOURCES.json. Component checks run without downloading those reference documents; all executable inputs are local and byte-bound. No selected-frontier cold replay is required because no selected source or parameter is changed. Hosted CI and a Linux runtime replay remain unrun unless separately documented. diff --git a/research/packed-ram-speedup/VERIFY.json b/research/packed-ram-speedup/VERIFY.json new file mode 100644 index 0000000000..983e0c0914 --- /dev/null +++ b/research/packed-ram-speedup/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 authenticated package; full finite transition tables and independent TM replay; nonhalting/table/word guards; packed codec reversal/cap and seven mutations; short-product radix carries; actual fixed 144-state multiplication fixture for 16 pairs. No new TM kappa or Lean assertion." + } + ] +} diff --git a/research/packed-ram-speedup/end_to_end.py b/research/packed-ram-speedup/end_to_end.py new file mode 100644 index 0000000000..d50e6ea46a --- /dev/null +++ b/research/packed-ram-speedup/end_to_end.py @@ -0,0 +1,99 @@ +"""One fixed 144-state TM, composed packed-codec/tabulator multiplication fixture. +Apache-2.0. Dugongue with substantial OpenAI Codex assistance. +Only the 16-case finite machine constructor and reference oracle use Python MUL. +The runtime target uses no MUL/DIV. This is NOT an all-length multiplier. +""" +from pathlib import Path +import types +import hashlib +import json +from collections import defaultdict + + +def load(path,name): + pins=json.loads((Path(__file__).resolve().parent/'CONTENT-HASHES.json').read_text(encoding='utf-8')) + raw=path.read_bytes() + if hashlib.sha256(raw).hexdigest()!=pins[path.name]:raise ValueError('Dependency source drift: '+path.name) + module=types.ModuleType(name);module.__file__=str(path) + exec(compile(raw,str(path),'exec'),module.__dict__) + return module + + +def machine(): + delta={};halt=143 + # Prefix trie states 0,...,14 read exactly four MSB symbols. + for depth in range(4): + for prefix in range(1<>2,word&3 + product=left*right # compile-time finite truth table, not runtime arithmetic. + for j in range(4): + for symbol in range(3): + delta[base+j,(symbol,)]=(base+j+1,(symbol,),(-1,)) + for j in range(4): + bit=(product>>(3-j))&1 + nxt=halt if j==3 else base+4+j+1 + for symbol in range(3): + delta[base+4+j,(symbol,)]=(nxt,(1+bit,),(1,)) + return delta + +def check(): + here=Path(__file__).resolve().parent + codec_path=here/'packed_codec.py' + tab_path=here/'tabulated_tm.py' + codec_module=load(codec_path,'fixture_codec');tab=load(tab_path,'fixture_tabulator') + codec=codec_module.Codec(1,2,64) + sim=tab.Tabulator(1,3,144,machine(),1,64) + tables=sim.rows;setup=sim.setup_ops+codec.setup_ops + fixtures=macros=transitions=runtime=0 + for left in range(4): + for right in range(4): + # A fresh input/run preserves the already generated immutable table. + sim.v.mem=defaultdict(int,{a:v for a,v in sim.v.mem.items() if a>j)&1 for j in range(4)] + before=sim.v.ops+codec.ops + coded=codec.input_to_tm(digits,4,'msb') + # General contiguous-chunk insertion, preserving all neighboring cells. + mask=sim.v.sub(sim.v.shl(1,sim.r<=1 and r&(r-1)==0 and c>=2 and c&(c-1)==0,'power-of-two shape') + need(2*c*r+8>j)&1)) << (j<>(r-1-j))&1)) << (j<>(j<=self.r: + out.append(buffer & ((1<<(self.r<>= self.r< packed c-bit TM cells. + order selects TM's bit order; no uncharged bit-by-bit input is read. + """ + need(order in ('msb','lsb') and n>=0 and n+self.r<(1<>self.rlog + need(len(digits)==count,'packed input length') + out=[];buffer=used=0 + for index in (range(count-1,-1,-1) if order=='msb' else range(count)): + length=min(self.r,n-(index<> ((self.r-length)<=0 and cap+self.r<(1<>self.rlog;self.ops+=6 + while len(out)n:symbols += [0]+[rng.randrange(1<>(i*r))&codec.bmask for i in range((cap+r-1)//r)] + need(actual==expected,'packed MSB output codec mismatch') + need(codec.ops-before<=160*((cap+r-1)//r+1),'output operation envelope') + cases+=1 + # Real corrupted decoder entry must break a fixed integer-value example. + raw=codec.input_to_tm(codec.pack_bits([1]),1,'msb')[0] + old=codec.decode[raw];codec.decode[raw]=(1,0,True) + need(codec.tm_to_output([raw],1)!=[1],'decoder fault escaped');codec.decode[raw]=old;mutations+=1 + # Invalid symbol before terminator rejects; dirty data after blank does not. + try:codec.tm_to_output([3],1) + except ValueError:pass + else:raise ValueError('invalid symbol accepted') + need(codec.tm_to_output([0],1)==[0],'empty-zero output') + ops+=codec.ops + return dict(status='PASS',packed_io_cases=cases,charged_codec_operations=ops,charged_setup_operations=setup, + corrupted_decoder_controls=mutations,invalid_output_symbols_rejected=True, + leading_zeros=True,dirty_post_terminator=True,partial_chunks=True, + word_multiplication_or_division=False,emitted_RamStd_program=False,Lean_proof=False) + +if __name__=='__main__':print(json.dumps(check(),indent=2)) diff --git a/research/packed-ram-speedup/tabulated_multiply.py b/research/packed-ram-speedup/tabulated_multiply.py new file mode 100644 index 0000000000..dd1bb95fe5 --- /dev/null +++ b/research/packed-ram-speedup/tabulated_multiply.py @@ -0,0 +1,77 @@ +"""Independent radix-product replay; constructor/evaluator use no multiplication. +The multiplication in expected() is the specification only. +""" +import json +import random + +def need(ok, message): + if not ok: + raise ValueError(message) + +def build(b): + B = 1 << b + table = [] + for a in range(B): + v = 0 + for _ in range(B): + table.append(v) + v += a + return table + +def digits(x, b, k): + mask = (1 << b) - 1 + answer = [] + for _ in range(k): + answer.append(x & mask) + x >>= b + need(x == 0, "operand exceeds fixed digit bank") + return answer + +def product(x, y, b, k, table, corrupt=False): + B = 1 << b + aa, bb = digits(x, b, k), digits(y, b, k) + cc = [0 for _ in range(k + k)] + largest = 0 + for i in range(k): + carry = 0 + for j in range(k): + z = cc[i+j] + table[(aa[i] << b) + bb[j]] + carry + need(0 <= z < (1 << (b+b)), "temporary overflow") + largest = max(largest, z) + cc[i+j] = z & (B-1) + carry = z >> b + need(cc[i+k] == 0, "unexpected existing terminal carry") + cc[i+k] = 0 if corrupt else carry + result = 0 + for d in reversed(cc): + result = (result << b) | d + return result, largest + +def expected(x, y): + return x * y + +def main(): + rng = random.Random(20261022) + cases = 0 + for b in range(1, 7): + table = build(b) + B = 1 << b + for a in range(B): + for j in range(B): + need(table[(a << b) + j] == expected(a,j), "table mismatch") + for k in range(1, 9): + limit = 1 << (b*k) + samples = [(0,0),(1,1),(limit-1,limit-1),(limit-1,1)] + samples += [(rng.randrange(limit),rng.randrange(limit)) for _ in range(50)] + for x,y in samples: + got,_=product(x,y,b,k,table) + need(got==expected(x,y), "radix product mismatch") + cases+=1 + bad,_=product(15,15,2,2,build(2),True) + need(bad!=expected(15,15), "carry mutation survived") + print(json.dumps({"status":"PASS","product_cases":cases, + "b_range":[1,6],"k_range":[1,8],"carry_mutation_rejected":True, + "proof_status":"Finite reference replay, not emitted RamStd code or Lean proof."},indent=2)) + +if __name__=="__main__": + main() diff --git a/research/packed-ram-speedup/tabulated_tm.py b/research/packed-ram-speedup/tabulated_tm.py new file mode 100644 index 0000000000..a4ef5e3473 --- /dev/null +++ b/research/packed-ram-speedup/tabulated_tm.py @@ -0,0 +1,290 @@ +"""Uniform packed-window TM tabulation: exact bounded-word operational model. +Dugongue with substantial OpenAI Codex assistance. Apache-2.0. +No word multiplication/division, no timing oracle and no pre-supplied table. +This is not a Lean certificate or a fully emitted RamStd instruction program. +""" +from collections import defaultdict +from random import Random +import json + + +def need(ok,msg): + if not ok: raise ValueError(msg) + +class Words: + def __init__(self,w): + self.w=w; self.mask=(1<>b + def band(self,a,b):self.ops+=1;return a&b + def bor(self,a,b):self.ops+=1;return a|b + def bnot(self,a):self.ops+=1;return self.mask^a + def load(self,a):self.ops+=1;self.fit(a);return self.mem[a] + def store(self,a,x):self.ops+=1;self.fit(a);self.fit(x);self.mem[a]=x;self.high=max(self.high,a) + def test(self,a,b):self.ops+=1;return a==b + def tick(self):self.ops+=1 + +class Tabulator: + def __init__(self,k,A,Q,delta,r,w): + need(k>=1 and A>=2 and Q>=1 and r>=1 and r&(r-1)==0,'machine/epoch contract') + self.k,self.A,self.Q,self.delta,self.r=k,A,Q,dict(delta),r + for (state,reads),(nq,writes,moves) in self.delta.items(): + need(0<=statemax(self.keybits+self.rowlog+10,c*self.B+1),'finite-word table contract') + self.v=Words(w);self.symbol_mask=(1<=L:return v.band(low,mask) + rest=v.load(self.address(tape,v.add(block,1))) + remaining=v.sub(L,available);bits=v.shl(remaining,self.flog);restmask=v.sub(v.shl(1,bits),1) + return v.band(v.bor(low,v.shl(v.band(rest,restmask),v.shl(available,self.flog))),mask) + + def put_window(self,tape,start,window,length=None): + v=self.v;L=self.L if length is None else length + need(1<=L<=self.B,'packed chunk length') + block=v.shr(start,self.blog);j=v.band(start,self.B-1) + available=v.sub(self.B,j);count=min(available,L);v.tick() + bits=v.shl(count,self.flog);shift=v.shl(j,self.flog);mask=v.sub(v.shl(1,bits),1) + addr=self.address(tape,block);clear=v.shl(mask,shift) + result=v.bor(v.band(v.load(addr),v.bnot(clear)),v.shl(v.band(window,mask),shift));v.store(addr,result) + v.tick() + if available>=L:return + count=v.sub(L,available);bits=v.shl(count,self.flog);mask=v.sub(v.shl(1,bits),1) + addr=self.address(tape,v.add(block,1));rest=v.shr(window,v.shl(available,self.flog)) + v.store(addr,v.bor(v.band(v.load(addr),v.bnot(mask)),v.band(rest,mask))) + + def get_symbol(self,tape,pos): + v=self.v;block=v.shr(pos,self.blog);j=v.band(pos,self.B-1) + return v.band(v.shr(v.load(self.address(tape,block)),v.shl(j,self.flog)),self.symbol_mask) + def put_symbol(self,tape,pos,value): + v=self.v;block=v.shr(pos,self.blog);j=v.band(pos,self.B-1);shift=v.shl(j,self.flog) + mask=v.shl(self.symbol_mask,shift);addr=self.address(tape,block) + v.store(addr,v.bor(v.band(v.load(addr),v.bnot(mask)),v.shl(value,shift))) + + def macro(self,q,heads): + v=self.v;before=v.ops;key=q;keyshift=self.s + for i in range(self.k): + window=self.get_window(i,v.sub(heads[i],self.r)) + key=v.bor(key,v.shl(window,keyshift));keyshift=v.add(keyshift,self.wbits) + address=v.add(self.tablebase,v.shl(key,self.rowlog));row=[] + for _ in range(2*self.k+3):row.append(v.load(address));address=v.add(address,1) + for i in range(self.k): + self.put_window(i,v.sub(heads[i],self.r),row[3+i]) + heads[i]=v.sub(v.add(heads[i],row[3+self.k+i]),self.r) + need(v.ops-before<=250*(self.k+1),'constant-cost macro envelope') + return row[0],heads,bool(row[1]),row[2],v.ops-before + + +def reference_step(q,heads,tapes,delta): + symbols=tuple(tapes[i].get(heads[i],0) for i in range(len(heads))) + tr=delta.get((q,symbols)) + if tr is None:return None + nq,writes,moves=tr + for i in range(len(heads)):tapes[i][heads[i]]=writes[i];heads[i]+=moves[i] + return nq + + +def uniform_parameters(n,k,A,Q,d=2,a=8): + """Fixed-machine polynomial-envelope constants d,a; no execution-time input. + Target implements integer scaling by fixed constants with repeated addition. + The power-of-two divisions below are shifts. n is a supplied bit-length header. + """ + need(n>=0 and k>=1 and A>=2 and Q>=1 and d>=1 and a>=8,'uniform parameter contract') + lam=(n+2).bit_length()-1;ell=lam+1 + c=1 + while (1<>denominator_log;r=1<=3,'packed binary codec needs blank and two distinct bit symbols') + n=sum(length for _,length,_ in inputs.values()) + para=uniform_parameters(n,k,A,Q,d,a) + r=para['epoch'];w=para['width'] if word_width is None else word_width + need(w>=para['width'],'caller word width below uniform sufficient bound') + need(0<=output_tape=0,'output protocol') + sim=Tabulator(k,A,Q,delta,r,w);codec=codec_type(r,sim.c,w) + # Reserve explicit distinct codec banks before data; source lists model those + # bounded arrays. The generic proof also allocates IO/descriptor banks. + codec_words=(1<<((r<16*((n+2)**2+para['epoch']+n+1),'polynomial origin') + need(para['width']>para['keybits']+(2*k+2).bit_length()+10,'uniform table width') + if para['lambda_floor']>=max(64*(1<<(k-1).bit_length())*para['field_bits'],128): + need(16*para['keybits']<=para['lambda_floor'],'sublinear full-table budget') + parameter_cases+=1 + return {'uniform_parameter_cases':parameter_cases,'status':'PASS','machine_cases':cases,'macro_boundaries':boundaries,'TM_transitions':transitions,'precomputed_rows':tables,'maximum_macro_word_operations':max_macro,'maximum_setup_word_operations':max_setup,'dirty_window_frames':frames,'nonhalting_macros':30,'mutated_table_detected':True,'undersized_word_rejected':True,'word_mul_or_div':False,'scope':'exact finite operational model; not emitted RamStd code, Lean proof or improved TM kappa'} + +if __name__=='__main__':print(json.dumps(check(),indent=2)) diff --git a/research/packed-ram-speedup/verify.py b/research/packed-ram-speedup/verify.py new file mode 100644 index 0000000000..225dcf589c --- /dev/null +++ b/research/packed-ram-speedup/verify.py @@ -0,0 +1,25 @@ +"""Authenticated exact finite checks; Dugongue with OpenAI assistance; Apache-2.0.""" +from pathlib import Path +import hashlib,json,subprocess,sys +ROOT=Path(__file__).resolve().parent + +def need(ok,msg): + if not ok:raise ValueError(msg) + +def main(): + pins=json.loads((ROOT/'CONTENT-HASHES.json').read_text(encoding='utf-8')) + files={f.relative_to(ROOT).as_posix() for f in ROOT.rglob('*') if f.is_file() and '__pycache__' not in f.parts} + need(files==set(pins)|{'CONTENT-HASHES.json'},'Package inventory drift') + for name,digest in pins.items():need(hashlib.sha256((ROOT/name).read_bytes()).hexdigest()==digest,'Source drift: '+name) + reports={} + for name in ['tabulated_tm.py','packed_codec.py','tabulated_multiply.py','end_to_end.py']: + run=subprocess.run([sys.executable,'-I','-O','-B',str(ROOT/name)],capture_output=True,text=True,encoding='utf-8',timeout=120) + need(run.returncode==0,name+' failed: '+run.stderr[-2000:]);reports[name]=json.loads(run.stdout) + need(reports[name]['status']=='PASS',name+' did not pass') + m=reports['tabulated_tm.py'];c=reports['packed_codec.py'];e=reports['end_to_end.py'] + need(m['machine_cases']==224 and m['nonhalting_macros']==30 and m['mutated_table_detected'] and m['undersized_word_rejected'],'TM coverage/control missing') + need(c['packed_io_cases']==4277 and c['corrupted_decoder_controls']==7,'Codec coverage/control missing') + need(e['input_pairs']==16 and e['real_TM_halting'] and e['packed_contiguous_window_IO'] and not e['all_length_multiplier'],'Finite composed fixture scope mismatch') + print(json.dumps({'status':'PASS','scope':'Authenticated finite operational models and bounded composed fixture; informal universal proofs; no new TM kappa or Lean audit','reports':reports},indent=2)) + +if __name__=='__main__':main()