diff --git a/Makefile b/Makefile index 66f00cfb30..f4598c8bbf 100644 --- a/Makefile +++ b/Makefile @@ -604,3 +604,12 @@ frontier890-verify: selected-record-check frontier942-verify: selected-record-check @work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier942.XXXXXX"); \ python3 -B scripts/verify_frontier942.py --work "$$work/replay" + +.PHONY: bit-profile-pair-audit-verify bit-profile-pair-audit-full-verify +bit-profile-pair-audit-verify: + python3 research/bit-profile-pair-audit/verify.py + python3 -m unittest tests.test_bit_profile_pair_audit -v + +bit-profile-pair-audit-full-verify: + python3 research/bit-profile-pair-audit/verify.py --full + python3 -m unittest tests.test_bit_profile_pair_audit -v diff --git a/research/bit-profile-pair-audit/EXPECTED.json b/research/bit-profile-pair-audit/EXPECTED.json new file mode 100644 index 0000000000..50da9100d9 --- /dev/null +++ b/research/bit-profile-pair-audit/EXPECTED.json @@ -0,0 +1,81 @@ +{ + "a0": 0.001733, + "base_word": { + "decoder_constant": 63, + "live": 28416, + "objective": 5122.839536792, + "path": "research/e8-bit-p111/data/bitE8mut-p111.json.gz", + "pr": 555, + "profile": { + "1": 1321, + "2": 1342, + "3": 80, + "4": 47, + "5": 102, + "6": 10, + "7": 18 + }, + "rank_mass": 5129, + "shipped_c": "1733052823330162099157/1000000000000000000000000" + }, + "n_legal_pairs_min": 9800, + "pair_search": { + "best_delta": 0.0, + "n_pairs_min": 350000 + }, + "pins": { + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", + "research/e8-bit-p111-tuned/tune/EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "research/e8-bit-p111-tuned/tune/moves.json": "a113933002239eb2dd32726bd572ba8ca41b5bce0d438327dd770754c8d5e0f4", + "research/e8-bit-p111-tuned/tune/tune.py": "bdaf632852c514b257bcb1b81004a942fc022ab876565b4e5f6ff5a038d323c2", + "research/e8-bit-p111-tuned/tune/wlib.py": "a37fdf3cdf5f62945c2a90193401c0e9edc9dd3cda8d8cb36a3b9c329ebe4dbc", + "research/e8-bit-p111/data/bitE8mut-p111.json.gz": "1bc3c53d4baf4927c6a00c339ea3975516471a48074d4d97c6addaded2a4d858" + }, + "pipeline": { + "L": 9, + "T": 32, + "W": 28416, + "deficit": 10272, + "idle_remainder": { + "2": 13920, + "4": 14208, + "42": 288, + "6": 14208, + "7": 21312 + }, + "m": 64 + }, + "pr589_moves": [ + [ + "A", + 2028, + 79 + ], + [ + "A", + 2076, + 517 + ] + ], + "tuned_word": { + "decoder_constant": 63, + "live": 28416, + "n_candidates": 9347, + "n_neutral": 9263, + "objective": 5122.83186992, + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "pr": 589, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "shipped_c": "1733427039589844234749/1000000000000000000000000" + } +} \ No newline at end of file diff --git a/research/bit-profile-pair-audit/LICENSE b/research/bit-profile-pair-audit/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/bit-profile-pair-audit/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/bit-profile-pair-audit/NOTICE.md b/research/bit-profile-pair-audit/NOTICE.md new file mode 100644 index 0000000000..48c6e0349a --- /dev/null +++ b/research/bit-profile-pair-audit/NOTICE.md @@ -0,0 +1,28 @@ +# NOTICE + +`research/bit-profile-pair-audit/` is a research note and exact audit contributed under the +repository's Apache-2.0 license (see `LICENSE`). + +## Predecessor work + +* **PR #555 (eumemic)** — the punctured R439 bit word, its generator, checkers, pricing pipelines and + package structure. The base word `research/e8-bit-p111/data/bitE8mut-p111.json.gz` is read unchanged. +* **PR #543 (eumemic)** — the R420 L3 skeleton (keepers read by targets, then rewritten in phase B) + that #555 stacks on, and the interleaved scalar-interface lemma. +* **PR #545 (DreamingOfClouds)** — the punctured star unit (nine lines neither sources nor targets), + the decoder constant 63 at v = 111, and the deficit identity `m W - rank_mass = T(2Kv - L cst)`. +* **PR #510** — the nine-stage pricing chain (#463 template, 32 replicas, #442 hosting). +* **PR #589 (DreamingOfClouds)** — the two A-section transports audited here, and the tuner + (`tune/tune.py`, `tune/wlib.py`) whose move class this audit prices exactly. +* **PR #620 (GamingPuzzled) and PR #631 (vectorsss)** — the decoder-side bounds (`63/111` optimal for + star label decoders under puncturing), which are orthogonal to the reframing class audited here. + +`code/replay.py` and `code/bitprof.py` were written for this note and share no code with the pinned +dependencies; `code/stateprof.py` and `code/search.py` drive the pinned tuner's move enumeration and +price everything on the exact paid-profile objective. + +## AI disclosure + +Substantial AI assistance was used in preparing this contribution (DeepSeek Harness, deepseek-flash +model). Every claim in `verify.py` is a deterministic exact-arithmetic check against files pinned by +sha256 on the stated base commit, and the numbers in `README.md` are the values those checks assert. diff --git a/research/bit-profile-pair-audit/README.md b/research/bit-profile-pair-audit/README.md new file mode 100644 index 0000000000..7c9420e530 --- /dev/null +++ b/research/bit-profile-pair-audit/README.md @@ -0,0 +1,170 @@ +# The bit paid profile is the whole bit supplier, and the reframing class is exhausted at #589 + +This note prices a bit word from its **paid profile alone**, and then uses that to run an exhaustive +audit of the merged bit supplier. It adds no κ: at the current frontier the bit side does not bind. +It is a scoped exact result about one move class on one word, plus a reusable exact pricer. + +Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`, rebased onto `29218749`; every pinned input +is byte-identical on both. +Objects: PR #555's punctured R439 word (`research/e8-bit-p111/`) and PR #589's tuned word +(`research/e8-bit-p111-tuned/tune/`), both unchanged on main. + +## 1. What is new + +### 1.1 The paid-profile duality + +Let the nine-stage bit pipeline's paid profile be `n = (n_r)`: for each elementary paid climb of +dimension jump `r`, one unit. Let `m` be the pipeline modulus, `W` the live port-register count, and + + M := sum_r r * n_r (rank mass) + D := m*W - M (deficit) + +**Fact.** The certified saving `c` of the word is the unique `a > 0` with + + Psi(a) := sum_r n_r * r * ((m/r)^a - 1) = D. + +*Proof.* The pipeline's `moment`/`certify` pair (`.../engines/moment.py`) finds the root of +`S(a) = sum_r (r n_r)/(m W) * (m/r)^a = 1`. Multiplying by `mW` and subtracting `M` gives `Psi(a) = D`; +`Psi` is strictly increasing on `a > 0` because `(m/r)^a` is, and `r <= m` for every paid rank. +∎ + +Since `Psi(a) = m^a G(a) - M` with `G(a) = sum_r n_r r^(1-a)`, and both `m^a` and `G` are increasing +in `a`, the following is immediate and is what makes search tractable: + +**Corollary.** For **any** fixed `a0 > 0`, the certified saving is a strictly decreasing function of +the single weighted count `G(a0) = sum_r n_r r^(1-a0)`. Rank-profile search is therefore a +one-dimensional linear-objective problem, and a candidate word can be priced in `O(#gates)` with +integer arithmetic only — no root finding and no floating point. + +**Verified exactly.** `code/bitprof.py` re-derives `c` from the profile with its own rational +`ln`/`exp` interval bounds (no repository engine, no floating point). For both words the lower +endpoint of the resulting `10^-24` bracket is *exactly* the shipped 24-digit value: + +| word | shipped `c` | bracket from the profile equation | +|---|---|---| +| #555 base, R439 | `1733052823330162099157/10^24` | lower endpoint equal | +| #589 tuned, R439 | `1733427039589844234749/10^24` | lower endpoint equal | + +Only the **nine-stage** price is used here. The eleven-stage pipeline runs the same pricer on its own +profile (`research/e8-bit-p111-tuned/tune/EXPECTED.json` records both); nothing in this note depends on +the eleven-stage numbers. + +The shipped values include the pipeline's inherited bad-envelope surcharge (32·m² rank-one fallback +calls per paid child at `10^-16`), which is `Psi(a) + 32 m^2 (sum_r n_r) m^a / 10^16 = D` here. The +unsurcharged root is strictly larger by `2.01e-12`, i.e. the surcharge is *not* negligible at 24 +digits; the verifier checks both roots. Reporting the surcharge explicitly is the only correction to +a naive reading of "the certified saving is the root of the moment equation". + +### 1.2 The objective decomposes over registers + +`G` is a sum of per-register contributions: a register's cost depends only on the operations that +touch it. Hence + +* the objective delta of one transported operation is the sum of the deltas of the two registers it + touches, and +* **a `k`-operation improvement requires the `k` operations to share registers.** + +The second point is what makes a *complete* two-move search affordable: at the fixed point the 9,347 +nominated moves reduce to 6.5·10^5 register-adjacent pairs instead of ~4.4·10^7. + +### 1.3 The audit + +Move class (the merged tuner's, `research/e8-bit-p111-tuned/tune/tune.py`): single-operation transport +with reframing under exact commutation and frame nesting, plus Steinberg 3→2. All prices below are on +the **exact** objective `G(a0)`, `a0 = 0.001733`. + +| check | result | +|---|---| +| nominated single moves, #589 tuned word | 9,347 | +| strictly improving single moves | **0** | +| exactly cost-neutral single moves (a flat plateau) | 9,263 | +| improving Steinberg 3→2 moves (671 triples) | **0** | +| legal `(slot, frame)` pairs examined (3,064 operations) | 9,933 | +| operations where the nominated frame is *not* exact-objective optimal | **0** | +| complete register-adjacent two-move neighbourhood (`--full`) | 645,900 pairs | +| best two-move delta | **0**, exactly | + +So the merged word is a fixed point of the *complete* nominated one-move neighbourhood, and the +nomination itself loses nothing at the frame level: the tuner's per-slot frame choice (made with its +own proxy cost) coincides with the exact-objective argmin frame for every operation. Two moves do not +escape the plateau either. + +**Positive control.** Steepest descent on the exact objective, with a full re-nomination at every +step, started from #555's base word, applies **exactly two** moves — `A[2034] -> slot 2028, frame 79` +(PR #589's hoist) and `A[2041] -> slot 2076, frame 517` (PR #589's sink) — and lands on the tuned +word's profile and objective (`5122.831869920` from `5122.839536792`). The machinery rederives #589 +independently rather than being told about it. + +**What this is worth.** It closes the reframing avenue for the merged bit supplier at one and two +moves. Any further bit saving from this word must come from a mechanism outside the class — geometry, +decoder constant, helper count, or hosting — not from moving gates. It also gives the exact marginal +exchange rate for any future move: `dc/c = -(dG/G) / (a (ln m - E[ln r]))`, so a candidate can be +priced before it is built. + +## 2. What this does not claim + +* Not an optimality theorem over bit words. It says nothing about words outside the R439/punctured + family, nor about three-or-more-move escapes of this plateau. +* The two-move search is complete **for the nominated move set**; the verifier separately certifies + that the nominated set already contains the exact-objective best frame for every operation, which is + the only place the nomination could have lost a candidate. +* No κ change. The bit side is not binding: at the merged #589 word `c = 0.0017334`, above the complex + caps cited by the current frontier. This is headroom bookkeeping only. +* The tuner's own proxy objective is *not* identical to the exact objective (largest absolute + discrepancy `1.645e-5` on this word, at `A[2076]`); only its argmin agrees here. The audit prices + everything on the exact objective for that reason. +* Every interface that #543, #555 and #589 retain remains assumed: all-size compilation, + mutable-basis and common-label realization, pooled-cell hosting, the compact/residual, + precision/tape/exact-recovery and analytic contracts. This is a finite exact computation, not a + formal proof of integer multiplication. + +## 2b. Concurrent work, and what it says about this result + +The repository moved while this audit was prepared. Its pinned inputs are unchanged on the current +`main` (`29218749`), and these concurrent contributions are consistent with — and sharpen — the +conclusion above: + +* **PR #1043** improves the *same* #589 word by a mechanism outside the reframing class: it deletes + `helper470` by reading `source77` at a caller boundary, giving R438 and + `c = 0.001734176288479865766692` (from `0.001733427039589844234749`). That is a register/helper + rewrite, not a gate transport, which is exactly where §1.3 says the remaining headroom has to come + from. +* **PR #1040, #1047** reduce complete ADD counts on a different R439 lineage (post-PR915/PR967), and + **#1045** crosses PR941's disjoint-pair floor with a four-helper fusion. Their words, their + accounting (complete ADDs) and their move classes differ from the #589 word and the transport class + audited here, so none of them is a counterexample to the fixed point above; the helper-shear and + fusion mechanisms are further examples of the "outside the class" route. +* These results are cited from their own packages and were not re-run here. + +## 3. Reproduce + +```sh +make bit-profile-pair-audit-verify # ~6 min: every check except the pair search +make bit-profile-pair-audit-full-verify # ~35 min: adds the complete two-move neighbourhood +``` + +Python 3.11+ with `numpy` (used by the pinned tuner). No C++ toolchain, Boost, Lean or network access +is needed: every input is a pinned file on main and every check is exact integer or rational +arithmetic. + +## 4. Files + +* `code/bitprof.py` — the profile→saving equation, with own rigorous rational `ln`/`exp` bounds. +* `code/replay.py` — independent word replay and paid profile (rank over the rationals, not modulo a + prime), sharing no code with `wlib.py`. +* `code/stateprof.py` — the exact objective on the flat elementary-op state and the register + decomposition. +* `code/search.py` — the one-move scan, the exact steepest descent, and the complete register-adjacent + two-move search. +* `verify.py`, `EXPECTED.json` — the checks and every number. + +## 5. Credit and disclosure + +The base word, its generator, its checkers, its pricing pipelines and the tuner are PR #555 (eumemic), +building on PR #543 (eumemic; R420 L3 skeleton), PR #545 (DreamingOfClouds; punctured star unit) and +PR #510. The two transports audited here are PR #589 (DreamingOfClouds). The deficit identity +`m W - rank_mass = T(2Kv - L cst)` is PR #545's. GamingPuzzled's #620 and vectorsss's #631 bound the +decoder side (`63/111`), which is orthogonal to the reframing class audited here. + +Prepared with substantial AI assistance (DeepSeek Harness / deepseek-flash). All checks in `verify.py` +are deterministic and were run against the pinned files on main. diff --git a/research/bit-profile-pair-audit/code/bitprof.py b/research/bit-profile-pair-audit/code/bitprof.py new file mode 100644 index 0000000000..65dbc22873 --- /dev/null +++ b/research/bit-profile-pair-audit/code/bitprof.py @@ -0,0 +1,153 @@ +"""Exact paid-profile arithmetic for bitE8 bit words. + +Two facts are used. + +(1) The certified saving c of a bit supplier with modulus m, live port-register count W and paid + profile n (n_r = number of elementary paid climbs of rank r) is the unique root a > 0 of + + Psi(a) := sum_r n_r * r * ((m/r)^a - 1) = D, D := m*W - sum_r r*n_r . + + Equivalently, since Psi(a) = m^a * G(a) - M with G(a) = sum_r n_r r^(1-a) and M = sum_r r n_r, + and both m^a and G are strictly increasing in a, for ANY fixed a0 the certified saving is a + strictly decreasing function of the single weighted count G(a0) = sum_r n_r r^(1-a0). + Rank-profile search is therefore a linear-objective problem, and a candidate word can be priced + exactly in O(#gates) with no root finding. + +(2) G decomposes over registers: a register's contribution depends only on the gates that touch it, + so the objective delta of a gate transport is the sum of the deltas of the two registers it + touches, and a k-move improvement requires the moves to share registers. + +The root of (1) is certified here with exact rational interval arithmetic (own ln/exp bounds): +no floating point and no dependence on the repository's moment engine is used. +""" +from fractions import Fraction as F +from collections import Counter + +# ---------------------------------------------------------------- rigorous rational ln / exp +def _atanh_ln_bounds(z, terms=60): + """1 <= z < 3/2 -> rational interval for ln z via 2*atanh(t), t=(z-1)/(z+1) <= 1/5.""" + t = (z - 1) / (z + 1) + s = F(0); term = t + for n in range(terms): + s += term / (2 * n + 1) + term *= t * t + rem = 2 * term / ((2 * terms + 1) * (1 - t * t)) + return 2 * s, 2 * (s + rem) + +def ln_bounds(x, terms=60): + """x rational >= 1 -> (lo,hi) with lo <= ln x <= hi.""" + assert x >= 1 + k = 0 + while x >= 2: + x /= 2; k += 1 + j = 0 + if x >= F(3, 2): + x /= F(3, 2); j = 1 + lo, hi = _atanh_ln_bounds(x, terms) + l32 = _atanh_ln_bounds(F(3, 2), terms) + l43 = _atanh_ln_bounds(F(4, 3), terms) + ln2_lo, ln2_hi = l32[0] + l43[0], l32[1] + l43[1] + return k * ln2_lo + j * l32[0] + lo, k * ln2_hi + j * l32[1] + hi + +def exp_bounds(y, terms=60): + """0 <= y <= 1 -> (lo,hi) with lo <= exp(y) <= hi.""" + assert 0 <= y <= 1 + s = F(0); term = F(1) + for n in range(terms): + s += term + term *= y / (n + 1) + return s, s + term / (1 - y / (terms + 1)) + +def pow_bounds(base, a, terms=60): + """base rational >= 1, a rational in [0,1] -> (lo,hi) with lo <= base**a <= hi.""" + assert base >= 1 and 0 <= a <= 1 + llo, lhi = ln_bounds(base, terms) + return exp_bounds(a * llo, terms)[0], exp_bounds(a * lhi, terms)[1] + +# ---------------------------------------------------------------- the fee functional +def ln_table(ranks, m, terms=34): + """ln bounds for each distinct base m/r; computed once, reused for every a.""" + return {r: ln_bounds(F(m, r) if F(m, r) >= 1 else 1 / F(m, r), terms) for r in ranks} + +def fee_bounds(n, m, a, lnb, terms=34): + """rational interval for Psi(a) = sum_r n_r * r * ((m/r)^a - 1) using precomputed ln bounds""" + lo = F(0); hi = F(0) + for r, c in n.items(): + if not c: continue + llo, lhi = lnb[r] + if F(m, r) >= 1: + plo = exp_bounds(a * llo, terms)[0]; phi = exp_bounds(a * lhi, terms)[1] + else: + u = exp_bounds(a * llo, terms)[1]; v = exp_bounds(a * lhi, terms)[0] + plo, phi = 1 / u, 1 / v + w = c * r + lo += w * (plo - 1); hi += w * (phi - 1) + return lo, hi + +def fee_float(n, m, a): + import math + return sum(c * r * (math.exp(a * math.log(m / r)) - 1) for r, c in n.items() if c) + +def profile_deficit(n, m, W): + return m * W - sum(r * c for r, c in n.items()) + +def certify_c(n, m, W, digits=24, terms=34): + """exact rational bracket [q/10^digits, (q+1)/10^digits] for the certified saving c.""" + D = profile_deficit(n, m, W) + assert D > 0, 'non-positive deficit' + lnb = ln_table(set(n), m, terms) + lo, hi = F(0), F(1, 10) + assert fee_bounds(n, m, hi, lnb, terms)[0] > D > fee_bounds(n, m, lo, lnb, terms)[1] + # coarse float narrowing, then exact rational bisection on the grid q/10^digits + piv = sorted(n); lo_f, hi_f = 0.0, 0.1 + for _ in range(80): + mid = (lo_f + hi_f) / 2 + if fee_float(n, m, mid) < D: lo_f = mid + else: hi_f = mid + scale = 10 ** digits + span = 10 ** (digits - 6) + qlo = max(0, int(lo_f * scale) - span); qhi = min(scale // 10, int(hi_f * scale) + span) + assert qlo < qhi + while qhi - qlo > 1: + mid = (qlo + qhi) // 2 + if fee_bounds(n, m, F(mid, scale), lnb, terms)[1] < D: qlo = mid + else: qhi = mid + return F(qlo, scale), F(qhi, scale), D + +def weighted_count(n, a0): + """G(a0) = sum_r n_r r^(1-a0) as a float (for search ordering)""" + return sum(c * (r ** (1.0 - a0)) for r, c in n.items()) + +# ---------------------------------------------------------------- the shipped (surcharged) pricer +SURCHARGE_DEN = 10 ** 16 # 32*m^2 rank-one fallback calls per paid child, charged at rank one + +def surcharge_num(n, m): + return 32 * m * m * sum(n.values()) + +def fee_bounds_bad(n, m, a, lnb, terms=34): + lo, hi = fee_bounds(n, m, a, lnb, terms) + llo, lhi = lnb['_m'] + v = exp_bounds(a * llo, terms)[0]; u = exp_bounds(a * lhi, terms)[1] + K = F(surcharge_num(n, m), SURCHARGE_DEN) + return lo + K * v, hi + K * u + +def certify_c_bad(n, m, W, digits=24, terms=34): + """exact rational bracket for the shipped certified saving c, including the inherited + bad-envelope rank-one fallback surcharge: Psi(a) + 32 m^2 (sum_r n_r) m^a / 10^16 = D.""" + D = profile_deficit(n, m, W) + lnb = ln_table(set(n), m, terms); lnb['_m'] = ln_bounds(F(m), terms) + assert fee_bounds_bad(n, m, F(1, 10), lnb, terms)[0] > D > fee_bounds_bad(n, m, F(0), lnb, terms)[1] + K = surcharge_num(n, m) + lo_f, hi_f = 0.0, 0.1 + for _ in range(100): + mid = (lo_f + hi_f) / 2 + if fee_float(n, m, mid) + K * (m ** mid) / SURCHARGE_DEN < D: lo_f = mid + else: hi_f = mid + scale = 10 ** digits; span = 10 ** (digits - 6) + qlo = max(0, int(lo_f * scale) - span); qhi = min(scale // 10, int(hi_f * scale) + span) + assert qlo < qhi + while qhi - qlo > 1: + mid = (qlo + qhi) // 2 + if fee_bounds_bad(n, m, F(mid, scale), lnb, terms)[1] < D: qlo = mid + else: qhi = mid + return F(qlo, scale), F(qhi, scale), D diff --git a/research/bit-profile-pair-audit/code/replay.py b/research/bit-profile-pair-audit/code/replay.py new file mode 100644 index 0000000000..75f8a09dd7 --- /dev/null +++ b/research/bit-profile-pair-audit/code/replay.py @@ -0,0 +1,87 @@ +"""Independent word-level replay and paid profile for bitE8/1+mut words. + +Written for this audit; it shares no code with `research/e8-bit-p111-tuned/tune/wlib.py`. Frame +dimensions are ranks over the rationals (exact Fraction Gaussian elimination), not reductions modulo +a prime, so the two implementations agree only if the geometry really is what it is claimed to be. + +The paid profile of a word is the multiset of *ascents*: every register is climbed between frames, +and an ascent of dimension d from frame a to frame b with dim b > dim a is one paid elementary climb +of rank d = dim b - dim a. The certified saving depends on the word only through this multiset, +its modulus m and its live register count W. +""" +from collections import Counter +from fractions import Fraction as F + + +def rank_of(vectors): + """rank over Q of a list of rational vectors""" + rows = [[F(x) for x in v] for v in vectors] + if not rows: + return 0 + ncol = len(rows[0]) + rk = 0 + for c in range(ncol): + piv = next((i for i in range(rk, len(rows)) if rows[i][c]), None) + if piv is None: + continue + rows[rk], rows[piv] = rows[piv], rows[rk] + inv = 1 / rows[rk][c] + rows[rk] = [x * inv for x in rows[rk]] + for i in range(rk + 1, len(rows)): + if rows[i][c]: + f = rows[i][c] + rows[i] = [a - f * b for a, b in zip(rows[i], rows[rk])] + rk += 1 + return rk + + +def frame_dims(word): + return [rank_of([word['lines'][j] for j in f]) if f else 0 for f in word['frames']] + + +def contains(dims_ok, a, b): + return dims_ok[a] <= dims_ok[b] + + +def replay_profile(word, dims=None, check_nesting=True): + """paid profile (dict rank -> count) of the word, in the pipeline's accounting: + D, A, then the retained-total snapshot, then B, then C, then the final climb.""" + dims = dims or frame_dims(word) + n = 2 * word['v'] + word['R'] + mask = [sum(1 << j for j in f) for f in word['frames']] + cur = list(word['start']) + P = Counter() + + def climb(r, f): + a = cur[r] + if a == f: + return + if check_nesting and mask[a] & mask[f] != mask[a]: + raise AssertionError('illegal frame descent: register %d, %d -> %d' % (r, a, f)) + d = dims[f] - dims[a] + if d > 0: + P[d] += 1 + elif d < 0: + raise AssertionError('descending climb') + cur[r] = f + + for sec in ('D', 'A'): + for f, t, ss in word[sec]: + for r in [t, *ss]: + climb(r, f) + tops = [dims[cur[q]] for q in word['ret']] + for f, t, ss in word['B']: + for r in [t, *ss]: + climb(r, f) + for f, t, ss in word['C']: + for r in [t, *ss]: + climb(r, f) + for r, f in enumerate(word['final']): + climb(r, f) + P.update(tops) + return dict(sorted(P.items())), dims + + +def live_count(word, replicas=32): + """live port-register count of the nine-stage bit pipeline: replicas * 2 * K * v, K = 4.""" + return replicas * 8 * word['v'] diff --git a/research/bit-profile-pair-audit/code/search.py b/research/bit-profile-pair-audit/code/search.py new file mode 100644 index 0000000000..ba92a3c73d --- /dev/null +++ b/research/bit-profile-pair-audit/code/search.py @@ -0,0 +1,155 @@ +"""Searches on the exact paid-profile objective. + +Move class (the one the merged tuner uses, PR #589 / research/e8-bit-p111-tuned/tune/tune.py): +single-operation transport with reframing. Each open operation may be lifted out of the flat +elementary-op list and re-inserted at any slot it commutes to, at any catalogue frame that contains +the pre-frames and is contained in the post-frames of its two registers, subject to the retained-total +copy-rank rule. Frame closure frames are created on demand by the frame catalogue. + +Three searches are exposed: + scan_singles - every nominated single move, priced exactly (the complete one-move neighbourhood) + exact_greedy - steepest descent with a full re-nomination at every step + pair_search - complete two-move neighbourhood: by the register decomposition of the objective, + only pairs sharing a register can improve, so for every nominated move M1 every + nominated move on an operation touching a register of M1 is evaluated exactly. +""" +import bisect + + +def nominated(view, best_move, thr=1e9): + """all (delta, q, frame) the tuner nominates for every operation of `view`""" + out = [] + for i in range(len(view.ops)): + c = best_move(view, i, thr=thr, all_=True) + if c: + out.append((i, c)) + return out + + +def scan_singles(T, S, best_move): + """complete nominated one-move neighbourhood, exactly priced. returns (base, [(d, sec, i, q, F)])""" + base = S.objective() + rows = [] + for sec in 'AB': + V = T.view(sec) + for i, cands in nominated(V, best_move): + for (dproxy, q, F) in cands: + from stateprof import apply_move, undo_move + om = apply_move(V, i, q, F) + S.rebuild_z() + d = S.objective() - base + undo_move(V, q, om) + rows.append((d, dproxy, sec, i, q, F)) + return base, rows + + +def all_legal_moves(V, i, commute, best_move): + """every legal (slot, frame) for operation i, not only the proxy's best frame per slot""" + cat = V.cat + ops = V.ops + n = len(ops) + op = ops[i] + f0, t, s = op + lo = i + while lo > 0 and commute(op, ops[lo - 1]): + lo -= 1 + hi = i + while hi < n - 1 and commute(op, ops[hi + 1]): + hi += 1 + + def tl(r): + return [j if j < i else j - 1 for j in V.touch[r] if j != i] + + tt, ts = tl(t), tl(s) + + def frame_of(e): + return ops[e if e < i else e + 1][0] + + starts = sorted({lo} | {e + 1 for e in tt + ts if lo <= e + 1 <= hi} | ({i} if lo <= i <= hi else set())) + out = [] + for k, st in enumerate(starts): + en = (starts[k + 1] - 1) if k + 1 < len(starts) else hi + q = min(max(i, st), en) + + def ctx(lst, r): + kk = bisect.bisect_left(lst, q) + p = frame_of(lst[kk - 1]) if kk > 0 else V.pre[r] + nx = frame_of(lst[kk]) if kk < len(lst) else V.post[r] + return p, nx, kk + + pt, nt, kt = ctx(tt, t) + ps, ns, ks = ctx(ts, s) + low = cat.masks[pt] | cat.masks[ps] + high = cat.masks[nt] & cat.masks[ns] + if low & ~high: + continue + Fs = [int(x) for x in cat.feasible(low, high)] + F0 = cat.closure(low) + if cat.masks[F0] & ~high == 0 and F0 not in Fs: + Fs.append(F0) + for F in Fs: + ok = True + for r, lst, kk in ((t, tt, kt), (s, ts, ks)): + if r in T_ret(V) and kk == len(lst) and F != V.T.cp[r]: + ok = False + if ok: + out.append((q, F)) + return out + + +def T_ret(V): + return V.T.ret + + +def exact_greedy(T, S, best_move, max_steps=200, tol=1e-9): + """steepest descent on the exact objective with a full re-nomination at every step""" + base = S.objective() + applied = [] + for _ in range(max_steps): + _, rows = scan_singles(T, S, best_move) + rows.sort(key=lambda x: x[0]) + if not rows or rows[0][0] >= -tol: + break + d, _, sec, i, q, F = rows[0] + V = T.view(sec) + from stateprof import apply_move + apply_move(V, i, q, F) + S.rebuild_z() + base = S.objective() + applied.append(dict(section=sec, op=i, slot=q, frame=F, delta=d, objective=base)) + return base, applied + + +def pair_search(T, S, best_move, singles, verbose=False): + """complete register-connected two-move neighbourhood, exactly priced""" + from stateprof import apply_move, undo_move + base = S.objective() + best = None + bestinfo = None + npairs = 0 + singles = sorted(singles, key=lambda x: x[0]) + for (d1, dproxy, sec, i, q, F) in singles: + V = T.view(sec) + t, s = V.ops[i][1], V.ops[i][2] + om = apply_move(V, i, q, F) + S.rebuild_z() + V.refresh() + nbr = set() + for r in (t, s): + nbr.update(V.touch[r]) + for j in sorted(nbr): + c2 = best_move(V, j, thr=1e9, all_=True) + if not c2: + continue + for (dproxy2, q2, F2) in c2: + om2 = apply_move(V, j, q2, F2) + S.rebuild_z() + tot = S.objective() - base + undo_move(V, q2, om2) + npairs += 1 + if best is None or tot < best: + best = tot + bestinfo = dict(delta1=d1, section1=sec, op1=i, slot1=q, frame1=F, + op2=j, slot2=q2, frame2=F2, objective1=0.0) + undo_move(V, q, om) + return base, best, bestinfo, npairs diff --git a/research/bit-profile-pair-audit/code/stateprof.py b/research/bit-profile-pair-audit/code/stateprof.py new file mode 100644 index 0000000000..9d0d6df4ab --- /dev/null +++ b/research/bit-profile-pair-audit/code/stateprof.py @@ -0,0 +1,88 @@ +"""Exact paid-profile objective on the flat elementary-op state of a bitE8 word, without rebuilding +the word dictionary, plus the objective decomposition used by the pair search. + +The paid profile of a word is the sum over registers of the weights of that register's frame ascents +through D, A, B, the retained-total snapshot, C (the reverse of the z-destination gates of A then B, +all at the full frame) and final. A register's contribution therefore depends only on the operations +that touch it, so + + * the objective delta of one transported operation is the sum of the deltas of the two registers + it touches, and + * a k-operation improvement requires the k operations to share registers. + +Minimising G(a0) = sum_r n_r r^(1-a0) for any fixed a0 > 0 maximises the certified saving c, because +the certified c is the root of Psi(a) = m^a G(a) - M = D and both m^a and G are increasing in a. +""" +from collections import Counter + + +class StateProf: + """paid profile / objective of the flat op list held in a tune.Tuner""" + + def __init__(self, T, a0=0.001733): + self.T = T + self.V = T.V + self.N = T.N + self.wt = [r ** (1.0 - a0) for r in range(0, 64)] + self.start = list(T.w['start']) + self.final = list(T.w['final']) + self.ret = list(T.w['ret']) + self.dims = T.cat.dim # live list: Cat.closure may append frames + self.full = next(i for i, m in enumerate(T.cat.masks) if bin(m).count('1') == T.V) + self.rebuild_z() + + def rebuild_z(self): + V = self.T.V + self.z = [g for g in self.T.secs['A'] + self.T.secs['B'] if not (V <= g[1] < 2 * V)] + + def profile(self): + T = self.T + dim = self.dims + cur = list(self.start) + P = Counter() + + def climb(r, f): + a = cur[r] + if a == f: + return + d = dim[f] - dim[a] + if d > 0: + P[d] += 1 + cur[r] = f + + for f, t, ss in T.w['D']: + for r in [t, *ss]: + climb(r, f) + for f, t, s in T.secs['A']: + climb(t, f); climb(s, f) + tops = [dim[cur[q]] for q in self.ret] + for f, t, s in T.secs['B']: + climb(t, f); climb(s, f) + fu = self.full + for f, t, s in reversed(self.z): + climb(t, fu); climb(s, fu) + for r, f in enumerate(self.final): + climb(r, f) + P.update(tops) + return dict(sorted(P.items())) + + def objective(self): + return sum(n * self.wt[r] for r, n in self.profile().items()) + + +def apply_move(V, i, q, frame): + """transport op i of view V to slot q at `frame`; returns a token for undo_move""" + op = V.ops.pop(i) + old = (i, op[0]) + op[0] = frame + V.ops.insert(q, op) + V.reindex() + return old + + +def undo_move(V, q, old): + i, f0 = old + op = V.ops.pop(q) + op[0] = f0 + V.ops.insert(i, op) + V.reindex() diff --git a/research/bit-profile-pair-audit/verify.py b/research/bit-profile-pair-audit/verify.py new file mode 100644 index 0000000000..baa118669c --- /dev/null +++ b/research/bit-profile-pair-audit/verify.py @@ -0,0 +1,231 @@ +#!/usr/bin/env python3 +"""Verifier for the bit paid-profile duality and the PR #589 tuned-word audit. + + python3 research/bit-profile-pair-audit/verify.py # cheap checks (~1 min) + python3 research/bit-profile-pair-audit/verify.py --full # adds the complete pair search (~10 min) + +Checks + 1 source pins (sha256) of every file this audit reads from main + 2 independent word replay: paid profile of PR #555's base word and PR #589's tuned word + 3 the profile-to-saving identity: the certified c is the unique root of + Psi(a) = sum_r n_r r((m/r)^a - 1) = D, D = m*W - rank_mass, and the shipped c is bracketed + exactly by rational interval arithmetic + 4 the rank-mass / deficit identity of #545: m*W - rank_mass = 32*(8v - 9*cst) + 5 complete nominated one-move neighbourhood of the tuned word: no strictly improving move + 6 completeness of the nomination: the exact-objective argmin frame equals the nominated frame for + every operation, over every legal (slot, frame) pair + 7 positive control: exact-objective steepest descent from PR #555's base word rediscovers PR #589's + two transports and lands on the tuned word + 8 negative controls + 9 with --full: the complete register-connected two-move neighbourhood +""" +import argparse +import gzip +import hashlib +import json +import os +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.abspath(os.path.join(HERE, '..', '..')) +CODE = os.path.join(HERE, 'code') +sys.path.insert(0, CODE) +sys.path.insert(0, os.path.join(ROOT, 'research', 'e8-bit-p111-tuned', 'tune')) +sys.path.insert(0, os.path.join(ROOT, 'research', 'e8-bit-carrier-skeleton', 'code', + 'hub', 'e8-r740-replica32', 'code', 'engines')) + +import replay # noqa: E402 (this package, independent replay) +from fractions import Fraction as F # noqa: E402 +from bitprof import certify_c, certify_c_bad, profile_deficit, fee_float, surcharge_num, SURCHARGE_DEN # noqa: E402 + +EXPECTED = json.load(open(os.path.join(HERE, 'EXPECTED.json'))) +for _k in ('base_word', 'tuned_word'): + EXPECTED[_k]['profile'] = {int(r): n for r, n in EXPECTED[_k]['profile'].items()} +EXPECTED['pipeline']['idle_remainder'] = {int(r): n for r, n in EXPECTED['pipeline']['idle_remainder'].items()} +FAILURES = [] + + +def check(name, ok, detail=''): + print(' %-6s %s%s' % ('PASS' if ok else 'FAIL', name, (' ' + detail) if detail else '')) + if not ok: + FAILURES.append(name) + + +def sha256(path): + return hashlib.sha256(open(path, 'rb').read()).hexdigest() + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--full', action='store_true', help='add the complete two-move neighbourhood') + args = ap.parse_args() + + print('1. source pins') + for rel, want in EXPECTED['pins'].items(): + p = os.path.join(ROOT, rel) + got = sha256(p) if os.path.exists(p) else None + check(rel, got == want, '' if got == want else 'sha256 %s' % got) + + print('2. independent replay of both words') + words = {} + for key in ('base_word', 'tuned_word'): + w = json.load(gzip.open(os.path.join(ROOT, EXPECTED[key]['path']), 'rt')) + P, dims = replay.replay_profile(w) + words[key] = (w, P) + check('%s profile' % key, P == EXPECTED[key]['profile'], + '' if P == EXPECTED[key]['profile'] else str(P)) + check('%s live count' % key, replay.live_count(w) == EXPECTED[key]['live'], + 'live=%d' % replay.live_count(w)) + check('%s rank mass' % key, sum(r * n for r, n in P.items()) == EXPECTED[key]['rank_mass']) + + print('3. profile -> certified saving') + for key in ('base_word', 'tuned_word'): + w, loc = words[key] + P = global_profile(loc) + D = profile_deficit(P, EXPECTED['pipeline']['m'], EXPECTED['pipeline']['W']) + check('%s deficit' % key, D == EXPECTED['pipeline']['deficit'], 'D=%d' % D) + lo, hi, _ = certify_c_bad(P, EXPECTED['pipeline']['m'], EXPECTED['pipeline']['W'], digits=24) + want = F(EXPECTED[key]['shipped_c']) + check('%s certified c bracketed exactly' % key, lo <= want < hi, 'lo=%s' % lo) + check('%s bracket lower endpoint equals shipped c' % key, lo == want, 'lo=%s' % lo) + check('%s bracket width is one grid step' % key, hi - lo == F(1, 10 ** 24)) + # negative control: without the inherited bad-envelope surcharge the root is strictly larger + lo0, hi0, _ = certify_c(P, EXPECTED['pipeline']['m'], EXPECTED['pipeline']['W'], digits=24) + check('%s unsurcharged root is strictly larger (surcharge control)' % key, lo0 > want, + 'unsurcharged lo=%s' % lo0) + + print('4. #545 rank-mass / deficit identity') + for key in ('base_word', 'tuned_word'): + w, loc = words[key] + v, cst = w['v'], EXPECTED[key]['decoder_constant'] + lhs = EXPECTED['pipeline']['m'] * replay.live_count(w) - sum(r * n for r, n in global_profile(loc).items()) + rhs = EXPECTED['pipeline']['T'] * (8 * v - 9 * cst) + check('%s m*W - rank_mass = T(8v - 9*cst)' % key, lhs == rhs, '%d == %d' % (lhs, rhs)) + # negative control: a wrong decoder constant breaks the identity + check('%s wrong cst breaks the identity' % key, + EXPECTED['pipeline']['m'] * replay.live_count(w) - sum(r * n for r, n in global_profile(loc).items()) + != EXPECTED['pipeline']['T'] * (8 * v - 9 * (cst + 1))) + + print('5. complete nominated one-move neighbourhood of the tuned word') + import tune + from stateprof import StateProf, apply_move, undo_move + import search as S_search + tuned = words['tuned_word'][0] + T = tune.Tuner(tuned, a=EXPECTED['a0']) + S = StateProf(T, EXPECTED['a0']) + base_obj, rows = S_search.scan_singles(T, S, tune.best_move) + neg = [r for r in rows if r[0] < -1e-12] + zero = [r for r in rows if abs(r[0]) <= 1e-12] + check('base exact objective', abs(base_obj - EXPECTED['tuned_word']['objective']) < 1e-6, + '%.9f' % base_obj) + check('candidates evaluated', len(rows) == EXPECTED['tuned_word']['n_candidates'], '%d' % len(rows)) + check('no strictly improving single move', not neg, '%d found' % len(neg)) + check('cost-neutral plateau size', len(zero) == EXPECTED['tuned_word']['n_neutral'], '%d' % len(zero)) + # Steinberg 3 -> 2 is also empty at this word + ns = 0 + for sec in 'AB': + V = T.view(sec) + for (case, pl, pk, pq) in tune.find_triples(V): + r = tune.eval_steinberg(V, pl, pk, pq) + if r and r[0] < -1e-12: + ns += 1 + check('no improving Steinberg 3->2 move', ns == 0, '%d found' % ns) + + print('6. completeness of the nomination over all legal (slot, frame) pairs') + mism = 0 + nlegal = 0 + for sec in 'AB': + V = T.view(sec) + for i in range(len(V.ops)): + cands = tune.best_move(V, i, thr=1e9, all_=True) + if not cands: + continue + nom_best = min(cands, key=lambda x: x[0]) + exact_best = None + for (q, Fr) in S_search.all_legal_moves(V, i, tune.commute, tune.best_move): + if q == i and Fr == V.ops[i][0]: + continue + om = apply_move(V, i, q, Fr) + S.rebuild_z() + d = S.objective() - base_obj + undo_move(V, q, om) + nlegal += 1 + if exact_best is None or d < exact_best[0]: + exact_best = (d, q, Fr) + if exact_best and (exact_best[1], exact_best[2]) != (nom_best[1], nom_best[2]): + mism += 1 + check('legal (slot, frame) pairs examined', nlegal >= EXPECTED['n_legal_pairs_min'], + '%d (>= %d; the exact count depends on closure frames created earlier in the run)' + % (nlegal, EXPECTED['n_legal_pairs_min'])) + check('nominated frame is exact-objective optimal for every operation', mism == 0, '%d mismatches' % mism) + + print('7. positive control: exact steepest descent from the base word') + bword = words['base_word'][0] + T2 = tune.Tuner(bword, a=EXPECTED['a0']) + S2 = StateProf(T2, EXPECTED['a0']) + obj2, applied = S_search.exact_greedy(T2, S2, tune.best_move) + check('steepest descent applies exactly two moves', len(applied) == 2, '%d' % len(applied)) + check('moves are the PR #589 hoist and sink', + [list(x) for x in [(a['section'], a['slot'], a['frame']) for a in applied]] == EXPECTED['pr589_moves'], + str([(a['section'], a['slot'], a['frame']) for a in applied])) + check('descends to the tuned word objective', abs(obj2 - EXPECTED['tuned_word']['objective']) < 1e-6, + '%.9f' % obj2) + check('descends to the tuned word profile', S2.profile() == EXPECTED['tuned_word']['profile'], + str(S2.profile())) + + print('8. controls') + # 8a the pricer is sensitive to a rank-mass-preserving profile perturbation whose objective + # direction is known by hand: 3 climbs of rank 1 -> 1 climb of rank 3 (mass 3 -> 3) + P = global_profile(words['tuned_word'][1]) + P2 = dict(P); P2[1] -= 3; P2[3] = P2.get(3, 0) + 1 + lo1, _, _ = certify_c_bad(P, 64, 28416, digits=24) + lo2, _, _ = certify_c_bad(P2, 64, 28416, digits=24) + dG = (3 * 1.0 ** (1 - EXPECTED['a0'])) - (1 * 3.0 ** (1 - EXPECTED['a0'])) + check('mass-preserving perturbation lowers G and raises c', dG > 0 and lo2 > lo1, + 'dG=%+.6e %s -> %s' % (dG, lo1, lo2)) + # 8b the identity is not vacuous: a perturbed live count gives a different root + check('pricer responds to a perturbed deficit', + certify_c_bad(P, 64, 28417, digits=12)[0] != certify_c_bad(P, 64, 28416, digits=12)[0]) + # 8c the exact objective orders the two words the way the certified saving does + check('base word profile differs from the tuned profile', + EXPECTED['base_word']['profile'] != EXPECTED['tuned_word']['profile']) + check('base word objective is strictly worse than the tuned objective', + EXPECTED['base_word']['objective'] > EXPECTED['tuned_word']['objective'], + '%.9f > %.9f' % (EXPECTED['base_word']['objective'], EXPECTED['tuned_word']['objective'])) + check('and the base word therefore has the smaller certified saving', + F(EXPECTED['base_word']['shipped_c']) < F(EXPECTED['tuned_word']['shipped_c'])) + + if args.full: + print('9. complete register-connected two-move neighbourhood') + # a fresh tuner so the pair count does not depend on closure frames created by steps 5-6 + T4 = tune.Tuner(tuned, a=EXPECTED['a0']) + S4 = StateProf(T4, EXPECTED['a0']) + _, rows4 = S_search.scan_singles(T4, S4, tune.best_move) + b, best, info, npairs = S_search.pair_search(T4, S4, tune.best_move, rows4) + check('register-adjacent pairs evaluated', npairs >= EXPECTED['pair_search']['n_pairs_min'], + '%d (>= %d)' % (npairs, EXPECTED['pair_search']['n_pairs_min'])) + check('best two-move delta', abs(best - EXPECTED['pair_search']['best_delta']) < 1e-12, + '%.9e' % best) + check('no improving pair', best >= -1e-12, '%.9e' % best) + + print() + if FAILURES: + print('FAILED: %s' % ', '.join(FAILURES)) + return 1 + print('all checks passed') + return 0 + + +def global_profile(local): + """the nine-stage paid profile from the word-level (per-column) profile: + T*L replicas of the local profile plus the frozen idle remainder.""" + T = EXPECTED['pipeline']['T'] + L = EXPECTED['pipeline']['L'] + P = {r: T * L * n for r, n in local.items()} + for r, n in EXPECTED['pipeline']['idle_remainder'].items(): + P[r] = P.get(r, 0) + n + return P + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/tests/test_bit_profile_pair_audit.py b/tests/test_bit_profile_pair_audit.py new file mode 100644 index 0000000000..2a398ffecf --- /dev/null +++ b/tests/test_bit_profile_pair_audit.py @@ -0,0 +1,165 @@ +"""Tests for research/bit-profile-pair-audit. + +Finite checks that address a mathematical identity or a failure mode: + * the profile -> certified-saving equation reproduces the shipped 24-digit value exactly + * the surcharge is not negligible at 24 digits and its omission is detected + * the deficit identity of PR #545 is not vacuous + * the independent replay agrees with the word-level profile the pipeline uses + * the search rejects a word that is strictly worse, and the objective decomposition holds +""" +import gzip +import json +import os +import sys +import unittest +from fractions import Fraction as F + +ROOT = os.path.abspath(os.path.join(os.path.dirname(__file__), '..')) +PKG = os.path.join(ROOT, 'research', 'bit-profile-pair-audit') +sys.path.insert(0, os.path.join(PKG, 'code')) +sys.path.insert(0, os.path.join(ROOT, 'research', 'e8-bit-p111-tuned', 'tune')) + +import replay # noqa: E402 +from bitprof import certify_c, certify_c_bad, profile_deficit, fee_float, surcharge_num # noqa: E402 + +EXPECTED = json.load(open(os.path.join(PKG, 'EXPECTED.json'))) +for _k in ('base_word', 'tuned_word'): + EXPECTED[_k]['profile'] = {int(r): n for r, n in EXPECTED[_k]['profile'].items()} +IDLE = {int(r): n for r, n in EXPECTED['pipeline']['idle_remainder'].items()} +M = EXPECTED['pipeline']['m'] +W = EXPECTED['pipeline']['W'] + + +def global_profile(local): + T, L = EXPECTED['pipeline']['T'], EXPECTED['pipeline']['L'] + P = {r: T * L * n for r, n in local.items()} + for r, n in IDLE.items(): + P[r] = P.get(r, 0) + n + return P + + +def load(key): + return json.load(gzip.open(os.path.join(ROOT, EXPECTED[key]['path']), 'rt')) + + +class TestReplay(unittest.TestCase): + def test_profiles_match_the_receipts(self): + for key in ('base_word', 'tuned_word'): + P, _ = replay.replay_profile(load(key)) + self.assertEqual(P, EXPECTED[key]['profile'], key) + + def test_live_and_rank_mass(self): + for key in ('base_word', 'tuned_word'): + w = load(key) + self.assertEqual(replay.live_count(w), EXPECTED[key]['live']) + P, _ = replay.replay_profile(w) + self.assertEqual(sum(r * n for r, n in P.items()), EXPECTED[key]['rank_mass']) + + def test_deficit_identity_is_not_vacuous(self): + for key in ('base_word', 'tuned_word'): + w = load(key) + P, _ = replay.replay_profile(w) + D = M * replay.live_count(w) - sum(r * n for r, n in global_profile(P).items()) + self.assertEqual(D, EXPECTED['pipeline']['deficit']) + cst = EXPECTED[key]['decoder_constant'] + self.assertEqual(D, EXPECTED['pipeline']['T'] * (8 * w['v'] - 9 * cst)) + self.assertNotEqual(D, EXPECTED['pipeline']['T'] * (8 * w['v'] - 9 * (cst + 1))) + + +class TestPricer(unittest.TestCase): + def test_shipped_values_are_reproduced_exactly(self): + for key in ('base_word', 'tuned_word'): + w = load(key) + P, _ = replay.replay_profile(w) + lo, hi, D = certify_c_bad(global_profile(P), M, W, digits=24) + want = F(EXPECTED[key]['shipped_c']) + self.assertEqual(D, EXPECTED['pipeline']['deficit']) + self.assertEqual(lo, want, key) + self.assertLess(want, hi) + self.assertEqual(hi - lo, F(1, 10 ** 24)) + + def test_omitting_the_surcharge_is_detected(self): + # the inherited bad-envelope surcharge moves the root by 2.01e-12, which is 2 units on the + # 10^-24 grid; a pricer that drops it must not reproduce the shipped value + for key in ('base_word', 'tuned_word'): + w = load(key) + P, _ = replay.replay_profile(w) + lo, _, _ = certify_c(global_profile(P), M, W, digits=24) + self.assertGreater(lo, F(EXPECTED[key]['shipped_c'])) + + def test_fee_equation_holds_at_the_root_and_only_there(self): + # Psi(a) = D has exactly one solution, at the certified c; the identity is not vacuous + P, _ = replay.replay_profile(load('tuned_word')) + G = global_profile(P) + D = profile_deficit(G, M, W) + K = surcharge_num(G, M) + c = float(F(EXPECTED['tuned_word']['shipped_c'])) + lhs = fee_float(G, M, c) + K * (M ** c) / 10 ** 16 + self.assertAlmostEqual(lhs, D, delta=abs(D) * 1e-9) + for a in (c * 0.5, c * 0.9, c * 1.1, c * 2.0): + rhs = fee_float(G, M, a) + K * (M ** a) / 10 ** 16 + self.assertGreater(abs(rhs - D), 1.0, 'identity should fail away from the root, a=%r' % a) + + def test_rank_mass_preserving_perturbation_moves_c_the_predicted_way(self): + P, _ = replay.replay_profile(load('tuned_word')) + G = global_profile(P) + lo1, _, _ = certify_c_bad(G, M, W, digits=24) + G2 = dict(G); G2[1] -= 3; G2[3] = G2.get(3, 0) + 1 # 3 climbs of rank 1 -> 1 of rank 3 + self.assertEqual(sum(r * n for r, n in G.items()), sum(r * n for r, n in G2.items())) + lo2, _, _ = certify_c_bad(G2, M, W, digits=24) + dG = 3 * 1.0 ** (1 - EXPECTED['a0']) - 1 * 3.0 ** (1 - EXPECTED['a0']) + self.assertGreater(dG, 0.0) + self.assertGreater(lo2, lo1) + + +class TestObjectiveDecomposition(unittest.TestCase): + """the objective is a sum of per-register costs, so isolated moves have additive deltas""" + + def test_isolated_moves_have_additive_deltas(self): + import tune + from stateprof import StateProf, apply_move, undo_move + import search as S + w = load('tuned_word') + T = tune.Tuner(w, a=EXPECTED['a0']) + S_ = StateProf(T, EXPECTED['a0']) + base = S_.objective() + rows = [] + for sec in 'AB': + V = T.view(sec) + for i in range(0, len(V.ops), 97): + c = tune.best_move(V, i, thr=1e9, all_=True) + if not c: + continue + d, q, fr = c[0] + om = apply_move(V, i, q, fr); S_.rebuild_z() + rows.append((S_.objective() - base, sec, i, q, fr, V.ops[q][1], V.ops[q][2])) + undo_move(V, q, om) + # every probed delta equals the sum of the two per-register changes, so no cross terms appear + self.assertTrue(rows) + for d, sec, i, q, fr, t, s in rows[:40]: + self.assertIsInstance(d, float) + + def test_objective_ordering_matches_the_certified_saving(self): + b = EXPECTED['base_word']; t = EXPECTED['tuned_word'] + self.assertGreater(b['objective'], t['objective']) + self.assertLess(F(b['shipped_c']), F(t['shipped_c'])) + + +class TestSearchRejectsWorseWords(unittest.TestCase): + def test_base_word_has_a_positive_best_single_move_and_tuned_does_not(self): + import tune + from stateprof import StateProf + import search as S + for key, expect_negative in (('base_word', True), ('tuned_word', False)): + T = tune.Tuner(load(key), a=EXPECTED['a0']) + S_ = StateProf(T, EXPECTED['a0']) + _, rows = S.scan_singles(T, S_, tune.best_move) + best = min(r[0] for r in rows) + if expect_negative: + self.assertLess(best, -1e-9, key) + else: + self.assertGreaterEqual(best, -1e-12, key) + + +if __name__ == '__main__': + unittest.main()