diff --git a/research/wordram-double-twiddles/CREDITS.md b/research/wordram-double-twiddles/CREDITS.md new file mode 100644 index 0000000000..cf447c9ad1 --- /dev/null +++ b/research/wordram-double-twiddles/CREDITS.md @@ -0,0 +1,10 @@ +# Attribution and exposure + +Prepared for ToikY with substantial source-aware OpenAI Codex proposal/integration, refinement/checker implementation, mathematical/code challenge, overlap and metadata assistance. Root/scouts read provisional recipes and exact source prose/code, including the original6802verifier, before claim19447201. No constructor/import/interpreter/site census/operand experiment preceded that claim. No blind discovery, independent human, proof-kernel or independent-end-to-end verification is asserted. + +- Nick Petalas/petalas6802, headb792a58669a3bd2372a38db567ba04241b562519: unit-twiddle transformer, complete VALUE/TEMP identity, literal macro/lifetime gates, relocation, existing counts/tests and released known-nonunit question. Its47,523unit saving and old finite census remain prior work. Its exact unit transformer actually executed before the new pass. +- David Ganz/Dugongue5466: original bounded64-bit Word RAM multiplier/ISA/NTT schedule, setup/range, original admitted-input correctness, constants, carry/cleanup and exact-count contract. Its builder/runtime actually executed as authenticated predecessor code; its complete theorem/checklist is not independently audited here. +- Nick Petalas5886and6435: distinct address/liveness allocation and optimized-assertion portability. Neither is silently composed, rerun or credited as a new arithmetic gain. +- Shilun-Allan-Li/tcslib, including retained Anthropic/PBC formal-math attribution; Thomas Ahle/FastPoly; Bas Spitters/CatCrypt; Brett Saiki/mpfx; original compiler/multiplication authors and notices remain credited. Preserve root Apache-2.0 LICENSE/NOTICE and the additional source NOTICE; upstream interfaces are not claimed rebuilt/imported as Lean libraries. + +Constant specialization, arithmetic reduction, write-lifetime reasoning and block simulation are classical. Written scoped proof and first finite corroboration complete:31inverse sites,additional1395static/930executed saving,4.108s/220.625MiB. Authenticated source builder/unit pass/ISA actually executed as credited components; old broad verifier was fetched/read inertly and not imported/run. Unit47523is prior theorem association, not a newP0whole comparison. The formal-interface card is changed/partial, with no Lean/native/selected-consumer/full-invoice/all-five-assumption admission or optimality claim. diff --git a/research/wordram-double-twiddles/LICENSE b/research/wordram-double-twiddles/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/wordram-double-twiddles/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/wordram-double-twiddles/NOTICE b/research/wordram-double-twiddles/NOTICE new file mode 100644 index 0000000000..59d8e0cf31 --- /dev/null +++ b/research/wordram-double-twiddles/NOTICE @@ -0,0 +1,415 @@ +A sharper exponent for integer multiplication +Copyright 2026 Douglas Colkitt + +This project includes unmodified source files from OpenAI's manuscript +"Integer multiplication below n log n" and its accompanying repository: +https://github.com/openai/math +Commit: adc7f1241b42e322a6451854ab7e4b4c146bf78a + +The original manuscript identifies OpenAI as its author. Its Apache-2.0 +license is retained at upstream/LICENSE. The exact source URLs and hashes +are recorded in upstream/manifest.json. Proposed modifications are supplied +as separate files under patches/; upstream source files remain unchanged. + +The original local research note, scripts, certificates, patches, and +documentation were prepared by Douglas Colkitt with assistance from OpenAI +Codex. The community release incorporates work by the contributors identified +in the notices below; it is not solely Douglas Colkitt's work. +This project is not an official OpenAI release or an OpenAI endorsement. + +Related contributions (not imported in this checkpoint): +Zhihao Chen (jacklightChen), PR #7, supplied an earlier ternary five-subset +motif, finite-alphabet transfer and a different compressed producer: +https://github.com/CrocSwap/integer-mult-bounds/pull/7 +The present checkpoint claims no priority for that motif. Related compressed +complex-network work was submitted by eumemic in PR #3: +https://github.com/CrocSwap/integer-mult-bounds/pull/3 +The pending contributions and their stronger bounds require their own review; +this notice does not represent adoption or verification of their claims. + +Additional community work, including parallel and superseded submissions, is +acknowledged in CONTRIBUTORS.md, with pinned submission metadata in +docs/research/contribution-snapshot.json. These acknowledgements do not imply +joint authorship of the checkpoint, incorporation of pending code, or verification +of submitted mathematical claims. Original source-specific notices remain in force. + +Community release (accepted by conditional maintainer audit): +The following original contributor notices apply to the imported PR #39 chain. +The preceding non-import statements describe the preserved 2^-30 checkpoint. + +Ternary five-subset construction and common-four-point resynthesis +Copyright 2026 Zhihao Chen (jacklightChen) + +This is Zhihao Chen's first submission of this specific construction to this +repository. Research, proof development, code and verification were prepared +with substantial assistance from GPT-6 Astra (OpenAI Codex), as identified by +the contributor. This is not independent review or an OpenAI endorsement. +Future research building on this contribution should explicitly acknowledge +Zhihao Chen (jacklightChen), cite the accompanying note and pull request, and +retain the preceding contributors' attribution. This notice records research +provenance; the repository's Apache-2.0 license remains unchanged. + +Dependencies retained from eumemic's Claude-assisted PRs #3 and #5: +https://github.com/CrocSwap/integer-mult-bounds/pull/3 +https://github.com/CrocSwap/integer-mult-bounds/pull/5 +PR #5 commit: d3d370c34937503bd3fa63c83d505a05e8e50893 +These include complex_circuit.py, complex_network.py, fast_gaussian.py, +their generators, construction notes and certificates. The Gaussian input +scaling proof is corrected in this derivative; see the modification notice below. +Aligned pairing also appears in Bortlesboat's PR #2. Retained totals and bank +sharing appear in dleen's PR #4 and cheaper retained centers in eumemic's PR #6. +Their results and ideas are credited separately from this new construction. + +Bulk recursion and controlled tensor basis, 8 October 2026 +Copyright 2026 icekylinx + +The new projector batching, controlled simultaneous basis, mixed-width tape +recursions, whole-residual complex recursion, and dependency-path precision +guard in the batched-23 proof package are contributed by icekylinx, developed +with substantial OpenAI GPT-6 Astra assistance. Review corrections and +repository integration were prepared with OpenAI Codex assistance. They build on the retained +PR #7 finite producers and the preceding contributions credited above. +The new package retains the repository's Apache-2.0 license and the original +authors' attribution. It is not an official OpenAI release or endorsement. + +Modification notice, 8 October 2026 (icekylinx): the retained fast Gaussian +proof now bounds shifted approximation error by F=2^ceil(1.14 alpha^2). +The P=34p precision budget and asymptotic exponent are unchanged. New batching +checks are integrated into make verify. Existing attribution and licenses +are retained. + +Partial-swap extension, 8 October 2026 +Copyright 2026 icekylinx + +The partial-swap framing, binary retained-total triple construction, +dependency-preserving positive labels and carrier reuse, unequal (25,23,57) +common basis, improved complex batching, and exact assembly are contributed +by icekylinx with substantial OpenAI GPT-6 Astra and Codex assistance. +This extension directly inherits PR #10, commit +62691e395a0458ce089a1c7b5d89e74291e95e29. The portable producer adapters +modify the retained paired-exclusion and shared-point implementations credited +above. The original licenses, attribution, and Gaussian correction are retained. + +Endpoint-gauge extension, 8 October 2026 +Copyright 2026 icekylinx + +The complementary auxiliary endpoint gauges, (32,30,40) controlled basis, +general nondegenerate binary phase residuals, retained-center complex producer, +updated path guard and exact assembly are contributed by icekylinx with +substantial OpenAI GPT-6 Astra and Codex assistance. This extension inherits +f2ab41aebad47861caf6316282c1793e5513845e and its PR #10 ancestry. New portable +adapters retain the paired-exclusion and shared-point contributions credited +above. Original licenses, notices and the Gaussian correction are retained. + +Structured-basis and semantic-bulk extension, 8 October 2026 +Copyright 2026 icekylinx + +The selected (32,30,36) bit construction, A1/A5 block refinements, fixed +middle-axis I+J profiles with bounded-minor CRT certificates, mixed dyadic +complex centers, complete data-front batching and circuit-specific assembly +are contributed by icekylinx with substantial OpenAI GPT-6 Astra and Codex +assistance. The immediate parent is ed90fd940279c336ebc45968631bdebfb087b505. + +The semantic/bulk compatibility argument, literal scalar charge, product row +stock and parameterization adapt Zhihao Chen (jacklightChen)'s PR #23, +commit 661ebabc1076c9f525d7ce4967c876b203fa9827. Translated complex endpoints +are adopted from the same contributor's PR #21, +commit 5ba6cf0bfb68f2be8d15610e7972207c50254d6a, following eumemic's source-frame +work and the earlier nested-basis contributions. + +Completed-child semantic precision, arbitrary-coordinate routing, phase-cell +Gaussian inversion and bulk tape transfer are credited to the RaD project +(hipotures), commit 45d9b60355872041f9275f77c057514def0d45bc, exposed through +PR #20 at 4f8d6c8272b5ff307a0da51df545ec3cd96a8b6e. Their selected proof +sources retain their separate CC0 license and original NOTICE under +references/semantic-bulk/rad20. The PR #23 source retains its recorded OpenAI +Codex assistance; RaD retains its recorded Codex and GPT-6.1-Sol Ultra +assistance. These are source attributions, not claims about this session's +runtime model. Related contributions by Rohan Arun and Aurel Prosz remain +acknowledged in the imported notices. No exclusive priority or additional +license condition is asserted. + +Copied retained-center extension, 8 October 2026 +Copyright 2026 icekylinx + +The copied retained-center schedule in both orientations, its complex-phase +transfer, the Wm-N+L rank budget, and the selected (25,23)/(28,28) composition +are contributed by icekylinx with substantial OpenAI GPT-6 Astra and Codex +assistance. This extension inherits PR #32 at +0ef3aeb61f55cc0b321ce6a0ef00acee25cefe52 and the preceding PR #10/#18/#24 work. + +The two-stage topology and paid copied-stream endpoint correction are due +to Aurel Prosz (Paureel), c82d09eb4781b68435e3fa3eb6beea72fa900fab, +through Zhihao Chen (jacklightChen)'s PR #29 unequal-axis composition, +9d963275075fa98f1da821e27757b238dafd6b3c. That source also credits Swapnil +Jain's two-stage development at ae405eb474d1486b2d8aef90139869f927f4836a. + +The contiguous corner method, incidence factorization and exact partition +certificates are due to Rohan Arun (PR #31), method commit +02f68f95369c39955c5ffcfddbd75cd83e26b305. The selected (25,23) certificate +specializes Dominik Scholz's parameterization (PR #33), +a499a345c040aa15b68e984a0904eadc485c7a7e. Their source notices and proof +snapshots are preserved in references/copied-centers. Historical OpenAI +Codex, GPT-6 Astra and Anthropic Claude Opus 5.5 assistance is credited to +the respective imported sources. Existing PR #21/#23 and RaD attribution, +licenses and the Gaussian correction remain in force. + +Copied centers with reversed (23,25) data corners, 2026-10-08 +Rohan Arun with substantial OpenAI Codex assistance supplies the composition, +exact dimension23 controls and cost/assembly integration. James Chang's PR34 +supplies the reversed boundary family; icekylinx's PR36 supplies copied retained +centers and the selected complex graph. The balanced assembly remains attributed +to RaD/hipotures and its PR34 specialization. Retain Dominik Scholz PR33, Rohan +Arun PR31, Zhihao Chen PR29/21/23, Paureel/Aurel Prosz, Swapnil Jain, icekylinx, +eumemic, Douglas Colkitt, OpenAI and all earlier notices and hypotheses. +This is not a claim of formal verification, new foundational rank identities, +global optimality or measured runtime speedup. + +Fixed middle basis with copied reversed corners (2026-10-08): +Rohan Arun, with substantial OpenAI Codex assistance. Composition and +simultaneous-basis proof retain icekylinx PR32/36, James Chang PR34, +Dominik Scholz PR35/38, Zhihao Chen, Paureel, Swapnil Jain, RaD/hipotures, +eumemic and all preceding attribution and licenses. See research/copied-fixed-reversed. + +Changed-graph composition with copied centers and fixed bases, 8 October 2026 +Prepared with OpenAI Codex assistance. +The new composition uses icekylinx PR36 copied centers and PR32 fixed-I+J +projectors/profiler, Dominik Scholz PR35 two fixed factors and CRT argument, +Zhihao Chen (jacklightChen) PR29/23 interfaces, Aurel Prosz (Paureel) and +Swapnil Jain's two-stage development, Rohan Arun PR25/31 corner methods, +Dominik Scholz PR33/38 dimension/composition work; James Chang (jamesyc) +PR34 reversed geometry and balanced transfer; Rohan Arun PR37/39/40 +reversed integration, modular data tests and both-fixed baseline; +RaD (hipotures) PR41 changed scalar DAGs, alternating point order and +independent role compiler; RaD balanced routing/bulk interfaces, and all +retained predecessors. +Complete attribution and the conditional proof boundary are recorded in +research/copied-fixed/PROOF.md; imported originals and source pins are retained. +Original Apache-2.0 and CC0 notices remain applicable. + +Community follow-up integration (PRs #49, #45 and #26), 8 October 2026: +Rohan Arun contributes weighted carrier matching and climbed summand/leave-one-out +orders (PRs #44/#47/#49), with Anthropic Claude assistance. The final construction +composes Chafik Boukhalfa's changed-graph checks, exact rational data recovery and +reordered exclusion sums (PRs #43/#46/#48, OpenAI Codex assistance) with RaD / +hipotures's alternating pair order and independent physical role compiler (#41). +All predecessor attribution and conditional proof interfaces remain in force. + +Alejandro Zarzuelo Urdiales contributes Gaussian parity and canonical arithmetic +proofs, finite tensor execution, profile precision accounting and mixed-center +reference checks (#45), with substantial OpenAI Codex assistance. See +research/gaussian-parity-synthesis/PROVENANCE.md for his full attribution. +Ryan S / princezuda contributes historical Lean certificate arithmetic, algebraic +frame/movement/guard lemmas and independent paired-circuit checks (#26). Original +source notices and historical snapshots are preserved. Neither formal package +claims a full formal proof of the multiplication algorithm or a new kappa. + +Joint frame compilation of skip-prefix strips + +The local compiler and exact finite witnesses were prepared by eumemic with +substantial OpenAI Codex assistance. Avi Eisenberg / ikeboy with Anthropic +Claude assistance supplied the unmodified PR #53 skip-prefix producer. +The pinned PR #48 pipeline is Chafik Boukhalfa's contribution, incorporating +Rohan Arun, RaD / hipotures, icekylinx, Dominik Scholz, James Chang, +Zhihao Chen, Aurel Prosz / Paureel, Swapnil Jain, eumemic, Douglas Colkitt, +OpenAI, David Harvey, Joris van der Hoeven and the earlier contributors +credited in the retained sources. See references/frame-compiler/pr48/NOTICE +and references/frame-compiler/pr53/NOTICE for their original attribution. +No authorship or review by those predecessors is claimed for this compiler. + +Joint dual-skip/frame-compiler composition (2026-10-08) +--------------------------------------------------- +Rohan Gupta / gupt1156 with Anthropic Claude assistance: PR55 dual-skip +scalar graph; original LICENSE and NOTICE are retained under +references/frame-compiler/pr55. eumemic with substantial OpenAI Codex +assistance: PR57 joint reversible frame compiler, serialized physical-word +replay and profile reconstruction. Chafik Boukhalfa with OpenAI Codex +assistance: this composition, independent integration and exact certificate. +Avi Eisenberg / ikeboy, Rohan Arun, RaD / hipotures, icekylinx, and all +predecessor authors retain the notices above and in pinned source files. +No original copyright or Apache-2.0 notice is removed. + +Ranked reclamation after the PR58 joint-dual composition (2026-10-08) +---------------------------------------------------------------- +Chafik Boukhalfa with OpenAI Codex assistance: prioritize retired physical +slots by descending current frame rank, retaining slot ID as the tie-breaker; +complete replay, exact profiles, comparison and adversarial controls. +The dedicated joint_dual_reclaim_compiler.py is derived from eumemic's PR57 +compiler. Its original shared compiler remains byte-identical. The PR55 +producer and all preceding attribution remain unchanged. The complete PR58 +comparison certificate and its original source/proof provenance are retained +under references/frame-compiler/pr58. + +Skip-prefix strip producer, 8 October 2026 +By Avi Eisenberg (ikeboy), with Anthropic Claude (Claude Opus 5.5) +assistance. The skip-prefix leave-one-out strip layout in +research/skip-strips/skip_graph.py is new. Everything else reuses Chafik +Boukhalfa's PR #43/#46/#48 research/copied-fixed pipeline, its verification +code, exact data recovery and support-order sorting, together with: +- Rohan Arun's PR #44 weighted carrier matching optimizer; +- RaD (hipotures) PR #41 alternating point order; +- every predecessor credited above. +Complete attribution and the conditional proof boundary are recorded in +research/skip-strips/PROOF.md. Original Apache-2.0 and CC0 notices remain +applicable. + +Local split-pair skip-prefix research continuation (2026-10-08) +Prepared with substantial OpenAI Codex assistance at the user's request. +New contribution: singleton/pair recursive partition refinement, finite summand +order and moment search, and verified composition with inherited paid clones. +Avi Eisenberg/ikeboy with Anthropic Claude assistance: PR53 skip-prefix strips. +Chafik Boukhalfa with OpenAI Codex assistance: PR54 original-envelope clone +specialization and PR43/46/48 checking interfaces. RaD/hipotures: PR51 +whole-chain/source-partition cloning and earlier producer/interfaces. +Rohan Arun: PR44 weighted matching and earlier fixed/reversed work, with all +stated historical AI assistance. All predecessor notices remain applicable. + +Original-envelope whole-chain clones on skip-prefix strips (research/skip-clones): +Chafik Boukhalfa, prepared with OpenAI Codex assistance. The complete-chain +source-partition clone operation is adapted from RaD / hipotures, PR #51, +with original envelopes retained here. The scalar base is Avi Eisenberg's +PR #53 skip-prefix layout, prepared with Anthropic Claude assistance. +All credited PR #43/#46/#48, PR #44 and earlier code/proof notices remain +in force. This extension is provided under the repository's Apache-2.0 terms. + +Community review checkpoint #50–#61, 8 October 2026 +Maintainer integration and independent arithmetic: Douglas Colkitt, with OpenAI Codex. +Avi Eisenberg / ikeboy: skip-prefix strip framework (#53), with Anthropic Claude. +Rohan Gupta / gupt1156: parallel order search (#50, stated Antigravity assistance) +and dual-suffix strips (#55, Anthropic Claude assistance). +Eumemic: equal-frame joint compilation and paid signal reclamation (#57), with Codex. +Chafik Boukhalfa: original-envelope paid clones (#54), composition (#58) and ranked +reclamation (#60), with Codex. Rohan Arun: order search (#52) and positive-frame +composition (#56), with Anthropic Claude and stated Codex validation assistance. +RaD / hipotures: enlarged frames, source partitions and paid whole-chain clones +(#51), with Codex. Rohan Garg / rohangar1: singleton/pair recursion and paid-clone +composition (#59), with Codex. Alejandro Zarzuelo Urdiales: exact parameter +refinement, scoped Lean arithmetic, matrix/parity and search tools (#61), with +his disclosed multi-tool and Codex assistance. +Parallel #50/#52 records are reviewed and credited without replacing the earlier +climbed-48 implementation; their exact commit history is retained. The separate +#51 witness is retained as research; its source-graph/negative-basis data proof +has not received the same full replay as #56's consumed compiler machinery. +See docs/research/community-round2-review.md for precise validation boundaries. +All earlier licenses, contributions and notices remain applicable. + +Interval strips and core-aware pair assembly + +The interval leave-one-out strips and the core-aware group-pair assembly in +research/pair-assembly were prepared by Avi Eisenberg / ikeboy with Anthropic +Claude assistance. They build on PR #53's skip-prefix pipeline and its +inherited PR #48 sources. The stacked witness in research/pair-assembly/frame +uses eumemic's PR #57 joint frame compiler unchanged; its driver and verifier +are adaptations of PR #57's skip_frame_compiler.py, skip_frame_compose.py and +verify_skip_frame.py. Original notices are retained. + +Stopped product-ring extension, 9 October 2026 +Copyright 2026 icekylinx + +The opposite-bank generic projector factorization, componentwise atom-ring +adapters, stopped recurrence and outer ordinary-interchange conversion, +aligned pair-star producer with rational centers, exact denominator-21 +grid and selected (23,23)/(24,24) composition are contributed by icekylinx +with substantial OpenAI GPT-6 Astra and Codex assistance. This extension +builds on merged PR #36, 11817ccacb564bb7f98789c20dc11d3fece207e3, and is +integrated on upstream main 56b66d58297deca1d7dd130247d720e960f77a37. + +The retained ordinary leaf uses the preceding projector, corner and +copied-center proofs. The selected two-stage topology retains Aurel Prosz +(Paureel), Swapnil Jain and Zhihao Chen's credits; the semantic assembly +retains PR #21/#23 and RaD's attribution. Paired producers, carrier matching, +original source notices and each imported license remain unchanged. + +Partial-gauge extension, 9 October 2026 +Copyright 2026 icekylinx + +The pair-first cube assembly, compatible backward frame enlargement, +partial source-gauge schedule and stopped whole-projector composition are +contributed by icekylinx with substantial OpenAI GPT-6 Astra and Codex +assistance, extending PR #104 at 948ce1510df750f4c18b96bdaef436a86f8bf834. + +The physical deferred bit word, reflected event accounting, fan-order +clarification and signed two-stage endpoint are adopted from Zhihao Chen +(jacklightChen), PR #97, e15350b66e4bf796153a68c240a6cc1b788abe3e, with +Codex assistance. Its deferred readouts, V leaves, lifted frames and frozen +witness originate in Swapnil Jain's 741e7aa078392553815df7926ee17ac5e25a8c38, +with the original Claude disclosure retained. Cyclic interval and core-aware +pair primitives build on Avi Eisenberg (ikeboy), PR #62, +ad0f25ff7b23cff7f08ad237c2254e6ecf74257e, with Anthropic Claude assistance. +Prior two-stage, copied-center, ordinary-leaf, semantic/bulk, routing and +precision credits remain in force. Imported source notices and licenses +are preserved under references/partial-gauge/; see SOURCES.json. + +Three-stage cover extension, 9 October 2026 +Copyright 2026 icekylinx + +The arbitrary-subspace Clifford frame theorem, three-stage Cayley geometry, +weighted q-adic GL cover, unit-lower weighted compiler, charged local-ring +fallback, uniform batching, internal row borrowing and exact composition +are contributed by icekylinx with substantial OpenAI GPT-6 Astra assistance. This +repository integration uses Codex assistance and extends +PR #115, cf60442983c153a3a0f5272ea4713f99eba13c86. + +The selected local complex DAG and support/label replay are adopted from +Copyright 2026 eumemic, PR #117, cbb05ce504d571546d9b7794c186a613c659c3bf, +with its original Apache-2.0 terms and Claude assistance disclosure. +The unchanged bit physical word retains Zhihao Chen (jacklightChen), +PR #97, and Swapnil Jain's underlying witness and assistance notices. +The prior opposite-bank, stopped ordinary-leaf, copied-center, topology, +semantic/bulk, precision and analytic credits remain applicable. +Original source notices and license bytes are preserved in +references/three-stage-cover/pr117/ and references/partial-gauge/. + +Paired-cube and shared-core extension, 9 October 2026 +Copyright 2026 icekylinx + +The paired-coordinate triple-cube identity, signed overlap channels, +original-source involution, coordinate-star centers, concrete frame/carrier +compiler, chronological source gauges, PR97 gauge-subset selection, +orthogonal cross-stage routing and exact supplier/assembly integration +are contributed by icekylinx with substantial OpenAI GPT-6 Astra assistance. +Repository integration uses Codex assistance and extends PR #130 at +6a9970a530119174507904e23592fd59ede19a5d. + +The substantial completed-core workspace-sharing principle is credited to +an664, PR #128, 530588a019b4a74f09180680c9e3961bf649ec89, with its reported +OpenAI Codex assistance. No source code, partition or serialized witness +from that PR is imported. The new routing and paired-motif integration +are described separately and claim no exclusive priority for broad sharing, +paired-coordinate, Fourier or carrier-matching ideas. + +Selected coarse queries restrict the retained eumemic PR #117 positive DAG; +its original Apache-2.0 and Claude assistance notices remain unchanged. +The bit word and original frames retain Zhihao Chen's PR #97 and Swapnil +Jain's frozen witness, notices and historical assistance disclosures. +Earlier generalized Clifford, three-stage, uniform weighted recursion, +ordinary-leaf, semantic/bulk, precision and analytic credits remain in force. +Source-specific license bytes are preserved under references/. + +October 9 recycled-bit integration: +DaysSky (#150), William Porter/hpst3r (#147), Thomas Marchand/Th0rgal (#146), +Rohan Gupta/gupt1156 (#148), James Chang/jamesyc (#124), SovereignSteak (#122). +The original notices and assistance disclosures are retained under research/, +including research/recycled-bit-integration/NOTICE. Andrew Barnes/Bortlesboat +(#101) repairs shared verifiers using rfu08's #64 counterexample. rfu08's +scoped finite and formal-transfer packages are included separately; they do +not establish the full multiplication theorem. Earlier and parallel credits +remain applicable. Douglas Colkitt integrated these with OpenAI Codex assistance. + +SovereignSteak PR151 independently supplies the matching gauge/recycling +composition and the selected 473/10^6 atom refinement; its original package +and assistance disclosure are retained under research/gauge-recycling/. + +October 9 coordinated-frame and completed-entrance-bank integration: +Dugongue PR186, 166a34d75e853e933855f0f7e940fe77c4bb6b8d, builds on +Chafik Boukhalfa/chafreaky's PR181, 7fb2194801e3a10f54772c7f0d5505035a4fc0ad, +and eumemic's PR168 v4, 4a3c769e5c5430e7114c4d3e099ff34664677f17. +The frozen package and prerequisite archive preserve all author, source-license +and assistance notices, including PR175's compiler optimization. DaysSky's +carrier closure, James Chang's terminal substitution and balanced assembly, +geckods' stopping refinements and all preceding framework credits remain. +Rohan Arun's PR185 bootstrap and chafreaky's PR182 bit refinement are reviewed +parallel contributions; their gains are not added to the selected witness. +Douglas Colkitt integrated the package and supplied the bank scheduling +supplement with OpenAI Codex assistance, under Apache-2.0. The all-size +interfaces remain conditional; finite verification is not full formalization. diff --git a/research/wordram-double-twiddles/PROOF.md b/research/wordram-double-twiddles/PROOF.md new file mode 100644 index 0000000000..8e7722cd26 --- /dev/null +++ b/research/wordram-double-twiddles/PROOF.md @@ -0,0 +1,164 @@ +# A full-state constant-two refinement after the unit pass + +Prepared for ToikY with substantial source-aware OpenAI Codex assistance. +Apache-2.0. Constant specialization and block simulation are classical. +The exact predecessor programs, proofs and notices are credited in CREDITS +and bound by SOURCE-PINS. Their original multiplication theorem is a premise, +not a theorem independently re-audited here. + +## 1. Fixed caller and comparison + +Fix the authenticated producer's fused template with s=t=256 hexadecimal +digits, n=512, p=65537 and 64-bit modular Word RAM. Inputs are arbitrary +admitted digits0..15; owned scratch, temporaries and output cells may start +dirty. Arbitrary exterior memory and both operands are part of the frame. +The ISA is the source's literal one/add/sub/mul/load/store/bltz/accept/reject +model. There is no introduced shift, division or remainder instruction. + +Let P0 be that exact emitted producer program. Let P1 be Nick Petalas6802's +authenticated unit refinement applied to P0. Its complete-state correctness, +producer coefficient/setup invariants and executed-initializer/control facts +are cited premises. P1 is the comparison baseline for the NEW refinement. +The existing unit saving is not included in our new saving. No address- +allocation pass, changed instruction tariff or native BIT model is composed. + +At a transform butterfly, the producer supplies a residue b with0<=b=1, threshold_i>=2p>z. Its subtraction +is strictly negative and has magnitude below2^32. The stored modular word +therefore has the intended negative signed interpretation. Its branch is +taken, its copy is skipped, and VALUE remains z. All fifteen groups have +this behavior; none supplies a hidden reduction of VALUE. + +Their successive TEMP values are overwritten by the retained final group. +That final subtraction has signed value z-p in[-65537,65535]. The branch +skips its copy exactly when z=p and0 otherwise. The generic block executes +1+2*15+2+delta=33+delta instructions; the replacement executes3+delta. +It thus saves exactly45 static and30 executed instructions for EVERY +admitted b. The original MUL and last conditional copy remain charged. +No scratch clearing, constant synthesis, setup or exit instruction is free. + +## 3. Identifying actual constant-two blocks + +The source-bound transformer checks the direct-address instruction grammar, +forward branch targets and terminal accept. Its complete write inventory +recognizes a coefficient cell only if its three writes are one(cell), the +immediately following add(cell,cell,cell), and a final sub(cell,cell,cell). +It checks that each matched use is after both initializer instructions and +that the entire49-instruction macro lies before the clear. There is no +intervening write to that cell. In the authenticated producer, initialization +executes before use and all setup/range facts above hold. These are explicit +premises, not consequences of the grammar check on arbitrary programs. + +Only MUL into the retained VALUE cell qualifies. The following entire generic +macro, including each threshold, data operand and old internal branch target, +must match exactly. Operand/scratch alias exclusions apply. Inverse scales +and pointwise products write other fresh cells and are unchanged. Constant +pool reuse elsewhere is not a separate rewrite target. P1's unit blocks and +these coefficient-two blocks are disjoint: their authenticated coefficient +values differ. Their already charged initializers and final clears remain. + +Actual coefficient addresses, site counts and emitted-program hashes are +generated evidence, not assumptions silently borrowed from6802's unit census. +The result concerns this one fixed512 template, not every length pair or an +unrestricted constant optimizer. If no qualified site exists, there is no +positive caller saving to report. + +## 4. Label relocation and full-program simulation + +Partition P1 into qualifying49-instruction blocks and unchanged singleton +instructions. Map each original block entry to its new instruction index. +Every surviving old branch must target an entry represented by this map. +A surviving external branch into ANY removed block interior is rejected. +The new retained BLTZ targets the MAPPED OLD EXIT at old_pc+49; it is not +left at its old numeric offset or relocated twice as a new-coordinate label. + +The replaced block's internal high-threshold branches are deleted. Their +behavior on admitted entries is exactly the taken/skipped-copy behavior +proved in section2. The retained final conditional branch exits either +directly or after its copy, in both cases to the mapped next block entry. +Unchanged branches read equal words and therefore take equal outcomes. +Induction over executed blocks establishes equal complete memory at every +corresponding boundary, hence equal final accept, operands, outputs, owned +cleanup and arbitrary exterior values. + +Every source butterfly MUL is executed once on every admitted input. In the +pinned producer, control is forward-only and branches skip only optional +reduction/carry updates, not initialization or whole butterflies. The cited +unit refinement preserves this fact at corresponding boundaries. The new +structural matcher alone does NOT prove that fact for arbitrary instruction +lists. Together with these exact source-control premises, if r is the actual +number of qualified sites then the new program P2 satisfies + + len(P2)=len(P1)-45r, + steps(P2,input)=steps(P1,input)-30r + +for every admitted input to this fixed template. All setup, pooled constant +construction/reuse, unaffected butterflies, normalization, carrying, clearing +and charged accept remain. Space addresses and the complete memory frame +remain those of P1. The new invoice is incremental to P1, not a recount of +the unit pass or a claim that the source baseline is globally optimal. + +## 5. Evidence boundary and remaining work + +The universal implication is this written local range/full-memory proof plus +block simulation under the authenticated producer premises. A new verifier +must authenticate source bytes before import, inspect the emitted fixed +template, compare local literal execution over all65,537residues, and compare +bounded whole dirty-memory fixtures with meaningful structural and semantic +controls. Actual counts, program hashes, runtime and memory are reported only +after observation. Finite operand fixtures are not exhaustive over all256-digit +inputs and do not independently establish the original NTT/multiplier theorem. + +The exact original producer, unit transformer and ISA interpreter may execute +as credited components of those checks. That is predecessor code/program +execution, even though the old verification suite is not rerun. Source-aware +related AI proof/code review is not blind, human or proof-kernel acceptance. + +There is no all-size paid compiler, native arbitrary-integer multiplication +tariff, selected consumer, physical word-to-bit/routing/storage/precision bill, +or complete supplier admission here. The formal-interface-lemma card remains +CHANGED/partial: no Lean proposition is claimed formalized. All five selected +assumptions remain; no new kappa, frontier/adoption change, global optimum or +merge follows. Credit David Ganz/Dugongue5466, Nick Petalas6802/5886/6435, +tcslib/Anthropic-PBC, Shilun-Allan-Li, Thomas Ahle/FastPoly, Bas Spitters/ +CatCrypt, Brett Saiki/mpfx and the retained original notices and lineage. diff --git a/research/wordram-double-twiddles/README.md b/research/wordram-double-twiddles/README.md new file mode 100644 index 0000000000..199bef2db0 --- /dev/null +++ b/research/wordram-double-twiddles/README.md @@ -0,0 +1,145 @@ +# Save 930 further instructions at constant-two twiddles + +A source-bound program-refinement proof with finite corroboration. In the fixed +fused `s=t=256`, `n=512` bounded Word RAM multiplier, replace 31 constant-two +butterfly reductions **after** Nick Petalas's [#6802 unit pass](https://github.com/CrocSwap/integer-mult-bounds/pull/6802). +The new pass preserves complete memory, including TEMP, and saves exactly +**930 executed instructions on every admitted input**, conditional on the +credited producer/setup/range/control premises. Static length drops by 1,395, +from 435,650 to 434,255. These are additional ISA counts; #6802's existing +47,523 unit saving is predecessor work. + +[PROOF.md](PROOF.md) supplies the written full-domain local identity and +fixed-template block simulation. This is not a new multiplication theorem, +global instruction optimum, all-length optimizer or proof-kernel acceptance. +Only this new scoped package is added; original sources remain unchanged. + +## Exact boundary and cost + +Use David Ganz/Dugongue's [#5466](https://github.com/CrocSwap/integer-mult-bounds/pull/5466) +64-bit modular Word RAM ISA and modulus 65,537. Its bounded multiplication, +residue/setup, executed-initialization and traversal contracts are cited +premises, not independently re-audited. There is no invented shift/div/mod +instruction or native arbitrary-integer multiplication tariff. + +For each eligible residue b in 0..65,536 and coefficient cell containing 2, +the new body retains MUL and the final SUB/BLTZ/conditional copy. The 15 higher +threshold groups always branch past their copies. Four static instructions +replace 49; `3+delta` executed instructions replace `33+delta`, saving 45/30. +Both leave VALUE equal to 2b modulo p and TEMP equal to **unreduced `2b-p` +modulo 2^64**, independent of incoming VALUE/TEMP dirt. In particular TEMP is +not always reduced VALUE minus p. Every exterior word agrees at block exit. + +Complete write inventories bind one initialization, adjacent doubling and final +self-clear. Exact macro/alias/lifetime checks and a once-applied old-to-new +entry map preserve the retained last branch and reject surviving entries into +removed interiors. Source execution/initialization hypotheses are necessary; +the matcher does not certify arbitrary instruction lists from syntax alone. +All setup, literal constants, thresholds, unaffected work, inverse normalization, +carrying, clearing and charged halt remain. No address/liveness pass is composed. + +## Observed fixed-template certificate + +The first new diagnostic passed on CPython 3.12.14 in **4.108 seconds**, with +**220.625 MiB** maximum host RSS, under its 120-second/256-MiB forecast. This +is checker resource use, not a physical workspace bill or elapsed-time speedup +against a predecessor. All 20 package files retained identical before/after hashes. + +The exact emitted source has 31 eligible sites, all in the inverse transform: +16 at width 32, 8 at 64, 4 at 128, 2 at 256 and 1 at 512. The coefficient is +cell 23590; its post-unit writes are at 288639, 288640 and 431300. Every site +records original, post-unit and new PCs, stage/block/exponent, operands and +lifetime. Pointwise products and inverse scales are excluded. + +Normalized-JSON program SHA256 identities: + +- Original producer: `d48881159830fd17c13a244816999136dc1e1ef23f7ee40986ff2e1e546b7534`, 507,701 instructions. +- Post-unit comparison: `2f8c8aa0c2c2cf0d5c8f8d4d6b1ce9a0d423598801d0a2320dee8eba1bbb4559`, 435,650 instructions. +- New program: `43a0fe618b3a03cf6e0550ce0daa76047b5f34c9fdb2e2cdc2f73f8886537928`, 434,255 instructions. + +The unit count 1,533 is regenerated for source binding. Its associated 47,523 +executed saving is the credited theorem's value, **not** a newly executed +original-versus-post-unit whole-program comparison. New whole cases compare +post-unit P1 with new P2. + +## Finite corroboration and reproduction + +The new checker executes literal source-ISA programs for all 65,537 local +residues, with one dirty scratch/exterior pattern per residue, complete memory +and write-frame comparison, independent VALUE/TEMP oracles and exact 30-step +deltas. Arbitrary dirt/exterior preservation rests separately on the written +write-frame proof. The local transcript SHA256 is +`c8e7dc7b9ae30a07444fb714f984d2fe0b0ec315abbbdbc6fd84bbc099e7b236`. + +Three complete fixed-template dirty-memory fixtures passed: + +| Fixture | Post-unit steps | New steps | Additional saving | +| --- | ---: | ---: | ---: | +| Zero | 314,002 | 313,072 | 930 | +| Maximum digits | 343,556 | 342,626 | 930 | +| Declared deterministic patterns | 342,989 | 342,059 | 930 | + +Each checks complete memory/write sets, integer multiplication, cleanup and +operand/exterior preservation. Eight controls pass: six exact-reason structural +rejections (coefficient 3, missing self-clear, threshold, internal branch, +external interior entry, scratch alias), a VALUE-correct/TEMP-wrong execution, +and an actual difference outside the admitted residue domain. The latter +illustrates a necessary premise; it is not rejection of a valid producer input. + +```sh +python3.12 -I -B research/wordram-double-twiddles/verify.py +python3.12 -I -O -B research/wordram-double-twiddles/verify.py +python3.12 -B scripts/research_package.py --package research/wordram-double-twiddles +``` + +The two registered commands have 120-second caps and no dependencies beyond +Python 3.12's standard library. The deterministic stdout receipt binds all +actual package files, exact sources, all 31 sites and fixture/control evidence. +Normal/optimized, committed/exported and hosted outcomes are later delivery +observations and must be checked separately. No runtime Git/network/subprocess +or installation is used. `VERIFY.inputs=[]` means the nine runtime/proof inputs +are package-local, not that no files are read. + +The authenticated original builder, ISA interpreter and unit transformer +**actually executed** as credited components. The original broad #6802 verifier +was fetched/read inertly in preparation and was not imported/run. This is not +code-disjoint end-to-end verification. No nine-template census or exhaustive +256-digit operand/length-pair test is claimed. Related source-aware static +proof/code reviews found no blocker; no blind, human or kernel acceptance follows. + +## Provenance, credit and limits + +[TASK.json](TASK.json) retains the complete canonical formal-interface-lemma +card, explicitly CHANGED/partial: no Lean proposition is formalized and its +original selected-interface gate is unmet. [SOURCES.json](SOURCES.json) binds +canonical provenance; [SOURCE-PINS.json](SOURCE-PINS.json) authenticates nine +local bodies, 51,318 bytes, before imports. Imported module paths must also +match their expected local files. LICENSE/NOTICE and the additional original +source notice are retained. [CREDITS.md](CREDITS.md) distinguishes #6802, +#5466, separate #5886/#6435, tcslib/Anthropic-PBC, FastPoly, CatCrypt, mpfx +and the original compiler/multiplication lineage. + +Substantial source-aware OpenAI Codex proposal, implementation, proof/code +challenge, overlap and metadata assistance is disclosed. Source/provisional +recipe exposure before claim and pre-first provenance/import-origin corrections +are preserved. The first receipt binds initial metadata; later metadata-only +updates must not be described as its original document hashes. + +CPython dynamic allocation, pinned module imports and emitted literal labels +are scoped Power of Ten deviations; no fixed-allocation implementation or +static-analyzer certification is claimed. Host generation is separate from +the emitted ISA bill and does not establish an all-size paid compiler. +Native/physical word-to-bit costs, selected caller/consumer conversion, routing, +storage, precision, ownership/restoration and the complete supplier invoice +remain open. All five selected assumptions remain; no new kappa/frontier, +supplier/adoption change or merge is claimed. Stop at this first verified gain. + +## Open next questions + +1. **Bind one selected consumer with a complete bill.** Name its operand sizes, + word/bit tariff, conversions, constant delivery, layout, precision and + restoration/ownership. The bounded ISA delta cannot supply that contract. +2. **Install only the exact scoped refinement after review.** Retain the source, + site/lifetime/control evidence and post-unit baseline; first review the + emitted fixed template. Other coefficients, liveness composition, asymmetric + lengths and global optimality require separate claims and evidence. diff --git a/research/wordram-double-twiddles/SOURCE-PINS.json b/research/wordram-double-twiddles/SOURCE-PINS.json new file mode 100644 index 0000000000..77d3c8a4e2 --- /dev/null +++ b/research/wordram-double-twiddles/SOURCE-PINS.json @@ -0,0 +1,104 @@ +{ + "schema_version": 1, + "files": [ + { + "local_path": "vendor/PR6802-PROOF.md", + "source_repository": "petalas/integer-mult-bounds", + "source_commit": "b792a58669a3bd2372a38db567ba04241b562519", + "source_path": "research/wordram-unit-twiddles/PROOF.md", + "mode": "100644", + "kind": "proof_or_document", + "bytes": 6396, + "sha256": "dce63dfbf52a1da9b9218878d2d03bfb31d4c3e11aad99cd7edfcc637bcf1946", + "git_blob": "9467bc69fb8ad0316257faa33cf0c4dfe72dc97d" + }, + { + "local_path": "vendor/PR6802-README.md", + "source_repository": "petalas/integer-mult-bounds", + "source_commit": "b792a58669a3bd2372a38db567ba04241b562519", + "source_path": "research/wordram-unit-twiddles/README.md", + "mode": "100644", + "kind": "proof_or_document", + "bytes": 7151, + "sha256": "de6cea5553b5d2e3b22d420e57e8bbbbdb624d1edd625b202bfd9675a15f5f85", + "git_blob": "1088fab13c773b5afced478d56d78d20f557aa4e" + }, + { + "local_path": "vendor/source/NOTICE.txt", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "source_path": "research/wordram-ntt-kernel/NOTICE.txt", + "mode": "100644", + "kind": "proof_or_notice", + "bytes": 529, + "sha256": "c7a35a43ceeca4d0b820c00e5b3c589d119033748a46de91769f284e869ac33b", + "git_blob": "b0dc94cb9d5ed24d2ebddc2eae0f41792a2abe69" + }, + { + "local_path": "vendor/source/PROOF.txt", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "source_path": "research/wordram-ntt-kernel/PROOF.txt", + "mode": "100644", + "kind": "proof_or_notice", + "bytes": 8908, + "sha256": "f1d6549b55337e6704b575806fb6be6cec8bbc9a761a6bf3a320aec40cbee9df", + "git_blob": "d0d0d6486e833fb4711fcdd22a5aaa1853815189" + }, + { + "local_path": "vendor/source/ntt/exact_ntt.py", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "source_path": "research/wordram-ntt-kernel/ntt/exact_ntt.py", + "mode": "100644", + "kind": "program", + "bytes": 5471, + "sha256": "b512200d63c736c5d347247028eb1b1f3431cea44aba01c86f2772910d6b41bf", + "git_blob": "5982128975472dfeb472dbe848c5d3617076662b" + }, + { + "local_path": "vendor/source/ram/PROOFS.txt", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "source_path": "research/wordram-ntt-kernel/ram/PROOFS.txt", + "mode": "100644", + "kind": "proof_or_notice", + "bytes": 8926, + "sha256": "e62d76c0caaa4e24651d2282a7a19cb935c63e16932c90a14cb74182d3934df8", + "git_blob": "21907aa9c4aa4c135a49ff5652bbfa08e722b757" + }, + { + "local_path": "vendor/source/ram/wordram_kernel.py", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "source_path": "research/wordram-ntt-kernel/ram/wordram_kernel.py", + "mode": "100644", + "kind": "program", + "bytes": 5888, + "sha256": "b1a6133e505e5faf5832a5274eea23f96b033257c3d16cc24479c4a4c7059a2e", + "git_blob": "f5c6e00699db701f02c23c0d776f6db9d8a28854" + }, + { + "local_path": "vendor/source/ram_multiplier.py", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "source_path": "research/wordram-ntt-kernel/ram_multiplier.py", + "mode": "100644", + "kind": "program", + "bytes": 4604, + "sha256": "6c3ae23ad90c92741f5a505ae9dd85a4bbaaafb72ebdf50291e07d1ae4c52476", + "git_blob": "09ca74343b741af876043059d0cd0d1db8b393ed" + }, + { + "local_path": "vendor/unit_refine.py", + "source_repository": "petalas/integer-mult-bounds", + "source_commit": "b792a58669a3bd2372a38db567ba04241b562519", + "source_path": "research/wordram-unit-twiddles/refine.py", + "mode": "100644", + "kind": "program", + "bytes": 3445, + "sha256": "5c62f1d7ed451ff7b86172bbe37686975b2a96cfac18b66c5e42acc3bdf1a60a", + "git_blob": "1a0aeb321407517ea0636fc895eb84dceef81248" + } + ] +} diff --git a/research/wordram-double-twiddles/SOURCES.json b/research/wordram-double-twiddles/SOURCES.json new file mode 100644 index 0000000000..bf2aaea016 --- /dev/null +++ b/research/wordram-double-twiddles/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec" + }, + { + "path": "certificates/selected-result.json", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a" + }, + { + "path": "research/wordram-ntt-kernel/NOTICE.txt", + "sha256": "c7a35a43ceeca4d0b820c00e5b3c589d119033748a46de91769f284e869ac33b", + "usage": "provenance", + "git_blob": "b0dc94cb9d5ed24d2ebddc2eae0f41792a2abe69" + }, + { + "path": "research/wordram-ntt-kernel/PROOF.txt", + "sha256": "f1d6549b55337e6704b575806fb6be6cec8bbc9a761a6bf3a320aec40cbee9df", + "usage": "provenance", + "git_blob": "d0d0d6486e833fb4711fcdd22a5aaa1853815189" + }, + { + "path": "research/wordram-ntt-kernel/ntt/exact_ntt.py", + "sha256": "b512200d63c736c5d347247028eb1b1f3431cea44aba01c86f2772910d6b41bf", + "usage": "provenance", + "git_blob": "5982128975472dfeb472dbe848c5d3617076662b" + }, + { + "path": "research/wordram-ntt-kernel/ram/PROOFS.txt", + "sha256": "e62d76c0caaa4e24651d2282a7a19cb935c63e16932c90a14cb74182d3934df8", + "usage": "provenance", + "git_blob": "21907aa9c4aa4c135a49ff5652bbfa08e722b757" + }, + { + "path": "research/wordram-ntt-kernel/ram/wordram_kernel.py", + "sha256": "b1a6133e505e5faf5832a5274eea23f96b033257c3d16cc24479c4a4c7059a2e", + "usage": "provenance", + "git_blob": "f5c6e00699db701f02c23c0d776f6db9d8a28854" + }, + { + "path": "research/wordram-ntt-kernel/ram_multiplier.py", + "sha256": "6c3ae23ad90c92741f5a505ae9dd85a4bbaaafb72ebdf50291e07d1ae4c52476", + "usage": "provenance", + "git_blob": "09ca74343b741af876043059d0cd0d1db8b393ed" + } + ], + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a" +} diff --git a/research/wordram-double-twiddles/TASK.json b/research/wordram-double-twiddles/TASK.json new file mode 100644 index 0000000000..e9fd3df4ca --- /dev/null +++ b/research/wordram-double-twiddles/TASK.json @@ -0,0 +1,125 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Fixed fused s=t=256,n=512 bounded Word RAM template after6802unit refinement; a complete-state constant-two pass at31inverse-butterfly sites preserves memory/TEMP/control under exact source premises and saves an additional1395static/930executed instructions. Written proof and first finite corroboration complete; original formalization/selected-consumer gate remains CHANGED/partial.", + "scope_change_reason": "Take6802released known-nonunit refinement question as one bounded compiler/cost interface. The original formalization gate is unmet: no Lean/kernel proposition, selected native consumer or complete supplier invoice is supplied.", + "scope_key": "636f26dec98e26b296e8", + "seed": "fa17cc5f934b5ae4c05bcf47c44b6b58", + "started_at": "2026-11-06T18:57:11.580102+00:00", + "time_budget_minutes": 120, + "minimum_verification_minutes": 30, + "question": "Does a constant-two macro at actual emitted transform-butterfly sites preserve complete64-bit VALUE/TEMP/frame/control state and yield a positive additional static/executed saving after6802unit refinement?", + "success_rule": "Authenticate actual constant-two presence/orientation and full initialization/write lifetime, source macro/alias/control/relocation; prove complete-state local equivalence and whole-template block simulation under credited original range/setup/correctness premises; corroborate bounded local/full-program cases and report only incremental post-unit gain.", + "stop_rule": "Stop at one fixed512-point refinement or precise failure. No eligible site, failed complete-state/lifetime/control proof or nonpositive additional charged gain means stop/narrow, not switch coefficient/ISA/family. Science cutoff 2026-11-06T20:27:11.580102+00:00; reserve final30minutes through 2026-11-06T20:57:11.580102+00:00 for verification/handoff.", + "method": "Source-aware written range/signed64-bit/block simulation and new bounded checker. Actual all65537local residues and threefixed512dirty wholefixtures executed; exact authenticated original builder/unit transformer/ISA are credited components. Old6802verifier fetched/read inertly, not imported/run. No blind/source-independent/end-to-end acceptance.", + "bottleneck_link": "A real complete-state macro can remove literal bounded ISA work at a released nonunit interface, but an emitted instruction delta is not a selected BIT/native/full supplier invoice.", + "family_decision": "Only the fixed constant-two post-unit maximal template is taken; no nine-template/all-operand/asymmetric census, general optimizer or wider family search. Original formalization/consumer gate remains unmet.", + "outcome": "partial", + "scientific_status": "SCOPED_WRITTEN_PROGRAM_REFINEMENT_WITH_FINITE_CORROBORATION", + "author": "ToikY", + "ai_assistance": "Substantial source-aware OpenAI Codex proposal/integration, refinement/checker, mathematical/code challenge, overlap and metadata roles; provisional recipe and actual source/old-verifier text exposed before claim, with no source/new constructor/import/interpreter/science execution at that stage. No blind/human/kernel/end-to-end acceptance.", + "credit": "NickPetalas6802unit transformer/identity/relocation/counts/tests/nonunit question; DavidGanz/Dugongue5466kernel/ISA/schedule/setup/range/correctness/cleanup; Petalas5886liveness and6435assertion portability separate; Shilun-Allan-Li/tcslib(Anthropic/PBC),ThomasAhle/FastPoly,BasSpitters/CatCrypt,BrettSaiki/mpfxand retained lineage. Constant specialization/block simulation classical.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19447201", + "overlap": "Freshmain7c49/rev8,759fullopenbody/head records across8pages; current6802head unchangedb792a586and0issue/inline/review feedback, nearest5466/5886/6435heads/bodies and7allstate searches. RootliveHub/index saw released question/no direct activeclaim; helper coverage limited, hidden/unindexed work unknown. Prior109plusB14first4results excluded.", + "evidence": "First19:13:54.722415\u219219:13:58.830019UTC,4.107520834s220.625MiB,exit0/empty stderr/all20hashes unchanged. Actual31sites allinverse,width32/64/128/256/512counts16/8/4/2/1,coefficientcell23590/lifetime288639,288640,431300postunit. Static435650\u2192434255 (1395), executedadditional930peradmittedinput bywrittenproof; observedthreefixtures314002\u2192313072,343556\u2192342626,342989\u2192342059. Local65537residues/fullmemory/TEMP/frame/30stepdelta and8controls (6structural+2actualsemantic) pass. Normal/O/registered/export/publication/CI are separate later observations. Unit47523field is creditedtheorem association, not newP0wholecomparison; nooldbroadsuite or9template replay.", + "power_of_ten_deviations": [ + "CPython checker uses dynamic lists/dictionaries, allocated program/maps and authenticated pinned module imports; no fixed-allocation/static-analyzer certification is claimed.", + "Generated literal instructions/branch labels and bounded source ISA are the executed model; host program generation/allocation is separate from counted runtime instructions and not an all-size paid compiler.", + "Original pinned source modules are retained unchanged; written proof and explicit guard/finite corroboration are not Lean, complete machine formalization or proof-kernel acceptance." + ], + "remaining_obligations": [ + "The scoped written local/fixed-template proof and first finite corroboration are complete. Frozen delivery and publication observations are recorded separately; original formalization/native/full-invoice gates remain open.", + "Original5466correctness/range/setup and source executed-initialization/traversal premises and6802unit theorem are cited, not independently re-audited. A general arbitrary-program optimizer is not certified.", + "Original builder/unit transformer/ISA actually executed as credited code; old broad6802verifier was only fetched/read inertly. Preserve prior ownership of unitcounts/saving and all source notices.", + "Native/physical selected consumer, word/bit tariff, all-size compiler, conversion/routing/storage/precision/ownership/restoration and complete supplier invoice remain missing. All five assumptions remain.", + "Other coefficients, asymmetric/all-length scope, liveness composition and global optimality require separate evidence; no kappa/frontier or supplier/adoption change, human/kernel acceptance or broader search follows." + ], + "open_questions": [ + { + "question": "Can the fixed refined kernel serve one actual selected consumer under a complete matched paid/productive bill?", + "why_it_matters": "A bounded literal64-bit ISA saving does not establish physical BIT/native costs, conversion or full supplier admission.", + "first_step": "Bind one named current consumer and operand sizes; price word multiplication, constant delivery/routing, layout, storage, precision and restoration/ownership before comparing full totals.", + "blocked_by": "No selected-consumer conversion/native/full-invoice contract is supplied; all five assumptions remain." + }, + { + "question": "What exact installed scope is justified once this fixed post-unit refinement is checked?", + "why_it_matters": "A structural recognizer on one authenticated producer is not a general program optimizer or all-length compilation theorem.", + "first_step": "Freeze eligible site/write-lifetime/control evidence, final code/data hashes and incremental baseline; treat other coefficients, liveness composition or asymmetric templates as separate future scopes.", + "blocked_by": "Exact fixed-template sites/proof/firstcorroboration supplied; installation/adoption review and formal/native/selected-consumer boundary remain open. No wider census or global instruction optimum supplied." + } + ] +} diff --git a/research/wordram-double-twiddles/VERIFY.json b/research/wordram-double-twiddles/VERIFY.json new file mode 100644 index 0000000000..23c6edaad0 --- /dev/null +++ b/research/wordram-double-twiddles/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All65537localresidues, completeVALUE/TEMP/writeframe and45static/30executed localdelta; exact31source/baseline/newsite bindings of fixed512template; threecomplete dirtyfixtures,6exactreasonstructuraland2actualsemanticcontrols. Executescreditedoriginalbuilder/ISA/unitrefiner; nooldverifier." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat complete fixed finite corroboration with explicit guards under optimized Python. Authenticate9bodies+manifestand5importorigins; fullrecursivepackageSHAmap. Written universal/sourcepremises and physical/full-invoice obligations remain separate." + } + ] +} diff --git a/research/wordram-double-twiddles/refine.py b/research/wordram-double-twiddles/refine.py new file mode 100644 index 0000000000..2d6b7fcf6b --- /dev/null +++ b/research/wordram-double-twiddles/refine.py @@ -0,0 +1,106 @@ +"""Source-bound constant-two butterfly reduction after Petalas's unit rewrite. + +The producer's setup, residue, allocation and executed-initializer contracts +are premises. These structural gates do not certify arbitrary programs. +""" +from dataclasses import dataclass + +P = 65537 +VALUE, TEMP, ZERO, ONE = 8, 9, 10, 11 +THRESHOLDS = tuple(range(20, 36)) +SCRATCH = frozenset((VALUE, TEMP, ZERO, ONE, *THRESHOLDS)) +MAX_PROGRAM = 600_000 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def validate(program): + require(type(program) is list and 0 < len(program) <= MAX_PROGRAM, 'program capacity') + arities = {'one': 2, 'add': 4, 'sub': 4, 'mul': 4, 'bltz': 3, 'accept': 1} + for pc, instruction in enumerate(program): + require(type(instruction) is tuple and instruction, 'instruction tuple') + require(instruction[0] in arities and len(instruction) == arities[instruction[0]], 'ISA') + require(all(type(x) is int for x in instruction[1:]), 'integer operands') + if instruction[0] == 'bltz': + require(pc < instruction[2] < len(program), 'forward branch') + require(program[-1] == ('accept',), 'terminal accept') + + +def double_lifetimes(program): + writes = {} + for pc, instruction in enumerate(program): + if instruction[0] in ('one', 'add', 'sub', 'mul'): + writes.setdefault(instruction[1], []).append(pc) + result = {} + for cell, sites in writes.items(): + if cell in SCRATCH or len(sites) != 3: + continue + first, doubled, cleared = sites + if (doubled == first + 1 and program[first] == ('one', cell) + and program[doubled] == ('add', cell, cell, cell) + and program[cleared] == ('sub', cell, cell, cell)): + result[cell] = (first, doubled, cleared) + return result + + +def macro(program, pc): + first = program[pc] + require(first[0] == 'mul' and first[1] == VALUE, 'macro entry') + require(first[2] not in SCRATCH and first[3] not in SCRATCH + and first[2] != first[3], 'data/coefficient ABI') + expected = [first] + for threshold in reversed(THRESHOLDS): + sub_pc = pc + len(expected) + expected.extend((('sub', TEMP, VALUE, threshold), + ('bltz', TEMP, sub_pc + 3), ('add', VALUE, TEMP, ZERO))) + require(program[pc:pc + 49] == expected, 'generic reduction macro') + # Retain the original last branch's OLD exit label. Relocate exactly once. + return (first, *program[pc + 46:pc + 49]) + + +@dataclass(frozen=True) +class Refinement: + program: list + replacements: tuple + old_to_new: dict + + +def refine(program): + validate(program) + lifetimes = double_lifetimes(program) + pieces, replacements, mapping = [], [], {} + pc = new_pc = 0 + for _ in range(len(program)): + if pc == len(program): + break + instruction = program[pc] + mapping[pc] = new_pc + hit = (instruction[0] == 'mul' and instruction[1] == VALUE + and instruction[3] in lifetimes) + if hit: + first, doubled, cleared = lifetimes[instruction[3]] + require(first < doubled < pc and pc + 49 <= cleared, 'double lifetime') + replacement = macro(program, pc) + pieces.append(replacement) + replacements.append((pc, instruction[3], instruction[2])) + pc += 49 + new_pc += 4 + else: + pieces.append((instruction,)) + pc += 1 + new_pc += 1 + require(pc == len(program), 'bounded scan finished') + require(replacements, 'no constant-two sites') + output = [] + for instructions in pieces: + for instruction in instructions: + if instruction[0] == 'bltz': + require(instruction[2] in mapping, 'branch into removed macro') + instruction = ('bltz', instruction[1], mapping[instruction[2]]) + output.append(instruction) + require(len(output) == len(program) - 45 * len(replacements), 'static delta') + validate(output) + return Refinement(output, tuple(replacements), mapping) diff --git a/research/wordram-double-twiddles/vendor/PR6802-PROOF.md b/research/wordram-double-twiddles/vendor/PR6802-PROOF.md new file mode 100644 index 0000000000..9467bc69fb --- /dev/null +++ b/research/wordram-double-twiddles/vendor/PR6802-PROOF.md @@ -0,0 +1,130 @@ +# A two-instruction unit-twiddle refinement + +This scoped proof was produced by Nick Petalas. Apache-2.0. + +## Contract and cited inputs + +Use David Ganz / Dugongue's bounded multiplier from PR #5466, retained at +`research/wordram-ntt-kernel/`. Its literal 64-bit Word RAM semantics, exact +NTT schedule, all-input multiplication theorem and range invariant are cited +inputs. They are not re-proved or audited here. In particular, at every +transform butterfly the multiplicand b is an integer in [0,65537), ZERO +contains zero, the threshold cells 20+i contain p*2^i for p=65537, and the +twiddle cell contains the requested residue. Inputs have 1..256 hexadecimal +digits. The generated transform size n is a power of two at most 512. + +The new result concerns the exact emitted program, including its complete +memory, scratch values, branch targets and instruction count. No selected +supplier admission, asymptotic saving or proof-kernel verification follows. + +## Local full-state equivalence + +At a constant-one twiddle, the original 49-instruction macro is + +```text +mul VALUE, b, one_cell +for i = 15,...,0: + sub TEMP, VALUE, threshold_i + bltz TEMP, after_copy_i + add VALUE, TEMP, ZERO +``` + +The loop is notation for a completely unrolled instruction list. Every +subtraction has signed value b-p*2^i < 0, with absolute value below 2^32. +There is no signed overflow. Therefore every branch is taken and every copy +is skipped. At exit VALUE=b and TEMP=b-p modulo 2^64. All other cells have +their incoming values. This macro executes exactly 1+2*16=33 instructions. + +Replace it by these two literal instructions: + +```text +add VALUE, b, ZERO +sub TEMP, VALUE, threshold_0 +``` + +The exit memory is identical at every address, including TEMP. The replacement +uses the same write addresses and preserves arbitrary incoming dirt elsewhere. +It saves exactly 47 static instructions and 31 executed instructions. This +identity holds for every b in the admitted residue interval; it does not +require any particular original values in VALUE or TEMP. It also explains +why the second replacement instruction is retained. + +## Binding replacements and relocating control flow + +The source files are authenticated before importing the producer. The +transformer accepts only the direct-address instruction subset emitted by +that producer, with forward branches and a terminal accept. It identifies a +unit cell by its complete write inventory: one `one` initialization and one +final `sub cell,cell,cell`, with no intervening writes. For the pinned +producer these initializations execute before use; its conditional skips +only omit modular-reduction/carry updates, not literal initialization. + +Only a `mul` into the retained VALUE cell with such a unit operand qualifies. +The transformer checks every instruction and branch target in the following +49-instruction macro, checks the unit's lifetime and excludes data aliasing +with VALUE, TEMP, ZERO or a threshold cell. Its structural gates alone are +not a soundness theorem for arbitrary +programs: coefficient bounds, setup and executed initialization remain the +cited producer premises. Corrupt source bytes are rejected before assembly. + +Partition the original instruction list into replacement blocks and singleton +unchanged instructions. Map each block entry to its new instruction index. +Every surviving branch must target such an entry; a branch into the interior +of a removed macro is rejected. Translate all surviving labels by this map. +The removed internal branches have exactly the local behavior proved above. + +Induction over executed blocks now gives equal complete memory at corresponding +entries. Unchanged conditional branches take the same outcome because they +read equal values. Replacement blocks reach equal memory at their mapped exit. +Thus both programs reach accept with identical complete memory, including all +operand, output, scratch, temporary and exterior addresses. All setup, literal +synthesis, carry normalization, final clearing and halt instructions remain +charged. The new program is a direct-address literal program in the same ISA. + +## Exact uniform savings + +At a radix-two transform stage of width 2^l there are n/2^l blocks. Each has +one unit twiddle, at its first butterfly. There are no others: the stage root +has exact order 2^l and its used exponents range from zero through 2^(l-1)-1. +Consequently one transform has + +```text +sum_(l=1..log2 n) n/2^l = n-1 +``` + +unit-twiddle butterflies, including the empty sum at n=1. The two forward +transforms and the inverse transform give 3(n-1) replacements. All execute on +every admitted input. Pointwise products and inverse normalization use other +output cells and are unchanged. Hence the exact static and dynamic savings are + +```text +static saving = 141(n-1), +executed saving = 93(n-1). +``` + +This proves a uniform all-input refinement of each admitted fixed template, +conditional on the cited original multiplication/range theorem. The finite +certificate independently enumerates the replacement sites of nine balanced +templates; it is not an enumeration of every operand or every length pair. + +At n=512 the emitted program has 1,533 replacement sites. Its static length +is 435,650 rather than 507,701, a decrease of 72,051. Every admitted input to +that template saves 47,523 executed instructions. These are exact ISA counts, +not elapsed-time measurements. No unrestricted optimality is claimed. + +## Evidence and limits + +The verifier compares complete local memory for all 65,537 residues and dirty +VALUE/TEMP/exterior initial values. It then executes the refined templates on +36 complete dirty-memory fixtures and checks both full-memory equivalence +and direct integer multiplication of the new outputs. The former execution +is the transformation specification, not a deliverable re-verification of +the predecessor's mathematical theorem. Structural controls corrupt a +threshold, a macro branch, an exterior branch entry, the data operand and +terminal control flow. Explicit guards remain enabled under Python -O. + +The universal implication rests on this block simulation and the cited +producer invariants. Finite executions corroborate it. We do not claim an +independent human review, complete machine formalization, physical selected +consumer, selected cold replay, or new kappa. Other constant-specialization, +liveness and cleanup changes are outside this first improvement. diff --git a/research/wordram-double-twiddles/vendor/PR6802-README.md b/research/wordram-double-twiddles/vendor/PR6802-README.md new file mode 100644 index 0000000000..1088fab13c --- /dev/null +++ b/research/wordram-double-twiddles/vendor/PR6802-README.md @@ -0,0 +1,122 @@ +# Save 47,523 executed instructions in the bounded NTT multiplier + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped program-refinement proof with a source-bound finite +certificate. Replace each constant-one transform-twiddle reduction in David +Ganz / Dugongue's [PR #5466](https://github.com/CrocSwap/integer-mult-bounds/pull/5466) +by two literal Word RAM instructions. The replacement preserves complete +memory, including the scratch temporary, on every admitted input. + +For transform size n, the static saving is exactly 141(n-1) instructions and +the executed saving is exactly 93(n-1). At n=512, all 1,533 unit-twiddle +sites are enumerated: static length falls from 507,701 to 435,650, and every +input saves 47,523 executed instructions. [PROOF.md](PROOF.md) proves the +all-input block simulation and counting formula. These are exact instruction +counts, with no runtime benchmark or optimality claim. + +The original bounded multiplication theorem and residue-range invariants +are cited premises, not audit targets. Frozen source bytes remain unchanged. +This arithmetic refinement is separate from Nick Petalas's #5886 address +allocation and #6435 optimized-checklist portability. It does not extend +their open questions. Constant-one specialization and block simulation are +standard; the new contribution is the exact full-state rewrite and complete +charged saving for this literal program. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/wordram-unit-twiddles/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/wordram-unit-twiddles/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/wordram-unit-twiddles +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/wordram-unit-twiddles --check-source-history +``` + +Substitute another CPython 3.12 executable as needed. The direct verifier +prints `PASS_WORDRAM_UNIT_TWIDDLES` in a generated JSON receipt bound to every +package file and to all nine emitted refined-program hashes. It writes no +files. SOURCES.json authenticates the exact producer/runtime/proof inputs; +VERIFY.json declares all six external inputs for replay selection. A Git-free +export must retain those repository-relative input paths. + +The finite checks cover all 65,537 local residues, nine balanced templates +with operand lengths 1,2,4,8,16,32,64,128,256, 36 full dirty-memory cases, +and five structural rejection controls. Both complete and local memory are +compared at every address represented by the executed direct-address programs. +The proof supplies preservation at every exterior address, since neither +program writes it. All original setup, constants, carrying, clearing and halt +instructions remain. The template census is not a complete length-pair census. + +## Scope and coordination + +Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision +8. The selected-record binding baseline passed. TASK.json explicitly changes +the formal-interface-lemma card to this bounded compiler/cost side result: +there is no proof-assistant formalization or selected assumption discharge. +The selected complex supplier still binds, and its recursive rank invoice +differs from this kernel's ISA invoice. No new kappa is claimed. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19441308) +reserves this original arithmetic-refinement question. Live PR bodies and +handoffs, all-state #5466/Word RAM/NTT searches, and merged/main searches for +unit-twiddle and constant-specialization terms were checked. The overlap helper +reported complete live pagination of 744 open PRs and 6,864 Discussion records; +its sparse local note coverage was incomplete. Targeted main searches also +read the retained liveness and assertion-portability packages. No equivalent +arithmetic rewrite was found in that coverage; unpublished work and arbitrary +historical diffs remain outside it. + +No asymptotic algorithm, unrestricted instruction optimum, independent human +or proof-kernel review, full machine formalization or selected consumer is +claimed. No Lean, Docker, selected cold replay or approximate FFT backend +check is part of this contribution. + +## Open next questions + +- Can one known nonunit twiddle use a shorter fully charged macro? First + specify the constant and prove complete memory and cost equivalence. + No such refinement is supplied here. +- Can an actual selected consumer use this kernel at a favorable complete + cost? First name its sizes, conversions, restoration and charged machine + model. The two interfaces and cost models are currently different. + +Structured first steps and blockers are in [TASK.json](TASK.json). + +## Verifier constraints + +The transformer accepts at most 600,000 direct-address instructions and +scans each finite list with a fixed list-length bound. The verifier accepts no +CLI inputs: its local domain is 65,537 residues, its template list has nine +entries, and each has four full fixtures. Source inputs are each under one +MiB. Functions stay below 60 lines; explicit exceptions keep every new check +active under -O. Warning-strict normal and optimized commands are registered. +There is no recursion, subprocess or network in the new code. + +Power of Ten rule 3 deviation: CPython allocates integers, tuples, dictionaries +and source-produced plans dynamically. The fixed domains, program cap and +serial execution bound live data to a fixed multiple of one largest template; +no unbounded stream or concurrent plan cache exists. Rule 8 deviation: the +transformer emits a literal instruction list, required for this compiler +refinement. The bounded, authenticated input and explicit old-to-new label +map constrain generation; the full macro and instruction-simulation checks +inspect the emitted result. There is no Python eval, exec or source rewriting. +Rule 9 deviation: the +authenticated producer and its exact ISA interpreter are imported from their +fixed declared source directory. Calls have these named targets only. The +original interpreter's nested helper and bounded instruction loop remain +unchanged; this package adds no dependency on arbitrary callback dispatch. +An embedded fixed-allocation implementation and source-to-machine theorem +would need a separate implementation. Normal/optimized replay and the source +hash gates verify these scoped controls; no external static analyzer is claimed. + +## Credit + +David Ganz / Dugongue supplied PR #5466's bounded multiplier, ISA interpreter, +NTT schedule and original correctness/cost arguments. Shilun-Allan-Li and the +tcslib contributors, Thomas Ahle and FastPoly, Bas Spitters and CatCrypt, and +Brett Saiki and mpfx retain the original interface credit and the predecessors +named in the unchanged source NOTICE.txt. The new arithmetic refinement, +simulation proof and verifier were produced by Nick Petalas. No predecessor +notice or credit line is edited. diff --git a/research/wordram-double-twiddles/vendor/source/NOTICE.txt b/research/wordram-double-twiddles/vendor/source/NOTICE.txt new file mode 100644 index 0000000000..b0dc94cb9d --- /dev/null +++ b/research/wordram-double-twiddles/vendor/source/NOTICE.txt @@ -0,0 +1,3 @@ +Original bounded-kernel integration prepared for Dugongue with substantial OpenAI Codex assistance. Apache-2.0. Reusable mathematical/formal interfaces retain all upstream credit listed in SOURCES.json and README.md. CatCrypt source attribution and MIT notice are retained in ntt/. No complete upstream library is vendored. + +The base Word RAM semantics retain Anthropic, PBC / anthropics/formal-math [AFM26], `3sum-apsp/EndStatement.lean` at `e1a4e6508154ea59f030480661590a9fe3018011`, as attributed in tcslib’s source header. diff --git a/research/wordram-double-twiddles/vendor/source/PROOF.txt b/research/wordram-double-twiddles/vendor/source/PROOF.txt new file mode 100644 index 0000000000..d0d0d6486e --- /dev/null +++ b/research/wordram-double-twiddles/vendor/source/PROOF.txt @@ -0,0 +1,38 @@ +BOUNDED INTEGER MULTIPLICATION: SUFFICIENT ASSEMBLY AND COST PROOF + +1. Frozen scope and computation model. +Fix 1<=s,t<=256, hexadecimal digits a_i,b_j in {0,...,15}, p=65537 and N the least power of two >=s+t-1. Thus N<=512. Input words occupy addresses 1000+i and 2000+j; output words 3000..3000+N. The owned temporary region is exactly the generated fresh addresses >=10000 plus the explicitly reserved scratch set. Regions are disjoint. Arbitrary other memory, including negative signed addresses, is permitted. Initial owned words can be dirty. +The machine uses 64-bit modular words, signed comparison against zero, direct arithmetic operands and a charged halt. Word multiplication is unit cost by this explicitly chosen model; full arbitrary-size multiplication is not a primitive. The program generator uses only lengths and fixed field constants, never input digits. It creates a fixed finite program for each pair of lengths; its generation is not claimed as free work in an all-size algorithm. + +2. Prime and roots. +The concrete checker tests primality by trial divisors through floor(sqrt(p)); every integer in that finite exhaustive divisor interval is checked, so a passing test is a primality certificate by the elementary least-prime-factor argument. For each actual N it sets omega=3^((p-1)/N) mod p and checks omega^N=1 and, if N>1, omega^(N/2)!=1. Since N is a power of two, these two conditions imply exact order N: every proper divisor of N divides N/2. N=1 is direct. Hence geometric-sum orthogonality and division by N are valid in F_p. + +3. No wrap and unique coefficients. +Extend both digit vectors by zero to N. Ordinary product coefficients c_k=sum_{i+j=k}a_i b_j satisfy 0<=c_k<=225 min(s,t)<=57600