diff --git a/research/two-clean-checkpoints/CLAIM.md b/research/two-clean-checkpoints/CLAIM.md new file mode 100644 index 0000000000..638b318ca3 --- /dev/null +++ b/research/two-clean-checkpoints/CLAIM.md @@ -0,0 +1,37 @@ +# Sprint claim + +- Track: recursive interfaces; OS-random assignment seed: **50**. +- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Start: 2026-10-13 05:45 UTC; planned finish: 06:30 UTC. Final quarter reserved for verification and handoff. +- No pinned coordination issue exists; claim recorded locally. +- Object: ordered binary product-shear trees with two initially clean, reusable arrays, arbitrary remaining dirt, and reserved ancestor connectors. +- Method: exact interval/resource recurrence, literal forward/inverse words, independent exhaustive tree enumeration, and exact noncommutative/rounded execution. +- Seed-selected fixture: 50 ordered factors, six total scratch arrays, two initially clean versus one. Weighted small fixtures provide separate controls. +- Deliverable: one research note, executable construction, exact evidence, full cost recurrence and explicit clean-provisioning obligation; no new kappa claim. + +## Candidates considered + +1. Borrow idle ancestor connectors in all-dirty echoes. Harder lifetime proof; pending #730/#758 already cover adjacent static scheduling classes. +2. Two reusable clean checkpoints at fixed total scratch (selected). #714 has one clean root; #788 permits one clean array to move between sequential subtrees. Neither allows a second clean connector while the first remains reserved. +3. Optimize #788 with dispatch-aware prices. Useful but less directly addresses restoration work and depends on an actual cost model. + +The selected search changes the explicit initial-space contract, not just computation or the random seed. Domain: ordered binary trees, positive integer leaf prices, fixed total scratch and clean counts. Dynamic programming exhausts every split and legal connector type; it does not search arbitrary reversible programs. + +Overlap reviewed: #628, #663, #673, #689, #714, #730, #744, #758, #784, #788; initial open PR metadata through #794; full 618-open-PR overlap refresh through #799. The ledger ends at #626; it records no maintainer review of these pending interface PRs. The selected result remains #626/#543 at kappa 0.001635527380375392. + +## Result + +The two-clean recurrence attains 1,248 complete leaf calls at 50 factors and six scratch arrays, versus the independently checked one-clean minimum 1,728. Full-capacity unit cost is exactly `4^(s-c)3^c`. Complete dispatch/provisioning/precision costs and inherited obligations are stated. Exhaustive, symbolic, actual rounded-leaf and corruption checks passed; see VALIDATION.md. + +Publication overlap refresh: 638 open PRs through #825; #788 remains the sole reusable one-clean comparator and its pinned head is unchanged. No pinned sprint issue appeared. Source pins and credit distinguish this changed two-clean contract from pending all-dirty work. + +Concurrent #805 (VictorLiwentao, `ef34bd5b32fcf2d5640dae90b5b8f28488738d5a`) supplies a different in-place real cyclic leaf plus dirty scalar. Its contract and execution prices differ from the additive leaves optimized here; no source is consumed and no cross-contract runtime comparison is claimed. + +Result branch: https://github.com/Better-Call-Paul/integer-mult-bounds/tree/research/two-clean-checkpoints-seed50/research/two-clean-checkpoints + +Verification extended beyond the planned finish to resolve local dependency +configuration and complete the selected cold replay. Remaining unrelated +historical searches were stopped after `verify-certificates` and +`verify-ternary` passed; no full-suite pass is claimed. + +Immediate pre-submission review also read #822 (@shhxera, `8c5e1b557f59bca29139c4c2dcc65edfb808372b`): it proposes reuse of restored sibling connectors with entirely dirty scratch. That changes connector lifetimes; this contribution keeps ancestor connectors reserved and changes the number of clean inputs. Neither minimum is asserted over the other class. No #822 source is imported. diff --git a/research/two-clean-checkpoints/EXPECTED.json b/research/two-clean-checkpoints/EXPECTED.json new file mode 100644 index 0000000000..65931dd284 --- /dev/null +++ b/research/two-clean-checkpoints/EXPECTED.json @@ -0,0 +1,1178 @@ +{ + "format": 1, + "independent": { + "budgets": "every 0<=clean<=scratch<=n-1", + "decorated_trees_by_leaf_count": { + "1": 1, + "2": 2, + "3": 8, + "4": 40, + "5": 224, + "6": 1344 + }, + "feasible_optimum_comparisons": 449, + "forward_leaf_calls_checked": 61804, + "noncommutative_symbolic_cases": 1619, + "nonlinear_mod101_cases": 1619, + "prices": "all {1,3}^n for 1<=n<=5; unit prices for n=6", + "status": "passed", + "tree_resource_admissions_checked": 32039, + "trees_checked": 1619, + "whole_tree_optimum_comparisons": 723 + }, + "negative_controls": [ + "invalid_plan_0", + "invalid_plan_1", + "invalid_plan_2", + "invalid_plan_3", + "invalid_plan_4", + "invalid_plan_5", + "insufficient_total_scratch", + "insufficient_clean", + "role_alias", + "bad_sign", + "reversed_order", + "duplicate_leaf", + "omit_restoration", + "reverse_factor_order", + "wrong_sign", + "dirty_as_clean_algebra", + "positive_calls_only_undercharge", + "mutation_after_lazy_validation" + ], + "predecessor": { + "comparisons": 137, + "scope": "all-dirty and one-clean restrictions match pinned PR788", + "weighted_seed": 50 + }, + "primary": [ + { + "clean": 0, + "clean_dispatches": 0, + "cost": 2752, + "dirty_dispatches": 917, + "leaf_calls": 2752, + "literal_word_sha256": "ef12d314a32ff7b8c414eba5a7f8b53bd37ade1a829b5d380f327e13161020e9", + "multiplicities": [ + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64 + ], + "prices": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "scratch": 6, + "tree": [ + "D", + [ + "D", + [ + "D", + [ + "D", + [ + "D", + 0, + 1 + ], + [ + "D", + 2, + 3 + ] + ], + [ + "D", + [ + "D", + 4, + 5 + ], + [ + "D", + 6, + 7 + ] + ] + ], + [ + "D", + [ + "D", + [ + "D", + 8, + 9 + ], + [ + "D", + 10, + 11 + ] + ], + [ + "D", + [ + "D", + 12, + 13 + ], + [ + "D", + [ + "D", + 14, + 15 + ], + [ + "D", + 16, + 17 + ] + ] + ] + ] + ], + [ + "D", + [ + "D", + [ + "D", + [ + "D", + [ + "D", + 18, + 19 + ], + [ + "D", + 20, + 21 + ] + ], + [ + "D", + [ + "D", + 22, + 23 + ], + [ + "D", + 24, + 25 + ] + ] + ], + [ + "D", + [ + "D", + [ + "D", + 26, + 27 + ], + [ + "D", + 28, + 29 + ] + ], + [ + "D", + [ + "D", + 30, + 31 + ], + [ + "D", + 32, + 33 + ] + ] + ] + ], + [ + "D", + [ + "D", + [ + "D", + [ + "D", + 34, + 35 + ], + [ + "D", + 36, + 37 + ] + ], + [ + "D", + [ + "D", + 38, + 39 + ], + [ + "D", + 40, + 41 + ] + ] + ], + [ + "D", + [ + "D", + [ + "D", + 42, + 43 + ], + [ + "D", + 44, + 45 + ] + ], + [ + "D", + [ + "D", + 46, + 47 + ], + [ + "D", + 48, + 49 + ] + ] + ] + ] + ] + ] + }, + { + "clean": 1, + "clean_dispatches": 1, + "cost": 1728, + "dirty_dispatches": 575, + "leaf_calls": 1728, + "literal_word_sha256": "19c989427c00a0841e6bbcb6a9caab000f24f54f6b1096280100310e3ab8f6f0", + "multiplicities": [ + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 64, + 64, + 64, + 64, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32 + ], + "prices": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "scratch": 6, + "tree": [ + "C", + [ + "D", + [ + "D", + [ + "D", + [ + "D", + 0, + 1 + ], + [ + "D", + 2, + 3 + ] + ], + [ + "D", + [ + "D", + 4, + 5 + ], + [ + "D", + 6, + 7 + ] + ] + ], + [ + "D", + [ + "D", + [ + "D", + 8, + 9 + ], + [ + "D", + 10, + 11 + ] + ], + [ + "D", + [ + "D", + 12, + 13 + ], + [ + "D", + [ + "D", + 14, + 15 + ], + [ + "D", + 16, + 17 + ] + ] + ] + ] + ], + [ + "D", + [ + "D", + [ + "D", + [ + "D", + [ + "D", + 18, + 19 + ], + [ + "D", + 20, + 21 + ] + ], + [ + "D", + [ + "D", + 22, + 23 + ], + [ + "D", + 24, + 25 + ] + ] + ], + [ + "D", + [ + "D", + [ + "D", + 26, + 27 + ], + [ + "D", + 28, + 29 + ] + ], + [ + "D", + [ + "D", + 30, + 31 + ], + [ + "D", + 32, + 33 + ] + ] + ] + ], + [ + "D", + [ + "D", + [ + "D", + [ + "D", + 34, + 35 + ], + [ + "D", + 36, + 37 + ] + ], + [ + "D", + [ + "D", + 38, + 39 + ], + [ + "D", + 40, + 41 + ] + ] + ], + [ + "D", + [ + "D", + [ + "D", + 42, + 43 + ], + [ + "D", + 44, + 45 + ] + ], + [ + "D", + [ + "D", + 46, + 47 + ], + [ + "D", + 48, + 49 + ] + ] + ] + ] + ] + ] + }, + { + "clean": 2, + "clean_dispatches": 259, + "cost": 1248, + "dirty_dispatches": 243, + "leaf_calls": 1248, + "literal_word_sha256": "d94574cb34f833ca341108a86d598ec79cd13b3a90e046c1ab5d79993e605edb", + "multiplicities": [ + 16, + 16, + 16, + 16, + 16, + 16, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 16, + 32, + 16, + 32, + 16, + 32, + 16, + 32, + 16, + 32, + 16, + 32, + 16, + 32, + 16, + 32, + 16, + 32, + 16, + 32, + 16, + 32, + 16, + 32, + 16, + 32, + 16, + 32, + 16, + 32, + 16 + ], + "prices": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "scratch": 6, + "tree": [ + "C", + [ + "C", + [ + "D", + [ + "D", + 0, + 1 + ], + [ + "D", + 2, + 3 + ] + ], + [ + "D", + [ + "D", + [ + "D", + 4, + 5 + ], + [ + "D", + [ + "D", + 6, + 7 + ], + [ + "D", + 8, + 9 + ] + ] + ], + [ + "D", + [ + "D", + [ + "D", + 10, + 11 + ], + [ + "D", + 12, + 13 + ] + ], + [ + "D", + [ + "D", + 14, + 15 + ], + [ + "D", + 16, + 17 + ] + ] + ] + ] + ], + [ + "D", + [ + "D", + [ + "D", + [ + "D", + [ + "C", + 18, + 19 + ], + [ + "C", + 20, + 21 + ] + ], + [ + "D", + [ + "C", + 22, + 23 + ], + [ + "C", + 24, + 25 + ] + ] + ], + [ + "D", + [ + "D", + [ + "C", + 26, + 27 + ], + [ + "C", + 28, + 29 + ] + ], + [ + "D", + [ + "C", + 30, + 31 + ], + [ + "C", + 32, + 33 + ] + ] + ] + ], + [ + "D", + [ + "D", + [ + "D", + [ + "C", + 34, + 35 + ], + [ + "C", + 36, + 37 + ] + ], + [ + "D", + [ + "C", + 38, + 39 + ], + [ + "C", + 40, + 41 + ] + ] + ], + [ + "D", + [ + "D", + [ + "C", + 42, + 43 + ], + [ + "C", + 44, + 45 + ] + ], + [ + "D", + [ + "C", + 46, + 47 + ], + [ + "C", + 48, + 49 + ] + ] + ] + ] + ] + ] + } + ], + "rounded": { + "cases": 192, + "controls": [ + { + "name": "dirty_array_used_as_clean", + "rejected": true, + "source_and_dirt_restored": true, + "target_contaminated": true, + "target_error_squared": "7204381411091050477019123321216335169151476085037/93536104789177786765035829293842113257979682750464" + } + ], + "forward_leaf_calls": 3760, + "forward_phase_reads": 34112, + "rows_sha256": "c9630b70d6d7d8a6fec40c893dab3faa1594b1a9ca93a7798f57299833f69098", + "scope": "Synthetic stable inside/outside factors; exact dyadic rounding; dense represented-factor comparison. Phase generation and storage are external costs; no root certificate or machine performance claim.", + "status": "passed" + }, + "saturated": [ + { + "clean": 0, + "cost": 1, + "depth": 0 + }, + { + "clean": 0, + "cost": 4, + "depth": 1 + }, + { + "clean": 1, + "cost": 3, + "depth": 1 + }, + { + "clean": 0, + "cost": 16, + "depth": 2 + }, + { + "clean": 1, + "cost": 12, + "depth": 2 + }, + { + "clean": 2, + "cost": 9, + "depth": 2 + }, + { + "clean": 0, + "cost": 64, + "depth": 3 + }, + { + "clean": 1, + "cost": 48, + "depth": 3 + }, + { + "clean": 2, + "cost": 36, + "depth": 3 + }, + { + "clean": 3, + "cost": 27, + "depth": 3 + }, + { + "clean": 0, + "cost": 256, + "depth": 4 + }, + { + "clean": 1, + "cost": 192, + "depth": 4 + }, + { + "clean": 2, + "cost": 144, + "depth": 4 + }, + { + "clean": 3, + "cost": 108, + "depth": 4 + }, + { + "clean": 4, + "cost": 81, + "depth": 4 + }, + { + "clean": 0, + "cost": 1024, + "depth": 5 + }, + { + "clean": 1, + "cost": 768, + "depth": 5 + }, + { + "clean": 2, + "cost": 576, + "depth": 5 + }, + { + "clean": 3, + "cost": 432, + "depth": 5 + }, + { + "clean": 4, + "cost": 324, + "depth": 5 + }, + { + "clean": 5, + "cost": 243, + "depth": 5 + }, + { + "clean": 0, + "cost": 4096, + "depth": 6 + }, + { + "clean": 1, + "cost": 3072, + "depth": 6 + }, + { + "clean": 2, + "cost": 2304, + "depth": 6 + }, + { + "clean": 3, + "cost": 1728, + "depth": 6 + }, + { + "clean": 4, + "cost": 1296, + "depth": 6 + }, + { + "clean": 5, + "cost": 972, + "depth": 6 + }, + { + "clean": 6, + "cost": 729, + "depth": 6 + } + ], + "scope": "Ordered binary reserved connectors; no new kappa or full multiplication proof", + "sources": { + "files": 11, + "manifest_sha256": "ea4208df1e1729f77bf9554ce7a6338047d55781d479b3251a8fc6f0374f4335" + }, + "weighted": { + "clean": 2, + "clean_dispatches": 4, + "cost": 13, + "dirty_dispatches": 0, + "leaf_calls": 9, + "literal_word_sha256": "bd888658589ba8e12a5bac51f7ede96f5267ed281d69894dc373c01bbffea082", + "multiplicities": [ + 4, + 2, + 2, + 1 + ], + "prices": [ + 1, + 3, + 1, + 1 + ], + "scratch": 2, + "tree": [ + "C", + [ + "C", + 0, + 1 + ], + [ + "C", + 2, + 3 + ] + ] + } +} diff --git a/research/two-clean-checkpoints/LICENSE b/research/two-clean-checkpoints/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/two-clean-checkpoints/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/two-clean-checkpoints/NOTICE.md b/research/two-clean-checkpoints/NOTICE.md new file mode 100644 index 0000000000..d57ea10688 --- /dev/null +++ b/research/two-clean-checkpoints/NOTICE.md @@ -0,0 +1,39 @@ +# Attribution and license + +Prepared for **Paul Chan (@Better-Call-Paul)** with substantial **OpenAI Codex +assistance**, including separate proof, exhaustive-checking, rounded-execution +and adversarial-review workers. No independent human review is claimed. +New work is under Apache-2.0; see `LICENSE`. + +- **FanPUYen / Hao Yan, PR714**: the clean-root three-call construction and + complete interface accounting. +- **nightangelflowerwin-ops / Stephen Shore, PR788**: one clean array reused + between sequential subtrees and the ordered binary interval optimizer. + Its `checkpoint.py`, `README.md`, `PROOF.md`, and retained PR714 notice are + included unchanged under `vendor/pr788/`. +- **chafreaky / Chafik Boukhalfa, PR628**: rounded cyclic-factor leaves, + exact source restoration, dense rational comparison, and inherited error + estimates. Seven unchanged source/proof/notice files are in `vendor/pr628/`. +- **0xkilgore, PR663**: prior independent binary-restoration audit. +- **androolloyd, PR673**: multiway dirty echoes, immutable-phase alias repair, + and the scoped direct-adapter cost obstruction. No new supplier integration + is claimed here. +- **Dillon Amburgey, PR689; Sagar Thakrar, PR730; Ali Romman, PR744; + Koroffstrogov, PR758; Alexander Schwartzman, PR784**: concurrent all-dirty + scheduling and scratch-bound work. Those results concern different storage + contracts and are credited context, not competing bounds on this class. + +Concurrent **Wentao Li / VictorLiwentao, PR805** supplies an in-place real cyclic +leaf with a dirty scalar, a different contract from these additive leaves. +No PR805 code or comparative performance claim is imported. + +Concurrent **@shhxera, PR822** changes dirty-connector lifetimes by reusing +restored sibling connectors. This package keeps connectors reserved; no +PR822 code or cross-class optimum claim is imported. + +The original PR628 and PR714 notices retain their earlier mathematical and +software credits, including reversible-computation predecessors. Source bytes +and exact commits are recorded in `SOURCES.json`; no literature priority is +claimed for checkpointing or clean ancillas. The new contribution is the +explicit several-clean reserved-connector recurrence, its full-capacity +formula, complete witness bill and independently replayable evidence. diff --git a/research/two-clean-checkpoints/PROOF.md b/research/two-clean-checkpoints/PROOF.md new file mode 100644 index 0000000000..47f516400c --- /dev/null +++ b/research/two-clean-checkpoints/PROOF.md @@ -0,0 +1,245 @@ +# Several reusable clean checkpoints + +This extends FanPUYen's clean-root interface +([PR714](https://github.com/CrocSwap/integer-mult-bounds/pull/714), +`efad8a40094ab453c0525efef0b0eff2a5d8b850`) and +nightangelflowerwin-ops' reusable single-clean interface +([PR788](https://github.com/CrocSwap/integer-mult-bounds/pull/788), +`ff8251519e009a01ede6b27e3f5af703eaa70132`). The extension permits another +clean connector while a clean ancestor remains reserved. It changes the +initial-space contract; it supplies no new multiplication exponent. + +## Contract and restoration + +Payloads form an abelian group. A leaf is a deterministic, zero-preserving +increment `f_j`: its positive instruction adds `f_j(source)` to the target; +its negative instruction subtracts the identical value. Neither changes +the source nor reads the target to compute that value. Parameters are +immutable. Source, target and scratch arrays are pairwise distinct. + +There are `s` scratch arrays: `c` initially zero, `s-c` arbitrary. Every +invocation restores its entire scratch pool. A connector stays reserved +throughout its node invocation; descendants cannot borrow it, an ancestor +connector, or any other ancestor role. The remaining pool is available to +each child sequentially, including its remaining clean arrays. + +Write `B` for the left child's increment and `A` for the right child's +increment, with their shared initial scratch state held fixed. A dirty +connector `z`, initially `z0`, implements + +```text +z += B(source) +target += A(z) +z -= B(source) +target -= A(z) +``` + +Its net increment is `A(z0+B(source))-A(z0)`. The connector returns to +`z0`; both child calls restore the rest of the pool. The increment is +independent of the initial target and vanishes at source zero. + +A clean connector starts at zero. Omit the fourth call because `A(0)=0`. +The resulting increment is `A(B(source))`, and the connector returns to +zero. Its children receive `s-1` arrays with `c-1` clean. A dirty connector +instead leaves `c` clean arrays in the child pool. Every child restores +these arrays to zero before its sibling uses them. This proves reuse even +when another clean array remains reserved above them. + +Induction proves restoration, target independence and zero preservation +for arbitrary deterministic leaves satisfying the contract. Reversing the +entire instruction sequence and negating each sign gives its exact inverse. +This reverses instruction order, not merely signs in the forward order. + +For linear leaves the dirty increment also equals `A(B(source))`. +Consequently every legal tree realizes the ordered product +`f_(n-1) ... f_1 f_0`, with no commutation assumption. For nonlinear or +rounded leaves, increments may depend on the tree and dirty scratch. +Restoration still holds; equality between different trees does not follow. +On a fixed grid, addition/subtraction must be exact and free of overflow. +The negative leaf subtracts the same rounded increment; separately rounding +a negative expression is insufficient if rounding is asymmetric. + +## Exact optimization within the stated class + +Let `V(I,s,c)` be the minimum signed-leaf charge for a nonempty contiguous +factor interval `I`. Each factor has positive integer price `t_j`, bounding +both signs at one common precision. A singleton costs `t_j`, including when +`s=0`. Invalid resources and impossible nonleaf states cost infinity. +For every nonempty contiguous split `I=L R`, consider + +```text +dirty connector, s > c: 2 V(L,s-1,c) + 2 V(R,s-1,c) +clean connector, c > 0: 2 V(L,s-1,c-1) + V(R,s-1,c-1). +``` + +`V` is their minimum. A legal decorated tree has one of these root choices +and two legal children. Conversely each finite candidate composes legal +children under the restoration contract. Induction on interval length +therefore proves exact optimality over ordered binary trees with reserved +connectors. It does not optimize arbitrary reversible programs, higher +arities, or schedules that borrow live ancestor arrays. + +Equivalently, every root-to-leaf path has at most `c` clean nodes and at +most `s-c` dirty nodes. Both constraints matter: depth at most `s` and at +most `c` clean nodes alone permit too many dirty reservations. A leaf's +multiplicity is the product of its edge multipliers: two on every left +edge, two on a dirty right edge, one on a clean right edge. This gives a +separate decorated-tree enumeration criterion. + +No tree has more than `2^s` leaves. Conversely every count from one through +`2^s` is feasible: take a full-depth binary tree, label `c` levels clean +and the others dirty, then prune sibling subtrees until the desired count +remains. Hence `n <= 2^s` is the exact feasibility condition. + +At fixed total scratch, extra clean arrays cannot increase `V`. For `c= 0`, and +each signed numerical leaf has local error at most `a*u*(B+1)` for input +norm at most `B`, where `u=2^-w`, `a>0`, and `a*u <= 1`. These are assumed +leaf bounds; this package does not prove PR628's numerical accuracy. +Let all initial array norms be at most `D0`, and put `G=2+K`. + +For the maximum norm `M_j` of all arrays after `j` leaf instructions, + +```text +M_(j+1)+1 <= G*(M_j+1) <= G^(j+1)*(D0+1). +``` + +Let `e_j` be the maximum difference from executing the same instruction +word with ideal leaves, from identical initial data. Then + +```text +e_0 = 0 +e_(j+1) <= (1+K)*e_j + a*u*G^j*(D0+1) +e_N <= N*a*(D0+1)*u*G^(N-1). +``` + +Thus one sufficient precision for execution error at most `2^(-p-1)` is + +```text +w >= p+1 + ceil(log2(N*a*(D0+1))) + (N-1)*ceil(log2(G)), +``` + +together with `a*2^-w <= 1` and inherited stability conditions. Magnitude +capacity must cover `G^N*(D0+1)` at completed leaf boundaries. Each leaf +implementation must separately bound and provision its transient arithmetic +magnitudes and workspace; the local output-error assumption does not bound +those internal states. If preparation also perturbs initial data by at most +`eta`, add `(1+K)^N*eta` to the error +bound; coefficient preparation must establish the assumed uniform local +leaf error. Other preparation errors require their own propagation bound. + +Costs must be evaluated at this precision and magnitude capacity. A common +precision sufficient for both compared words gives a valid count comparison; +different per-word precision costs require repricing. This conservative +bound supplies no better asymptotic precision order or supplier moment. + +The executable finite checks support the written inductions and reject +specific failure modes. They do not establish leaf accuracy, clean-space +supply, routing, all-size physical compilation, analytic transfer, or the +full multiplication theorem. PR673's integration obstruction remains an +external obligation; the selected result is unchanged. diff --git a/research/two-clean-checkpoints/README.md b/research/two-clean-checkpoints/README.md new file mode 100644 index 0000000000..a0268c9c06 --- /dev/null +++ b/research/two-clean-checkpoints/README.md @@ -0,0 +1,85 @@ +# Two reusable clean checkpoints + +With **50 ordered factors and six scratch arrays**, two initially clean +arrays reduce the optimal signed-leaf bill from **1,728 to 1,248** compared +with one clean array. Source and scratch are restored exactly. The class is +ordered binary product-shear trees whose connectors remain reserved during +all descendant calls. **Research construction; no new κ.** + +For `n=2^s` unit-price factors, `s` scratch arrays and `c` initially clean +arrays, the written proof gives the exact class minimum + +```text +4^(s-c) * 3^c. +``` + +Each additional clean array therefore saves exactly 25% at full capacity. +The 50-factor example saves 480 calls (27.78%). It changes the initial-space +contract: four arrays may be dirty, but two must genuinely start at zero. +No borrowed information is erased. + +## Reproduce + +Python 3.10+; standard library; no network or solver: + +```sh +python3 -I -O -B research/two-clean-checkpoints/verify.py +``` + +Expected: + +```text +PASS_TWO_CLEAN_CHECKPOINTS: 1619 trees; 192 rounded cases; n50/s6: 1728 -> 1248; no new kappa +``` + +The verifier recomputes and compares `EXPECTED.json`; it never updates it +unless explicitly invoked with `--write`. It checks: + +- Every decorated binary tree through six factors, using an independent + preorder enumeration and path resource counts; 723 exhaustive weighted + optimum comparisons and 32,039 resource admissions. +- Exact noncommutative identities, nonlinear restoration and literal + inverses for all 1,619 trees, plus the larger frozen witnesses. +- 137 comparisons against the unchanged one-clean/all-dirty PR788 optimizer. +- 192 executions of the actual pinned PR628 rounded leaves, compared with + dense rational represented-factor solves. Both signs and shift directions, + dirty inputs, exact zero-source identities, inverse restoration, 3,760 + forward leaf calls and 34,112 forward phase reads are checked. +- Instruction, resource and dirty-as-clean controls. A dirty array mislabeled + clean can be restored while corrupting the target; the verifier rejects it. +- Eleven unchanged predecessor files against their recorded SHA-256 pins. + +`rounded_check.py --out PATH` exports all rounded-case invoices and output +hashes; their canonical digest is retained in `EXPECTED.json`. The dense +reference is the predecessor's Gaussian-elimination path, separate from its +rounded leaf execution. The synthetic factors isolate the recursive interface; +no root-factor certificate or preparation algorithm is claimed. + +## Cost and scope + +The supplied two-clean witness executes 243 dirty nodes and 259 clean nodes; +the one-clean witness executes 575 and one. At common complete leaf price `t` +and internal dispatch prices `g_D,g_C`, its saving before external costs is +`480t + 332g_D - 258g_C`. Initialization/admission, parameter preparation, +planning, routing, source access and magnitude/precision capacity remain +charged in [PROOF.md](PROOF.md). Leaf-count optimality is not a runtime benchmark. + +`planner.py` emits a streaming signed instruction word. Callers must provide +distinct physical arrays, immutable parameters, exactly zero clean inputs and +deterministic zero-preserving leaves whose negative instructions subtract the +identical increment. Clean admission is a caller obligation. Linear leaves +realize the ordered product; nonlinear rounded increments can depend on dirt. + +[PROOF.md](PROOF.md) gives the restoration induction, exact class recurrence, +full-capacity theorem and conditional error bound. [SOURCES.json](SOURCES.json) +pins the base and dependencies; [NOTICE.md](NOTICE.md) retains attribution. +[CLAIM.md](CLAIM.md) records scope selection and overlap checks; +[VALIDATION.md](VALIDATION.md) records executed checks and limits. + +This extends PR714's clean root and PR788's one reusable clean array by +allowing a second clean connector while the first stays reserved. PR730, +PR758 and PR784 optimize or bound different all-dirty echo classes; we make +no global optimum or literature-priority claim. The selected #626/#543 +construction and `upstream/` are unchanged. Clean-space supply, supplier +integration, physical hosting, all-size compilation, fixed-tape routing and +analytic transfer remain unresolved; this is not a multiplication theorem. diff --git a/research/two-clean-checkpoints/SOURCES.json b/research/two-clean-checkpoints/SOURCES.json new file mode 100644 index 0000000000..813a562f72 --- /dev/null +++ b/research/two-clean-checkpoints/SOURCES.json @@ -0,0 +1,101 @@ +{ + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "files": [ + { + "local_path": "vendor/pr628/DIRTY-PROOF.md", + "source_pr": 628, + "source_commit": "0768f97d06c623b8211e651543c66135796b62bf", + "source_path": "research/prime-power-cyclic-scan/DIRTY-PROOF.md", + "sha256": "bb7c2fdc1c4673d56531fd56fb8790c81a16813ac152c10f1afabc9efdd70d61" + }, + { + "local_path": "vendor/pr628/NOTICE.md", + "source_pr": 628, + "source_commit": "0768f97d06c623b8211e651543c66135796b62bf", + "source_path": "research/prime-power-cyclic-scan/NOTICE.md", + "sha256": "abeacf1ad1491d5797cfcf1f3832799bbf3b24b99597229d7bc884059a51ec68" + }, + { + "local_path": "vendor/pr628/check.py", + "source_pr": 628, + "source_commit": "0768f97d06c623b8211e651543c66135796b62bf", + "source_path": "research/prime-power-cyclic-scan/check.py", + "sha256": "a3e46b556894d71a1c83bbbac01c50c1a541285fc9422a3567d5eb1d1ee86e7d" + }, + { + "local_path": "vendor/pr628/dirty.py", + "source_pr": 628, + "source_commit": "0768f97d06c623b8211e651543c66135796b62bf", + "source_path": "research/prime-power-cyclic-scan/dirty.py", + "sha256": "09e7f41141594e6540828330d27be27c083ee6569660ae42c0cd519b09fc8d21" + }, + { + "local_path": "vendor/pr628/interval_kernel.py", + "source_pr": 628, + "source_commit": "0768f97d06c623b8211e651543c66135796b62bf", + "source_path": "research/prime-power-cyclic-scan/interval_kernel.py", + "sha256": "9b7bb24640a9a7d3f83c7951dfef483ec933db4c50de6c0130b85f450eeddfbe" + }, + { + "local_path": "vendor/pr628/scan.py", + "source_pr": 628, + "source_commit": "0768f97d06c623b8211e651543c66135796b62bf", + "source_path": "research/prime-power-cyclic-scan/scan.py", + "sha256": "1a9c01ca1a29a9be1e756858161202621db29d5d332a4266b4017a9502a50d7e" + }, + { + "local_path": "vendor/pr628/weighted.py", + "source_pr": 628, + "source_commit": "0768f97d06c623b8211e651543c66135796b62bf", + "source_path": "research/prime-power-cyclic-scan/weighted.py", + "sha256": "8b0f93d131a30e64eb0ccd893779daffea79c0c00f1d2a30a91d23eb2bf0bff5" + }, + { + "local_path": "vendor/pr788/PROOF.md", + "source_pr": 788, + "source_commit": "ff8251519e009a01ede6b27e3f5af703eaa70132", + "source_path": "research/reusable-clean-checkpoint/PROOF.md", + "sha256": "ac24b3753aba8edf9de07bf061846f14237ee6ca233da4df21111a3e47c4ec36" + }, + { + "local_path": "vendor/pr788/README.md", + "source_pr": 788, + "source_commit": "ff8251519e009a01ede6b27e3f5af703eaa70132", + "source_path": "research/reusable-clean-checkpoint/README.md", + "sha256": "4a2eb2754c9f83dba2cee604eb13841f7d79c6bc0714fa2604fe01be6b559580" + }, + { + "local_path": "vendor/pr788/checkpoint.py", + "source_pr": 788, + "source_commit": "ff8251519e009a01ede6b27e3f5af703eaa70132", + "source_path": "research/reusable-clean-checkpoint/checkpoint.py", + "sha256": "174ba95abe94c080f137365f3fcc0ebcab701cf01c2e499dc45a7ac28fe81f34" + }, + { + "local_path": "vendor/pr788/pr714-NOTICE.md", + "source_pr": 788, + "source_commit": "ff8251519e009a01ede6b27e3f5af703eaa70132", + "source_path": "research/reusable-clean-checkpoint/vendor/pr714-NOTICE.md", + "sha256": "6ceb5a6ea4cc8ddfa26b957aea3a571a1ca7032ca428e7ab8ed7e3e71563496a" + } + ], + "related_work": [ + { + "pr": 714, + "commit": "efad8a40094ab453c0525efef0b0eff2a5d8b850" + }, + { + "pr": 673, + "commit": "b3917936aafbd0d680a954a86e25c4ce7e28a9f9" + }, + { + "pr": 758, + "commit": "a164f06263e438ead570b169e5b7103aa45bf228" + }, + { + "pr": 784, + "commit": "548e42022b37a300f8bf745e848c38baccbce056" + } + ] +} diff --git a/research/two-clean-checkpoints/VALIDATION.md b/research/two-clean-checkpoints/VALIDATION.md new file mode 100644 index 0000000000..7496536df7 --- /dev/null +++ b/research/two-clean-checkpoints/VALIDATION.md @@ -0,0 +1,75 @@ +# Validation receipt + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +Platform: macOS 14.6, arm64; CPython 3.14.7. +The scoped checks below completed on 2026-10-13 UTC. + +```sh +python3 -I -B research/two-clean-checkpoints/verify.py +python3 -I -O -B research/two-clean-checkpoints/verify.py +python3 -B research/two-clean-checkpoints/test_package.py +python3 -B scripts/verify_selected_result.py +``` + +Both verifier modes matched the same frozen certificate. The package test +passed a relocated isolated/optimized replay and rejected three corruptions: +an altered integer cost, `true` substituted for clean count `1`, and changed +pinned proof bytes. Failed verification did not overwrite the evidence. +All eleven vendored files also matched `git show COMMIT:PATH` at the exact +source pins, independently of the JSON manifest. + +Completed mathematical coverage: + +- 1,619 decorated ordered binary trees through six factors, with independent + preorder enumeration; Catalan counts and uniqueness checked. +- 723 whole-tree optimum comparisons: every `{1,3}` price vector through five + factors and unit prices at six; every `0 <= clean <= scratch <= n-1`. + 449 states were feasible. 32,039 tree/resource admissions were checked. +- 61,804 forward instructions across complete free-noncommutative symbolic + checks; every source and scratch coefficient, ordered target product and + literal inverse checked. The same 1,619 trees passed nonlinear mod-101 + restoration and inversion, without claiming nonlinear product equality. +- The 50-factor witnesses passed separate whole-word symbolic execution; + all 28 full-capacity `(s,c)` entries through `s=6` matched `4^(s-c)3^c`. +- 137 exact minima matched the unchanged PR788 optimizer, restricting the + new recurrence to all-dirty or one-clean inputs. +- 192 actual PR628 rounded-leaf cases, including both signs/directions, + length one/three, zero/one/two clean arrays and two nonzero dirt choices. + Dense rational represented-factor comparisons, exact source/scratch and + spectator restoration, literal inverses, zero-source identity, 3,760 + forward calls and 34,112 phase reads passed. +- Eighteen admission/instruction/accounting controls plus a rounded + dirty-as-clean counterexample. Restoring a mislabeled dirty connector alone + does not establish a correct target. + +Separate workers reviewed the proof, implementation and evidence. Review +found and fixed a lazy-emission mutation hazard by freezing input trees, +and narrowed the magnitude statement to completed leaf boundaries; internal +leaf arithmetic still requires its own bound. These were AI-assisted checks, +not independent human review or a proof-assistant formalization. + +The selected-record checker passed. The new package makes no change to +`upstream/`, the selected certificate, any supplier or repository generator. +No remote CI, Linux replay, practical performance gain, new κ or full +multiplication theorem is claimed. + +## Repository baseline + +One `make verify` ran on a disposable checkout of the exact base. Its first +seven groups passed; `gen4-bank-verify` then stopped because SymPy was absent. +An isolated CPython 3.14.7 environment supplied SymPy 1.14.0, NumPy 2.5.4 +and SciPy 1.18.1. The resumed gen4 target passed all nine finite stages. + +`frontier626-verify` initially could not find Boost in `/usr/include`. With +`BOOST_INCLUDE=/opt/homebrew/include` (Boost 1.88), the complete selected +replay passed: bit543, declarations, complex626, independent owner accounting, +helper interfaces and exact bindings. The selected conditional κ remained +`51110230636731/31250000000000000`. No supplier source was patched. + +The resumed baseline also passed `verify-certificates` and `verify-ternary`. +The unrelated `verify-research` historical search group passed its bit and +mixed-point screens, then was deliberately stopped during +`audit_early_sharing.py` to bound the sprint. `verify-strips`, `verify-clones`, +`verify-positive`, `verify-joint`, `verify-pair` and `verify-tests` were not +reached. **No full `make verify` pass is claimed.** The complete new-package +verification and selected-frontier replay passed before this stop. diff --git a/research/two-clean-checkpoints/independent_check.py b/research/two-clean-checkpoints/independent_check.py new file mode 100644 index 0000000000..8d64b375c4 --- /dev/null +++ b/research/two-clean-checkpoints/independent_check.py @@ -0,0 +1,154 @@ +"""Whole-tree and symbolic checks independent of the planning recurrence.""" + +import json +from collections import Counter +from itertools import product +from math import comb + +import oracle +import planner + + +def _check(condition, message): + if not condition: + raise AssertionError(message) + + +def _add_polynomial(target, increment, sign): + for word, coefficient in increment.items(): + value = target.get(word, 0) + sign * coefficient + if value: + target[word] = value + else: + target.pop(word, None) + + +def _symbolic_execute(word, arrays): + # Factor i prefixes a noncommuting letter to each source monomial. + for factor, source, target, sign in word: + increment = {("f" + str(factor),) + monomial: coefficient + for monomial, coefficient in arrays[source].items()} + _add_polynomial(arrays[target], increment, sign) + + +def _nonlinear_execute(word, arrays): + # Zero-preserving, target-independent, and generally nonlinear. Modular + # arithmetic bounds the values without introducing inexact inverses. + for factor, source, target, sign in word: + x = arrays[source] + increment = (x * x + (factor + 1) * x) % 101 + arrays[target] = (arrays[target] + sign * increment) % 101 + + +def _check_tree(tree, n): + dirty, clean = oracle.required_resources(tree) + counts = oracle.leaf_multiplicities(tree) + produced_profile = planner.profile(tree) + _check(produced_profile["dirty"] == dirty, "dirty resource mismatch") + _check(produced_profile["clean"] == clean, "clean resource mismatch") + _check(produced_profile["leaves"] == dict(enumerate(counts)), + "leaf multiplicity mismatch") + + dirty_ids = tuple(range(2, 2 + dirty)) + clean_ids = tuple(range(2 + dirty, 2 + dirty + clean)) + word = tuple(planner.emit(tree, 0, 1, dirty_ids, clean_ids)) + inverse = tuple(planner.emit(tree, 0, 1, dirty_ids, clean_ids, -1)) + _check(inverse == tuple((i, s, d, -sign) for i, s, d, sign in reversed(word)), + "inverse must reverse the complete literal word") + _check(Counter(i for i, _, _, _ in word) == dict(enumerate(counts)), + "emitted call count mismatch") + + initial = [{("a" + str(i),): 1} if i not in clean_ids else {} + for i in range(2 + dirty + clean)] + arrays = [dict(value) for value in initial] + _symbolic_execute(word, arrays) + expected = [dict(value) for value in initial] + product_word = tuple("f" + str(i) for i in reversed(range(n))) + ("a0",) + _add_polynomial(expected[1], {product_word: 1}, 1) + _check(arrays == expected, "noncommutative product or scratch restoration") + _symbolic_execute(inverse, arrays) + _check(arrays == initial, "noncommutative forward/inverse restoration") + + nonlinear_initial = [(13 + 17 * i) % 101 if i not in clean_ids else 0 + for i in range(len(initial))] + nonlinear = nonlinear_initial.copy() + _nonlinear_execute(word, nonlinear) + _check(all(nonlinear[i] == nonlinear_initial[i] + for i in range(len(initial)) if i != 1), + "nonlinear source/scratch restoration") + _nonlinear_execute(inverse, nonlinear) + _check(nonlinear == nonlinear_initial, "nonlinear inverse restoration") + return len(word) + + +def run_checks(): + """Exhaust small trees; return stable, JSON-serializable check counts.""" + tree_counts = {} + emitted_leaf_calls = 0 + comparisons = 0 + feasible = 0 + tree_resource_checks = 0 + for n in range(1, 7): + trees = oracle.enumerate_trees(n) + expected_count = comb(2 * n - 2, n - 1) // n * 2 ** (n - 1) + _check(len(trees) == expected_count and len(set(trees)) == expected_count, + "decorated Catalan enumeration is incomplete or duplicated") + tree_counts[str(n)] = len(trees) + for tree in trees: + emitted_leaf_calls += _check_tree(tree, n) + # Verify admissions for every relevant fixed pool partition, + # including insufficient and surplus-resource cases. + for scratch in range(n): + for clean in range(scratch + 1): + allowed = oracle.admissible(tree, scratch, clean) + dirty_ids = tuple(range(2, 2 + scratch - clean)) + clean_ids = tuple(range(2 + scratch - clean, 2 + scratch)) + try: + planner.emit(tree, 0, 1, dirty_ids, clean_ids) + except ValueError: + _check(not allowed, "emitter rejected an admissible tree") + else: + _check(allowed, "emitter accepted insufficient resources") + tree_resource_checks += 1 + + price_vectors = product((1, 3), repeat=n) if n <= 5 else [(1,) * n] + # Whole-tree minima are grouped by resource profile only to avoid + # re-inspecting trees for each budget; no child solutions are reused. + profiles = [(tree, oracle.required_resources(tree), + oracle.leaf_multiplicities(tree)) for tree in trees] + for prices in price_vectors: + scored = [(sum(p * count for p, count in zip(prices, counts)), d, c) + for _, (d, c), counts in profiles] + for scratch in range(n): + for clean in range(scratch + 1): + costs = [cost for cost, d, c in scored + if d <= scratch - clean and c <= clean] + expected = min(costs) if costs else None + answer = planner.solve(prices, scratch, clean) + actual = None if answer is None else answer[0] + _check(actual == expected, + f"whole-tree optimum mismatch: {prices}, {scratch}, {clean}") + if answer is not None: + feasible += 1 + _check(answer[1] in trees, "producer tree outside enumeration") + _check(oracle.admissible(answer[1], scratch, clean), + "producer optimum violates resources") + _check(oracle.tree_cost(answer[1], prices) == answer[0], + "producer optimum has incorrect price") + comparisons += 1 + + return {"decorated_trees_by_leaf_count": tree_counts, + "trees_checked": sum(tree_counts.values()), + "tree_resource_admissions_checked": tree_resource_checks, + "forward_leaf_calls_checked": emitted_leaf_calls, + "noncommutative_symbolic_cases": sum(tree_counts.values()), + "nonlinear_mod101_cases": sum(tree_counts.values()), + "whole_tree_optimum_comparisons": comparisons, + "feasible_optimum_comparisons": feasible, + "prices": "all {1,3}^n for 1<=n<=5; unit prices for n=6", + "budgets": "every 0<=clean<=scratch<=n-1", + "status": "passed"} + + +if __name__ == "__main__": + print(json.dumps(run_checks(), indent=2, sort_keys=True)) diff --git a/research/two-clean-checkpoints/oracle.py b/research/two-clean-checkpoints/oracle.py new file mode 100644 index 0000000000..54f24c3369 --- /dev/null +++ b/research/two-clean-checkpoints/oracle.py @@ -0,0 +1,114 @@ +"""Exhaustive decorated-tree oracle, independent of interval optimization. + +Shapes are generated as preorder bit words, then every internal vertex is +decorated D or C. No resource recurrence or optimal-substructure assumption +is used. Apache-2.0. +""" + +from functools import lru_cache +from itertools import combinations, product + + +def _require(ok, message): + if not ok: + raise ValueError(message) + + +@lru_cache(None) +def enumerate_trees(n): + """Return every ordered decorated full binary tree on leaves 0,...,n-1.""" + _require(type(n) is int and n > 0, "positive integer leaf count") + result = [] + # One bit per vertex: 1 opens two children, 0 terminates a leaf. Exactly + # one open slot is present initially and every proper prefix leaves a + # positive number of slots. This tests complete shapes before decoration. + for internal_positions in combinations(range(2 * n - 1), n - 1): + internal = set(internal_positions) + slots = 1 + for position in range(2 * n - 1): + slots += 1 if position in internal else -1 + if slots == 0 and position != 2 * n - 2: + break + else: + if slots != 0: + continue + leaf_positions = [i for i in range(2 * n - 1) if i not in internal] + leaves = dict(zip(leaf_positions, range(n))) + for labels in product("DC", repeat=n - 1): + decorations = dict(zip(internal_positions, labels)) + stack = [] + for position in reversed(range(2 * n - 1)): + if position in internal: + left, right = stack.pop(), stack.pop() + stack.append((decorations[position], left, right)) + else: + stack.append(leaves[position]) + _require(len(stack) == 1, "invalid preorder shape") + result.append(stack[0]) + return tuple(result) + + +def _paths(tree): + """Yield (leaf, connector/side path), preserving left-to-right order.""" + stack = [(tree, ())] + while stack: + node, path = stack.pop() + if type(node) is int: + _require(node >= 0, "nonnegative leaf index") + yield node, path + else: + _require(isinstance(node, tuple) and len(node) == 3 + and node[0] in ("D", "C"), "decorated binary tree") + kind, left, right = node + stack.append((right, path + ((kind, "R"),))) + stack.append((left, path + ((kind, "L"),))) + + +def required_resources(tree): + """Peak separately reserved dirty and clean arrays over all leaf paths.""" + paths = [path for _, path in _paths(tree)] + return (max(sum(kind == "D" for kind, _ in path) for path in paths), + max(sum(kind == "C" for kind, _ in path) for path in paths)) + + +def leaf_multiplicities(tree): + """Count invocations by multiplying path-edge call multiplicities.""" + paths = list(_paths(tree)) + _require([leaf for leaf, _ in paths] == list(range(len(paths))), + "leaves must be 0,...,n-1 in order") + # All edges double calls except the right edge of a clean connector. + return tuple(2 ** sum(kind == "D" or side == "L" for kind, side in path) + for _, path in paths) + + +def tree_cost(tree, prices): + prices = tuple(prices) + _require(prices and all(type(p) is int and p > 0 for p in prices), + "positive integer prices") + counts = leaf_multiplicities(tree) + _require(len(counts) == len(prices), "one price per leaf") + return sum(count * price for count, price in zip(counts, prices)) + + +def admissible(tree, total_scratch, clean_budget): + _require(type(total_scratch) is int and type(clean_budget) is int + and 0 <= clean_budget <= total_scratch, "scratch contract") + dirty, clean = required_resources(tree) + return dirty <= total_scratch - clean_budget and clean <= clean_budget + + +def best_tree(prices, total_scratch, clean_budget): + """Minimize by inspecting all whole trees; return (cost, tree) or None.""" + prices = tuple(prices) + _require(prices and all(type(p) is int and p > 0 for p in prices), + "positive integer prices") + _require(type(total_scratch) is int and type(clean_budget) is int + and 0 <= clean_budget <= total_scratch, "scratch contract") + best = None + for tree in enumerate_trees(len(prices)): + if admissible(tree, total_scratch, clean_budget): + candidate = tree_cost(tree, prices), tree + # Tree tie-breaking is deliberately independent of the producer. + if best is None or candidate[0] < best[0]: + best = candidate + return best diff --git a/research/two-clean-checkpoints/planner.py b/research/two-clean-checkpoints/planner.py new file mode 100644 index 0000000000..5217b9a2f2 --- /dev/null +++ b/research/two-clean-checkpoints/planner.py @@ -0,0 +1,116 @@ +"""Exact ordered binary checkpoint planning; Python standard library only.""" +from functools import lru_cache + + +def natural(value, name): + if type(value) is not int or value < 0: + raise ValueError(f'{name} must be a nonnegative integer') + + +def solve(prices, scratch, clean): + """Return (minimum complete signed-leaf price, literal tree), or None. + + Nodes are ('C' or 'D', left, right); leaves are ordered factor indices. + Ties minimize completed leaf calls, then follow split/connector order. + """ + prices = tuple(prices) + if not prices or any(type(p) is not int or p <= 0 for p in prices): + raise ValueError('prices must be nonempty positive integers') + natural(scratch, 'scratch') + natural(clean, 'clean') + if clean > scratch: + raise ValueError('clean cannot exceed scratch') + dirty = min(scratch - clean, len(prices) - 1) + clean = min(clean, len(prices) - 1) + + @lru_cache(None) + def visit(lo, hi, d, c): + n = hi - lo + if n == 1: + return prices[lo], 1, lo + if n > 1 << (d + c): + return None + best = None + for cut in range(lo + 1, hi): + for kind, dd, cc, right_mult in ( + ('D', d - 1, c, 2), ('C', d, c - 1, 1)): + if dd < 0 or cc < 0: + continue + left = visit(lo, cut, dd, cc) + right = visit(cut, hi, dd, cc) + if left is None or right is None: + continue + candidate = (2 * left[0] + right_mult * right[0], + 2 * left[1] + right_mult * right[1], + (kind, left[2], right[2])) + if best is None or candidate[:2] < best[:2]: + best = candidate + return best + + result = visit(0, len(prices), dirty, clean) + return None if result is None else (result[0], result[2]) + + +def profile(tree): + """Count complete leaf/internal invocations and simultaneous connectors.""" + if type(tree) is int and tree >= 0: + return {'leaves': {tree: 1}, 'C': 0, 'D': 0, 'clean': 0, 'dirty': 0} + if not isinstance(tree, (tuple, list)) or len(tree) != 3 or tree[0] not in ('C', 'D'): + raise ValueError('invalid tree') + kind, left, right = tree + a, b = profile(left), profile(right) + if set(a['leaves']) & set(b['leaves']): + raise ValueError('duplicate factor') + if max(a['leaves']) >= min(b['leaves']): + raise ValueError('factors must remain ordered') + m = 1 if kind == 'C' else 2 + leaves = {i: 2 * v for i, v in a['leaves'].items()} + leaves.update({i: m * v for i, v in b['leaves'].items()}) + return {'leaves': leaves, + 'C': 2 * a['C'] + m * b['C'] + int(kind == 'C'), + 'D': 2 * a['D'] + m * b['D'] + int(kind == 'D'), + 'clean': max(a['clean'], b['clean']) + int(kind == 'C'), + 'dirty': max(a['dirty'], b['dirty']) + int(kind == 'D')} + + +def emit(tree, source, target, dirty, clean, sign=1): + """Validate roles and return a streaming literal instruction iterator. + + Caller must supply zero clean arrays and deterministic zero-preserving, + target-independent leaf increments. Negative leaves must be exact inverses. + """ + # JSON trees use lists: snapshot them before validating a lazy program. + def freeze(node): + if type(node) is int and node >= 0: + return node + if not isinstance(node, (tuple, list)) or len(node) != 3 or node[0] not in ('C', 'D'): + raise ValueError('invalid tree') + return node[0], freeze(node[1]), freeze(node[2]) + + tree = freeze(tree) + dirty, clean = tuple(dirty), tuple(clean) + roles = (source, target) + dirty + clean + if any(type(x) is not int or x < 0 for x in roles) or len(set(roles)) != len(roles): + raise ValueError('array roles must be distinct nonnegative integers') + if type(sign) is not int or sign not in (-1, 1): + raise ValueError('sign must be +1 or -1') + p = profile(tree) + if p['dirty'] > len(dirty) or p['clean'] > len(clean): + raise ValueError('insufficient scratch by type') + + def walk(node, src, dst, ds, cs, direction): + if type(node) is int: + yield node, src, dst, direction + return + kind, left, right = node + z = cs[0] if kind == 'C' else ds[0] + dd, cc = (ds, cs[1:]) if kind == 'C' else (ds[1:], cs) + ops = [(left, src, z, 1), (right, z, dst, 1), (left, src, z, -1)] + if kind == 'D': + ops.append((right, z, dst, -1)) + if direction == -1: + ops = [(child, x, y, -s) for child, x, y, s in reversed(ops)] + for child, x, y, s in ops: + yield from walk(child, x, y, dd, cc, s) + + return walk(tree, source, target, dirty, clean, sign) diff --git a/research/two-clean-checkpoints/rounded_check.py b/research/two-clean-checkpoints/rounded_check.py new file mode 100644 index 0000000000..f541de4124 --- /dev/null +++ b/research/two-clean-checkpoints/rounded_check.py @@ -0,0 +1,184 @@ +"""Exact-rational replay of the checkpoint words with PR628 rounded leaves. + +Synthetic stable factors isolate scheduling from factor preparation. The dense +reference solves each represented factor matrix without calling the leaf. +""" +import argparse +from collections import Counter +from fractions import Fraction as F +import hashlib +import importlib.util +from itertools import product +import json +from pathlib import Path + +import planner + +ROOT = Path(__file__).resolve().parent + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def load_leaf(): + spec = importlib.util.spec_from_file_location('checkpoint_pr628', ROOT / 'vendor/pr628/dirty.py') + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def digest(value): + return hashlib.sha256(json.dumps(value, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + + +def ceil_log2(value): + need(value > 0, 'positive logarithm argument') + result = value.numerator.bit_length() - value.denominator.bit_length() + while F(2) ** result < value: + result += 1 + while F(2) ** (result - 1) >= value: + result -= 1 + return result + + +def precision(calls, magnitude, target=64): + # PR628 DIRTY-PROOF.md: beta=1/2, maximum leaf multiplier r=3. + beta, r = F(1, 2), 3 + a, growth = 13 * (r + 1) / beta ** 3, 2 + F(r) / beta + bits = max(ceil_log2(a), ceil_log2(2 / beta ** 2), + target + 1 + ceil_log2(calls * a * (magnitude + 1)) + + (calls - 1) * ceil_log2(growth)) + unit = F(1, 1 << bits) + bound = calls * a * (magnitude + 1) * unit * growth ** (calls - 1) + need(a * unit <= 1 and unit <= beta ** 2 / 2, 'leaf precision conditions') + need(bound <= F(1, 1 << (target + 1)), 'whole-word precision budget') + return bits, bound + + +class Phases: + """Count every indexed read, including the inherited stability validation.""" + + def __init__(self, values): + self.values, self.reads = values, 0 + + def __getitem__(self, index): + self.reads += 1 + return self.values[index] + + +def execute(leaf, arrays, steps, factors, phases, bits, direction): + stats = dict(leaves=0, scalar_steps=0) + for factor, source, target, sign in steps: + leaf.leaf(arrays[source], arrays[target], factors[factor], phases, + F(1, 2), bits, direction, sign, stats) + return stats + + +def case(leaf, nf, scratch, clean, length, direction, sign, dirt): + c = leaf.c + factors = [(i % 2 == 0, (F(1, 4), F((-1) ** i, 8)), F(3 if i == 0 else 1)) + for i in range(nf)] + prices = tuple((6 if inside else 5) * length - 2 for inside, _, _ in factors) + plan = planner.solve(prices, scratch, clean) + need(plan is not None, 'rounded fixture is feasible') + price, tree = plan + clean_slots = tuple(range(2, 2 + clean)) + dirty_slots = tuple(range(2 + clean, 2 + scratch)) + steps = list(planner.emit(tree, 0, 1, dirty_slots, clean_slots, sign)) + inverse = list(planner.emit(tree, 0, 1, dirty_slots, clean_slots, -sign)) + need(inverse == [(f, s, t, -q) for f, s, t, q in reversed(steps)], 'inverse chronology') + counts = Counter(f for f, _, _, _ in steps) + need(sum(prices[i] * counts[i] for i in range(nf)) == price, 'planned phase price') + + # Include an untouched spectator beyond the supplied scratch roles. + arrays = [[(F(2 + j + i, 8), F(3 - j + 2 * i, 8)) for i in range(length)] + for j in range(scratch + 3)] + for j in dirty_slots: + arrays[j] = [(a + dirt, b - dirt) for a, b in arrays[j]] + for j in clean_slots: + arrays[j] = [c.ZERO] * length + initial = [row[:] for row in arrays] + magnitude = max(abs(a) + abs(b) for row in arrays for a, b in row) + bits, bound = precision(len(steps), magnitude) + units = (c.ONE, (F(0), F(1)), (F(3, 5), F(4, 5))) + values = [units[i % len(units)] for i in range(length)] + phases = Phases(values) + stats = execute(leaf, arrays, steps, factors, phases, bits, direction) + need(arrays[0] == initial[0] and arrays[2:] == initial[2:], 'exact source/scratch restoration') + need(all(arrays[j] == [c.ZERO] * length for j in clean_slots), 'exact clean-zero restoration') + need(phases.reads == price, 'actual phase-access invoice') + need(stats == dict(leaves=len(steps), scalar_steps=3 * length * len(steps)), 'actual traversal invoice') + + expected = leaf.exact_operator(initial[0], factors, values, direction) + net = [c.sub(value, start) for value, start in zip(arrays[1], initial[1])] + need(all(c.norm2(c.sub(value, leaf.scaled(exact, sign))) <= bound ** 2 + for value, exact in zip(net, expected)), 'dense rational comparison') + output_hash = digest([[str(a), str(b)] for a, b in net]) + execute(leaf, arrays, inverse, factors, phases, bits, direction) + need(arrays == initial, 'exact rounded whole-word inverse') + need(phases.reads == 2 * price, 'inverse phase-access invoice') + + # The clean connector requires exact F(0)=0, not merely a small residual. + arrays = [row[:] for row in initial] + arrays[0] = [c.ZERO] * length + zero_initial = [row[:] for row in arrays] + execute(leaf, arrays, steps, factors, Phases(values), bits, direction) + need(arrays == zero_initial, 'exact zero-source identity') + return dict(factors=nf, scratch=scratch, clean=clean, length=length, + direction=direction, sign=sign, dirt=dirt, calls=len(steps), + phase_reads=price, lift_loop_visits=3 * length * len(steps), + working_bits=bits, target_bits=64, output_sha256=output_hash) + + +def dirty_as_clean_control(leaf): + """A nonzero C connector restores its dirt but contaminates the target.""" + c = leaf.c + tree = ('C', 0, 1) + steps = list(planner.emit(tree, 0, 1, (), (2,))) + factors = [(True, (F(1, 4), F(1, 8)), F(1)), + (False, (F(1, 4), F(-1, 8)), F(1))] + # Zero source makes the invalid clean assumption particularly observable. + arrays = [[c.ZERO] * 3, [c.ONE] * 3, + [(F(1), F(1, 2)), (F(-3, 4), F(1, 4)), (F(1, 2), F(-1))]] + initial = [row[:] for row in arrays] + values = [c.ONE, (F(0), F(1)), (F(3, 5), F(4, 5))] + bits, bound = precision(len(steps), F(2)) + execute(leaf, arrays, steps, factors, Phases(values), bits, 1) + need(arrays[0] == initial[0] and arrays[2] == initial[2], 'control source/dirt restoration') + errors = [c.norm2(c.sub(x, y)) for x, y in zip(arrays[1], initial[1])] + need(max(errors) > bound ** 2, 'dirty-as-clean mutation must fail the dense target contract') + return dict(name='dirty_array_used_as_clean', rejected=True, + source_and_dirt_restored=True, target_contaminated=True, + target_error_squared=str(max(errors))) + + +def run_checks(): + leaf = load_leaf() + configurations = ((1, 0, 0), (2, 1, 0), (2, 1, 1), + (3, 2, 0), (3, 2, 1), (3, 2, 2), + (5, 3, 0), (5, 3, 1), (5, 3, 2), + (8, 3, 0), (8, 3, 1), (8, 3, 2)) + rows = [case(leaf, nf, scratch, clean, length, direction, sign, dirt) + for nf, scratch, clean in configurations + for length, direction, sign, dirt in product((1, 3), (-1, 1), (-1, 1), (-7, 5))] + controls = [dirty_as_clean_control(leaf)] + return dict(status='passed', cases=len(rows), rows=rows, controls=controls, + scope='Synthetic stable inside/outside factors; exact dyadic rounding; ' + 'dense represented-factor comparison. Phase generation and storage ' + 'are external costs; no root certificate or machine performance claim.') + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--out', type=Path) + args = parser.parse_args() + result = run_checks() + if args.out: + args.out.write_text(json.dumps(result, indent=2) + '\n') + print(json.dumps(dict(status=result['status'], cases=result['cases'], controls=len(result['controls'])))) + + +if __name__ == '__main__': + main() diff --git a/research/two-clean-checkpoints/test_package.py b/research/two-clean-checkpoints/test_package.py new file mode 100644 index 0000000000..11427dce0d --- /dev/null +++ b/research/two-clean-checkpoints/test_package.py @@ -0,0 +1,51 @@ +#!/usr/bin/env python3 +"""Relocated optimized replay and source/certificate corruption controls.""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +ROOT = Path(__file__).resolve().parent + + +def run(path, expected_error=None): + result = subprocess.run([sys.executable, '-I', '-O', '-B', str(path / 'verify.py')], + cwd=path.parent, text=True, capture_output=True) + if expected_error is None: + if result.returncode or 'PASS_TWO_CLEAN_CHECKPOINTS' not in result.stdout: + raise ValueError(result.stdout + result.stderr) + elif result.returncode == 0 or expected_error not in result.stderr: + raise ValueError('wrong corruption result: ' + result.stdout + result.stderr) + + +def main(): + with tempfile.TemporaryDirectory(prefix='two-clean-checkpoints-') as tmp: + root = Path(tmp) + package = root / 'relocated' + shutil.copytree(ROOT, package, ignore=shutil.ignore_patterns('__pycache__', '*.pyc')) + run(package) + expected = package / 'EXPECTED.json' + original = expected.read_bytes() + for mutation in ('cost', 'boolean'): + data = json.loads(original) + if mutation == 'cost': + data['primary'][2]['cost'] = 1249 + else: + # Python equality treats True == 1; canonical JSON must not. + data['primary'][1]['clean'] = True + expected.write_text(json.dumps(data)) + changed = expected.read_bytes() + run(package, 'certificate mismatch') + if expected.read_bytes() != changed: + raise ValueError('verification overwrote a corrupt certificate') + expected.write_bytes(original) + source = package / 'vendor/pr628/DIRTY-PROOF.md' + source.write_bytes(source.read_bytes() + b'\nsource mutation\n') + run(package, 'source drift') + print('PASS_TWO_CLEAN_PACKAGE: relocated optimized replay; 3 corruptions rejected without overwrite') + + +if __name__ == '__main__': + main() diff --git a/research/two-clean-checkpoints/vendor/pr628/DIRTY-PROOF.md b/research/two-clean-checkpoints/vendor/pr628/DIRTY-PROOF.md new file mode 100644 index 0000000000..caf4aafc78 --- /dev/null +++ b/research/two-clean-checkpoints/vendor/pr628/DIRTY-PROOF.md @@ -0,0 +1,128 @@ +# Cyclic inverse shears with dirty array restoration + +This extends the classical rounded cyclic-inverse primitive of PR628. It removes +its need for a clean length-L intermediate array. It does not supply a common-label +Clifford realization, reversible bit arithmetic, transform layout, or the complete +integer-multiplication reduction. No new kappa follows from this lemma. + +## Contract + +Input x, target y and h borrowed arrays are complex dyadic grids of spacing u=2^-w. +Every array has length L>=1 and may initially contain arbitrary data. The arrays +are distinct. Their initial infinity norms are at most D. Read-only phases tau_i +have modulus one. Phase generation/storage and coefficient preparation are paid; +there is no free phase table. The primitive adds an approximation to Q(W)^-1 x +to y, restores x and every borrowed array exactly, and needs only a constant number +of clean scalar arithmetic registers besides loop counters and factor descriptors. +Here (Wx)_i=tau_i*x_(i-d), initially for d=+/-1 in a cyclic layout, and +Q(z)=r^-1 product_(j=1)^n(z-rho_j), n=r-1, with stable reciprocal/inner factors +of norm at most 1-beta. The final increment can depend on the initial dirt within +the stated approximation error. Exact independence of the increment from dirt is +not claimed for rounded arithmetic. + +## One factor + +First consider T x = y defined by y_i=x_i+b_i*y_(i-d), |b_i|<=1-beta. +Choose the cyclic order in direction d. Let z be the zero-boundary causal solution +and p_i the product of b from the first position through i. Let c be the complete +product. Then y_i=z_i+p_i*s, s=z_last/(1-c). The stable cyclic equation itself +implies ||y||<=B/beta when ||x||<=B, so |s|<=B/beta. + +On the dyadic grid, perform the causal pass directly in x, skipping the first +position: x_i += round(b_i*x_previous). These are integer lifts. Reversing their +order and subtracting the same rounded source products restores x exactly, +including arbitrary nonzero initial values. During the first pass also accumulate +the rounded scalar product c_hat. Compute s_hat=round(z_hat_last/(1-c_hat)). +In a second pass accumulate rounded prefix products p_hat_i and add +round(m_i*(z_hat_i+round(p_hat_i*s_hat))) to the appropriate target position. +Finally undo the causal lifts. Each target position is written exactly once; +its existing value never enters the computed increment. Scalar arithmetic and +coefficient scratch can be cleared classically; no reversible arithmetic gate +claim is made. Three passes suffice, excluding validation scans and paid +coefficient access. O(1) clean scalar words and O(log L) indexing bits suffice. + +Nearest complex rounding has norm error at most u. Assuming u<=beta^2/2, +|z_hat-z|<=u/beta, |p_hat-p|<=u/beta, |c_hat-c|<=u/beta, and +|1-c_hat|>=beta/2. Using s=z_last/(1-c), rather than separately bounding the +numerator and denominator, gives + + |s_hat-s| <= u + (2/beta)*(u/beta + (B/beta)*(u/beta)) + <= 5*(B+1)*u/beta^3. + +Also |p_hat|<=1+u/beta<=3/2. Hence the corrected output before m multiplication +has error at most 12*(B+1)*u/beta^3. If |m_i|<=r, the final rounded multiplication +has error at most a*(B+1)*u, a=13*(r+1)/beta^3. None of these constants depends +on L. + +For an outer root, b_i=rho^-1*tau_i, m_i=-rho^-1. For an inner root, scan in +direction -d with b_i=rho*conjugate(tau_(i+d)); the value at position i is +multiplied by conjugate(tau_i) and added at i-d. This is +(W-rho I)^-1=(I-rho W^-1)^-1 W^-1. The scalar r is included in one leaf's +multiplier. Each exact factor has operator norm at most K=r/beta. No permutation +of the mutable source array is required for the inner factor. + +## Product of factors + +For exact linear maps A,B and a dirty scratch array z, the sequence + + z += B*x; y += A*z; z -= B*x; y -= A*z + +adds AB*x to y and restores z. Split the factor list in halves recursively; +use one distinct borrowed array per recursion depth. A negative call executes +the exact inverse instruction word (reverse operation order and invert signs). +It is not obtained by negating signs in the original order. + +The rounded construction still restores every borrowed array and x exactly. +Inductively each call preserves its input and all deeper scratch, and its increment +is independent of its target. The paired calls computing B therefore see the same +input and deeper initial dirt. Never use an ancestor input or target as deeper +scratch: the ancestor target may have changed between the paired calls. This is +an explicit alias exclusion in the executable contract. + +There are h=ceil(log2 n) borrowed arrays and at most N=4*n^2 leaf calls. Pad to the +next power of two for this count if desired (identity leaves require no rounded +inverse). The implementation splits without padding and checks the actual count. + +For the ideal elementary shears, the joint max norm grows by at most C=1+K per +leaf. With a*u<=1 the computed trajectory satisfies + + M_j+1 <= G^j*(D+1), G=C+1. + +Comparing the complete rounded word with the ideal word on the same initial +arrays, and summing the propagated leaf errors, gives + + E_N <= N*a*(D+1)*u*G^(N-1). + +The ideal word cancels all borrowed initial data exactly. This proves the target +error bound for every length and every initial dirt bounded by D, while actual +restoration is exact without an error allowance. Choosing + + w >= p+1+ceil(log2(N*a*(D+1)))+(N-1)*ceil(log2 G) + +and enforcing a*u<=1 and u<=beta^2/2 gives execution error <=2^(-p-1). +PR628's coefficient/phase perturbation bound, budgeted to <=2^(-p-1) for the +original x, then gives total <=2^-p. That perturbation bound scales with ||x||; +for general input bound X use p+ceil(log2(max(1,X))) in its preparation budget. +The initial borrowed dirt does not enter the ideal operator perturbation bound. + +PR628 has log2(beta^-1)=O(r^3). Therefore these deliberately loose budgets need +w=O(p+log(D+1)+r^5) bits, and O(r^2) passes. Inside a leaf, the causal state and closure scalars add at most another +O(log(beta^-1)+log r) magnitude bits. Maximum transient magnitudes thus add +O(log(D+1)+r^5) integer bits, already covered by this word-size bound. Standard +fast fixed-precision arithmetic yields soft-O((L*r^2+r^3)*(p+log(D+1)+r^5)) +bit work plus charged phase-oracle and routing costs. Factor preparation and +coefficient enclosures are inherited from PR628. Borrowed storage is +O(L log r) words; clean arithmetic storage is O(w+log L) bits up to the chosen +multiplication implementation's workspace, plus O(r) read-only factor descriptors. +A machine with only a fixed number of dirty data arrays is not covered by this +contract. Arbitrary stride still incurs PR628's explicitly charged routing. + +## Executable evidence + +`dirty.py` uses exact rational arithmetic and explicit nearest dyadic rounding. +It checks generic variable-coefficient leaves, dense independently assembled +factor inverses, both orientations, nonzero targets, several initial dirty arrays, +exact source/scratch restoration, exact whole-word inversion, and the leaf count. +Finite checks support the implementation; the inequalities above are the all-L +argument. The exact-rational prototype does not itself implement the claimed +fast fixed-precision arithmetic cost. diff --git a/research/two-clean-checkpoints/vendor/pr628/NOTICE.md b/research/two-clean-checkpoints/vendor/pr628/NOTICE.md new file mode 100644 index 0000000000..22fbeb8ef0 --- /dev/null +++ b/research/two-clean-checkpoints/vendor/pr628/NOTICE.md @@ -0,0 +1,24 @@ +# Attribution and scope + +Ali Romman's PR621, exact head 520774462b19b29af41554b74def31f9d01e997e, +supplies the prime-power kernel circle bound. Its kernel attribution is +OpenAI's exact-DFT preprint at adc7f1241b42e322a6451854ab7e4b4c146bf78a +(`loc:newton`, `loc:fourier-factorization`) and classical q-Pochhammer/Newton +factorization, including Alexey Kuznetsov's cited q-calculus work. This +package does not claim to originate those constructions. + +Pan's approximate-factorization theorem is used in the form stated by +Mehlhorn, Sagraloff and Wang; Brent's work supplies fast elementary-function +evaluation. Causal/anticausal recursive filtering is standard, as illustrated +by the Briand-Davy source listed in SOURCE.json. Sources are cited for these +specific tools, not as proofs of this package's complete claim. + +The scan rounding analysis, explicit budget composition, interval and +factor certificates, routed reference execution, and packaging were +prepared with substantial OpenAI Codex assistance for chafreaky. The dense +matrix solver and algebraic coefficient crosschecks provide independent +computational paths, not human peer review or formal Lean verification. + +No new multiplication exponent, literature priority, maintainer acceptance, +physical tape execution, or production performance result is claimed. +The code and documents use the repository's Apache-2.0 license. diff --git a/research/two-clean-checkpoints/vendor/pr628/check.py b/research/two-clean-checkpoints/vendor/pr628/check.py new file mode 100644 index 0000000000..5ef6dd67b6 --- /dev/null +++ b/research/two-clean-checkpoints/vendor/pr628/check.py @@ -0,0 +1,178 @@ +"""Rational proof of mixed inside/outside cyclic factor inversion.""" +from pathlib import Path +from fractions import Fraction as F +import argparse,importlib.util,json,math,sys +sys.set_int_max_str_digits(100000) +P=Path(__file__).resolve().parent +def module(name): + s=importlib.util.spec_from_file_location(name,P/(name+'.py'));m=importlib.util.module_from_spec(s);s.loader.exec_module(m);return m +c=module('scan');ik=module('interval_kernel') + +def prime_power(r): + if type(r)!=int or r<3:return False + p=next((d for d in range(2,math.isqrt(r)+1) if r%d==0),r) + while r%p==0:r//=p + return r==1 + +def certify(data): + r,k=data['radix'],data['embedding'] + c.need(prime_power(r) and type(k)==int and 00 and type(target)==int and target>0,'precision budget') + c.need(type(fb)==int and 0=F(1,2),'gauge chart') + parameters=[im/(1+re) for im in v[1] for re in v[0]] + mid=(min(parameters)+max(parameters))/2 + t=c.rounded((mid,F(0)),1024)[0] + sigma=c.mul(center,((1-t*t)/(1+t*t),2*t/(1+t*t))) + c.need(c.norm2(sigma)==1,'exact rational unit phase') + error=sum(max(abs(endpoint-coordinate) for endpoint in iv) for iv,coordinate in zip(box,sigma)) + c.need(error0) + for name in ('unit_root','missing_root','wrong_embedding','low_precision','bad_margin'): + row=json.loads(json.dumps(mixed)) + if name=='unit_root':row['roots'][0]=['1','0'] + if name=='missing_root':row['roots'].pop() + if name=='wrong_embedding':row['embedding']=row['radix'] + if name=='low_precision':row['working_bits']=8 + if name=='bad_margin':row['beta']='1' + try:certify(row) + except ValueError as error:controls.append(dict(name=name,rejected=str(error))) + else:raise ValueError('bad control accepted '+name) + state=certify(mixed);x=[c.ONE,c.ZERO,(F(1,2),F(1,4))] + bad=apply(x,state,1,omit_inner_shift=True) + try:residual_check(x,bad,state,1) + except ValueError as error:controls.append(dict(name='omitted_inner_shift',rejected=str(error))) + else:raise ValueError('inner-shift mutation accepted') + try:apply(x,state,1,(F(1),F(1))) + except ValueError as error:controls.append(dict(name='nonunit_gauge',rejected=str(error))) + else:raise ValueError('nonunit gauge accepted') + args.out.write_text(json.dumps(dict(status='passed',kernel_crosschecks=crosschecks,irrational_gauge=gauge_record,certificates=certificates,cases=cases,controls=controls),indent=2)+'\n') + print(json.dumps(dict(status='passed',certificates=len(certificates),cases=len(cases),dense_cases=sum(row['dense_comparison'] for row in cases),controls=len(controls)))) + +if __name__=='__main__':main() diff --git a/research/two-clean-checkpoints/vendor/pr628/dirty.py b/research/two-clean-checkpoints/vendor/pr628/dirty.py new file mode 100644 index 0000000000..2b94710837 --- /dev/null +++ b/research/two-clean-checkpoints/vendor/pr628/dirty.py @@ -0,0 +1,133 @@ +"""Integer lifting for cyclic inverse shears using borrowed dirty arrays. +Exact rational prototype. Arithmetic workspace and phase access are charged in the proof; +this is not a common-label Clifford word or a bit-reversible arithmetic compiler. +""" +from pathlib import Path +from fractions import Fraction as F +import importlib.util,json,argparse,itertools +P=Path(__file__).resolve().parent +s=importlib.util.spec_from_file_location('weighted',P/'weighted.py');w=importlib.util.module_from_spec(s);s.loader.exec_module(w);c=w.c + +def scaled(z,q):return(z[0]*q,z[1]*q) +def conj(z):return(z[0],-z[1]) +def ordered(n,d):return range(n)if d==1 else range(n-1,-1,-1) + +def lift(x,y,coefficient,beta,bits,d,sign=1,destination=None,multiplier=None,stats=None): + """y += sign*F(x), restoring x exactly; no length-dependent clean data array.""" + n=len(x);c.need(x is not y and n==len(y)>0,'distinct equally sized arrays') + c.need(d in(-1,1)and sign in(-1,1),'orientation and sign') + c.need(0=(beta/2)**2,'closure denominator') + seed=c.rounded(c.div(x[previous],denominator),bits) + power=c.ONE + for i in ordered(n,d): + power=c.rounded(c.mul(coefficient(i),power),bits) + value=c.add(x[i],c.rounded(c.mul(power,seed),bits)) + value=c.rounded(c.mul(multiplier(i),value),bits) + j=destination(i);y[j]=c.add(y[j],scaled(value,sign)) + # The scalar seed and coefficient scratch may be cleared by ordinary classical + # arithmetic. The dirty data itself is restored by exact inverse integer lifts. + first=0 if d==1 else n-1 + for i in ordered(n,-d): + if i!=first:x[i]=c.sub(x[i],c.rounded(c.mul(coefficient(i),x[i-d]),bits)) + if stats is not None:stats['leaves']+=1;stats['scalar_steps']+=3*n + +def leaf(x,y,factor,phases,beta,bits,d,sign,stats): + inside,b,scale=factor;n=len(x) + if inside: + lift(x,y,lambda i:c.mul(b,conj(phases[(i+d)%n])),beta,bits,-d,sign, + lambda i:(i-d)%n,lambda i:scaled(conj(phases[i]),scale),stats) + else: + lift(x,y,lambda i:c.mul(b,phases[i]),beta,bits,d,sign, + multiplier=lambda i:scaled(c.neg(b),scale),stats=stats) + +def compose(x,y,factors,scratch,phases,beta,bits,d,sign=1,stats=None): + """Balanced commutator; negative call is the exact inverse instruction word.""" + c.need(sign in(-1,1)and d in(-1,1),'orientation and sign') + c.need(factors and len(scratch)>=(len(factors)-1).bit_length(),'dirty depth') + arrays=[x,y]+scratch;c.need(len({id(v)for v in arrays})==len(arrays),'all ancestor arrays distinct') + c.need(len(x)>0 and all(len(v)==len(x)for v in arrays)and len(phases)==len(x),'array lengths') + c.need(all(c.norm2(t)==1 for t in phases),'unit phases') + if len(factors)==1:return leaf(x,y,factors[0],phases,beta,bits,d,sign,stats) + mid=len(factors)//2;B,A=factors[:mid],factors[mid:];z=scratch[0];rest=scratch[1:] + operations=[(x,z,B,1),(z,y,A,1),(x,z,B,-1),(z,y,A,-1)] + if sign==-1:operations=[(src,dst,fs,-sgn)for src,dst,fs,sgn in reversed(operations)] + for src,dst,fs,sgn in operations:compose(src,dst,fs,rest,phases,beta,bits,d,sgn,stats) + +def exact_operator(x,factors,phases,d): + # Dense rational oracle constructed independently from the lifting recurrence. + n=len(x);out=x[:] + for inside,b,scale in factors: + a=[[c.ZERO for _ in range(n)]for _ in range(n)] + if inside: + for i in range(n):a[i][i]=c.neg(b);a[i][(i-d)%n]=c.add(a[i][(i-d)%n],phases[i]) + else: + rho=c.div(c.ONE,b) + for i in range(n):a[i][i]=c.neg(rho);a[i][(i-d)%n]=c.add(a[i][(i-d)%n],phases[i]) + out=[scaled(z,scale)for z in w.solve(a,out)] + return out + +def certificate(n,beta,r,D,bits): + N=4*n*n;a=13*(r+1)/beta**3;G=2+F(r)/beta;u=F(1,1<4:raise ValueError('angle bound') + itheta=(point(0),theta) + total=term=ONE + # Taylor remainder for complex exp: <=exp(4)*4^(N+1)/(N+1)! <128*... + n=0 + while True: + n+=1;term=cmul(term,itheta);term=(scale(term[0],F(1,n)),scale(term[1],F(1,n)));total=cadd(total,term) + remainder=F(128*4**(n+1),math.factorial(n+1)) + if remainder 0, 'empty cycle') + need(direction in (-1, 1), 'invalid direction') + need(0 < beta <= 1, 'invalid margin') + need(norm2(b) <= (1-beta)**2, 'uncertified stable factor') + u = F(1, 1 << bits) + need(u <= beta*beta/2, 'precision too low for closure') + order = list(range(len(x))) if direction == 1 else list(reversed(range(len(x)))) + z, power = ZERO, ONE + for i in order: + z = rounded(add(x[i], mul(b, z)), bits) + power = rounded(mul(b, power), bits) + den = sub(ONE, power) + need(norm2(den) >= (beta/2)**2, 'closure lower bound failed') + seed = rounded(div(z, den), bits) + y, previous = [ZERO]*len(x), seed + for i in order: + previous = rounded(add(x[i], mul(b, previous)), bits) + y[i] = previous + return y + +def dense_solve(x, b, direction): + """Independent exact Gaussian elimination on the cyclic matrix.""" + n = len(x) + a = [[ZERO for _ in range(n)] + [x[i]] for i in range(n)] + for i in range(n): + a[i][i] = add(a[i][i], ONE) + j = (i-direction) % n + a[i][j] = sub(a[i][j], b) + for k in range(n): + pivot = next(i for i in range(k, n) if a[i][k] != ZERO) + a[k], a[pivot] = a[pivot], a[k] + p = a[k][k] + a[k] = [div(v, p) for v in a[k]] + for i in range(n): + if i == k: continue + p = a[i][k] + a[i] = [sub(v, mul(p, w)) for v, w in zip(a[i], a[k])] + return [row[-1] for row in a] + +def residual_bound(x, y, b, beta, direction, bound): + # Neumann inverse norm <= 1/beta converts residual to forward error. + for i in range(len(x)): + residual = sub(sub(y[i], mul(b, y[(i-direction) % len(x)])), x[i]) + need(norm2(residual) <= (beta*bound)**2, 'residual error bound failed') + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--out', type=Path, required=True) + args = parser.parse_args() + cases = [] + for beta in (F(1, 2), F(1, 16), F(1, 4096)): + for unit in (ONE, (F(-1), F(0)), (F(3, 5), F(4, 5))): + b = mul((1-beta, F(0)), unit) + for n in (1, 2, 3, 8, 17, 64): + x = [(F((i*7)%13-6, 8), F((i*11)%17-8, 16)) for i in range(n)] + B = max(abs(v[0])+abs(v[1]) for v in x) + for direction in (-1, 1): + bits = 64 + bound = 6*(B+1)*F(1, 1 << bits)/beta**3 + y = scan(x, b, beta, bits, direction) + residual_bound(x, y, b, beta, direction, bound) + if n <= 8: + exact = dense_solve(x, b, direction) + need(all(norm2(sub(v,w)) <= bound**2 for v,w in zip(y,exact)), 'dense comparison failed') + cases.append(dict(beta=str(beta), b=[str(v) for v in b], length=n, + direction=direction, bits=bits, forward_error_bound=str(bound), + dense_crosscheck=n<=8, residual_check=True)) + controls = [] + for name, x, b, beta, bits, direction in ( + ('unstable', [ONE], ONE, F(1,2), 64, 1), + ('underprecision', [ONE], (F(15,16),F(0)), F(1,16), 3, 1), + ('empty', [], ZERO, F(1,2), 64, 1), + ('bad_direction', [ONE], ZERO, F(1,2), 64, 0), + ): + try: scan(x,b,beta,bits,direction) + except ValueError as error: controls.append(dict(name=name,rejected=str(error))) + else: raise ValueError('negative control accepted: '+name) + x = [ONE, ZERO, ONE] + b, beta = (F(1,2),F(0)), F(1,2) + y = scan(x,b,beta,64,1) + y[0] = add(y[0],ONE) + try: residual_bound(x,y,b,beta,1,F(1,1<<40)) + except ValueError as error: controls.append(dict(name='corrupt_output',rejected=str(error))) + else: raise ValueError('corrupt output accepted') + args.out.write_text(json.dumps(dict(status='passed',cases=cases,controls=controls),indent=2)+'\n') + print(json.dumps(dict(status='passed',cases=len(cases),dense_cases=sum(c['dense_crosscheck'] for c in cases),controls=len(controls)))) + +if __name__ == '__main__': main() diff --git a/research/two-clean-checkpoints/vendor/pr628/weighted.py b/research/two-clean-checkpoints/vendor/pr628/weighted.py new file mode 100644 index 0000000000..da90ee6e83 --- /dev/null +++ b/research/two-clean-checkpoints/vendor/pr628/weighted.py @@ -0,0 +1,118 @@ +"""Exact certificates for varying unit phases on a cyclic neighbor shift.""" +from pathlib import Path +from fractions import Fraction as F +import argparse, importlib.util, json +P=Path(__file__).resolve().parent +s=importlib.util.spec_from_file_location('kernel',P/'check.py');k=importlib.util.module_from_spec(s);s.loader.exec_module(k) +c=k.c + +def scan(x,bs,beta,bits,direction): + c.need(len(x)>0 and len(bs)==len(x),'coefficient length') + c.need(direction in (-1,1),'direction') + c.need(0=(beta/2)**2,'closure denominator') + previous=c.rounded(c.div(z,den),bits);y=[c.ZERO]*len(x) + for i in order: + previous=c.rounded(c.add(x[i],c.mul(bs[i],previous)),bits);y[i]=previous + return y + +def apply(x,state,phases,direction,wrong_phase=False): + n=len(x);c.need(n>0 and len(phases)==n,'phase length') + c.need(all(c.norm2(t)==1 for t in phases),'unit phases') + y=[(v[0]*state['radix'],v[1]*state['radix'])for v in x] + for inside,b in state['factors']: + if inside: + inv=[(phases[(i+direction)%n][0],-phases[(i+direction)%n][1])for i in range(n)] + if wrong_phase:inv=[(v[0],-v[1])for v in phases] + bs=[c.mul(b,t)for t in inv] + y=scan(y,bs,state['beta'],state['bits'],-direction) + y=[c.rounded(c.mul(inv[i],y[(i+direction)%n]),state['bits'])for i in range(n)] + else: + y=scan(y,[c.mul(b,t)for t in phases],state['beta'],state['bits'],direction) + y=[c.rounded(c.neg(c.mul(b,v)),state['bits'])for v in y] + return y + +def matrix(q,phases,direction): + # Independently expand W^j entry-by-entry, including wrap-around phases. + n=len(phases);a=[[c.ZERO for _ in range(n)]for _ in range(n)] + for i in range(n): + weight=c.ONE + for j,v in enumerate(q): + col=(i-direction*j)%n;a[i][col]=c.add(a[i][col],c.mul(v,weight)) + weight=c.mul(weight,phases[col]) + return a + +def residual(x,y,a,bound): + for i,row in enumerate(a): + v=c.ZERO + for z,t in zip(row,y):v=c.add(v,c.mul(z,t)) + c.need(c.norm2(c.sub(v,x[i]))<=bound**2,'expanded weighted residual') + +def solve(a,x): + a=[row[:]+[v]for row,v in zip(a,x)];n=len(a) + for j in range(n): + i=next(i for i in range(j,n)if a[i][j]!=c.ZERO);a[i],a[j]=a[j],a[i] + z=a[j][j];a[j]=[c.div(v,z)for v in a[j]] + for i in range(n): + if i!=j: + z=a[i][j];a[i]=[c.sub(v,c.mul(z,t))for v,t in zip(a[i],a[j])] + return [row[-1]for row in a] + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--out',type=Path,required=True);a=ap.parse_args() + units=[c.ONE,(F(0),F(1)),(F(3,5),F(4,5)),(F(-5,13),F(12,13))] + cases=[];certs=[];generic=[];controls=[] + for beta in (F(1,2),F(1,16),F(1,4096)): + for n in (1,2,3,8,17,64): + bs=[c.mul((1-beta,F(0)),units[(i*i+3*i+1)%4])for i in range(n)] + # Alternate magnitudes as well as phases. + bs=[(z[0]/(1+i%2),z[1]/(1+i%2))for i,z in enumerate(bs)] + x=[(F(i%5-2,4),F(i%7-3,8))for i in range(n)] + B=max(abs(z[0])+abs(z[1])for z in x);bound=6*(B+1)*F(1,1<<64)/beta**3 + for d in (-1,1): + y=scan(x,bs,beta,64,d) + m=[[c.ZERO for _ in range(n)]for _ in range(n)] + for i in range(n):m[i][i]=c.ONE;m[i][(i-d)%n]=c.sub(m[i][(i-d)%n],bs[i]) + residual(x,y,m,beta*bound) + if n<=8:c.need(all(c.norm2(c.sub(v,t))<=bound**2 for v,t in zip(y,solve(m,x))),'generic dense') + generic.append(dict(beta=str(beta),length=n,direction=d,dense=n<=8)) + sigma,nu,phase_cert=k.irrational_gauge() + for row in json.loads((P/'FACTORS.json').read_text()): + if row['radix'] not in (4,9,16):continue + st=k.certify(row);A=F(st['certificate']['inverse_norm_bound']) + eps=F(st['certificate']['coefficient_error_bound'])+sum(j*(abs(v[0])+abs(v[1]))for j,v in enumerate(st['q']))*nu + c.need(A*eps<1 and A*A*eps/(1-A*eps)+st['budgets'][-1]<=F(1,1<= 2 +} +``` + +Every admissible tree has exactly one such root choice and split. Conversely +each finite entry composes legal children under the reserved-connector rule. +Induction on |I| proves the minimum over this class. It is not a minimum over +all reversible programs, higher-arity trees, or alternative lifetime rules. +A factor count larger than 2^s is impossible because every binary leaf path +has at most s reserved connectors. In C a path with no clean reservation may +use only s-1 dirty connectors. The independent census instead computes these +path constraints and the product of edge multiplicities on decorated trees. + +For t=(1,3,1,1), s=2, a clean-root tree must split 2+2 and costs +2*(2*1+2*3)+(2*1+2*1)=20. A dirty root with two clean children costs +2*(2*1+3)+2*(2*1+1)=16. Each child returns the same clean array to zero. +The node constraints force these shapes at cap two, so 16 is the class minimum. +The actual word has factor multiplicities (4,2,4,2); charging each invocation +at the given prices gives 16. The root-only word has (4,4,2,2), giving 20. +Both contain twelve invocations. With unit prices these two shapes tie. + +There are extra internal dispatches: the reusable word executes one dirty +node and four clean nodes; the root-only word executes one clean node and +three dirty nodes. Both execute twelve leaves. If those equal-sized node +dispatches cost g_D and g_C, respectively, and leaf dispatch costs g_L, +the complete local charges (excluding identical preparation/routing) are +16+g_D+4g_C+12g_L versus 20+3g_D+g_C+12g_L. The saving survives exactly +when 3g_C-2g_D<4. For equal internal price g this is g<4. Unequal routing +or preparation must also be included; no wall-time improvement is asserted. + +## Complete work, memory and precision accounting + +The displayed D/C formulas optimize only one specified signed-leaf bill. +Each t_j must include preparation internal to a leaf, source/target scans, +coefficient/phase access, arithmetic, and restoration. External parameter +preparation is charged separately. If sign prices differ use their maximum, +or a sign-aware extension; the current optimizer does not claim that optimum. + +For a fixed tree let R(t)=t_j+g_leaf at a leaf. At a dirty node, +R=2 R(left)+2 R(right)+g_dirty; at a clean node, +R=2 R(left)+R(right)+g_clean. These g terms pay dispatch, descriptor and +alias checks, controller work and any per-invocation parameter scans. Exact +signed word costs can replace upper prices when measured. The complete charge is + +``` +factor/phase preparation + clean provisioning + clean admission scan ++ R(tree) + routing/access work not already charged + optimization cost. +``` + +No child connector is cleared by erasing borrowed information. Provisioning +requires a real clean length-L array (L writes when that operation is allowed), +and admission scans L values. Data scratch is exactly s arrays of L words, +one initially zero, apart from source and target. This work may need s+2 +payload arrays plus scalar arithmetic workspace and immutable descriptions. +Magnitude bits as well as fractional bits count toward each word's storage. + +The interval optimization has O(n^2 s) cached entries and O(n) split choices +per entry, hence O(n^3 s) arithmetic comparisons (with integer bit costs). +The reference stores literal tree tuples; this is offline preparation, not a +free runtime oracle. A descriptor implementation can use child references. +The emitter materializes N instructions, O(N) memory and time; the interpreter +uses that representation. A streaming compiler could avoid the materialized +word, but is not supplied here. Array admission and instructions are validated +before mutation. Matrix dimensions and the leaf contract remain caller +obligations; failures of a supplied leaf are not transactional. + +Conditionally inherit a per-leaf ideal norm bound K and local error +a*u*(B+1), u=2^-w, for both signs. Put G=2+K, assume a*u<=1, and bound all +initial array norms by D0. After j leaves M_j+1 <= G^j(D0+1). Comparing the +complete word to its ideal linear word yields +e_(j+1) <= (1+K)e_j + a*u*G^j(D0+1), hence +e_N <= N*a*(D0+1)*u*G^(N-1). +For requested error 2^(-p-1), one sufficient common precision is + +``` +w >= p+1+ceil(log2(N*a*(D0+1)))+(N-1)*ceil(log2(G)), +``` + +together with inherited stability conditions. Preparation must separately +meet its scaled error budget. This is a conditional pathwise estimate; the +package does not prove PR628's leaf accuracy or improve its precision order. +The weighted gain uses the SAME twelve calls and does not imply lower N. + +The local weighted fixture does not supply actual cheaper factors, a new +hosted operator or a complete supplier moment. PR673's direct all-role +adapter obstruction remains applicable: its favorable unit-leaf bill already +fails. No new kappa, analytic transfer or complete multiplication proof follows. diff --git a/research/two-clean-checkpoints/vendor/pr788/README.md b/research/two-clean-checkpoints/vendor/pr788/README.md new file mode 100644 index 0000000000..48b0e5b281 --- /dev/null +++ b/research/two-clean-checkpoints/vendor/pr788/README.md @@ -0,0 +1,60 @@ +# Reuse one clean checkpoint across weighted binary subtrees + +**Recursive-interface research; no new kappa.** With four ordered leaf prices +`(1,3,1,1)` and two scratch arrays, a dirty root reuses the same clean connector +in both children. Its weighted signed-leaf bill is **16**, versus **20** for +the optimal clean-root-only binary tree at that same cap. Both execute twelve +leaf calls: the gain concerns unequal complete leaf prices, not fewer calls. +The two nonuniformly priced children are small fixtures, not measured PR628 +supplier costs. For 54 unit-price factors and six arrays the optimum remains +**2112**, matching FanPUYen's PR714. No uniform improvement is asserted. +The changed word adds one internal dispatch. With a common internal dispatch +price g, the full local gain survives only for g<4 in the fixture's units; +the proof also gives the unequal-dispatch threshold. No runtime saving is claimed. + +Run from the repository root, Python 3.10+ and standard library only: + +```sh +python -I -O -B research/reusable-clean-checkpoint/verify.py +``` + +Expected final line: +`PASS_REUSABLE_CLEAN_CHECKPOINT 516 census cases; 1016 basis cases; weighted 20 -> 16; uniform54 2112; no new kappa` + +The package contains an interval optimizer, a signed word emitter, an exact +reference interpreter, an independent decorated-tree census, complete frozen +trees, source hashes and [the proof and cost recurrence](PROOF.md). +The census covers every `{1,3}` price vector through six leaves and every +scratch cap 1 through n-1. All 109 admissible decorated trees through five +leaves receive full noncommutative 2D basis and nonlinear-restoration checks. +The two larger fixtures also receive complete 2D endpoint and inverse basis checks. +Eight controls detect wrong order/sign, omitted restoration, insufficient +scratch, nonzero clean input, aliases and invalid prices. This is finite +evidence supporting a written class-specific induction, not a formal theorem. + +## Comparison and provenance + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. Seed: **54**. +PR714 head: `efad8a40094ab453c0525efef0b0eff2a5d8b850`. +Its proof, notice and count implementation are retained unchanged under +`vendor/`, pinned by SHA-256 in SOURCES.json. This verifier freshly runs its +actual count function as an additional comparison. No predecessor dispatcher +or rounded numerical leaf is used by the new interpreter. + +Credit FanPUYen's clean-root contract and proof, Chafik Boukhalfa / chafreaky's +PR628 leaves, 0xkilgore's PR663 restoration/count audit, androolloyd's PR673 echo +and integration obstruction, and concurrent PR730 (Sagar Thakrar), PR744 (Ali +Romman), PR758 (Koroffstrogov) for distinct all-dirty scheduling work. No +literature priority or superiority to the all-arity all-dirty class is claimed. +The stronger root-only comparator here even allows unbalanced dirty children; +PR714's original unit-price formula remains intact. Selected #626/#543 and +all its contributor lineage supply context, not this new implementation. + +Prepared for **nightangelflowerwin-ops**, with substantial **OpenAI Codex** +assistance in mathematics, implementation, verification and writing. +Apache-2.0; original predecessor notice retained. No independent human review. + +Clean-array supply, actual unequal leaf prices, common precision, routing, +physical hosting, all-size compilation and analytic transfer remain obligations. +No PR628 numerical leaf replay, complete supplier or multiplication theorem is +verified. `upstream/`, the selected result and existing generators are untouched. diff --git a/research/two-clean-checkpoints/vendor/pr788/checkpoint.py b/research/two-clean-checkpoints/vendor/pr788/checkpoint.py new file mode 100644 index 0000000000..81afa31a37 --- /dev/null +++ b/research/two-clean-checkpoints/vendor/pr788/checkpoint.py @@ -0,0 +1,85 @@ +"""One reusable clean connector, ordered binary echo trees. Apache-2.0.""" +from functools import lru_cache + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def optimize(prices, cap, clean=True): + prices = tuple(prices) + require(prices and all(type(p) is int and p > 0 for p in prices), 'positive integer prices') + require(type(cap) is int and cap >= 0 and type(clean) is bool, 'scratch contract') + require(not clean or cap >= 1, 'one clean array must be supplied') + + @lru_cache(None) + def solve(lo, hi, space, available): + if hi - lo == 1: + return prices[lo], ('leaf', lo) + if space == 0 or hi - lo > 2**space: + return None + best = None + for mid in range(lo + 1, hi): + for kind in ('dirty', 'clean'): + if kind == 'clean' and not available: + continue + # Reserving a dirty connector requires a dirty array. If the + # pool contains the one clean array, space must exceed one. + if kind == 'dirty' and available and space == 1: + continue + child_clean = available and kind == 'dirty' + a = solve(lo, mid, space - 1, child_clean) + b = solve(mid, hi, space - 1, child_clean) + if a is None or b is None: + continue + cost = 2*a[0] + (1 if kind == 'clean' else 2)*b[0] + candidate = (cost, (kind, a[1], b[1])) + if best is None or candidate < best: + best = candidate + return best + answer = solve(0, len(prices), cap, clean) + require(answer is not None, 'insufficient scratch') + return answer + + +def emit(tree, source=0, target=1, dirty=(), clean=None, sign=1): + """Signed leaf word. Inverses reverse the complete emitted word.""" + require(sign in (-1, 1), 'sign') + def forward(t, src, dst, pool, zero): + kind = t[0] + if kind == 'leaf': + return [(t[1], src, dst, 1)] + if kind == 'clean': + require(zero is not None, 'missing clean connector') + connector, rest, child_zero = zero, pool, None + elif kind == 'dirty': + require(bool(pool), 'missing dirty connector') + connector, rest, child_zero = pool[0], pool[1:], zero + else: + raise ValueError('unknown node') + left = forward(t[1], src, connector, rest, child_zero) + right = forward(t[2], connector, dst, rest, child_zero) + inv_left = [(i, s, d, -v) for i, s, d, v in reversed(left)] + inv_right = [(i, s, d, -v) for i, s, d, v in reversed(right)] + # Both children restore their own scratch, so the same pool is reused. + return left + right + inv_left + ([] if kind == 'clean' else inv_right) + roles = [source, target] + list(dirty) + ([] if clean is None else [clean]) + require(len(set(roles)) == len(roles), 'role aliases') + word = forward(tree, source, target, tuple(dirty), clean) + return word if sign == 1 else [(i, s, d, -v) for i, s, d, v in reversed(word)] + + +def execute(word, arrays, factors, clean=None, leaf=None): + """Reference indexed-RAM interpreter, with admission before mutation.""" + require(len({id(a) for a in arrays}) == len(arrays), 'array aliases') + require(arrays and len(arrays[0]) > 0 and all(len(a) == len(arrays[0]) for a in arrays), 'lengths') + if clean is not None: + require(0 <= clean < len(arrays) and all(v == 0 for v in arrays[clean]), 'clean array must be zero') + for i, s, d, sign in word: + require(0 <= i < len(factors) and 0 <= s < len(arrays) and 0 <= d < len(arrays) and s != d and sign in (-1, 1), 'instruction') + for i, s, d, sign in word: + value = (leaf(i, arrays[s]) if leaf else + [sum(a*b for a, b in zip(row, arrays[s])) for row in factors[i]]) + require(len(value) == len(arrays[d]), 'leaf output') + arrays[d][:] = [a + sign*b for a, b in zip(arrays[d], value)] diff --git a/research/two-clean-checkpoints/vendor/pr788/pr714-NOTICE.md b/research/two-clean-checkpoints/vendor/pr788/pr714-NOTICE.md new file mode 100644 index 0000000000..8c41f77fac --- /dev/null +++ b/research/two-clean-checkpoints/vendor/pr788/pr714-NOTICE.md @@ -0,0 +1,34 @@ +# Attribution and disclosure + +Prepared for GitHub contributor **FanPUYen**, with substantial **OpenAI Codex** +assistance in mathematical derivation, implementation, verification and writing. +Separate Codex agents reviewed the mathematics and checker and built the rounded +evidence. These are automated reviews, not independent human peer review. + +Chafik Boukhalfa / **chafreaky** contributed PR628's cyclic rounded leaves, +dirty product-shear dispatcher, restoration proof and precision/cost estimates. +Its original notice is retained verbatim in `vendor/pr628-NOTICE.md`. +**@0xkilgore** and OpenAI Codex contributed PR663's exact balanced count and +independent nonlinear-restoration audit; its notice is retained verbatim in +`vendor/pr663-NOTICE.md`. That concurrent result is a credited dependency, +not displaced by the clean-storage tradeoff here. + +**@androolloyd** and OpenAI Codex contributed concurrent PR673's phase-array +alias admission finding and repair. The adapter adopts the corresponding +identity exclusion; its original patch is retained and pinned. PR673's distinct +multiway echo schedule is credited as concurrent work, not incorporated or +independently re-verified here. + +PR628 credits **Ali Romman** for PR621's prime-power circle bound, OpenAI's +exact-DFT manuscript, classical q-Pochhammer/Newton identities and the cited +factorization, elementary-function and recursive-filtering literature. +Those credits are preserved. This contribution claims no literature priority +for compute/use/uncompute or reversible checkpointing. + +The selected #626/#543 construction and its Jeremy Kothe, Chafik Boukhalfa, +eumemic, DreamingOfClouds, Rohan Arun and earlier contributor lineage provide +the repository context. They are not claimed as implementations of this new +interface, and their conditional frontier is not modified. + +New code and writing use the repository's **Apache-2.0** license. All vendored +files are unchanged, with their source-specific notices and exact pins retained. diff --git a/research/two-clean-checkpoints/verify.py b/research/two-clean-checkpoints/verify.py new file mode 100644 index 0000000000..9681105205 --- /dev/null +++ b/research/two-clean-checkpoints/verify.py @@ -0,0 +1,187 @@ +#!/usr/bin/env python3 +"""Reproduce the finite checkpoint evidence; fail closed on changed inputs.""" +import argparse +from collections import Counter +import hashlib +import importlib.util +import json +from pathlib import Path +import random +import sys + +sys.dont_write_bytecode = True +ROOT = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT)) +import independent_check +import planner +import rounded_check + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')) + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def source_check(): + manifest = json.loads((ROOT / 'SOURCES.json').read_text()) + for entry in manifest['files']: + path = ROOT / entry['local_path'] + require(path.resolve().is_relative_to(ROOT), 'source outside package') + require(sha(path.read_bytes()) == entry['sha256'], 'source drift: ' + entry['local_path']) + return dict(files=len(manifest['files']), manifest_sha256=sha((ROOT / 'SOURCES.json').read_bytes())) + + +def witness(prices, scratch, clean): + answer = planner.solve(prices, scratch, clean) + require(answer is not None, 'fixture is infeasible') + cost, tree = answer + dirty_ids = tuple(range(2, 2 + scratch - clean)) + clean_ids = tuple(range(2 + scratch - clean, 2 + scratch)) + word = tuple(planner.emit(tree, 0, 1, dirty_ids, clean_ids)) + counts = Counter(i for i, _, _, _ in word) + prof = planner.profile(tree) + require(dict(counts) == prof['leaves'], 'profile differs from word') + require(cost == sum(prices[i] * count for i, count in counts.items()), 'word bill differs') + # Free-algebra execution checks every initial source/dirt coefficient at + # once, including the larger witness beyond the exhaustive small census. + initial = [{('a' + str(i),): 1} if i not in clean_ids else {} + for i in range(2 + scratch)] + actual = [dict(row) for row in initial] + independent_check._symbolic_execute(word, actual) + expected = [dict(row) for row in initial] + expected[1][tuple('f' + str(i) for i in reversed(range(len(prices)))) + ('a0',)] = 1 + require(actual == expected, 'large witness product/restoration') + return dict(prices=list(prices), scratch=scratch, clean=clean, cost=cost, + leaf_calls=len(word), clean_dispatches=prof['C'], dirty_dispatches=prof['D'], + multiplicities=[counts[i] for i in range(len(prices))], tree=tree, + literal_word_sha256=sha(canonical(word).encode())) + + +def predecessor_check(): + spec = importlib.util.spec_from_file_location('predecessor788', ROOT / 'vendor/pr788/checkpoint.py') + previous = importlib.util.module_from_spec(spec) + spec.loader.exec_module(previous) + rng = random.Random(50) + fixtures = [(tuple([1] * n), (n - 1).bit_length()) for n in range(1, 55)] + fixtures += [(tuple(rng.choice((1, 3, 5)) for _ in range(n)), (n - 1).bit_length()) + for n in range(2, 17)] + checks = 0 + for prices, cap in fixtures: + for clean in (0, 1): + if cap < clean: + continue + ours = planner.solve(prices, cap, clean) + old = previous.optimize(prices, cap, bool(clean)) + require(ours[0] == old[0], 'one-clean predecessor minimum changed') + checks += 1 + return dict(comparisons=checks, weighted_seed=50, + scope='all-dirty and one-clean restrictions match pinned PR788') + + +def negative_controls(): + rejected = [] + invalid = [([], 1, 1), ([True], 1, 1), ([0], 1, 1), ([1], -1, 0), + ([1], 1, 2), ([1], 2, True)] + for args in invalid: + try: + planner.solve(*args) + except ValueError: + rejected.append('invalid_plan_' + str(len(rejected))) + else: + raise ValueError('invalid planning input accepted') + require(planner.solve([1] * 5, 2, 2) is None, 'capacity violation accepted') + rejected.append('insufficient_total_scratch') + t = ('C', ('C', 0, 1), ('C', 2, 3)) + for label, call in ( + ('insufficient_clean', lambda: planner.emit(t, 0, 1, (2,), (3,))), + ('role_alias', lambda: planner.emit(t, 0, 1, (2,), (0, 3))), + ('bad_sign', lambda: planner.emit(t, 0, 1, (), (2, 3), True)), + ('reversed_order', lambda: planner.profile(('D', 1, 0))), + ('duplicate_leaf', lambda: planner.profile(('C', 0, 0))), + ): + try: + call() + except ValueError: + rejected.append(label) + else: + raise ValueError('invalid interface accepted: ' + label) + + word = tuple(planner.emit(t, 0, 1, (), (2, 3))) + initial = [{('a0',): 1}, {('a1',): 1}, {}, {}] + correct = [dict(x) for x in initial] + independent_check._symbolic_execute(word, correct) + mutants = {'omit_restoration': word[:-1], + 'reverse_factor_order': tuple((3 - i, s, d, z) for i, s, d, z in word), + 'wrong_sign': ((word[0][0], word[0][1], word[0][2], -word[0][3]),) + word[1:]} + for label, mutant in mutants.items(): + result = [dict(x) for x in initial] + independent_check._symbolic_execute(mutant, result) + require(result != correct, 'undetected word mutation: ' + label) + rejected.append(label) + # A claimed clean connector may be restored yet still corrupt the target. + dirty = [dict(x) for x in initial] + dirty[2] = {('unexpected_dirt',): 1} + independent_check._symbolic_execute(word, dirty) + require(dirty[1] != correct[1], 'nonzero clean input undetected') + rejected.append('dirty_as_clean_algebra') + require(sum(planner.profile(t)['leaves'].values()) == 9, 'two-clean count') + require(sum(1 for step in word if step[3] == 1) < len(word), 'cleanup is charged') + rejected.append('positive_calls_only_undercharge') + mutable_tree = ['C', 0, 1] + stream = planner.emit(mutable_tree, 0, 1, (), (2,)) + mutable_tree[2] = 0 + require(tuple(stream) == tuple(planner.emit(('C', 0, 1), 0, 1, (), (2,))), + 'mutation after validation changed the instruction stream') + rejected.append('mutation_after_lazy_validation') + return rejected + + +def evidence(): + sources = source_check() + independent = independent_check.run_checks() + main = [witness([1] * 50, 6, clean) for clean in range(3)] + require([w['cost'] for w in main] == [2752, 1728, 1248], 'primary fixture changed') + saturated = [] + for depth in range(7): + for clean in range(depth + 1): + cost = planner.solve([1] * (1 << depth), depth, clean)[0] + expected = 4 ** (depth - clean) * 3 ** clean + require(cost == expected, 'saturated formula failed') + saturated.append(dict(depth=depth, clean=clean, cost=cost)) + rounded = rounded_check.run_checks() + # Bind every exact rounded output and invoice without duplicating 192 rows. + rounded_summary = {key: value for key, value in rounded.items() if key != 'rows'} + rounded_summary['rows_sha256'] = sha(canonical(rounded['rows']).encode()) + rounded_summary['forward_leaf_calls'] = sum(row['calls'] for row in rounded['rows']) + rounded_summary['forward_phase_reads'] = sum(row['phase_reads'] for row in rounded['rows']) + return dict(format=1, sources=sources, independent=independent, + primary=main, saturated=saturated, + weighted=witness([1, 3, 1, 1], 2, 2), + predecessor=predecessor_check(), negative_controls=negative_controls(), + rounded=rounded_summary, + scope='Ordered binary reserved connectors; no new kappa or full multiplication proof') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true', help='explicitly regenerate EXPECTED.json') + args = parser.parse_args() + result = evidence() + path = ROOT / 'EXPECTED.json' + if args.write: + path.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + else: + require(canonical(result) == canonical(json.loads(path.read_text())), 'certificate mismatch') + print('PASS_TWO_CLEAN_CHECKPOINTS: 1619 trees; 192 rounded cases; n50/s6: 1728 -> 1248; no new kappa') + + +if __name__ == '__main__': + main()