diff --git a/research/bit-early-retirement-cut/CERTIFICATE.json b/research/bit-early-retirement-cut/CERTIFICATE.json new file mode 100644 index 0000000000..b7a8d17755 --- /dev/null +++ b/research/bit-early-retirement-cut/CERTIFICATE.json @@ -0,0 +1,1302 @@ +{ + "assignment_seed": 8, + "baseline_ADDs": { + "A": 2130, + "B": 934, + "C": 2629, + "D": 18085, + "scatter": 527 + }, + "baseline_target_access_violations": 0, + "baseline_total_ADDs": 24305, + "construction": { + "baseline": { + "ADDs": 24305, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "COPYs": 9, + "ERASEs": 9, + "MOVEs": 2911, + "children": 2920, + "positive_majorant_bits": 16, + "positive_majorant_peak": "49347", + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "records": 27234 + }, + "candidate": { + "ADDs": 24307, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "COPYs": 9, + "ERASEs": 9, + "MOVEs": 2912, + "children": 2921, + "positive_majorant_bits": 16, + "positive_majorant_peak": "49347", + "profile": { + "1": 1324, + "2": 1342, + "3": 79, + "4": 44, + "5": 103, + "6": 11, + "7": 18 + }, + "rank_mass": 5128, + "records": 27237 + }, + "cleanup_omit_gate": 2343, + "cleanup_replace_source": { + "gate": 580, + "new_source": 77, + "old_source": 470 + }, + "final_helper_frame": 513, + "helper470_paths": { + "baseline": [ + 0, + 79, + 1 + ], + "candidate": [ + 0, + 79, + 186, + 513 + ] + }, + "local_profile_delta": { + "1": 1, + "5": 1, + "7": -1 + }, + "optimistic_hosting": { + "cases": [ + { + "old_remainder": 2, + "profile_delta": { + "1": 1, + "10": 1, + "2": -1, + "5": 1, + "7": -2 + }, + "weighted_delta_interval": [ + "-2568382991222829559063/604462909807314587353088", + "-5136765982445659118125/1208925819614629174706176" + ] + }, + { + "old_remainder": 4, + "profile_delta": { + "1": 1, + "12": 1, + "4": -1, + "5": 1, + "7": -2 + }, + "weighted_delta_interval": [ + "-10670579842591789867125/1208925819614629174706176", + "-2667644960647947466781/302231454903657293676544" + ] + }, + { + "old_remainder": 6, + "profile_delta": { + "1": 1, + "14": 1, + "5": 1, + "6": -1, + "7": -2 + }, + "weighted_delta_interval": [ + "-14706987581348896605997/1208925819614629174706176", + "-3676746895337224151499/302231454903657293676544" + ] + } + ], + "exponent": "1733427039589844234749/1000000000000000000000000", + "scope": "Optimistic two-slot relocation only; new owner/window and H4 admission are unresolved.", + "weight": "g(r)=r*(64/r)^a" + }, + "other_register_paths_unchanged": 660, + "retirement_gates": [ + [ + 186, + 470, + [ + 77 + ] + ], + [ + 513, + 444, + [ + 470 + ] + ], + [ + 513, + 475, + [ + 470 + ] + ] + ] + }, + "coverage": { + "helpers": 6, + "lost_target_contracts": 59, + "star_ADD_occurrences": 22, + "target_contracts": 666 + }, + "dimensions": { + "registers": 661, + "targets": 111 + }, + "no_new_kappa": true, + "retirements": [ + { + "dirty_column": [ + 163, + 381, + 465, + 474 + ], + "forced_participants": [ + 0, + 163, + 381, + 465, + 474 + ], + "helper": 465, + "illegal_target_promotions": [ + 163 + ], + "least_frame_restoration": { + "donors": [ + 0, + 465 + ], + "frame": 507, + "lost_targets": [ + { + "boundary_coordinates": [ + 0 + ], + "target": 122 + } + ], + "rank": 4 + }, + "lost_dependency_rank": 2, + "lost_targets": [ + { + "boundary_coordinates": [ + 0 + ], + "target": 116 + }, + { + "boundary_coordinates": [ + 0 + ], + "target": 120 + }, + { + "boundary_coordinates": [ + 0 + ], + "target": 122 + }, + { + "boundary_coordinates": [ + 0 + ], + "target": 157 + }, + { + "boundary_coordinates": [ + 0 + ], + "target": 158 + }, + { + "boundary_coordinates": [ + 0 + ], + "target": 159 + }, + { + "boundary_coordinates": [ + 163, + 465 + ], + "target": 163 + }, + { + "boundary_coordinates": [ + 0 + ], + "target": 165 + }, + { + "boundary_coordinates": [ + 0 + ], + "target": 167 + }, + { + "boundary_coordinates": [ + 0 + ], + "target": 169 + } + ], + "promotion_rank_sum": 16, + "promotions": [ + { + "from_frame": 2, + "rank_increment": 6, + "register": 0 + }, + { + "from_frame": 0, + "rank_increment": 7, + "register": 163 + }, + { + "from_frame": 507, + "rank_increment": 3, + "register": 465 + } + ], + "restore_row": [ + 0, + 465 + ], + "star_ADDs": 4, + "star_gates": [ + [ + 465, + 0 + ], + [ + 163, + 465 + ], + [ + 381, + 465 + ], + [ + 474, + 465 + ] + ], + "star_isolates_all_661_columns": true, + "terminal_frame": 512, + "witness": { + "boundary_coordinate": 0, + "original_input_delta": [ + 0, + 111, + 116, + 120, + 122, + 157, + 158, + 159, + 165, + 167, + 169, + 222, + 223, + 252, + 465 + ], + "separation": { + "dot": 1, + "line": 30, + "normal": [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0 + ] + }, + "target": 116 + } + }, + { + "dirty_column": [ + 198, + 385, + 466, + 476 + ], + "forced_participants": [ + 19, + 198, + 385, + 466, + 476 + ], + "helper": 466, + "illegal_target_promotions": [ + 198 + ], + "least_frame_restoration": { + "donors": [ + 19, + 466 + ], + "frame": 508, + "lost_targets": [ + { + "boundary_coordinates": [ + 19 + ], + "target": 208 + } + ], + "rank": 4 + }, + "lost_dependency_rank": 2, + "lost_targets": [ + { + "boundary_coordinates": [ + 19 + ], + "target": 133 + }, + { + "boundary_coordinates": [ + 19 + ], + "target": 144 + }, + { + "boundary_coordinates": [ + 19 + ], + "target": 149 + }, + { + "boundary_coordinates": [ + 19 + ], + "target": 161 + }, + { + "boundary_coordinates": [ + 19 + ], + "target": 171 + }, + { + "boundary_coordinates": [ + 19 + ], + "target": 178 + }, + { + "boundary_coordinates": [ + 19 + ], + "target": 188 + }, + { + "boundary_coordinates": [ + 198, + 466 + ], + "target": 198 + }, + { + "boundary_coordinates": [ + 19 + ], + "target": 203 + }, + { + "boundary_coordinates": [ + 19 + ], + "target": 208 + } + ], + "promotion_rank_sum": 15, + "promotions": [ + { + "from_frame": 152, + "rank_increment": 5, + "register": 19 + }, + { + "from_frame": 0, + "rank_increment": 7, + "register": 198 + }, + { + "from_frame": 508, + "rank_increment": 3, + "register": 466 + } + ], + "restore_row": [ + 19, + 466 + ], + "star_ADDs": 4, + "star_gates": [ + [ + 466, + 19 + ], + [ + 198, + 466 + ], + [ + 385, + 466 + ], + [ + 476, + 466 + ] + ], + "star_isolates_all_661_columns": true, + "terminal_frame": 514, + "witness": { + "boundary_coordinate": 19, + "original_input_delta": [ + 19, + 130, + 133, + 144, + 149, + 161, + 171, + 178, + 188, + 203, + 208, + 264, + 265, + 280, + 466 + ], + "separation": { + "dot": 2, + "line": 0, + "normal": [ + 1, + 1, + 0, + 0, + 0, + 0, + 1, + 1 + ] + }, + "target": 133 + } + }, + { + "dirty_column": [ + 208, + 444, + 468, + 475 + ], + "forced_participants": [ + 38, + 208, + 444, + 468, + 475 + ], + "helper": 468, + "illegal_target_promotions": [ + 208 + ], + "least_frame_restoration": { + "donors": [ + 38, + 468 + ], + "frame": 509, + "lost_targets": [ + { + "boundary_coordinates": [ + 38 + ], + "target": 144 + } + ], + "rank": 4 + }, + "lost_dependency_rank": 2, + "lost_targets": [ + { + "boundary_coordinates": [ + 38 + ], + "target": 130 + }, + { + "boundary_coordinates": [ + 38 + ], + "target": 138 + }, + { + "boundary_coordinates": [ + 38 + ], + "target": 144 + }, + { + "boundary_coordinates": [ + 38 + ], + "target": 146 + }, + { + "boundary_coordinates": [ + 38 + ], + "target": 168 + }, + { + "boundary_coordinates": [ + 38 + ], + "target": 176 + }, + { + "boundary_coordinates": [ + 38 + ], + "target": 177 + }, + { + "boundary_coordinates": [ + 38 + ], + "target": 185 + }, + { + "boundary_coordinates": [ + 38 + ], + "target": 200 + }, + { + "boundary_coordinates": [ + 208, + 468 + ], + "target": 208 + } + ], + "promotion_rank_sum": 15, + "promotions": [ + { + "from_frame": 188, + "rank_increment": 5, + "register": 38 + }, + { + "from_frame": 0, + "rank_increment": 7, + "register": 208 + }, + { + "from_frame": 509, + "rank_increment": 3, + "register": 468 + } + ], + "restore_row": [ + 38, + 468 + ], + "star_ADDs": 4, + "star_gates": [ + [ + 468, + 38 + ], + [ + 208, + 468 + ], + [ + 444, + 468 + ], + [ + 475, + 468 + ] + ], + "star_isolates_all_661_columns": true, + "terminal_frame": 513, + "witness": { + "boundary_coordinate": 38, + "original_input_delta": [ + 38, + 130, + 138, + 144, + 146, + 149, + 168, + 176, + 177, + 185, + 200, + 302, + 303, + 390, + 468 + ], + "separation": { + "dot": -2, + "line": 0, + "normal": [ + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0 + ] + }, + "target": 130 + } + }, + { + "dirty_column": [ + 413, + 469, + 479 + ], + "forced_participants": [ + 50, + 413, + 469, + 479 + ], + "helper": 469, + "illegal_target_promotions": [], + "least_frame_restoration": { + "donors": [ + 50, + 469 + ], + "frame": 517, + "lost_targets": [ + { + "boundary_coordinates": [ + 50 + ], + "target": 130 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 138 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 146 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 154 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 168 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 177 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 178 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 185 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 200 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 208 + } + ], + "rank": 7 + }, + "lost_dependency_rank": 1, + "lost_targets": [ + { + "boundary_coordinates": [ + 50 + ], + "target": 130 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 138 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 146 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 154 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 168 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 177 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 178 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 185 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 200 + }, + { + "boundary_coordinates": [ + 50 + ], + "target": 208 + } + ], + "promotion_rank_sum": 6, + "promotions": [ + { + "from_frame": 52, + "rank_increment": 6, + "register": 50 + } + ], + "restore_row": [ + 50, + 469 + ], + "star_ADDs": 3, + "star_gates": [ + [ + 469, + 50 + ], + [ + 413, + 469 + ], + [ + 479, + 469 + ] + ], + "star_isolates_all_661_columns": true, + "terminal_frame": 517, + "witness": { + "boundary_coordinate": 50, + "original_input_delta": [ + 50, + 130, + 138, + 146, + 154, + 161, + 168, + 177, + 178, + 185, + 200, + 208, + 330, + 331, + 334, + 469 + ], + "separation": { + "dot": -2, + "line": 0, + "normal": [ + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0 + ] + }, + "target": 130 + } + }, + { + "dirty_column": [ + 444, + 470, + 475 + ], + "forced_participants": [ + 77, + 444, + 470, + 475 + ], + "helper": 470, + "illegal_target_promotions": [], + "least_frame_restoration": { + "donors": [ + 77, + 470 + ], + "frame": 186, + "lost_targets": [], + "rank": 2 + }, + "lost_dependency_rank": 1, + "lost_targets": [ + { + "boundary_coordinates": [ + 77 + ], + "target": 130 + }, + { + "boundary_coordinates": [ + 77 + ], + "target": 138 + }, + { + "boundary_coordinates": [ + 77 + ], + "target": 149 + }, + { + "boundary_coordinates": [ + 77 + ], + "target": 154 + }, + { + "boundary_coordinates": [ + 77 + ], + "target": 168 + }, + { + "boundary_coordinates": [ + 77 + ], + "target": 176 + }, + { + "boundary_coordinates": [ + 77 + ], + "target": 177 + }, + { + "boundary_coordinates": [ + 77 + ], + "target": 185 + }, + { + "boundary_coordinates": [ + 77 + ], + "target": 200 + }, + { + "boundary_coordinates": [ + 77 + ], + "target": 208 + } + ], + "promotion_rank_sum": 11, + "promotions": [ + { + "from_frame": 186, + "rank_increment": 5, + "register": 77 + }, + { + "from_frame": 79, + "rank_increment": 6, + "register": 470 + } + ], + "restore_row": [ + 77, + 470 + ], + "star_ADDs": 3, + "star_gates": [ + [ + 470, + 77 + ], + [ + 444, + 470 + ], + [ + 475, + 470 + ] + ], + "star_isolates_all_661_columns": true, + "terminal_frame": 513, + "witness": { + "boundary_coordinate": 77, + "original_input_delta": [ + 77, + 130, + 138, + 149, + 154, + 168, + 176, + 177, + 185, + 188, + 200, + 208, + 292, + 390, + 391, + 470 + ], + "separation": { + "dot": -2, + "line": 0, + "normal": [ + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0 + ] + }, + "target": 130 + } + }, + { + "dirty_column": [ + 476 + ], + "forced_participants": [ + 67, + 328, + 331, + 385, + 476 + ], + "helper": 476, + "illegal_target_promotions": [], + "least_frame_restoration": { + "donors": [ + 67, + 328, + 331, + 385, + 476 + ], + "frame": 514, + "lost_targets": [ + { + "boundary_coordinates": [ + 67 + ], + "target": 130 + }, + { + "boundary_coordinates": [ + 67 + ], + "target": 138 + }, + { + "boundary_coordinates": [ + 67 + ], + "target": 146 + }, + { + "boundary_coordinates": [ + 67 + ], + "target": 154 + }, + { + "boundary_coordinates": [ + 67 + ], + "target": 168 + }, + { + "boundary_coordinates": [ + 331 + ], + "target": 171 + }, + { + "boundary_coordinates": [ + 67 + ], + "target": 177 + }, + { + "boundary_coordinates": [ + 67 + ], + "target": 200 + }, + { + "boundary_coordinates": [ + 67 + ], + "target": 208 + } + ], + "rank": 7 + }, + "lost_dependency_rank": 2, + "lost_targets": [ + { + "boundary_coordinates": [ + 67 + ], + "target": 130 + }, + { + "boundary_coordinates": [ + 67 + ], + "target": 138 + }, + { + "boundary_coordinates": [ + 67 + ], + "target": 146 + }, + { + "boundary_coordinates": [ + 67 + ], + "target": 154 + }, + { + "boundary_coordinates": [ + 67 + ], + "target": 168 + }, + { + "boundary_coordinates": [ + 331 + ], + "target": 171 + }, + { + "boundary_coordinates": [ + 67 + ], + "target": 177 + }, + { + "boundary_coordinates": [ + 67 + ], + "target": 200 + }, + { + "boundary_coordinates": [ + 67 + ], + "target": 208 + } + ], + "promotion_rank_sum": 6, + "promotions": [ + { + "from_frame": 192, + "rank_increment": 5, + "register": 67 + }, + { + "from_frame": 431, + "rank_increment": 1, + "register": 331 + } + ], + "restore_row": [ + 67, + 328, + 331, + 385, + 476 + ], + "star_ADDs": 4, + "star_gates": [ + [ + 476, + 67 + ], + [ + 476, + 328 + ], + [ + 476, + 331 + ], + [ + 476, + 385 + ] + ], + "star_isolates_all_661_columns": true, + "terminal_frame": 514, + "witness": { + "boundary_coordinate": 67, + "original_input_delta": [ + 67, + 130, + 138, + 146, + 154, + 168, + 177, + 178, + 200, + 208, + 331, + 370, + 371, + 476 + ], + "separation": { + "dot": -2, + "line": 0, + "normal": [ + -1, + 0, + 1, + 0, + -1, + 0, + 1, + 0 + ] + }, + "target": 130 + } + } + ], + "status": "SCOPED_COMMON_FRAME_EARLY_RETIREMENT_OBSTRUCTION" +} diff --git a/research/bit-early-retirement-cut/CLAIM.md b/research/bit-early-retirement-cut/CLAIM.md new file mode 100644 index 0000000000..e16fe5ac29 --- /dev/null +++ b/research/bit-early-retirement-cut/CLAIM.md @@ -0,0 +1,21 @@ +# Bit early-retirement investigation + +- Track: bit supplier; OS-random assignment seed **8**, drawn 2026-10-13 20:44:34 UTC. +- Base: `49b3157d1d89adcef16df8be98445451672be5ba`. +- Selected record: PR1094, kappa `836330098538459/500000000000000000`; bit supplier PR589/555; complex binds. +- Three candidates: semantic helper-star H2/K repair (overlap PR1194); local R439 gate synthesis (overlap PR1188/1208/1221); early retirement of PR1128's six necessary-condition survivors (chosen). +- Scope: fixed PR589 D/A/scatter prefix; helpers 465,466,468,469,470,476; retire one helper at its rank-seven common frame using exact dirty restoration and erasure. Test whether promotion destroys required target access. Seed 8 rotates the six-helper order to begin at 468; it is not a novelty claim. +- Predecessor: Ali Romman's PR1128 at `df29b159239b79d7e451d6ddda826a73e0e50a67`; leaves these six early-cut candidates open. The present test changes the after-B fixed-prefix restriction by retiring before B, but bounds its explicit common-frame mechanism. +- Method: exact F2 boundary inversion, rational frame containment, constructive restore/clear stars, and target dependency cuts. Check optimistic complete expense before attempting any full supplier. +- Expected deliverable: one exact finite construction or a scoped obstruction with machine-checkable witnesses, negative controls, source pins and remaining obligations. No new kappa without complete admission. +- Budget: at most 60 minutes; orientation at most 12 minutes; final 15 minutes reserved for verification and handoff. Expected finish by 2026-10-13 21:44 UTC; earlier if the decisive test closes the mechanism. +- Overlap: full 838-open-PR/body and 12-discussion snapshot plus 322 local records; PR1128 is the only precise boundary lead. No pinned sprint issue. Local claim follows the donor's no-pinned-issue fallback; no separate reservation issue. +- Attribution: Ross Richardson, with substantial OpenAI Codex assistance; Apache-2.0. Predecessor PR589/555 and PR1128 authors retained. + +## Result and handoff + +Completed the six-helper domain: all six fail a single rank-seven retirement block; five also fail their least possible first restoration frame. Helper470 admits a lower-frame restore/clear schedule with the original D/A/scatter/B unchanged, all661 symbolic columns correct, and local rank mass5129 ->5128 for two additional ADDs. This is finite construction/interface evidence, not a new supplier bound or kappa. PR1043's earlier source-deletion result is explicitly credited and is not improved upon. + +Exact implementation and evidence: [source-pinned artifact](https://github.com/RossRichardson/integer-mult-bounds/blob/2a6d342645ba919392c121f94f3345430afe0240/research/bit-early-retirement-cut/README.md). The Python3.12 registered replay, Python3.9.6 standalone replay, both independently represented checkers and all eleven test groups pass. The CPython3.14.6 receipt regenerates byte-identically. Native hosting, changed H4 admission, packed precision/tape and an outer bound remain unresolved. + +Submission refresh: main `dadfea6e8a78ff6ba901705f87532a71c6f5bbb8`, same selected certificate and identical input blob; 845 open PRs and17 discussions checked with complete pagination. Nearest work PR1043/1079/1128/1179 is distinguished in the README. No pinned coordination issue existed. This is the one local claim update, with the immutable artifact link; the focused PR is the publication handoff. No upstream or selected-frontier changes, merge, or closure is authorized or performed. diff --git a/research/bit-early-retirement-cut/README.md b/research/bit-early-retirement-cut/README.md new file mode 100644 index 0000000000..4f3716685c --- /dev/null +++ b/research/bit-early-retirement-cut/README.md @@ -0,0 +1,255 @@ +# Early retirement in the fixed PR589 bit prefix + +**Finite construction and scoped negative result; no new kappa.** After the +unchanged PR589 `D/A/scatter` prefix, five of PR1128's six width-seven candidates +cannot even be restored by a first single-frame block without losing a required +target input. Helper **470** is the exception: restore it at rank two, clear its +dirt at rank seven, and change two cleanup instructions. The complete finite +word preserves all 661 input columns and reduces that helper's terminal width +from eight to seven. + +This fills a concrete early-cut opening in Ali Romman's +[PR1128](https://github.com/CrocSwap/integer-mult-bounds/pull/1128), pinned at +`df29b159239b79d7e451d6ddda826a73e0e50a67`. It does **not** improve on his +[PR1043](https://github.com/CrocSwap/integer-mult-bounds/pull/1043), pinned at +`e309e17f83f5759b1ea1fa24a76f24838784cb4d`, which already deletes helper470 by +changing the earlier source boundary and supplies a complete hosted invoice. +Here `D`, `A`, retained copies, scatter, and the original `B` are byte-for-byte +unchanged; a three-gate block is inserted between scatter and B. No savings +from the two constructions are combined. + +The base is `49b3157d1d89adcef16df8be98445451672be5ba`. Its selected conditional +kappa is `836330098538459/500000000000000000` (PR1094), with the complex side +binding. The selected record and `upstream/` are unchanged. Assignment seed 8 +selected the bit-supplier track and rotated the six-case inspection order to +start at helper468. This is a complete six-case calculation, not a randomized +optimization or a universal bit-supplier obstruction. + +## Exact finite construction + +Use the original register/frame identifiers in the pinned PR589 word. Insert: + +| Frame | Operation | Purpose | +|---:|---|---| +| 186 (rank 2) | `470 ^= 77` | Restore helper470 to its original dirty input | +| 513 (rank 7) | `444 ^= 470` | Remove that dirty input from register444 | +| 513 (rank 7) | `475 ^= 470` | Remove it from the retained-total register475 | + +The earlier scatter already consumed the unchanged snapshots; it is not rerun. +After these three gates, helper470 holds its initial input and no other register +contains its dirty column. The original B does not touch register470. +In C, replace zero-based gate 580, `444 ^= 470`, by `444 ^= 77` at the same +full frame. Omit zero-based gate 2343, `470 ^= 77`. End helper470 at frame513; +all other final frames remain unchanged. These indices are checked against the +pinned operands, not accepted as unverified positions. + +The complete patch is recorded in [CERTIFICATE.json](CERTIFICATE.json). +`patched_sections` in [verify.py](verify.py) reconstructs its literal stream +without copying or editing the frozen source word. Both checkers replay the +whole stream and its literal scalar inverse, including every dirty column. +Forward frame legality is checked over Q. The inverse replay is scalar only; +it does not claim that reversed frame climbs are a legal physical program. + +| Complete local quantity | PR589 | Early retirement | +|---|---:|---:| +| ADDs, including 527 scatter ADDs | 24,305 | 24,307 | +| MOVEs | 2,911 | 2,912 | +| COPY / ERASE | 9 / 9 | 9 / 9 | +| COPY ranks | nine rank-seven copies | unchanged | +| Records | 27,234 | 27,237 | +| Paid children, including COPY charges | 2,920 | 2,921 | +| Paid rank mass | 5,129 | 5,128 | +| Helper470 frame dimensions | `0 -> 1 -> 8` | `0 -> 1 -> 2 -> 7` | +| Other 660 frame itineraries | baseline | identical | + +The exact local histogram changes by `+H1 + H5 - H7`. Both words have scalar +positive-majorant row-sum peak 49,347 (16 bits), calculated by replacing every +XOR by addition on initial unit row sums. This is a finite scalar coefficient +bound, **not** the packed/native precision invoice or the nine-stage prefix +bound. All nine existing COPY/ERASE charges are retained; this package does not +recompile their native implementations. + +## Why the other eager restorations fail + +The cut is the finite 661-register scalar contract of PR1128: `w = M u` just +after D/A/scatter, with its original current frames. Retained scatter-copy +channels are unavailable for new suffix reads. M is invertible over F2. +Allowed suffix operations are invertible scalar operations at a common rational +frame and monotone frame enlargements, with no new COPY, descent, reset or other +high-to-low transport. Extra workspace starts with independent dirty inputs. + +For a helper h, let `a_h = e_h^T M^-1` be its restoration row and `d_h` the +support of its dirty column in M. A **first single-frame restoration block** +performs all scalar work at one frame F, with no earlier lower-frame preparation. +It returns h to its original input. Every boundary coordinate in `support(a_h)` +must participate: otherwise the block cannot distinguish two independent +boundary states differing only in that coordinate. Participating registers +must reach F. This argument allows arbitrary block length, register mixing, +target feedback and any number of independent dirty auxiliaries at F. + +If the block also isolates h's dirty input from every other register, every +member of `d_h` must participate too. Hence its forced footprint contains +`P_h = support(a_h) union d_h union {h}`. A rational-span computation gives a +unique rank-seven join U for these six footprints, reproducing the specific +necessary-condition survivors named in PR1128. We do not rerun that PR's +separate exclusion of the other 433 helpers. + +For target t the desired final value is `y_t + x_(t-111)`, whose row in boundary +coordinates is `b_t = (e_t + e_(t-111))^T M^-1`. Suppose F is not contained in +that target's final frame V_t. No dependency path from a register at F can ever +reach t, even through later scalar mixing: every subsequent frame contains F. +If `b_t` has a nonzero coefficient on a boundary coordinate forced into the +block, then two inputs differing only in that coordinate have identical +remaining accessible information but different required target values. No +allowed completion exists. Moving additional registers to F cannot repair it. + +This is an information-access obstruction, even if the block, all remaining +scalar work, and every permitted frame change are optimistically priced at +zero. An improved invoice cannot fix this failed identity. It does not exclude +lower-frame preprocessing, additional transported information, delayed +restoration after target reads, different copies, or a changed prefix. + +| Helper | Full-isolation U | Lost target obligations at U | First restoration frame J | Rank J | Lost targets already at J | +|---:|---:|---:|---:|---:|---:| +| 465 | 512 | 10 | 507 | 4 | 1 (target122) | +| 466 | 514 | 10 | 508 | 4 | 1 (target208) | +| 468 | 513 | 10 | 509 | 4 | 1 (target144) | +| 469 | 517 | 10 | 517 | 7 | 10 | +| 470 | 513 | 10 | 186 | 2 | 0 | +| 476 | 514 | 9 | 514 | 7 | 9 | + +J is the rational span of the restoration donors' current frames. Thus the +five exclusions at J also exclude every larger first restoration frame, +including unlisted rational frames. Helper470 instead uses J before U; its +source77 stays available at frame186. This is the evidence-driven refinement +of the initially tested one-common-frame mechanism, not a rerun with another +random seed. + +The certificate contains all 666 target checks, the 59 nonzero U-cut rows, +exact rational separating normals, and six pairs of original inputs witnessing +failure. The ranks of the six restricted missing-dependency matrices are +`2,2,2,1,1,2`. These are scalar dependency ranks, not recursive COPY prices. +The common-frame restore/clear stars have 4,4,4,3,3,4 ADDs respectively and do +isolate their dirty inputs; their failure is geometric, not a scalar mismatch. +For helpers465/466/468 they would additionally force targets163/198/208 into +frames that cannot reach those targets' required final frames. + +## Favorable complete slot relaxation, and its limit + +A local rank reduction alone is not a supplier improvement. As a planning test, +move the width-seven residual from its old width-eight allocation into one +formerly idle rank-seven slot. In the old host, return the full eight freed +coordinates to an existing idle remainder r. For the incumbent occupied-slot +remainders `r in {2,4,6}`, all local children, freed idle rank and consumed idle +rank give the **two-slot relaxation** + +`Delta H = e1 + e5 - 2 e7 + e_(r+8) - e_r`. + +One `-e7` is the changed local path and the other is the consumed idle slot. +Both child count and rank mass are unchanged. The inherited child-count +surcharge would therefore be unchanged under this exact relaxation. At the +pinned bit exponent `a = 1733427039589844234749/10^24`, an exact rational +atanh/Taylor enclosure certifies a strictly negative change in +`sum H_r * r * (64/r)^a` for all three cases (approximately -0.0042490, +-0.0088265 and -0.0121653 per local conversion). The complete rational intervals +and profile deltas are in the certificate. No root search or new exponent is +claimed. This accounts for every child in the stated slot model; it does not +establish that these slots can be occupied in the real chronology. + +**Unresolved:** an actual owner/window assignment for this endpoint, native +five/nine/eleven-stage compilation, packed precision and tape invoices, and a +replacement/adaptation of H4 (which currently requires literal full-frame +cleanup of every helper). The source still has the original H1/H2/H3/H5 scalar +shape; the changed endpoint is outside the selected H4 contract. The two-slot +calculation assumes successful admission and unchanged allowances and supplies +no proof of either. The complex supplier also remains limiting. None of this +selects a new frontier, a physical supplier, a practical speedup or a complete +multiplication theorem. + +## Reproduce and verification coverage + +Python standard library only. From the repository root: + +```sh +python3 -I -O -B research/bit-early-retirement-cut/verify.py +python3 -I -O -B research/bit-early-retirement-cut/independent.py +python3 -I -O -B research/bit-early-retirement-cut/test_package.py +``` + +The first command ends with: + +```text +PASS_BIT_EARLY_RETIREMENT_CUT helpers=6 lost=59 least_frame_survivor=470 width=8->7 ADDs=24305->24307 mass=5129->5128 no_new_kappa +``` + +`verify.py` uses packed binary rows and Fraction geometry; `independent.py` +uses set-valued rows, separate Gaussian inversion, and fraction-free integer +geometry. They share the authenticated source and declarative receipt, and +neither imports the other or predecessor executable code. The second checker +independently verifies the cut classification, input pairs, full construction, +frame paths and local invoice; the analytic slot intervals are certified by +the first checker. Separate implementations written with the same AI assistance +do not constitute independent human review. + +Eleven test groups include all 22 star-gate omissions, three retirement-gate +omissions, both cleanup mistakes, premature source promotion, invalid final +frame, altered input/geometry witnesses, 60 small invertible-matrix fixtures, +the returned-idle accounting check, four receipt corruptions rejected by both +checkers, source corruption, and read-only offline relocation. Decimal values +are only a diagnostic cross-check of the rational intervals. Full-frame target +and smaller-first-frame controls explicitly guard against overstating the +negative result. + +`--emit NEW_PATH` regenerates the complete canonical receipt and refuses to +overwrite a file. The registered hook in [VERIFY.json](VERIFY.json) runs the +three commands on Python3.12. Standalone replay also works from a source-only +export containing this package and its one declared input. Metadata provenance +checking additionally needs the pinned Git history. + +No full `make verify`, selected cold replay, native supplier replay or Lean +compilation is claimed. This package changes no generator or selected input; +its focused checks cover the new evidence. Hosted CI status is separate from +local validation. The registered Python3.12 replay and all eleven test groups +passed locally; both checkers and all eleven groups also passed on CPython3.9.6. +Receipt regeneration on CPython3.14.6 was byte-identical. The selected-record +integrity check and all five selected-result tests passed. The final overlap +refresh covered 845 open PRs and 17 discussions, with complete pagination; it +found the explicitly credited neighboring work above. Refreshed main +`dadfea6e8a78ff6ba901705f87532a71c6f5bbb8` retains the exact input blob and the +same selected result. + +## Open next questions + +1. Can the rank-seven endpoint pass the native recursive and owner/window + contracts? Start by emitting helper470's `0,79,186,513` path and checking an + exact rank-seven idle window, including pending source access. A positive + slot moment is useful only after the H4 and physical admission gaps close. + Compare with PR1043 before investing: its helper deletion may remain better. +2. Can helpers465/466/468 be restored after their single blocking target read + while retaining a favorable complete profile? Start with targets122/208/144 + respectively, recompute the inverse-row cut at the corresponding B boundary, + then check every dirty column and subsequent target dependency. The present + fixed-after-scatter theorem does not cover those later cuts. No search there + was performed. + +Structured next steps and the deliberate H2/K-to-H4 scope change are recorded +in [TASK.json](TASK.json). + +## Attribution and source status + +Ross Richardson prepared this contribution with substantial OpenAI Codex +assistance in mathematical reasoning, code, tests and writing. New material is +Apache-2.0, the repository license. + +Credit DreamingOfClouds (PR589/545), eumemic (PR555/543 and the interleaved +interface), their retained E8/native supplier lineage, and Ali Romman +(PR1128's two-sided boundary conditions and PR1043's earlier helper470 +source-deletion construction). Sagar Thakrar's PR1023 motivates width-seven +hosting. Hanson Sun's PR1079 independently identifies helper470 in the distinct +source-substitution class. Adam Gall's PR1179 changes a kernel entrance; +that mechanism is not imported or combined here. Frozen sources and their +original notices remain untouched. + +Exact Git/SHA256 input and historical context pins are in [SOURCES.json](SOURCES.json). +Pending PRs are research predecessors, not accepted replacements for the +selected source. [CLAIM.md](CLAIM.md) records task choice and overlap coverage. diff --git a/research/bit-early-retirement-cut/SOURCES.json b/research/bit-early-retirement-cut/SOURCES.json new file mode 100644 index 0000000000..ca4195b68e --- /dev/null +++ b/research/bit-early-retirement-cut/SOURCES.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/e8-bit-p111-tuned/tune/README.md", + "usage": "provenance", + "git_blob": "5b1554369682c8344d4f0767111d9b2b35eecbec", + "sha256": "46c7917fb252949f38b7bcd88cf568efc282e3ea065b61d11e457e41673d0b2d" + }, + { + "path": "research/e8-bit-p111-tuned/code/xcheck_p.py", + "usage": "provenance", + "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e" + }, + { + "path": "research/bit589-width-packing/README.md", + "usage": "provenance", + "git_blob": "a915381a7a38d3728205a2120aa034f94537ca0f", + "sha256": "671ca8a9d9e78348eae1e5c605ead1606df3d5e23d251600f0bdf60175479f1e" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "provenance", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + } + ], + "external_predecessors": [ + { + "pr": 1128, + "head": "df29b159239b79d7e451d6ddda826a73e0e50a67", + "author": "Ali Romman", + "role": "Six early-cut necessary-condition candidates and monotone-frame boundary model; no executable imported." + }, + { + "pr": 1043, + "head": "e309e17f83f5759b1ea1fa24a76f24838784cb4d", + "author": "Ali Romman", + "role": "Earlier superior helper470 source-deletion construction; not replayed or combined." + }, + { + "pr": 1079, + "head": "bb20dab261884412f2d2a7955cdb2fd8e2e64a16", + "author": "Hanson Sun", + "role": "Distinct source-substitution census; not replayed or combined." + } + ] +} diff --git a/research/bit-early-retirement-cut/TASK.json b/research/bit-early-retirement-cut/TASK.json new file mode 100644 index 0000000000..2108d6b98b --- /dev/null +++ b/research/bit-early-retirement-cut/TASK.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 2, + "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Classify eager single-frame restoration of the six PR1128 early-cut survivors; construct a fixed-prefix rank-seven endpoint for helper470.", + "scope_change_reason": "The donor assigned the bit-supplier track. The closest catalogue card concerns H2/K; overlap with PR1194 led to this distinct H4/terminal-frame question on PR1128's explicit early-cut opening.", + "bottleneck_link": "A width-seven helper could use otherwise idle rank-seven slots. This is finite interface evidence and an optimistic fully charged slot relaxation; the complex supplier still binds and physical/H4 admission is unresolved.", + "budget_minutes": 60, + "stop_rule": "Complete the six named helpers and all 111 target contracts at each common retirement frame. Permit one evidence-driven smaller-first-frame refinement. Stop after a complete finite endpoint or an exact obstruction; no later-B-cut search.", + "outcome": "completed", + "evidence": "CERTIFICATE.json; verify.py; independent.py; eleven fault-sensitive test groups in test_package.py.", + "author": "Ross Richardson", + "ai_assistance": "Substantial OpenAI Codex assistance in the proof, both implementations, tests, and writing; no independent human review is implied.", + "open_questions": [ + { + "question": "Can the helper470 endpoint be hosted and compiled under a justified cleanup contract?", + "why_it_matters": "The local rank reduction and favorable two-slot relaxation are not a supplier bound.", + "first_step": "Emit the path 0,79,186,513 and check one exact rank-seven idle window with source/pending access; compare total admission and price with PR1043.", + "blocked_by": "Changed H4 and native/owner-window/precision/tape admission are unproved." + }, + { + "question": "Can delayed restoration avoid the sole first-cut obstruction for helpers465,466,468?", + "why_it_matters": "Each has exactly one target obligation blocking its least-frame first restoration.", + "first_step": "Advance to the B boundaries completing target122,208,144 respectively; recompute the inverse-row and dirt-column cuts before proposing a schedule.", + "blocked_by": "Later cuts, their changed frames, and a fully charged new schedule have not been investigated." + } + ], + "assignment_seed": 8, + "seed_source": "Python secrets.randbelow(100), operating-system randomness, 2026-10-13T20:44:34.832556Z" +} diff --git a/research/bit-early-retirement-cut/VERIFY.json b/research/bit-early-retirement-cut/VERIFY.json new file mode 100644 index 0000000000..8b3fd1ca44 --- /dev/null +++ b/research/bit-early-retirement-cut/VERIFY.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact cut classification, full finite word and paid local/optimistic slot invoices" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separate set replay and integer geometry for all six cuts and both scalar directions" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 120, + "checks": "Eleven test groups including gate omissions, frame faults, corruptions and offline relocation" + } + ] +} diff --git a/research/bit-early-retirement-cut/independent.py b/research/bit-early-retirement-cut/independent.py new file mode 100644 index 0000000000..e0fa10dcf7 --- /dev/null +++ b/research/bit-early-retirement-cut/independent.py @@ -0,0 +1,225 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Set-valued scalar replay and fraction-free rational geometry; no verify.py import. +Ross Richardson, with substantial OpenAI Codex assistance. +""" +import argparse +import gzip +import hashlib +import json +import math +from collections import Counter +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def integer_basis(vectors): + basis = {} + for v in vectors: + a = list(v) + for p, b in sorted(basis.items()): + if a[p]: + x, y = b[p], a[p] + a = [x*u-y*v for u, v in zip(a, b)] + gcd = 0 + for z in a: + gcd = math.gcd(gcd, z) + if gcd: + a = [z//gcd for z in a] + if any(a): + p = next(i for i, x in enumerate(a) if x) + basis[p] = a + return list(basis.values()) + + +def inverse_sets(rows): + left, right = [r.copy() for r in rows], [{i} for i in range(len(rows))] + for c in range(len(rows)): + p = next(i for i in range(c, len(rows)) if c in left[i]) + left[c], left[p] = left[p], left[c] + right[c], right[p] = right[p], right[c] + for r in range(len(rows)): + if r != c and c in left[r]: + left[r].symmetric_difference_update(left[c]) + right[r].symmetric_difference_update(right[c]) + require(left == [{i} for i in range(len(rows))], 'independent inverse') + return right + + +def set_rank(rows): + basis = {} + for row in rows: + row = set(row) + while row: + p = min(row) + if p in basis: + row ^= basis[p] + else: + basis[p] = row + break + return len(basis) + + +def check(root): + pins = json.loads((HERE/'SOURCES.json').read_text()) + pin, = [x for x in pins['files'] if x['usage'] == 'input'] + raw = (root/pin['path']).read_bytes() + require(hashlib.sha256(raw).hexdigest() == pin['sha256'], 'independent source hash') + w = json.loads(gzip.decompress(raw)) + cert = json.loads((HERE/'CERTIFICATE.json').read_text()) + v, n = w['v'], 2*w['v']+w['R'] + bases = [integer_basis(w['lines'][i] for i in f) for f in w['frames']] + dims = [len(b) for b in bases] + contain_cache = {} + + def contains(a, b): + key = (a, b) + if key not in contain_cache: + contain_cache[key] = len(integer_basis(bases[a]+bases[b])) == dims[b] + return contain_cache[key] + + state = [{i} for i in range(n)] + frames = w['start'][:] + for name in ['D', 'A']: + for f, t, ss in w[name]: + for r in [t, *ss]: + require(contains(frames[r], f), 'prefix frame') + frames[r] = f + for s in ss: + state[t] ^= state[s] + for t, ss in enumerate(w['scatter']): + for s in ss: + state[v+t] ^= state[w['ret'][s]] + inverse = inverse_sets(state) + require([x['helper'] for x in cert['retirements']] == [465, 466, 468, 469, 470, 476], 'helper coverage') + lost_total, least_survivors = 0, [] + for case in cert['retirements']: + h, U = case['helper'], case['terminal_frame'] + restore = inverse[h] + dirt = {i for i, r in enumerate(state) if h in r} + participants = restore | dirt | {h} + require(case['restore_row'] == sorted(restore) and case['dirty_column'] == sorted(dirt), 'cut row/column') + require(case['forced_participants'] == sorted(participants), 'forced participant coverage') + require(dims[U] == 7 and all(contains(frames[r], U) for r in participants), 'retirement geometry') + join = integer_basis(z for r in participants for z in bases[frames[r]]) + require(len(join) == 7, 'terminal uniqueness') + missed = [{'target': t, 'boundary_coordinates': sorted((inverse[t] ^ inverse[t-v]) & participants)} + for t in range(v, 2*v) if not contains(U, w['final'][t]) and + (inverse[t] ^ inverse[t-v]) & participants] + require(missed == case['lost_targets'], 'all target obligations') + require(set_rank(x['boundary_coordinates'] for x in missed) == case['lost_dependency_rank'], 'lost rank') + lost_total += len(missed) + least = case['least_frame_restoration'] + minimum = integer_basis(z for r in restore for z in bases[frames[r]]) + matches = [f for f in range(len(bases)) if dims[f] == len(minimum) and + all(contains(frames[r], f) for r in restore)] + require(matches == [least['frame']] and dims[matches[0]] == least['rank'], 'least frame') + missed_least = [{'target': t, 'boundary_coordinates': sorted((inverse[t] ^ inverse[t-v]) & restore)} + for t in range(v, 2*v) if not contains(matches[0], w['final'][t]) and + (inverse[t] ^ inverse[t-v]) & restore] + require(missed_least == least['lost_targets'], 'least-frame target cut') + if not missed_least: + least_survivors.append(h) + example = case['witness'] + donor, target = example['boundary_coordinate'], example['target'] + require(donor in restore and donor < v, 'source witness') + delta = set(example['original_input_delta']) + require([len(r & delta) % 2 for r in state] == [int(r == donor) for r in range(n)], 'two-input witness') + require(len({target, target-v} & delta) % 2 == 1, 'distinguishable output') + sep = example['separation'] + dot = lambda line: sum(a*b for a, b in zip(sep['normal'], w['lines'][line])) + require(all(dot(line) == 0 for line in w['frames'][w['final'][target]]), 'target annihilator') + require(sep['line'] in w['frames'][U] and dot(sep['line']) == sep['dot'] != 0, 'separating vector') + copied = [x.copy() for x in state] + for t, s in case['star_gates']: + copied[t] ^= copied[s] + require(copied[h] == {h} and all(h not in row for r, row in enumerate(copied) if r != h), 'common-frame star') + require(lost_total == 59 and least_survivors == [470], 'classification') + + construction = cert['construction'] + for candidate in [False, True]: + state = [{i} for i in range(n)] + frames = w['start'][:] + paths, histogram, tape = [[f] for f in frames], Counter(), [] + positive, peak, copy_ranks = [1]*n, 1, [] + adds = moves = 0 + sections = ['D', 'A', 'scatter', 'E', 'B', 'C'] if candidate else ['D', 'A', 'scatter', 'B', 'C'] + final = w['final'][:] + if candidate: + final[470] = construction['final_helper_frame'] + + def move(r, f): + nonlocal moves + require(contains(frames[r], f), 'whole-word frame legality') + if frames[r] != f: + d = dims[f]-dims[frames[r]] + require(d > 0, 'strict frame climb') + histogram[d] += 1 + paths[r].append(f) + moves += 1 + frames[r] = f + + def add(t, s): + nonlocal adds, peak + state[t] ^= state[s] + positive[t] += positive[s] + peak = max(peak, positive[t]) + adds += 1 + tape.append((t, s)) + + for section in sections: + if section == 'scatter': + copy_ranks = [dims[frames[r]] for r in w['ret']] + histogram.update(copy_ranks) + for t, ss in enumerate(w['scatter']): + for s in ss: + add(v+t, w['ret'][s]) + continue + gates = construction['retirement_gates'] if section == 'E' else w[section] + for i, (f, t, ss) in enumerate(gates): + if candidate and section == 'C': + if i == construction['cleanup_omit_gate']: + continue + if i == construction['cleanup_replace_source']['gate']: + ss = [construction['cleanup_replace_source']['new_source']] + for r in [t, *ss]: + move(r, f) + for s in ss: + add(t, s) + if section == 'E': + require(state[470] == {470} and all(470 not in row for r, row in enumerate(state) if r != 470), 'E separation') + expected = [{r, r-v} if v <= r < 2*v else {r} for r in range(n)] + require(state == expected, 'complete 661-column endpoint') + reverse = [{i} for i in range(n)] + for t, s in tape[::-1]: + reverse[t] ^= reverse[s] + require(reverse == expected, 'literal inverse') + for r, f in enumerate(final): + move(r, f) + actual = {'ADDs': adds, 'MOVEs': moves, 'COPYs': 9, 'ERASEs': 9, 'COPY_ranks': copy_ranks, + 'records': adds+moves+18, 'profile': {str(k): x for k, x in sorted(histogram.items())}, + 'rank_mass': sum(k*x for k, x in histogram.items()), 'children': sum(histogram.values()), + 'positive_majorant_peak': str(peak), 'positive_majorant_bits': peak.bit_length()} + require(actual == construction['candidate' if candidate else 'baseline'], 'complete local invoice') + if candidate: + require([i for i in range(n) if paths[i] != base_paths[i]] == [470], 'other paths changed') + else: + base_paths = paths + print('PASS_INDEPENDENT_EARLY_RETIREMENT sets=661 geometry=integer ' + 'target_contracts=666 lost=59 least_frame_survivor=470 complete_word=both_directions') + + +if __name__ == '__main__': + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--root', type=Path, default=HERE.parents[1]) + args = ap.parse_args() + try: + check(args.root) + except (ValueError, OSError, KeyError, IndexError, StopIteration) as exc: + raise SystemExit('REJECT: ' + str(exc)) diff --git a/research/bit-early-retirement-cut/test_package.py b/research/bit-early-retirement-cut/test_package.py new file mode 100644 index 0000000000..ff1012fdf7 --- /dev/null +++ b/research/bit-early-retirement-cut/test_package.py @@ -0,0 +1,212 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Fault-sensitive algebra, frame, invoice and portable-package controls.""" +import copy +import importlib.util +import json +import random +import shutil +import subprocess +import sys +import tempfile +import unittest +from decimal import Decimal, localcontext +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('early_retirement_check', HERE/'verify.py') +check = importlib.util.module_from_spec(spec) +spec.loader.exec_module(check) + + +class PackageTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.root = HERE.parents[1] + cls.word = check.load_word(cls.root) + cls.geometry = check.Geometry(cls.word) + cls.frames, cls.values, _ = check.prefix_and_baseline(cls.word, cls.geometry) + cls.inverse = check.invert(cls.values) + cls.cert = json.loads((HERE/'CERTIFICATE.json').read_text()) + + def candidate(self, sections=None, final=None): + if final is None: + final = self.word['final'][:] + final[470] = 513 + return check.replay_complete(self.word, self.geometry, + check.patched_sections(self.word) if sections is None else sections, final) + + def test_complete_receipt_and_independent_replay(self): + self.assertEqual(check.canonical(check.analyze(self.word)), check.canonical(self.cert)) + p = subprocess.run([sys.executable, '-I', '-O', '-B', str(HERE/'independent.py')], + capture_output=True, text=True, timeout=30) + self.assertEqual(p.returncode, 0, p.stdout+p.stderr) + self.assertIn('PASS_INDEPENDENT_EARLY_RETIREMENT', p.stdout) + + def test_all_22_star_gate_omissions(self): + count = 0 + for case in self.cert['retirements']: + h = case['helper'] + for omitted in range(len(case['star_gates'])): + state = self.values[:] + for j, (t, s) in enumerate(case['star_gates']): + if j != omitted: + state[t] ^= state[s] + isolated = state[h] == 1 << h and all(not row >> h & 1 + for r, row in enumerate(state) if r != h) + self.assertFalse(isolated, (h, omitted)) + count += 1 + self.assertEqual(count, 22) + + def test_three_retirement_gate_omissions(self): + for j in range(3): + gates = [g for i, g in enumerate(check.RETIREMENT_GATES) if i != j] + with self.assertRaisesRegex(check.Reject, 'retirement separation'): + self.candidate(check.patched_sections(self.word, gates)) + + def test_both_cleanup_edits_are_necessary(self): + sections = check.patched_sections(self.word) + cleanup = copy.deepcopy(sections[-1][1]) + cleanup[580] = copy.deepcopy(self.word['C'][580]) + with self.assertRaisesRegex(check.Reject, 'complete dirty endpoint'): + self.candidate(sections[:-1]+[('C', cleanup)]) + cleanup = copy.deepcopy(sections[-1][1]) + cleanup.insert(2343, copy.deepcopy(self.word['C'][2343])) + with self.assertRaisesRegex(check.Reject, 'complete dirty endpoint'): + self.candidate(sections[:-1]+[('C', cleanup)]) + + def test_common_frame_promotion_breaks_target_access(self): + gates = copy.deepcopy(check.RETIREMENT_GATES) + gates[0][0] = 513 + with self.assertRaisesRegex(check.Reject, 'candidate frame descent'): + self.candidate(check.patched_sections(self.word, gates)) + final = self.word['final'][:] + final[470] = 0 + with self.assertRaisesRegex(check.Reject, 'candidate frame descent'): + self.candidate(final=final) + + def test_exact_input_pair_and_geometric_witnesses(self): + for case in self.cert['retirements']: + witness = case['witness'] + delta = sum(1 << i for i in witness['original_input_delta']) + wrong_delta = delta ^ (1 << case['helper']) + actual = [int(bin(row & wrong_delta).count('1') % 2) for row in self.values] + self.assertNotEqual(actual, [int(i == witness['boundary_coordinate']) for i in range(661)]) + target = witness['target'] + sep = witness['separation'] + normal = sep['normal'] + self.assertTrue(any(normal)) + self.assertTrue(all(sum(x*y for x, y in zip(normal, self.word['lines'][line])) == 0 + for line in self.word['frames'][self.word['final'][target]])) + self.assertNotEqual(sum(x*y for x, y in zip(normal, self.word['lines'][sep['line']])), 0) + + def test_geometry_scope_controls(self): + w = copy.deepcopy(self.word) + # Permitting every target to end at the full frame removes this cut. + for t in range(w['v'], 2*w['v']): + w['final'][t] = 1 + for case in self.cert['retirements']: + self.assertEqual(check.lost_targets(self.inverse, case['forced_participants'], + case['terminal_frame'], w, self.geometry), []) + # The smaller first frame really is a distinct allowed mechanism. + self.assertEqual([x['helper'] for x in self.cert['retirements'] + if not x['least_frame_restoration']['lost_targets']], [470]) + self.assertEqual([len(x['least_frame_restoration']['lost_targets']) + for x in self.cert['retirements']], [1, 1, 1, 10, 0, 9]) + + def test_small_binary_inverse_oracle(self): + rng = random.Random(8) + cases = 0 + for n in range(2, 7): + for trial in range(12): + rows = [1 << i for i in range(n)] + for _ in range(4*n): + t, s = rng.sample(range(n), 2) + rows[t] ^= rows[s] + inv = check.invert(rows) + for bits in range(1 << n): + image = sum((bin(row & bits).count('1') % 2) << i for i, row in enumerate(rows)) + restored = sum((bin(row & image).count('1') % 2) << i for i, row in enumerate(inv)) + self.assertEqual(restored, bits) + cases += 1 + self.assertEqual(cases, 60) + with self.assertRaisesRegex(check.Reject, 'singular'): + check.invert([1, 1]) + + def test_interval_arithmetic_and_returned_idle_charge(self): + invoice = self.cert['construction']['optimistic_hosting'] + a = Fraction(invoice['exponent']) + with localcontext() as context: + context.prec = 70 + exponent = Decimal(a.numerator)/Decimal(a.denominator) + for case in invoice['cases']: + delta = {int(k): v for k, v in case['profile_delta'].items()} + self.assertEqual(sum(delta.values()), 0) + self.assertEqual(sum(r*c for r, c in delta.items()), 0) + removed_charge = dict(delta) + del removed_charge[case['old_remainder']+8] + self.assertNotEqual(sum(r*c for r, c in removed_charge.items()), 0) + # Diagnostic cross-check of the rationally certified interval; + # Decimal is not used to certify the sign. + actual = sum(Decimal(c*r)*((Decimal(64)/r).ln()*exponent).exp() + for r, c in delta.items()) + lo, hi = map(Fraction, case['weighted_delta_interval']) + self.assertLess(Decimal(lo.numerator)/lo.denominator, actual) + self.assertLess(actual, Decimal(hi.numerator)/hi.denominator) + self.assertLess(hi, 0) + for r in (1, 2, 5, 7, 14): + lo, hi = check.weight_interval(r, Fraction(0)) + self.assertEqual((lo, hi), (r, r)) + + def test_offline_relocation_and_source_failure(self): + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) + package = root/'research'/'bit-early-retirement-cut' + package.mkdir(parents=True) + for name in ['verify.py', 'independent.py', 'SOURCES.json', 'CERTIFICATE.json']: + shutil.copy2(HERE/name, package/name) + source = root/check.WORD + source.parent.mkdir(parents=True) + shutil.copy2(self.root/check.WORD, source) + original = {str(p.relative_to(root)): p.read_bytes() for p in root.rglob('*') if p.is_file()} + for name in ['verify.py', 'independent.py']: + p = subprocess.run([sys.executable, '-I', '-O', '-B', str(package/name)], + cwd=temp, capture_output=True, text=True, timeout=30) + self.assertEqual(p.returncode, 0, p.stdout+p.stderr) + self.assertEqual(original, {str(p.relative_to(root)): p.read_bytes() for p in root.rglob('*') if p.is_file()}) + source.write_bytes(source.read_bytes()+b'corruption') + for name in ['verify.py', 'independent.py']: + p = subprocess.run([sys.executable, '-I', '-O', '-B', str(package/name)], + capture_output=True, text=True, timeout=30) + self.assertNotEqual(p.returncode, 0) + self.assertIn('source', p.stderr) + + def test_receipt_corruptions_rejected_by_both_checkers(self): + mutations = [] + for kind in ['cut', 'geometry', 'construction', 'invoice']: + receipt = copy.deepcopy(self.cert) + if kind == 'cut': + receipt['retirements'][0]['lost_targets'].pop() + elif kind == 'geometry': + receipt['retirements'][0]['witness']['separation']['normal'] = [0]*8 + elif kind == 'construction': + receipt['construction']['retirement_gates'].pop() + else: + receipt['construction']['candidate']['profile']['1'] -= 1 + mutations.append((kind, receipt)) + with tempfile.TemporaryDirectory() as temp: + folder = Path(temp) + for name in ['verify.py', 'independent.py', 'SOURCES.json']: + shutil.copy2(HERE/name, folder/name) + for kind, receipt in mutations: + (folder/'CERTIFICATE.json').write_text(check.canonical(receipt)) + for script in ['verify.py', 'independent.py']: + p = subprocess.run([sys.executable, '-I', '-O', '-B', str(folder/script), + '--root', str(self.root)], capture_output=True, text=True, timeout=30) + self.assertNotEqual(p.returncode, 0, (kind, script, p.stdout)) + self.assertIn('REJECT:', p.stderr) + + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/research/bit-early-retirement-cut/verify.py b/research/bit-early-retirement-cut/verify.py new file mode 100644 index 0000000000..245baf7e79 --- /dev/null +++ b/research/bit-early-retirement-cut/verify.py @@ -0,0 +1,457 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact common-frame retirement cut. No predecessor executable is imported. +Ross Richardson, with substantial OpenAI Codex assistance. +""" +import argparse +import gzip +import hashlib +import json +from collections import Counter +from fractions import Fraction +from functools import lru_cache +from pathlib import Path + +HERE = Path(__file__).resolve().parent +WORD = 'research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz' +SURVIVORS = ((465, 512), (466, 514), (468, 513), (469, 517), (470, 513), (476, 514)) +SEED = 8 + + +class Reject(ValueError): + pass + + +def need(ok, message): + if not ok: + raise Reject(message) + + +def canonical(data): + return json.dumps(data, sort_keys=True, indent=2) + '\n' + + +def support(row): + result = [] + while row: + bit = row & -row + result.append(bit.bit_length() - 1) + row ^= bit + return result + + +def binary_rank(rows): + pivots = {} + for row in rows: + while row: + p = row.bit_length() - 1 + if p in pivots: + row ^= pivots[p] + else: + pivots[p] = row + break + return len(pivots) + + +def invert(rows): + a = rows[:] + right = [1 << i for i in range(len(a))] + for col in range(len(a)): + pivot = next((r for r in range(col, len(a)) if a[r] >> col & 1), None) + need(pivot is not None, 'singular boundary') + a[col], a[pivot] = a[pivot], a[col] + right[col], right[pivot] = right[pivot], right[col] + for r in range(len(a)): + if r != col and a[r] >> col & 1: + a[r] ^= a[col] + right[r] ^= right[col] + need(a == [1 << i for i in range(len(a))], 'inverse residual') + return right + + +def rref(vectors): + rows = {} + for vector in vectors: + a = list(map(Fraction, vector)) + for p, b in sorted(rows.items()): + if a[p]: + q = a[p] + a = [x - q*y for x, y in zip(a, b)] + pivot = next((i for i, x in enumerate(a) if x), None) + if pivot is not None: + q = a[pivot] + rows[pivot] = [x/q for x in a] + return rows + + +class Geometry: + def __init__(self, word): + self.word = word + self.bases = [rref(word['lines'][line] for line in frame) + for frame in word['frames']] + + def rank(self, frame): + return len(self.bases[frame]) + + @lru_cache(maxsize=None) + def contained(self, small, large): + for vector in self.bases[small].values(): + a = vector[:] + for p, b in sorted(self.bases[large].items()): + q = a[p] + a = [x - q*y for x, y in zip(a, b)] + if any(a): + return False + return True + + def separation(self, small, large): + """An exact target annihilator detecting a vector in the retirement frame.""" + import math + basis = self.bases[large] + for free in range(self.word['h']): + if free in basis: + continue + normal = [Fraction(i == free) for i in range(self.word['h'])] + for pivot, row in sorted(basis.items(), reverse=True): + normal[pivot] = -sum(row[j]*normal[j] for j in range(pivot+1, len(row))) + scale = 1 + for x in normal: + scale = scale*x.denominator // math.gcd(scale, x.denominator) + normal = [int(x*scale) for x in normal] + for line in self.word['frames'][small]: + dot = sum(a*b for a, b in zip(normal, self.word['lines'][line])) + if dot: + return {'normal': normal, 'line': line, 'dot': dot} + raise Reject('no separating normal') + + +def load_word(root): + sources = json.loads((HERE / 'SOURCES.json').read_text()) + pins = [x for x in sources['files'] if x['usage'] == 'input'] + need(len(pins) == 1 and pins[0]['path'] == WORD, 'input inventory') + raw = (root / WORD).read_bytes() + need(hashlib.sha256(raw).hexdigest() == pins[0]['sha256'], 'source SHA256') + blob = hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() + need(blob == pins[0]['git_blob'], 'source Git blob') + return json.loads(gzip.decompress(raw)) + + +def prefix_and_baseline(word, geometry): + v, n = word['v'], 2*word['v'] + word['R'] + need((v, n, word['h']) == (111, 661, 8), 'pinned dimensions') + frames = word['start'][:] + values = [1 << i for i in range(n)] + operations = Counter() + + def section(name): + for f, target, donors in word[name]: + need(len(set([target, *donors])) == 1+len(donors), 'gate operands') + for r in [target, *donors]: + need(geometry.contained(frames[r], f), 'baseline frame descent') + frames[r] = f + for donor in donors: + values[target] ^= values[donor] + operations[name] += 1 + + section('D') + section('A') + need(all(frames[r] == 0 for r in range(v, 2*v)), 'pre-scatter target frame') + # Retained copies use the inherited PR589 scatter interface. This is the + # exact scalar cut immediately after scatter, not a native COPY compiler. + need(len(word['scatter']) == v and len(word['ret']) == 9, 'scatter coverage') + for t, donors in enumerate(word['scatter']): + for donor in donors: + values[v+t] ^= values[word['ret'][donor]] + operations['scatter'] += 1 + boundary_frames, boundary_rows = frames[:], values[:] + section('B') + section('C') + for r in range(n): + need(geometry.contained(frames[r], word['final'][r]), 'final frame descent') + expected = (1 << r) ^ (1 << (r-v)) if v <= r < 2*v else 1 << r + need(values[r] == expected, 'baseline dirty endpoint') + return boundary_frames, boundary_rows, dict(sorted(operations.items())) + + +def star(values, inverse, helper): + restore = support(inverse[helper]) + dirt = [r for r, row in enumerate(values) if row >> helper & 1] + need(helper in restore and helper in dirt, 'star pivot') + gates = [[helper, r] for r in restore if r != helper] + gates += [[r, helper] for r in dirt if r != helper] + result = values[:] + for t, s in gates: + result[t] ^= result[s] + need(result[helper] == 1 << helper, 'helper restoration') + need(all(not row >> helper & 1 for r, row in enumerate(result) if r != helper), + 'helper dirt remains') + return restore, dirt, gates, result + + +def lost_targets(inverse, participants, terminal, word, geometry): + mask = sum(1 << r for r in participants) + result = [] + v = word['v'] + for target in range(v, 2*v): + if geometry.contained(terminal, word['final'][target]): + continue + missing = (inverse[target] ^ inverse[target-v]) & mask + if missing: + result.append({'target': target, 'boundary_coordinates': support(missing)}) + return result + + +def least_restoration(word, geometry, frames, inverse, helper): + donors = support(inverse[helper]) + dimension = len(rref(vector for r in donors for vector in geometry.bases[frames[r]].values())) + matches = [f for f in range(len(word['frames'])) if geometry.rank(f) == dimension and + all(geometry.contained(frames[r], f) for r in donors)] + need(len(matches) == 1, 'least restoration frame not uniquely catalogued') + frame = matches[0] + return {'frame': frame, 'rank': dimension, 'donors': donors, + 'lost_targets': lost_targets(inverse, donors, frame, word, geometry)} + + +RETIREMENT_GATES = [[186, 470, [77]], [513, 444, [470]], [513, 475, [470]]] + + +def patched_sections(word, retirement=None): + cleanup = [] + removed, replaced = [], [] + for i, (f, t, donors) in enumerate(word['C']): + if t == 470: + need(donors == [77], 'unexpected cleanup restoration') + removed.append(i) + continue + if 470 in donors: + need(t == 444 and donors == [470], 'unexpected cleanup use') + donors = [77] + replaced.append(i) + cleanup.append([f, t, donors]) + need(removed == [2343] and replaced == [580], 'cleanup edit coverage') + return [('D', word['D']), ('A', word['A']), ('scatter', None), + ('E', RETIREMENT_GATES if retirement is None else retirement), + ('B', word['B']), ('C', cleanup)] + + +def replay_complete(word, geometry, sections, final): + n, v = 2*word['v'] + word['R'], word['v'] + values, positive = [1 << i for i in range(n)], [1]*n + frames = word['start'][:] + paths = [[f] for f in frames] + histogram, adds, moves, peak = Counter(), 0, 0, 1 + scalar_gates, copy_ranks = [], [] + + def climb(r, f): + nonlocal moves + need(geometry.contained(frames[r], f), 'candidate frame descent') + if f != frames[r]: + rank = geometry.rank(f) - geometry.rank(frames[r]) + need(rank > 0, 'candidate redundant frame alias') + histogram[rank] += 1 + moves += 1 + frames[r] = f + paths[r].append(f) + + def add(t, s): + nonlocal peak, adds + adds += 1 + values[t] ^= values[s] + positive[t] += positive[s] + peak = max(peak, positive[t]) + scalar_gates.append((t, s)) + + for name, gates in sections: + if name == 'scatter': + need(all(frames[r] == 0 for r in range(v, 2*v)), 'candidate scatter boundary') + for r in word['ret']: + histogram[geometry.rank(frames[r])] += 1 + copy_ranks.append(geometry.rank(frames[r])) + for t, donors in enumerate(word['scatter']): + for donor in donors: + add(v+t, word['ret'][donor]) + continue + for f, t, donors in gates: + need(len(set([t, *donors])) == len(donors)+1, 'candidate operands') + for r in [t, *donors]: + climb(r, f) + for s in donors: + add(t, s) + if name == 'E': + need(values[470] == 1 << 470 and all(not row >> 470 & 1 + for r, row in enumerate(values) if r != 470), 'retirement separation') + expected = [(1 << r) ^ (1 << (r-v)) if v <= r < 2*v else 1 << r for r in range(n)] + need(values == expected, 'candidate complete dirty endpoint') + for r, f in enumerate(final): + climb(r, f) + reverse = [1 << r for r in range(n)] + for t, s in reversed(scalar_gates): + reverse[t] ^= reverse[s] + need(reverse == expected, 'candidate literal inverse endpoint') + return {'ADDs': adds, 'MOVEs': moves, 'COPYs': len(word['ret']), 'ERASEs': len(word['ret']), + 'COPY_ranks': copy_ranks, 'records': adds + moves + 2*len(word['ret']), + 'profile': {str(k): x for k, x in sorted(histogram.items())}, + 'rank_mass': sum(k*x for k, x in histogram.items()), + 'children': sum(histogram.values()), 'positive_majorant_peak': str(peak), + 'positive_majorant_bits': peak.bit_length(), 'paths': paths} + + +def ln_interval(q): + """atanh series after exact power-of-two reduction; explicit geometric tail.""" + q, shift = Fraction(q), 0 + while q >= 2: + q /= 2 + shift += 1 + need(1 <= q < 2, 'log domain') + + def reduced(x): + z = (x-1)/(x+1) + lo = 2*sum(z**(2*j+1)/(2*j+1) for j in range(40)) + return lo, lo + 2*z**81/(81*(1-z*z)) + + lo, hi = reduced(q) + two_lo, two_hi = reduced(Fraction(2)) + return lo+shift*two_lo, hi+shift*two_hi + + +def rounded_interval(lo, hi, bits=100): + scale = 1 << bits + return (Fraction((lo*scale).__floor__(), scale), + Fraction((hi*scale).__ceil__(), scale)) + + +def weight_interval(rank, a): + import math + lo, hi = rounded_interval(*ln_interval(Fraction(64, rank)), bits=160) + lo, hi = a*lo, a*hi + need(0 <= lo <= hi < Fraction(1, 100), 'exponential domain') + lower = sum(lo**j/math.factorial(j) for j in range(13)) + upper = sum(hi**j/math.factorial(j) for j in range(13)) + upper += hi**13/math.factorial(13)/(1-hi/14) + return rounded_interval(rank*lower, rank*upper) + + +def invoice_relaxation(): + a = Fraction(1733427039589844234749, 10**24) + weights = {r: weight_interval(r, a) for r in (1, 2, 4, 5, 6, 7, 10, 12, 14)} + cases = [] + for remainder in (2, 4, 6): + delta = Counter({1: 1, 5: 1, 7: -2, remainder+8: 1, remainder: -1}) + need(sum(delta.values()) == sum(r*c for r, c in delta.items()) == 0, + 'two-slot child or mass balance') + lo = sum(c*weights[r][int(c < 0)] for r, c in delta.items()) + hi = sum(c*weights[r][int(c > 0)] for r, c in delta.items()) + need(hi < 0, 'optimistic two-slot invoice not favorable') + lo, hi = rounded_interval(lo, hi, bits=80) + cases.append({'old_remainder': remainder, + 'profile_delta': {str(r): c for r, c in sorted(delta.items())}, + 'weighted_delta_interval': [str(lo), str(hi)]}) + return {'exponent': str(a), 'weight': 'g(r)=r*(64/r)^a', 'cases': cases, + 'scope': 'Optimistic two-slot relocation only; new owner/window and H4 admission are unresolved.'} + + +def construction(word, geometry): + baseline = replay_complete(word, geometry, + [('D', word['D']), ('A', word['A']), ('scatter', None), ('B', word['B']), ('C', word['C'])], + word['final']) + final = word['final'][:] + final[470] = 513 + candidate = replay_complete(word, geometry, patched_sections(word), final) + changed_paths = [r for r in range(len(final)) if baseline['paths'][r] != candidate['paths'][r]] + need(changed_paths == [470], 'unexpected frame itinerary change') + paths = {'baseline': baseline.pop('paths')[470], 'candidate': candidate.pop('paths')[470]} + delta = {str(r): candidate['profile'].get(str(r), 0)-baseline['profile'].get(str(r), 0) + for r in range(1, 9)} + delta = {r: x for r, x in delta.items() if x} + need(delta == {'1': 1, '5': 1, '7': -1}, 'paid profile delta') + need(candidate['ADDs'] == baseline['ADDs']+2 == 24307, 'ADD count') + return {'retirement_gates': RETIREMENT_GATES, + 'cleanup_replace_source': {'gate': 580, 'old_source': 470, 'new_source': 77}, + 'cleanup_omit_gate': 2343, 'final_helper_frame': 513, + 'baseline': baseline, 'candidate': candidate, 'helper470_paths': paths, + 'other_register_paths_unchanged': 660, 'local_profile_delta': delta, + 'optimistic_hosting': invoice_relaxation()} + + +def analyze(word): + geometry = Geometry(word) + frames, values, ops = prefix_and_baseline(word, geometry) + inverse = invert(values) + n, v = len(values), word['v'] + # Positive control: the unmodified cut has no inaccessible target donor. + for target in range(v, 2*v): + for donor in support(inverse[target] ^ inverse[target-v]): + need(geometry.contained(frames[donor], word['final'][target]), + 'baseline target dependency inaccessible') + rows = [] + for helper, terminal in SURVIVORS[SEED % 6:] + SURVIVORS[:SEED % 6]: + restore, dirt, gates, isolated = star(values, inverse, helper) + participants = sorted(set(restore) | set(dirt) | {helper}) + need(all(geometry.contained(frames[r], terminal) for r in participants), + 'retirement input outside terminal') + union = rref(vector for r in participants for vector in geometry.bases[frames[r]].values()) + need(len(union) == geometry.rank(terminal) == 7, 'unique rank-seven terminal') + lost = lost_targets(inverse, participants, terminal, word, geometry) + need(lost, 'no target obstruction') + # Prefer a source-register witness, so the counterexample is not just + # the separately listed illegal promotion of a target register. + witness = next((entry, donor) for entry in lost + for donor in entry['boundary_coordinates'] if donor < v) + entry, donor = witness + need(donor in restore, 'witness must already be forced by restoration') + target = entry['target'] + original_delta = [j for j in range(n) if inverse[j] >> donor & 1] + delta = sum(1 << j for j in original_delta) + need([sum(1 for j in support(row & delta)) % 2 for row in values] == + [int(r == donor) for r in range(n)], 'input pair does not isolate boundary coordinate') + need(((delta >> target) ^ (delta >> (target-v))) & 1, 'desired target does not distinguish') + promotions = [{'register': r, 'from_frame': frames[r], + 'rank_increment': 7-geometry.rank(frames[r])} + for r in participants if frames[r] != terminal] + immediate = [r for r in participants if v <= r < 2*v and + not geometry.contained(terminal, word['final'][r])] + rows.append({'helper': helper, 'terminal_frame': terminal, + 'restore_row': restore, 'dirty_column': dirt, + 'forced_participants': participants, 'star_gates': gates, + 'star_ADDs': len(gates), 'star_isolates_all_661_columns': True, + 'promotions': promotions, + 'promotion_rank_sum': sum(x['rank_increment'] for x in promotions), + 'illegal_target_promotions': immediate, 'lost_targets': lost, + 'lost_dependency_rank': binary_rank(sum(1 << r for r in x['boundary_coordinates']) for x in lost), + 'least_frame_restoration': least_restoration(word, geometry, frames, inverse, helper), + 'witness': {'target': target, 'boundary_coordinate': donor, + 'original_input_delta': original_delta, + 'separation': geometry.separation(terminal, word['final'][target])}}) + rows.sort(key=lambda x: x['helper']) + return {'status': 'SCOPED_COMMON_FRAME_EARLY_RETIREMENT_OBSTRUCTION', + 'assignment_seed': SEED, 'dimensions': {'registers': n, 'targets': v}, + 'baseline_ADDs': ops, 'baseline_total_ADDs': sum(ops.values()), + 'baseline_target_access_violations': 0, 'retirements': rows, + 'coverage': {'helpers': 6, 'target_contracts': 666, + 'lost_target_contracts': sum(len(r['lost_targets']) for r in rows), + 'star_ADD_occurrences': sum(r['star_ADDs'] for r in rows)}, + 'construction': construction(word, geometry), 'no_new_kappa': True} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--root', type=Path, default=HERE.parents[1]) + parser.add_argument('--emit', type=Path, help='create a new receipt; never overwrite') + args = parser.parse_args() + result = analyze(load_word(args.root)) + encoded = canonical(result) + if args.emit: + with args.emit.open('x') as stream: + stream.write(encoded) + else: + expected = json.loads((HERE / 'CERTIFICATE.json').read_text()) + need(canonical(expected) == encoded, 'certificate mismatch') + print('PASS_BIT_EARLY_RETIREMENT_CUT helpers=6 lost=59 least_frame_survivor=470 ' + 'width=8->7 ADDs=24305->24307 mass=5129->5128 no_new_kappa') + + +if __name__ == '__main__': + try: + main() + except (Reject, OSError, ValueError, KeyError, IndexError) as error: + raise SystemExit('REJECT: ' + str(error))