From b9348c6907516e55dc07e135ad4d7a480d4f9840 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ian=20Lib=C3=A2nio?= <38297269+ianlibanio@users.noreply.github.com> Date: Tue, 13 Oct 2026 10:13:23 -0300 Subject: [PATCH] Scoped negative result: no relocation or Steinberg rewrite with exact reframing raises PR589's bit c Exhaustive search over every commuting relocation of a phase-A or phase-B summand or gate of the selected PR589 R439 bit word (within a phase, in-place splits, and across the scatter): 10,886 classes covering 1,442,430 insertion indices. Each class gets the exact optimum over all closed frame assignments (forward/backward bounds, independent free components, exhaustive enumeration). Result: 2,805 classes have no legal framing, 7,968 reproduce PR589's profile and 113 are worse; none is better. All 17 distinct worse profiles are certified with the repository's exact rational moment engine. All 659 Steinberg 3->2 rewrites of single-source gates (PR548's mechanism) preserve the exact F2 map and are neutral under exact reframing. Depth two: 891,589 interacting pairs of relocations (685,524 legal) give no improvement; their 58 distinct worse profiles are certified exactly. Controls: on PR555's word the search rediscovers PR589's hoist and sink, and the pair search reaches PR589's exact profile; the rebuilt control word passes PR589's exact F2 replay and the unchanged xcheck_p.py interface audit. A code-disjoint implementation reproduces every class outcome (0 mismatches), and a seed-14 sample of 2,000 interacting pairs agrees with it. Negative controls reject a non-commuting swap and a frame below its forced bound. Standard library only. Only research/bit589-transport-reframe/ is added. Assignment seed 14 (bit-supplier track); local claim in CLAIM.json. Co-Authored-By: Claude Opus 5.5 --- research/bit589-transport-reframe/CLAIM.json | 23 + .../bit589-transport-reframe/EXPECTED.json | 320 +++++++++++++ research/bit589-transport-reframe/README.md | 225 +++++++++ research/bit589-transport-reframe/certify.py | 75 +++ research/bit589-transport-reframe/export.py | 66 +++ .../independent_check.py | 443 ++++++++++++++++++ .../pair_sample_check.py | 95 ++++ research/bit589-transport-reframe/pairs.py | 116 +++++ research/bit589-transport-reframe/reframe.py | 337 +++++++++++++ research/bit589-transport-reframe/search.py | 231 +++++++++ .../bit589-transport-reframe/steinberg.py | 167 +++++++ research/bit589-transport-reframe/verify.py | 164 +++++++ 12 files changed, 2262 insertions(+) create mode 100644 research/bit589-transport-reframe/CLAIM.json create mode 100644 research/bit589-transport-reframe/EXPECTED.json create mode 100644 research/bit589-transport-reframe/README.md create mode 100644 research/bit589-transport-reframe/certify.py create mode 100644 research/bit589-transport-reframe/export.py create mode 100644 research/bit589-transport-reframe/independent_check.py create mode 100644 research/bit589-transport-reframe/pair_sample_check.py create mode 100644 research/bit589-transport-reframe/pairs.py create mode 100644 research/bit589-transport-reframe/reframe.py create mode 100644 research/bit589-transport-reframe/search.py create mode 100644 research/bit589-transport-reframe/steinberg.py create mode 100644 research/bit589-transport-reframe/verify.py diff --git a/research/bit589-transport-reframe/CLAIM.json b/research/bit589-transport-reframe/CLAIM.json new file mode 100644 index 0000000000..8b290fcd75 --- /dev/null +++ b/research/bit589-transport-reframe/CLAIM.json @@ -0,0 +1,23 @@ +{ + "status": "local sprint claim (no pinned coordination issue existed at 2026-10-13T11:35Z; no authenticated GitHub access from this session)", + "track": "00-19 bit supplier", + "assignment_seed": 14, + "seed_source": "python3 secrets.randbelow(100) (OS randomness)", + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "object": "PR589's tuned punctured R439 bit word (research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz), the selected #799 bit supplier", + "question": "Does one commuting relocation of a phase-A or phase-B summand or gate, followed by an exact optimum over all frame assignments, raise the nine-stage bit c = 1733427039589844234749/10^24?", + "why_not_a_duplicate": "PR589's tuner relocates one summand greedily with all other frames held fixed; open PR886 proves frame-only optimality with the gate order fixed and names gate-order moves as the remaining avenue; PR711 covers adjacent swaps on the older R420 word. This class contains both PR589's single-transport class and PR886's frame-only class.", + "method": "standard-library exact enumeration of every commuting relocation slot; per-candidate forward/backward frame bounds, independent free-gate components and exhaustive component enumeration; exact moment certification of any improvement", + "expected_deliverable": "either a verified word with larger bit c (construction, no new kappa because the selected assembly is complex-bound) or a scoped negative result with complete coverage counts", + "expected_finish": "2026-10-13T16:00Z", + "result": { + "status": "scoped negative result; no new kappa", + "scope_extensions_during_work": "cross-scatter relocations, Steinberg 3->2 rewrites (PR548's mechanism) and interacting pairs of relocations were added to the claimed class", + "depth_one_relocations": "10,886 classes (1,442,430 insertion indices): 2,805 no legal framing, 7,968 identical profile, 113 worse (17 distinct, certified), 0 better", + "steinberg_3_to_2": "659 rewrites, all F2-checked, all identical profile", + "depth_two_interacting_pairs": "891,589 pairs, 685,524 legal: 663,741 identical profile, 21,783 worse (58 distinct, certified), 0 better", + "independent_checks": "code-disjoint implementation: 0 mismatches on all depth-one classes and all 659 Steinberg optima; seed-14 sample of 2,000 pairs agrees", + "finished": "2026-10-13 (local)", + "link": "submitted as one pull request to CrocSwap/integer-mult-bounds from ianlibanio:research/bit589-transport-reframe-seed14 (2026-10-13); gh became available after the claim was recorded" + } +} diff --git a/research/bit589-transport-reframe/EXPECTED.json b/research/bit589-transport-reframe/EXPECTED.json new file mode 100644 index 0000000000..8e07a60713 --- /dev/null +++ b/research/bit589-transport-reframe/EXPECTED.json @@ -0,0 +1,320 @@ +{ + "pins": { + "tuned": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "base555": "1bc3c53d4baf4927c6a00c339ea3975516471a48074d4d97c6addaded2a4d858", + "moment": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", + "xcheck": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e" + }, + "depth1": { + "candidates": 10886, + "legal": 8081, + "illegal": 2805, + "improving": 0, + "same_cost": 7968, + "by_kind": { + "summand/A": { + "candidates": 6779, + "legal": 4972, + "improving": 0, + "same_cost": 4925 + }, + "gate/A": { + "candidates": 23, + "legal": 1, + "improving": 0, + "same_cost": 0 + }, + "summand/B": { + "candidates": 3788, + "legal": 2951, + "improving": 0, + "same_cost": 2886 + }, + "gate/B": { + "candidates": 56, + "legal": 0, + "improving": 0, + "same_cost": 0 + }, + "xsummand/A": { + "candidates": 224, + "legal": 153, + "improving": 0, + "same_cost": 153 + }, + "xsummand/B": { + "candidates": 16, + "legal": 4, + "improving": 0, + "same_cost": 4 + } + }, + "base_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "base_free_gates": 149, + "base_components": 125 + }, + "control555": { + "improving": 5, + "top": [ + [ + [ + "summand", + "A", + 1993, + 470, + 1993 + ], + { + "1": 1322, + "2": 1342, + "3": 80, + "4": 45, + "5": 102, + "6": 10, + "7": 19 + } + ], + [ + [ + "summand", + "A", + 1993, + 470, + 2037 + ], + { + "1": 1322, + "2": 1342, + "3": 79, + "4": 46, + "5": 102, + "6": 11, + "7": 18 + } + ], + [ + [ + "summand", + "A", + 1994, + 469, + 2029 + ], + { + "1": 1322, + "2": 1342, + "3": 79, + "4": 46, + "5": 102, + "6": 11, + "7": 18 + } + ], + [ + [ + "summand", + "A", + 1993, + 470, + 1994 + ], + { + "1": 1321, + "2": 1343, + "3": 79, + "4": 46, + "5": 103, + "6": 10, + "7": 18 + } + ], + [ + [ + "summand", + "A", + 1994, + 469, + 1995 + ], + { + "1": 1321, + "2": 1343, + "3": 79, + "4": 46, + "5": 103, + "6": 10, + "7": 18 + } + ] + ] + }, + "independent": { + "insertion_indices": 1323506, + "cross_scatter_indices": 118924, + "classes": 10886, + "primary_candidates": 10886, + "base_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "outcome": { + "same": 7968, + "illegal": 2805, + "worse": 113 + }, + "mismatches_vs_primary": 0, + "first_mismatches": [] + }, + "certify_depth1": { + "distinct_profiles": 18, + "certified_below": 17, + "base": 1, + "not_certified": 0, + "smallest_moment_excess": "1.442682815942970358633218113399708916169425181805479623411127407509955E-7", + "base_endpoint_control": "pass" + }, + "explicit_control": { + "moves": [ + [ + "summand", + "A", + 1993, + 470, + 1993 + ], + [ + "summand", + "A", + 1995, + 469, + 2030 + ] + ], + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "xcheck_last_line": "PASS interleaved interface lemma: hypotheses H1-H5 hold and the conclusion decomposes as U, J = I, D = K, C = U^-1" + }, + "negative_controls": { + "noncommuting_index": 603, + "noncommuting_endpoint_holds": false, + "lowered_gate": 241, + "lowered_profile_legal": false + }, + "pair_control555": { + "first": [ + [ + "summand", + "A", + 1993, + 470, + 1993 + ] + ], + "improving_pairs": 1, + "best_m2": [ + "summand", + "A", + 1995, + 469, + 2030 + ], + "best_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + } + }, + "depth2": { + "first_candidates": 10886, + "first_moves": 8081, + "pairs": 891589, + "legal_pairs": 685524, + "improving_pairs": 0, + "distinct_optimal_profiles": 59, + "pairs_with_base_profile": 663741 + }, + "certify_depth2": { + "distinct_profiles": 59, + "certified_below": 58, + "base": 1, + "not_certified": 0, + "smallest_moment_excess": "1.442682815942970358633218113399708916169425181805479623411127407509955E-7", + "base_endpoint_control": "pass" + }, + "steinberg": { + "word": "bitE8mut-p111-tuned.json.gz", + "c": "1733427039589844234749/1000000000000000000000000", + "triples": 659, + "by_section_case": { + "A/case2": 503, + "A/case1": 16, + "B/case2": 121, + "B/case1": 19 + }, + "f2_checked": 659, + "independent_agree": 659, + "outcome": { + "same": 659 + } + }, + "steinberg_control": { + "pair_index": 1778, + "c_slot": 1778, + "moved_by": -2, + "triples_in_expanded_A": 518, + "recovering_triples": [ + [ + 1, + 1779, + 1780, + 1778 + ] + ], + "recovered_word_identical": true, + "recovered_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + } + }, + "pair_sample": { + "seed": 14, + "pairs": 2000, + "agree": 2000, + "disagree": 0, + "primary_outcomes": { + "illegal": 481, + "base": 1476, + "other": 43 + }, + "first_disagreements": [] + } +} \ No newline at end of file diff --git a/research/bit589-transport-reframe/README.md b/research/bit589-transport-reframe/README.md new file mode 100644 index 0000000000..a1af337e68 --- /dev/null +++ b/research/bit589-transport-reframe/README.md @@ -0,0 +1,225 @@ +# One relocation or Steinberg rewrite plus exact reframing cannot raise PR589's bit c + +**Status: scoped negative result (exhaustive finite search with exact certification). No new κ, no new supplier.** + +The selected #799 assembly is complex-bound (bit lower 0.001733427…, complex lower 0.001664400…, κ = 0.001661634…), +so no bit-side change alone can move κ. This package settles a bit-side question that open +[PR886](https://github.com/CrocSwap/integer-mult-bounds/pull/886) leaves open. PR886 proves PR589's word frame-optimal +with the gate order fixed and concludes that further headroom on this word "must come from gate-order or structural +moves". Here the gate order changes by one relocation or two interacting relocations, or the gates change by one +Steinberg 3→2 rewrite, and every frame is then re-optimized exactly. + +## Statement + +Let W be PR589's tuned punctured R439 word (`research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz`, the +selected bit supplier), with nine-stage c = `1733427039589844234749/10^24`. Allow one of the following moves: + +- **summand relocation**: take one source s out of a phase-A or phase-B gate `t += {…, s, …}`, make it its own gate + `t += s`, and insert it at any index reachable by crossing only gates it commutes with. For a single-source gate, + the whole gate moves. The two indices next to its own remainder are the **in-place splits** of a multi-source gate. +- **gate relocation**: move a whole multi-source gate the same way. +- **cross-scatter relocation**: continue either move across the scatter into the other phase. This is allowed when the + moved gate commutes with the scatter: it writes neither a target nor a retained total, and reads no target. That + keeps H1–H5 syntactically: A still writes only z registers, and the new B gate writes z from z. + +Two XOR gates commute iff neither writes a register the other reads. Then give **every** phase-A/phase-B gate any +closed frame, from the catalogue or not, such that all register frame chains nest. D, start and final frames are +unchanged. The nine retained totals keep their COPY frames, so COPY ranks stay 7 and the decoder constant stays 63. +Targets stay at frame 0 until the scatter. C is the literal reverse of the z-destination gates at the full frame (H4). + +**Result (exhaustive over this class):** no relocation, under any frame assignment, gives a paid local profile with +c above W's. Of the 10,886 relocation classes: + +| outcome | summand/A | gate/A | summand/B | gate/B | across scatter A→B | B→A | total | +|---|---:|---:|---:|---:|---:|---:|---:| +| no legal frame assignment | 1,807 | 22 | 837 | 56 | 71 | 12 | 2,805 | +| optimum = W's exact profile | 4,925 | 0 | 2,886 | 0 | 153 | 4 | 7,968 | +| optimum strictly worse (c certified below) | 47 | 1 | 65 | 0 | 0 | 0 | 113 | +| **optimum better** | **0** | **0** | **0** | **0** | **0** | **0** | **0** | + +The classes cover all **1,442,430** individual insertion indices: 1,323,506 within a phase and 118,924 across the +scatter. Every class whose optimum differs from W's has one of 17 distinct profiles. For each, exact rational moment +bounds at W's published lower endpoint show that the nine-stage moment exceeds 1, so its c is strictly smaller +(smallest certified excess 1.44×10⁻⁷). The worse profiles are rearrangements of climbs such as {2,5}→{3,4} or +4→1+3. Every illegal class fails in the forward least-frame pass. In 853 of them a retained total's last phase-A gate +already needs more than its COPY hyperplane. In 1,952 a target's forced frame passes its final hyperplane. Least +frames are lower bounds for every legal assignment, so no framing can rescue these. + +**Steinberg 3→2 rewrites (PR548's mechanism, re-run greedily by PR589's tuner):** over F2, +`b: bt^=bs ; e: et^=bt` equals `e ; b ; (et^=bs)`, and `b ; e: bs^=es` equals `e ; b ; (bt^=es)`. So a triple +b, e, c whose members can be brought together through commuting gates collapses to `e ; b`. PR589's word has 659 +such triples among single-source gates: A 519 (16 case 1, 503 case 2) and B 140 (19, 121). Every rewritten word +passes an exact F2 replay of D, A, scatter, B and the rebuilt C on all columns. Every exact optimum, computed by both +implementations, is **PR589's exact profile**: 659 neutral, none better, none worse. + +**Depth-two extension (interacting pairs):** each of the 8,081 legal first moves m1 is applied, then every relocation +m2 of the changed word, including across the scatter, is enumerated on that word. m2 must come out of a gate that +touches a register of m1's moved operands or of m1's remainder gate. This gives **891,589 pairs**, 685,524 of them +legal. 663,741 legal pairs reproduce W's exact profile. The other 21,783 have one of 58 distinct profiles, each +certified exactly to have c below W's. **None is better.** The class covers "neutral move, then improving move" chains +on a common register, and contains PR589's own two-move path on PR555's word (see Controls). Pairs whose moves share no +register are not covered. + +**Implications.** Under exact reframing, PR589's word is a local optimum of the paid profile for single relocations +(including in-place splits and cross-scatter moves), for interacting pairs of relocations, and for single Steinberg +3→2 rewrites. On this word, further bit headroom has to come from outside these classes: + +- longer or non-interacting reorderings; +- changes to the op multiset (new or removed helpers, resynthesis); +- different COPY frames or decoder; +- the hosting remainder. + +ADD-count constructions that preserve every register's frame path leave the paid profile unchanged by construction. +None of this can move κ until a complex supplier exceeds the bit side (now 0.0017334 vs 0.0016644). + +## Relation to earlier work + +- **PR589** (DreamingOfClouds; the selected bit supplier; tuner from PR541/548 by Dugongue and PR542 by rohanarun) + relocates one elementary op and applies Steinberg 3→2 rewrites greedily, choosing frames locally with all other + frames held fixed. It reached a fixed point after two moves and claims no optimality. Both of its move types are + covered here, plus in-place splits, whole-gate and cross-scatter moves, with all frames re-optimized exactly after + the move. +- **PR886** (SethBurkart123, open) is the exact frame-only optimum at the fixed order. Its class relaxes C beyond H4. + This package keeps H4 and the COPY frames fixed, and reproduces its fixed-order conclusion on the A/B gates + (149 free gates in 125 components here, versus 159 in 133 with C relaxed there). +- **PR711** (thakrarsagar, open; adjacent A swaps) and **PR661** (yuj1r0, open; phase-B frames at fixed order) treat + the older R420 word, not the selected R439 word. Here the moves are not restricted to adjacent swaps. +- The R439 native ADD-count constructions target scalar additions, not the paid profile, so they are orthogonal to + this question. They include phase-A mini-nodes (PR728, PR792), phase-B blocks (PR873, PR880, PR891, PR906 and + others) and D compensation (PR915); those checked here (PR728, PR792, PR880, PR906) state that every frame path is + preserved. + +## Method + +`reframe.py` computes the exact optimum over all frame assignments for a given gate order: + +1. **Bounds.** Forward least frames `lo_g` are the closure of the operands' current least frames. A retained total's + last phase-A gate is set to its COPY frame, because that gate fixes the frame the scatter reads. Backward greatest + frames `hi_g` are the intersection of the operands' next upper bounds, with targets bounded by 0 before the scatter + and COPY frames pinned. By induction along each register chain, every legal assignment has `lo_g ⊆ f_g ⊆ hi_g`, and + the all-least assignment nests. If some `lo_g ⊄ hi_g`, or a least chain exceeds a final or COPY frame, no + assignment exists. +2. **Components.** Gates with `lo_g = hi_g` are forced. Free gates interact only through register chains, and a forced + gate between two free gates on a register fixes the frame there. The components of "consecutive free gates on a + register" are therefore independent in both legality and cost (as in PR886). +3. **Enumeration.** Each component is enumerated over every closed frame between its bounds, built by closure from + `lo_g`. Rank uses exact `Fraction` elimination. +4. **Objective.** At z = c the moment Σ n_d·d/(mW)·(m/d)^z is linear in the profile, the rank mass is invariant + (5,129), and the moment increases in z. So a profile raises c only if Σ n_d·d·(64/d)^c decreases. Ties are + compared as integer profiles, and every distinct non-base profile is then certified exactly (`certify.py`, using + the repository's rational moment engine with the inherited fallback term and PR589's idle remainder). + +D (all at frame 0 with operands at frame 0) and C (all at the full frame, every C operand ending at the full frame) +cannot add a climb beyond the last one to the final frame. `reframe.Word` asserts both facts, and the independent +implementation keeps D and C explicitly. + +**Slot equivalence.** Moving a gate only changes the gate sequences of its own operand registers, plus its phase for +a cross-scatter move. Inserting at index q changes them only through the number of operand-touching gates before q, +so one index per slot represents every index in it. `search.py` walks from the original index and records one index +each time it crosses a gate that touches the moved operands, or the scatter. `independent_check.py` instead enumerates +all 1,442,430 indices and groups them by prefix counts. Both give the same 6,802 + 3,844 within-phase and 224 + 16 +cross-scatter classes. + +## Controls + +- **Positive control (depth one).** On PR555's untuned word, the same search finds exactly five improving + relocations. They are PR589's hoist (summand 470 out of `A[1993]`, placed before its remainder; the best single + move) and PR589's sink (summand 469 out of `A[1994]`, placed after base gate 2028). The other three are a later + placement of summand 470 (after gate 2036) and the in-place splits of both gates. +- **Positive control (depth two).** From the hoist, the best interacting second move found by the pair search is + PR589's sink. The pair reaches exactly PR589's published local profile + `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}`; from the sink, the best second move is the hoist. +- **Explicit word.** `export.py` writes PR555 + hoist + sink with its optimal frames. PR589's `wlib.replay` checks the + exact F2 endpoint on all 661 columns and nesting, and returns that profile. The unchanged independent checker + `code/xcheck_p.py` accepts it: E8 labels, COPY ranks 7×9 at the punctured hyperplanes, H1–H5 and U/J/K/C⁻¹. +- **Steinberg detection control.** Under exact reframing, every inverse expansion `e ; b → b ; e ; c` of this word is + itself neutral, so this control tests detection rather than a gain. Phase A is expanded once (seeded choice, with c + moved to its farthest commuting slot). The 3→2 search on the expanded word lists the cancelling triple, and its + rewrite gives back PR589's phase A gate for gate. +- **Negative controls.** Swapping an op with an adjacent gate that reads its destination (non-commuting) breaks the + exact F2 endpoint. Lowering a gate frame below its forced bound makes the chains fail to nest. +- **Independent implementation** (`independent_check.py`, no shared code): frozenset frames, fraction-free integer + span tests, D and C kept explicitly, enumeration of every insertion index, and coarser any-shared-register groups. + On PR589's word it reproduces the class count (10,886 from 1,442,430 indices) and the outcome multiset of every + moved summand or gate, with **0 mismatches** (7,968 identical, 113 worse, 2,805 illegal). It also agrees on all 659 + Steinberg optima. A seeded sample (seed 14) of 2,000 interacting pairs, rebuilt by its own move builder, agrees on + every pair: 1,476 identical, 43 other, 481 illegal. + +## Reproduce + +Standard library only (no numpy, no compiler). From the repository root: + +```sh +python3 -B research/bit589-transport-reframe/verify.py /fresh/output/dir +``` + +Expected last line (5 min 34 s with `--jobs 10` on a 12-thread Linux machine; peak parent RSS 52 MB): + +```text +PASS_BIT589_TRANSPORT_REFRAME classes=10886 legal=8081 improving=0 control_rediscovered=2 independent_mismatches=0 certified=17 steinberg=659 pair_sample_agree=2000 no_new_kappa +``` + +The optional depth-two replay adds `--pairs`, which reruns the pair positive control, all 891,589 interacting pairs +and their exact certification (30 min 34 s with `--jobs 10`): + +```text +PASS_BIT589_TRANSPORT_REFRAME classes=10886 legal=8081 improving=0 control_rediscovered=2 independent_mismatches=0 certified=17 steinberg=659 pair_sample_agree=2000 pairs=685524 no_new_kappa +``` + +Each step prints `ok ` after comparing its output with `EXPECTED.json`, and any difference stops the replay with +`FAIL`. Validated on Fedora Linux 44 (x86_64): the default replay passes under CPython 3.14.8 (forkserver workers) +and CPython 3.12.15 (fork workers), and the `--pairs` replay passes under CPython 3.14.8. No macOS or Windows run and +no remote CI are claimed. + +`EXPECTED.json` freezes every count and profile. Individual entry points: `search.py WORD C [--detail]`, +`pairs.py WORD C`, `steinberg.py WORD C [--independent|--control]`, `independent_check.py WORD PRIMARY_DETAIL`, +`pair_sample_check.py WORD C N SEED`, `certify.py PROFILES`, `export.py WORD C OUT MOVES`. + +## Scope and non-claims + +- **Exhaustive only within the stated classes.** They are: + - one relocation within A, within B or across the scatter; + - interacting pairs of such relocations; + - one Steinberg 3→2 rewrite of single-source gates; + + each followed by arbitrary frames. Not covered: + - longer reorderings and non-interacting pairs; + - Steinberg rewrites combined with relocations or with each other, rewrites involving multi-source gates, and + other changes of the op multiset (pruning, new helpers, resynthesis); + - changes to D, C, COPY frames, the decoder or the hosting (the idle remainder is about 13% of the bit moment); + - other words. + + Absence of a candidate in this class is not an impossibility theorem for the bit supplier. +- The cost model is PR589's paid local profile priced by its `fastc` identity, c = certify(288·local + REM, 64, + 28416), with the idle remainder REM held at PR589's value, as PR589's own moves did. It is not a rerun of the C++ + hosting pipeline, which needs a compiler and Boost. A move that keeps the local profile could in principle change + the frozen hosting selection; that is outside this model. With no improving candidate there is no new word to host. +- All inherited assumptions of PR555/PR589 and of the selected #799 review remain: all-size compiler, + mutable-source realization, whole-call hosting, precision/tape and analytic hypotheses. This is not a Lean proof + and does not formalize the multiplication theorem. +- The selected record, the PR589 package and `upstream/` are unchanged. Only this directory is added. + +## Pins + +| item | value | +|---|---| +| base commit | `f567884aeb8851b6e794af1184119a3bfbe1e631` | +| PR589 word (selected bit supplier; PR589 head `a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46`) | sha256 `e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f`, content `5642fd0e…eba0b` (= PR589 `EXPECTED.json`) | +| PR555 word (positive control) | sha256 `1bc3c53d4baf4927c6a00c339ea3975516471a48074d4d97c6addaded2a4d858`, content `d0df3c89…5cbe3` | +| moment engine | sha256 `81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482` (= selected assembly input pin) | +| interface checker `code/xcheck_p.py` | sha256 `af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e` | +| compared open PRs | PR886 `881f72ec596a5c6d7aba801153792292ecc39737`, PR711 `ebd567a22d26fadc1c8292b5c57056fb52331266` | + +## Attribution + +Contributor: Ian Libânio (GitHub `ianlibanio`). Assignment seed **14** (OS randomness), bit-supplier track. No pinned +coordination issue existed, so the claim is local in `CLAIM.json`. The search, checkers, certification and this note +were prepared with substantial AI assistance (Claude Opus 5.5, Anthropic, via Claude Code). Apache-2.0. + +Built on: + +- eumemic's PR543/PR555 word, its `xcheck_p.py` and the R420 interface lemma; +- DreamingOfClouds' PR545/PR510/PR589 word, `wlib.py`, `fastc.py` and remainder identity; +- the transport and Steinberg 3→2 mechanisms of Dugongue's PR541/PR548 and rohanarun's PR542; +- SethBurkart123's PR886 bounds-and-components method; +- the R420 analogues of thakrarsagar (PR711) and yuj1r0 (PR661). diff --git a/research/bit589-transport-reframe/certify.py b/research/bit589-transport-reframe/certify.py new file mode 100644 index 0000000000..4c70cfca63 --- /dev/null +++ b/research/bit589-transport-reframe/certify.py @@ -0,0 +1,75 @@ +"""Exact rational certification that no reported optimal profile raises the nine-stage bit c. + +For a local paid profile P the nine-stage profile is 288 P + REM (REM is the idle remainder of the frozen hosting, +read off PR589's hosted audit; PR589's tune/fastc.py checks that this reproduces the pipeline c). The moment + M_P(a) = sum_d n_d d/(m W) (m/d)^a + 32 m (sum_d n_d)/(10^16 W) m^a, m = 64, W = 28416, +is strictly increasing in a, and c(P) is its root of M_P = 1. With c0 the base word's published lower endpoint, +a rigorous lower bound M_P(c0) > 1 proves c(P) < c0. The bounds come from the repository's exact engine +(alternating Mercator logarithms, 24-term exponential with geometric tail, outward dyadic rounding). + +Usage: certify.py PROFILES.json (a JSON list of local profiles {rank: count}) +Prepared with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0. +""" +import importlib.util +import json +import sys +from fractions import Fraction +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +ENG = ROOT / 'research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/moment.py' +spec = importlib.util.spec_from_file_location('pr589_moment', ENG) +M = importlib.util.module_from_spec(spec) +spec.loader.exec_module(M) + +REM = {2: 13920, 4: 14208, 6: 14208, 7: 21312, 42: 288} # PR589 tune/fastc.py +m, W, T = 64, 28416, 288 +BASE = {1: 1323, 2: 1342, 3: 79, 4: 44, 5: 102, 6: 11, 7: 19} +C0 = Fraction(1733427039589844234749, 10 ** 24) + + +def nine_stage(local): + P = {} + for d, n in local.items(): + P[int(d)] = P.get(int(d), 0) + T * n + for d, n in REM.items(): + P[d] = P.get(d, 0) + n + assert m * W - sum(d * n for d, n in P.items()) == 10272, 'rank mass changed' + return P + + +def main(): + profiles = json.load(open(sys.argv[1])) + # control: the base profile's moment brackets 1 at the published endpoint grid + lo_b, hi_b = M.moment(nine_stage(BASE), m, W, C0, True) + lo_u, hi_u = M.moment(nine_stage(BASE), m, W, C0 + Fraction(1, 10 ** 24), True) + assert hi_b < 1 < lo_u, 'base endpoint control failed' + seen = set() + worst = None + out = [] + for local in profiles: + local = {int(k): v for k, v in local.items() if v} + key = tuple(sorted(local.items())) + if key in seen: + continue + seen.add(key) + if local == BASE: + out.append(dict(profile=local, verdict='base')) + continue + lo, hi = M.moment(nine_stage(local), m, W, C0, True) + ok = lo > 1 + excess = lo - 1 + worst = excess if worst is None or excess < worst else worst + out.append(dict(profile=local, verdict='c below base' if ok else 'NOT CERTIFIED', + moment_minus_one_lower=M.decimal(excess))) + bad = [r for r in out if r['verdict'] == 'NOT CERTIFIED'] + print(json.dumps(dict(distinct_profiles=len(out), certified_below=sum(r['verdict'] == 'c below base' for r in out), + base=sum(r['verdict'] == 'base' for r in out), not_certified=len(bad), + smallest_moment_excess=None if worst is None else M.decimal(worst), + base_endpoint_control='pass'))) + if bad: + sys.exit(1) + + +if __name__ == '__main__': + main() diff --git a/research/bit589-transport-reframe/export.py b/research/bit589-transport-reframe/export.py new file mode 100644 index 0000000000..38046443f2 --- /dev/null +++ b/research/bit589-transport-reframe/export.py @@ -0,0 +1,66 @@ +"""Write the explicit word of a relocation sequence with its exact optimal frames, for the unchanged official checkers. + +Moves are applied in order, each to the word produced by the previous one (search.py's (kind, section, index, +source, insertion index) tuples). Frames come from reframe.optimum; closed frames outside the catalogue are appended. +D, start and final are unchanged; C is rebuilt as the literal reverse of the z-destination gates of A then B at the +full frame (H4). The written word is then replayed by PR589's tune/wlib.py (exact F2 endpoint on every column, frame +nesting, paid profile); run code/xcheck_p.py on it for the independent interface audit. + +Usage: export.py WORD.json.gz C OUT.json.gz MOVES_JSON +Prepared with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0. +""" +import copy +import json +import os +import sys +from fractions import Fraction +from pathlib import Path + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import reframe as R +import search as S +from pairs import View + +ROOT = Path(__file__).resolve().parents[2] +sys.path.insert(0, str(ROOT / 'research/e8-bit-p111-tuned/tune')) +import wlib # noqa: E402 (PR589's exact replay, unchanged) + + +def build(path, z, moves): + word = R.Word(R.load(path)) + cur = word + for mv in moves: + A, B = S.apply(cur, tuple(mv)) + cur = View(word, A, B) + opt = R.optimum(word, cur.A, cur.B, z, want_frames=True) + if opt is None: + raise SystemExit('no legal frame assignment') + w = copy.deepcopy(word.w) + idx = {m: i for i, m in enumerate(word.fm)} + + def fid(m): + if m not in idx: + idx[m] = len(w['frames']) + w['frames'].append([i for i in range(w['v']) if m >> i & 1]) + return idx[m] + + fr = opt['frames'] + nA = len(cur.A) + w['A'] = [[fid(fr[k]), t, list(ss)] for k, (f, t, ss) in enumerate(cur.A)] + w['B'] = [[fid(fr[nA + k]), t, list(ss)] for k, (f, t, ss) in enumerate(cur.B)] + w['C'] = wlib.rebuild_C(w) + return w, opt + + +def main(): + path, c, out, moves = sys.argv[1], Fraction(sys.argv[2]), sys.argv[3], json.loads(sys.argv[4]) + w, opt = build(path, float(c), moves) + replayed = {int(k): v for k, v in wlib.paid(w).items()} # asserts the exact endpoint and nesting + assert replayed == opt['profile'], (replayed, opt['profile']) + sha = wlib.save(w, out) + print(json.dumps(dict(out=out, sha256=sha, moves=moves, profile=replayed, frames=len(w['frames']), + gates={s: len(w[s]) for s in 'DABC'}))) + + +if __name__ == '__main__': + main() diff --git a/research/bit589-transport-reframe/independent_check.py b/research/bit589-transport-reframe/independent_check.py new file mode 100644 index 0000000000..64cb417d3f --- /dev/null +++ b/research/bit589-transport-reframe/independent_check.py @@ -0,0 +1,443 @@ +"""Independent re-implementation of the depth-one search (shares no code with reframe.py / search.py). + +Differences from the primary implementation, chosen so that a shared mistake is unlikely: + * frames are frozensets of line indices; spans use fraction-free integer elimination (no Fraction, no masks); + * every legal insertion index is enumerated (not one representative per slot), within a section and across the + scatter; indices are grouped by the prefix counts that fix every changed register sequence, which must reproduce + the primary slot count exactly; moves are rebuilt from their descriptions by separate code; + * D and C are kept in the replayed word (D at frame 0, C rebuilt as the literal reverse at the full frame) instead of + being argued away; + * free gates are grouped by any shared register (coarser than "consecutive on a register"), then each group is + enumerated exhaustively over all closed frames between the bounds. +For each class the optimal paid profile is compared with the primary result file. + +Usage: independent_check.py WORD.json.gz PRIMARY_DETAIL.json [--jobs N] +Prepared with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0. +""" +import gzip +import itertools +import json +import os +import sys +from collections import Counter, defaultdict +from math import gcd +from multiprocessing import Pool + + +def int_rank_basis(vectors): + """row echelon basis of integer vectors by fraction-free elimination (rows kept primitive)""" + basis = [] # list of (pivot, row) + for v in vectors: + row = list(v) + for piv, b in basis: + if row[piv]: + a, c = b[piv], row[piv] + row = [a * x - c * y for x, y in zip(row, b)] + g = 0 + for x in row: + g = gcd(g, x) + if g > 1: + row = [x // g for x in row] + piv = next((k for k, x in enumerate(row) if x), None) + if piv is not None: + basis.append((piv, row)) + return basis + + +def in_span(basis, v): + row = list(v) + for piv, b in basis: + if row[piv]: + a, c = b[piv], row[piv] + row = [a * x - c * y for x, y in zip(row, b)] + return not any(row) + + +class Geometry: + def __init__(self, lines): + self.lines = [tuple(l) for l in lines] + self.memo = {} + + def closure(self, S): + S = frozenset(S) + if S in self.memo: + return self.memo[S] + basis = int_rank_basis([self.lines[i] for i in sorted(S)]) + C = frozenset(i for i in range(len(self.lines)) if i in S or (basis and in_span(basis, self.lines[i]))) + out = (C, len(basis)) + self.memo[S] = out + self.memo[C] = out + return out + + +def word_parts(w): + V = w['v'] + N = 2 * V + w['R'] + fr = [frozenset(f) for f in w['frames']] + full = frozenset(range(V)) + return V, N, fr, full + + +def ops_commute(a, b): + (ta, sa), (tb, sb) = a, b + return ta not in sb and tb not in sa + + +def variants_of(gate): + """(source or None, moved op, remainder or None) for each summand of a gate, plus the whole multi-source gate""" + f, t, ss = gate + out = [(x, (t, (x,)), (t, tuple(y for y in ss if y != x)) if len(ss) > 1 else None) for x in ss] + if len(ss) > 1: + out.append((None, (t, tuple(ss)), None)) + return out + + +def without(L, i, rem): + rest = [(g[1], tuple(g[2])) for g in L] + del rest[i] + if rem is not None: + rest.insert(i, rem) + return rest + + +def prefix_counts(seq, regs): + pref = {r: [0] for r in regs} + for t2, s2 in seq: + for r in regs: + pref[r].append(pref[r][-1] + (t2 == r or r in s2)) + return pref + + +def move_classes(L): + """every insertion index of the same section reachable through commuting gates, grouped into classes. + + Moving op only changes the gate sequences of op's own registers (and, for a split, the gate key of the remainder, + which does not depend on the index). After inserting op at index q of `rest`, register r's sequence is fixed by + the number of gates of rest[:q] that touch r. So the tuple of those counts over op's registers is the class key. + Returns (number of indices, list of (i, source or None, representative index)).""" + out = [] + n_idx = 0 + for i, gate in enumerate(L): + for s, op, rem in variants_of(gate): + rest = without(L, i, rem) + regs = sorted({op[0], *op[1]}) + pref = prefix_counts(rest, regs) + reach = {i} + p = i + while p > 0 and ops_commute(op, rest[p - 1]): + p -= 1 + reach.add(p) + p = i + while p < len(rest) and ops_commute(op, rest[p]): + p += 1 + reach.add(p) + identity = tuple(pref[r][i] for r in regs) if (s is None or len(gate[2]) == 1) else None + seen = {} + for q in sorted(reach): + n_idx += 1 + key = tuple(pref[r][q] for r in regs) + if key != identity and key not in seen: + seen[key] = q + out += [(i, s, q) for q in seen.values()] + return n_idx, out + + +def cross_classes(w): + """relocations into the other section. The scatter writes the targets and reads the retained totals, so an op + commutes with it iff it does not write a retained total and reads no target; H3 further requires a phase-A gate + (and so any gate that ends up in A, or comes from A) to write no target. The op must reach the end of A (from A) + or the start of B (from B) through commuting gates; every index of the other section reachable from its near end + is then grouped by prefix counts as above. Returns (number of indices, list of (section, i, source, index)).""" + V = w['v'] + targets = set(range(V, 2 * V)) + ret = set(w['ret']) + out = [] + n_idx = 0 + for sec, other in (('A', 'B'), ('B', 'A')): + L, M = w[sec], [(g[1], tuple(g[2])) for g in w[other]] + for i, gate in enumerate(L): + for s, op, rem in variants_of(gate): + t, srcs = op + if t in ret or t in targets or any(x in targets for x in srcs): + continue + rest = without(L, i, rem) + if sec == 'A' and not all(ops_commute(op, g) for g in rest[i:]): + continue + if sec == 'B' and not all(ops_commute(op, g) for g in rest[:i]): + continue + regs = sorted({t, *srcs}) + pref = prefix_counts(M, regs) + if sec == 'A': + reach = [0] + while reach[-1] < len(M) and ops_commute(op, M[reach[-1]]): + reach.append(reach[-1] + 1) + else: + reach = [len(M)] + while reach[-1] > 0 and ops_commute(op, M[reach[-1] - 1]): + reach.append(reach[-1] - 1) + seen = {} + for q in reach: + n_idx += 1 + seen.setdefault(tuple(pref[r][q] for r in regs), q) + out += [(sec, i, s, q) for q in seen.values()] + return n_idx, out + + +def build(w, sec, i, s, dst, q): + """the (A, B) gate lists of one move, rebuilt from its description""" + L = w[sec] + gate = L[i] + s_, op, rem = next(v for v in variants_of(gate) if v[0] == s) + rest = without(L, i, rem) + other = 'B' if sec == 'A' else 'A' + if dst == sec: + new = rest[:q] + [op] + rest[q:] + lists = {sec: new, other: [(g[1], tuple(g[2])) for g in w[other]]} + else: + M = [(g[1], tuple(g[2])) for g in w[other]] + lists = {sec: rest, other: M[:q] + [op] + M[q:]} + return lists['A'], lists['B'] + + +class Problem: + def __init__(self, w): + self.w = w + self.V, self.N, self.fr, self.full = word_parts(w) + self.geo = Geometry(w['lines']) + self.start = [self.fr[f] for f in w['start']] + self.final = [self.fr[f] for f in w['final']] + self.ret = w['ret'] + cur = list(self.start) + for f, t, ss in w['D'] + w['A']: + for r in [t, *ss]: + cur[r] = self.fr[f] + self.copy = {q: cur[q] for q in self.ret} + self.D = [(t, tuple(ss)) for f, t, ss in w['D']] + self.Dframes = [self.fr[f] for f, t, ss in w['D']] + + def optimum(self, A, B): + """A, B: lists of (t, sources). Returns the optimal profile (dict) or None.""" + V, N = self.V, self.N + C = [(t, ss) for t, ss in reversed(A + B) if t < V or t >= 2 * V] + seq = [('D', g) for g in self.D] + [('A', g) for g in A] + [('S', None)] + [('B', g) for g in B] + \ + [('C', g) for g in C] + n = len(seq) + fixed = {} + for k in range(len(self.D)): + fixed[k] = self.Dframes[k] + for k in range(n - len(C), n): + fixed[k] = self.full + geo = self.geo + # forward least frames + lo = [None] * n + cur = list(self.start) + for k, (sec, g) in enumerate(seq): + if sec == 'S': + for q in self.ret: + if not cur[q] <= self.copy[q]: + return None + cur[q] = self.copy[q] + continue + t, ss = g + U = frozenset().union(*(cur[r] for r in (t, *ss))) + m = geo.closure(U)[0] + if k in fixed: + if not m <= fixed[k]: + return None + m = fixed[k] + lo[k] = m + for r in (t, *ss): + cur[r] = m + for r in range(N): + if not cur[r] <= self.final[r]: + return None + # backward greatest frames + hi = [None] * n + ub = list(self.final) + for k in range(n - 1, -1, -1): + sec, g = seq[k] + if sec == 'S': + for q in self.ret: + if not self.copy[q] <= ub[q]: + return None + ub[q] = self.copy[q] + for r in range(V, 2 * V): + ub[r] = frozenset() + continue + t, ss = g + m = frozenset.intersection(*(ub[r] for r in (t, *ss))) + if k in fixed: + if not fixed[k] <= m: + return None + m = fixed[k] + hi[k] = m + for r in (t, *ss): + ub[r] = m + for k in range(n): + if lo[k] is not None and not lo[k] <= hi[k]: + return None + # options of free gates + opts = {} + for k in range(n): + if lo[k] is None or lo[k] == hi[k]: + continue + found = {lo[k]} + frontier = [lo[k]] + while frontier: + m = frontier.pop() + for i in hi[k] - m: + c = geo.closure(m | {i})[0] + if c <= hi[k] and c not in found: + found.add(c) + frontier.append(c) + opts[k] = sorted(found, key=lambda s: (len(s), sorted(s))) + # register -> positions + regpos = defaultdict(list) + for k, (sec, g) in enumerate(seq): + if sec != 'S': + for r in (g[0], *g[1]): + regpos[r].append(k) + scat = next(k for k, (sec, g) in enumerate(seq) if sec == 'S') + frames = [lo[k] for k in range(n)] + + def climbs(r): + H = Counter() + c = self.start[r] + checked = r not in self.copy + for k in regpos[r]: + if not checked and k > scat: + if c != self.copy[r]: + return None + checked = True + m = frames[k] + if m != c: + if not c <= m: + return None + H[geo.closure(m)[1] - geo.closure(c)[1]] += 1 + c = m + if not checked and c != self.copy[r]: + return None + if c != self.final[r]: + if not c <= self.final[r]: + return None + H[geo.closure(self.final[r])[1] - geo.closure(c)[1]] += 1 + return H + + # groups of free gates sharing any register + regs_of = {k: {seq[k][1][0], *seq[k][1][1]} for k in opts} + unseen = set(opts) + groups = [] + while unseen: + k0 = unseen.pop() + grp, todo = [k0], [k0] + while todo: + k = todo.pop() + for r in regs_of[k]: + for k2 in regpos[r]: + if k2 in unseen: + unseen.discard(k2) + grp.append(k2) + todo.append(k2) + groups.append(sorted(grp)) + z = float(self.w.get('_z', 0.0017334)) + + def cost(H): + return sum(cnt * d * (64 / d) ** z for d, cnt in H.items()) + + for grp in groups: + regs = sorted(set().union(*(regs_of[k] for k in grp))) + best = None + for combo in itertools.product(*(opts[k] for k in grp)): + for k, m in zip(grp, combo): + frames[k] = m + H = Counter() + ok = True + for r in regs: + h = climbs(r) + if h is None: + ok = False + break + H.update(h) + if ok: + key = (cost(H), [sorted(m) for m in combo]) + if best is None or key < best: + best = (key[0], key[1], combo) + if best is None: + return None + for k, m in zip(grp, best[2]): + frames[k] = m + H = Counter() + for r in range(N): + h = climbs(r) + if h is None: + return None + H.update(h) + for q in self.ret: + H[geo.closure(self.copy[q])[1]] += 1 + return dict(sorted(H.items())) + + +_P = None + + +def _init(path, z): + global _P + w = json.load(gzip.open(path, 'rt')) + w['_z'] = z + _P = Problem(w) + + +def _job(moves): + out = [] + for mv in moves: + A, B = build(_P.w, *mv) + out.append((mv, _P.optimum(A, B))) + return out + + +def main(): + path, primary = sys.argv[1], sys.argv[2] + jobs = int(sys.argv[sys.argv.index('--jobs') + 1]) if '--jobs' in sys.argv else os.cpu_count() + w = json.load(gzip.open(path, 'rt')) + prim = json.load(open(primary)) + num, den = prim['c'].split('/') if '/' in prim['c'] else (prim['c'], '1') + z = int(num) / int(den) + V, N = w['v'], 2 * w['v'] + w['R'] + base_ops = {sec: [(t, tuple(ss)) for f, t, ss in w[sec]] for sec in 'AB'} + # enumerate every insertion index and group it into classes (identity classes dropped as in the primary search) + total_indices = 0 + reps = [] + for sec in 'AB': + n_idx, cl = move_classes(w[sec]) + total_indices += n_idx + reps += [(sec, i, s, sec, q) for i, s, q in cl] + n_cross, cl = cross_classes(w) + reps += [(sec, i, s, 'B' if sec == 'A' else 'A', q) for sec, i, s, q in cl] + items = [reps[k:k + 32] for k in range(0, len(reps), 32)] + with Pool(jobs, initializer=_init, initargs=(path, z)) as pool: + results = [x for part in pool.imap(_job, items) for x in part] + P = Problem(dict(w, _z=z)) + base = P.optimum(base_ops['A'], base_ops['B']) + + def cost(h): + return sum(n * d * (64 / d) ** z for d, n in h.items()) + + outcome = Counter('illegal' if h is None else 'same' if h == base else + 'better' if cost(h) < cost(base) - 1e-9 else 'worse' for _, h in results) + # per (section, gate, source) multiset of outcomes, compared with the primary detail rows + mine = defaultdict(Counter) + for (sec, i, s, dst, q), h in results: + mine[(sec, i, s, dst)][None if h is None else tuple(sorted(h.items()))] += 1 + theirs = defaultdict(Counter) + for row in prim['detail']: + h = row['profile'] + theirs[(row['sec'], row['i'], row['s'], row['dst'])][None if h is None else + tuple(sorted((int(k), v) for k, v in h.items()))] += 1 + mismatches = sorted(str(k) for k in set(mine) | set(theirs) if mine.get(k) != theirs.get(k)) + print(json.dumps(dict(insertion_indices=total_indices, cross_scatter_indices=n_cross, classes=len(results), primary_candidates=len(prim['detail']), + base_profile=base, outcome=dict(outcome), mismatches_vs_primary=len(mismatches), + first_mismatches=mismatches[:5]))) + + +if __name__ == '__main__': + main() diff --git a/research/bit589-transport-reframe/pair_sample_check.py b/research/bit589-transport-reframe/pair_sample_check.py new file mode 100644 index 0000000000..0b9a09a3e8 --- /dev/null +++ b/research/bit589-transport-reframe/pair_sample_check.py @@ -0,0 +1,95 @@ +"""Seeded random cross-check of the depth-two optimum: primary (reframe.py) versus independent (independent_check.py). + +Draws legal first moves m1 and, for each, one interacting second move m2 from the primary generator (pairs.py's +class). Each pair is rebuilt twice, by search.apply and by independent_check.build (separate code, translated move +descriptions), and its exact optimal profile (or illegality) is computed by both implementations. This checks the +optimum on two-move words, not the pair enumeration (the generator is the depth-one generator, whose class count the +independent enumeration reproduces). + +Usage: pair_sample_check.py WORD.json.gz C N SEED [--jobs J] +Prepared with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0. +""" +import gzip +import json +import os +import random +import sys +from collections import Counter +from fractions import Fraction +from multiprocessing import Pool + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import independent_check as I +import reframe as R +import search as S +from pairs import View, moved_regs + + +def describe(cand): + """search.py move tuple -> independent_check.build description (section, i, source, destination, index)""" + if len(cand) == 6: + kind, sec, i, s, dst, q = cand + return (sec, i, s, dst, q) + kind, sec, i, s, p = cand + return (sec, i, s, sec, p) + + +_W = _P = _Z = None + + +def _init(path, z): + global _W, _P, _Z + _W = R.Word(R.load(path)) + w = json.load(gzip.open(path, 'rt')) + w['_z'] = z + _P = I.Problem(w) + _Z = z + + +def _job(pairs): + out = [] + for m1, m2 in pairs: + A1, B1 = S.apply(_W, m1) + A2, B2 = S.apply(View(_W, A1, B1), m2) + o = R.optimum(_W, A2, B2, _Z) + prim = None if o is None else o['profile'] + a1, b1 = I.build(_P.w, *describe(m1)) + w1 = dict(_P.w, A=[[0, t, list(ss)] for t, ss in a1], B=[[0, t, list(ss)] for t, ss in b1]) + a2, b2 = I.build(w1, *describe(m2)) + assert [(t, tuple(ss)) for f, t, ss in A2] == a2 and [(t, tuple(ss)) for f, t, ss in B2] == b2, (m1, m2) + ind = _P.optimum(a2, b2) + out.append((m1, m2, prim, ind)) + return out + + +def main(): + path, c, n, seed = sys.argv[1], Fraction(sys.argv[2]), int(sys.argv[3]), int(sys.argv[4]) + jobs = int(sys.argv[sys.argv.index('--jobs') + 1]) if '--jobs' in sys.argv else os.cpu_count() + z = float(c) + word = R.Word(R.load(path)) + rng = random.Random(seed) + firsts = S.candidates(word) + S.cross_candidates(word) + sample = [] + while len(sample) < n: + m1 = rng.choice(firsts) + A1, B1 = S.apply(word, m1) + if R.optimum(word, A1, B1, z) is None: + continue + w1 = View(word, A1, B1) + regs = moved_regs(word, m1) + seconds = S.candidates(w1, regs) + S.cross_candidates(w1, regs) + if seconds: + sample.append((m1, rng.choice(seconds))) + with Pool(jobs, initializer=_init, initargs=(path, z)) as pool: + rows = [x for part in pool.imap(_job, [sample[k:k + 16] for k in range(0, n, 16)]) for x in part] + base = R.optimum(word, word.A, word.B, z)['profile'] + agree = sum(p == q for _, _, p, q in rows) + kinds = Counter('illegal' if p is None else 'base' if p == base else 'other' for _, _, p, _ in rows) + print(json.dumps(dict(seed=seed, pairs=n, agree=agree, disagree=n - agree, primary_outcomes=dict(kinds), + first_disagreements=[[list(a), list(b), p, q] for a, b, p, q in rows if p != q][:3]))) + if agree != n: + sys.exit(1) + + +if __name__ == '__main__': + main() diff --git a/research/bit589-transport-reframe/pairs.py b/research/bit589-transport-reframe/pairs.py new file mode 100644 index 0000000000..388e5c00cf --- /dev/null +++ b/research/bit589-transport-reframe/pairs.py @@ -0,0 +1,116 @@ +"""Depth-two extension: every legal first relocation m1 (any class of search.py, including across the scatter), then +every relocation m2 of the resulting word whose source gate touches a register of m1's moved operands or of m1's +remainder gate, then the exact frame optimum. + +This is the interacting part of the two-move neighbourhood: m2 is enumerated on the word after m1 (its slots are those +of the changed order), so chains of the form "neutral move, then improving move" on a common register are covered. +Pairs whose moved operands share no register are outside this class. + +Usage: pairs.py WORD.json.gz C [--jobs N] [--out FILE] [--first JSON_LIST_OF_FIRST_MOVES] +Prepared with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0. +""" +import json +import os +import sys +import time +from collections import Counter +from fractions import Fraction +from multiprocessing import Pool + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import reframe as R +import search as S + + +class View: + """a Word with replaced phase-A/phase-B gate lists""" + + def __init__(self, word, A, B): + self.__dict__.update(word.__dict__) + self.A, self.B = A, B + + +def moved_regs(word, cand): + kind, sec, i, s = cand[:4] + f, t, ss = getattr(word, sec)[i] + own = {t, s} if kind in ('summand', 'xsummand') else {t, *ss} + return own | {t, *ss} # the moved operands and the remainder gate's operands + + +_W = _Z = None + + +def _init(path, z): + global _W, _Z + _W = R.Word(R.load(path)) + _Z = z + + +def _eval(m1s): + out = [] + for m1 in m1s: + A1, B1 = S.apply(_W, m1) + if R.optimum(_W, A1, B1, _Z) is None: + continue + w1 = View(_W, A1, B1) + regs = moved_regs(_W, m1) + n = legal = 0 + best = None + prof = Counter() + for m2 in S.candidates(w1, regs) + S.cross_candidates(w1, regs): + assert moved_regs(w1, m2) & regs + n += 1 + A2, B2 = S.apply(w1, m2) + o = R.optimum(_W, A2, B2, _Z) + if o is None: + continue + legal += 1 + key = tuple(sorted(o['profile'].items())) + prof[key] += 1 + if best is None or o['cost'] < best[0]: + best = (o['cost'], m2, o['profile']) + out.append((m1, n, legal, best, dict(prof))) + return out + + +def main(): + path = sys.argv[1] + c = Fraction(sys.argv[2]) + z = float(c) + jobs = int(sys.argv[sys.argv.index('--jobs') + 1]) if '--jobs' in sys.argv else os.cpu_count() + outp = sys.argv[sys.argv.index('--out') + 1] if '--out' in sys.argv else None + t0 = time.time() + word = R.Word(R.load(path)) + base = R.optimum(word, word.A, word.B, z) + cands = S.candidates(word) + S.cross_candidates(word) + if '--first' in sys.argv: # restrict the first moves (used by the positive control) + cands = [tuple(m) for m in json.loads(sys.argv[sys.argv.index('--first') + 1])] + batches = [cands[k:k + 16] for k in range(0, len(cands), 16)] + rows = [] + with Pool(jobs, initializer=_init, initargs=(path, z)) as pool: + for part in pool.imap(_eval, batches): + rows.extend(part) + pairs = sum(r[1] for r in rows) + legal = sum(r[2] for r in rows) + profiles = Counter() + for r in rows: + for k, n in r[4].items(): + profiles[k] += n + allbest = sorted((r[3][0] - base['cost'], r[0], r[3][1], r[3][2]) for r in rows if r[3] is not None) + report = dict( + word=os.path.basename(path), c=str(c), base_profile=base['profile'], base_cost=base['cost'], + first_candidates=len(cands), first_moves=len(rows), pairs=pairs, legal_pairs=legal, + improving_pairs=sum(1 for r in rows if r[3] is not None and r[3][0] - base['cost'] < -1e-9), + distinct_optimal_profiles=len(profiles), + pairs_with_base_profile=profiles.get(tuple(sorted(base['profile'].items())), 0), + best=[dict(delta=d, m1=list(a), m2=list(b), profile=p) for d, a, b, p in allbest[:10]], + profiles=[[dict(k), n] for k, n in sorted(profiles.items(), key=lambda x: (-x[1], x[0]))], + seconds=round(time.time() - t0, 1)) + js = json.dumps(report, indent=1, default=str) + if outp: + open(outp, 'w').write(js + '\n') + print(js) + + +if __name__ == '__main__': + main() diff --git a/research/bit589-transport-reframe/reframe.py b/research/bit589-transport-reframe/reframe.py new file mode 100644 index 0000000000..dea4aea4a5 --- /dev/null +++ b/research/bit589-transport-reframe/reframe.py @@ -0,0 +1,337 @@ +"""Exact frame optimum of a bitE8/1+mut word whose phase-A/phase-B gate order may have been changed. + +Model (the paid local profile of PR589's wlib.replay): every gate puts all of its operands on its frame; each register's +frames nest from its start to its final frame; each strict climb is one paid call of rank equal to the dimension step. +A retained total's COPY rank is the dimension of its frame when the scatter reads it; here that frame is pinned to the +base word's (so the COPY ranks and the decoder constant 63 cannot change), which pins the total's last phase-A gate to +exactly that frame. Targets stay at frame 0 until the scatter. + +D (all frame 0, before any climb) and C (the literal reverse of the z-destination gates at the full frame, H4) cannot +contribute a climb other than the last climb to the full final frame; `Word` asserts both facts and drops them. + +For a gate order the optimum over all frame assignments is computed exactly: + 1. forward least frames lo_g and backward greatest frames hi_g; every legal assignment has lo_g <= f_g <= hi_g, and + the all-least assignment itself nests (so components can be enumerated with the others at any legal value); + 2. gates with lo_g != hi_g ("free") interact only when consecutive on a register, so the components of that + relation are independent in legality and in cost; + 3. every component is enumerated exhaustively over all closed frames (catalogue or not) between its bounds. +The cost of a profile is sum_d n_d d (64/d)^z at the base word's c, which is linear in the profile; with the rank mass +fixed, a profile can raise c only if it lowers this sum (see README). Standard library only. +Prepared with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0. +""" +import gzip +import itertools +import json +from collections import Counter +from fractions import Fraction + + +def load(path): + return json.load(gzip.open(path, 'rt')) + + +class Lattice: + """closed frames: sets of live lines closed under rational span membership, as int masks; exact Fraction RREF""" + + def __init__(self, lines): + self.lines = [tuple(map(Fraction, l)) for l in lines] + self.n = len(lines) + self.cache = {0: (0, 0)} + + def _reduce(self, basis, row): + row = list(row) + for piv, b in basis: + if row[piv]: + q = row[piv] + row = [a - q * c for a, c in zip(row, b)] + return row + + def close(self, mask): + """(closed mask, dimension) of the span of the lines in mask""" + hit = self.cache.get(mask) + if hit is not None: + return hit + basis = [] + for i in range(self.n): + if mask >> i & 1: + row = self._reduce(basis, self.lines[i]) + piv = next((k for k, x in enumerate(row) if x), None) + if piv is not None: + row = [x / row[piv] for x in row] + basis = [(p, [a - b[piv] * c for a, c in zip(b, row)]) for p, b in basis] + [(piv, row)] + closed = 0 + for i in range(self.n): + if mask >> i & 1 or not any(self._reduce(basis, self.lines[i])): + closed |= 1 << i + out = (closed, len(basis)) + self.cache[mask] = out + self.cache[closed] = out + return out + + def dim(self, mask): + return self.close(mask)[1] + + +class Word: + """phase A, scatter and phase B of a word as (frame mask, target, sources) gates; D and C checked and dropped""" + + def __init__(self, w, lat=None): + self.w = w + self.V = V = w['v'] + self.N = 2 * V + w['R'] + self.lat = lat or Lattice(w['lines']) + self.fm = [sum(1 << i for i in f) for f in w['frames']] + for m in self.fm: + assert self.lat.close(m)[0] == m, 'catalogue frame not closed' + self.full = max(self.fm, key=self.lat.dim) + assert self.lat.dim(self.full) == 8 + self.start = [self.fm[f] for f in w['start']] + self.final = [self.fm[f] for f in w['final']] + # D: frame 0 and every operand still at frame 0 there, so D contributes no climb and no lower bound + for f, t, ss in w['D']: + assert self.fm[f] == 0 and all(self.start[r] == 0 for r in [t, *ss]) + # C: every gate at the full frame, every C operand ends at the full frame + incC = set() + for f, t, ss in w['C']: + assert self.fm[f] == self.full + incC.update([t, *ss]) + assert all(self.final[r] == self.full for r in incC) + self.ret = list(w['ret']) + A = [(self.fm[f], t, tuple(ss)) for f, t, ss in w['A']] + B = [(self.fm[f], t, tuple(ss)) for f, t, ss in w['B']] + cur = list(self.start) + for f, t, ss in A: + for r in (t, *ss): + cur[r] = f + self.pin = {q: cur[q] for q in self.ret} # COPY frames of the retained totals + self.A, self.B = A, B + self.targets = range(V, 2 * V) + assert not any(V <= r < 2 * V for f, t, ss in A for r in (t, *ss)), 'a target is touched in phase A' + + def base_frames(self): + return [g[0] for g in self.A] + [g[0] for g in self.B] + + +def cost_of(H, z): + return sum(n * d * (64 / d) ** z for d, n in H.items()) + + +def optimum(word, A, B, z, want_frames=False): + """exact optimum over all frame assignments of the gate order (A, B); A/B gates are (frame, t, sources), frames + ignored except for reporting. Returns None if no legal assignment exists, else a dict with the optimal profile + (climbs plus COPY ranks), its cost and statistics.""" + lat = word.lat + close = lat.close + gates = [(t, ss) for f, t, ss in A] + [(t, ss) for f, t, ss in B] + nA = len(A) + G = len(gates) + pin = word.pin + # the last phase-A gate on a retained total fixes its frame at the scatter, so in every legal assignment that + # gate sits exactly at the total's COPY frame; using this as its least frame keeps the all-least assignment legal + lastA = {} + for g in range(nA): + t, ss = gates[g] + for r in (t, *ss): + if r in pin: + lastA[r] = g + pinned = {} + for q, g in lastA.items(): + if pinned.setdefault(g, pin[q]) != pin[q]: + return None + # 1. forward least frames + lo = [0] * G + cur = list(word.start) + for g in range(G): + if g == nA: + for q, m in pin.items(): + if cur[q] != m: + return None + t, ss = gates[g] + m = cur[t] + for s in ss: + m |= cur[s] + m = close(m)[0] + if g in pinned: + if m & ~pinned[g]: + return None + m = pinned[g] + lo[g] = m + cur[t] = m + for s in ss: + cur[s] = m + if G == nA: + raise ValueError('empty phase B') + for r in range(word.N): + if cur[r] & ~word.final[r]: + return None + # backward greatest frames (an intersection of closed sets is closed) + hi = [0] * G + ub = list(word.final) + for g in range(G - 1, -1, -1): + t, ss = gates[g] + m = ub[t] + for s in ss: + m &= ub[s] + hi[g] = m + ub[t] = m + for s in ss: + ub[s] = m + if g == nA: + for q, m2 in pin.items(): + if m2 & ~ub[q]: + return None + ub[q] = m2 + for r in word.targets: + ub[r] = 0 + for g in range(G): + if lo[g] & ~hi[g]: + return None + for r in range(word.N): + if word.start[r] & ~ub[r]: + return None + # per-register gate lists + touch = [[] for _ in range(word.N)] + for g, (t, ss) in enumerate(gates): + touch[t].append(g) + for s in ss: + touch[s].append(g) + free = [g for g in range(G) if lo[g] != hi[g]] + frames = list(lo) + + def chain(r, fr): + """(Counter of climbs, legal) of register r under frames fr""" + c = word.start[r] + H = Counter() + crossed = r not in pin + for g in touch[r]: + if not crossed and g >= nA: + if c != pin[r]: + return None + crossed = True + m = fr[g] + if m != c: + if c & ~m: + return None + H[lat.dim(m) - lat.dim(c)] += 1 + c = m + if not crossed and c != pin[r]: + return None + m = word.final[r] + if m != c: + if c & ~m: + return None + H[lat.dim(m) - lat.dim(c)] += 1 + return H + + # 2. components of free gates (consecutive on a register) + parent = {g: g for g in free} + + def find(x): + while parent[x] != x: + parent[x] = parent[parent[x]] + x = parent[x] + return x + + fs = set(free) + for r in range(word.N): + prev = None + for g in touch[r]: + if g in fs and prev in fs: + a, b = find(prev), find(g) + if a != b: + parent[a] = b + prev = g + comps = {} + for g in free: + comps.setdefault(find(g), []).append(g) + # 3. exhaustive enumeration per component + enumerated = illegal = 0 + for members in comps.values(): + opts = [] + for g in members: + seen, todo = {lo[g]}, [lo[g]] + while todo: + m = todo.pop() + rest = hi[g] & ~m + while rest: + b = rest & -rest + rest ^= b + n = close(m | b)[0] + if n & ~hi[g] == 0 and n not in seen: + seen.add(n) + todo.append(n) + opts.append(sorted(seen)) + regs = sorted({r for g in members for r in (gates[g][0], *gates[g][1])}) + best = None + for combo in itertools.product(*opts): + fr = frames + saved = [fr[g] for g in members] + for g, m in zip(members, combo): + fr[g] = m + enumerated += 1 + H = Counter() + ok = True + for r in regs: + h = chain(r, fr) + if h is None: + ok = False + break + H.update(h) + if ok: + c = cost_of(H, z) + key = (c, combo) + if best is None or key < best: + best = key + else: + illegal += 1 + for g, m in zip(members, saved): + fr[g] = m + if best is None: + return None + for g, m in zip(members, best[1]): + frames[g] = m + # total profile under the optimal frames + H = Counter() + for r in range(word.N): + h = chain(r, frames) + if h is None: + return None + H.update(h) + for q in word.ret: + H[lat.dim(pin[q])] += 1 # COPY ranks + out = dict(profile=dict(sorted(H.items())), cost=cost_of(H, z), free=len(free), components=len(comps), + component_sizes=dict(Counter(len(v) for v in comps.values())), enumerated=enumerated, illegal=illegal, + mass=sum(d * n for d, n in H.items())) + if want_frames: + out['frames'] = frames + return out + + +def fixed_profile(word, A, B): + """paid profile of the given frames (no optimisation); None if they do not nest""" + lat = word.lat + gates = [(f, t, ss) for f, t, ss in A] + [(f, t, ss) for f, t, ss in B] + nA = len(A) + cur = list(word.start) + H = Counter() + for g, (f, t, ss) in enumerate(gates): + if g == nA: + for q, m in word.pin.items(): + if cur[q] != m: + return None + for r in (t, *ss): + c = cur[r] + if c != f: + if c & ~f: + return None + H[lat.dim(f) - lat.dim(c)] += 1 + cur[r] = f + for r in range(word.N): + c, m = cur[r], word.final[r] + if c != m: + if c & ~m: + return None + H[lat.dim(m) - lat.dim(c)] += 1 + for q in word.ret: + H[lat.dim(word.pin[q])] += 1 + return dict(sorted(H.items())) diff --git a/research/bit589-transport-reframe/search.py b/research/bit589-transport-reframe/search.py new file mode 100644 index 0000000000..2fec6b5420 --- /dev/null +++ b/research/bit589-transport-reframe/search.py @@ -0,0 +1,231 @@ +"""Exhaustive search: one commuting relocation of a phase-A or phase-B summand or gate of PR589's word, then the +exact frame optimum over all frame assignments. + +Move classes (D and C are never changed; C is the literal reverse of the z-destination gates and is accounted for +implicitly, see reframe.py): + summand take one source s out of a gate t += {..., s, ...} as its own gate t += s and insert it at any position of + the same section reachable by crossing only gates it commutes with (single-source gates: the whole gate + moves). The positions next to its own remainder are the in-place splits of a multi-source gate. + gate move a whole multi-source gate the same way. + xsummand, xgate the same moves continued across the scatter into the other section; allowed only when the moved + gate commutes with the scatter (it writes neither a target nor a retained total and reads no target), + which keeps H1-H5 syntactically (A writes only z registers, B z-gates write z from z). +Two XOR gates commute iff neither writes a register the other reads. A position matters only through the order of +the gates on the moved operands (and the section), so one representative per slot between consecutive gates that touch +the moved operands is evaluated; positions in one slot give identical register sequences and hence identical optima. + +Usage: search.py WORD.json.gz C_NUMERATOR/C_DENOMINATOR [--jobs N] [--out FILE] +Prepared with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0. +""" +import json +import os +import sys +import time +from fractions import Fraction +from multiprocessing import Pool + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import reframe as R + + +def commute(a, b): + return a[1] not in b[2] and b[1] not in a[2] + + +def touches(g, regs): + return g[1] in regs or any(s in regs for s in g[2]) + + +def slots(L2, o, p0): + """insertion indices into L2 for gate o, one per slot, starting from its legal original index p0""" + regs = {o[1], *o[2]} + out = [p0] + p = p0 + while p > 0 and commute(o, L2[p - 1]): + p -= 1 + if touches(L2[p], regs): + out.append(p) + p = p0 + while p < len(L2) and commute(o, L2[p]): + p += 1 + if touches(L2[p - 1], regs): + out.append(p) + return out + + +def candidates(word, regs=None): + """(kind, section, index, source or None, insertion index) for every relocation slot except the identity; + with regs, only moves out of gates that touch one of those registers""" + out = [] + for sec in 'AB': + L = getattr(word, sec) + for i, (f, t, ss) in enumerate(L): + if regs is not None and t not in regs and not any(x in regs for x in ss): + continue + for s in ss: + o = (f, t, (s,)) + if len(ss) > 1: + L2 = L[:i] + [(f, t, tuple(x for x in ss if x != s))] + L[i + 1:] + else: + L2 = L[:i] + L[i + 1:] + for p in slots(L2, o, i): + if len(ss) == 1 and p == i: + continue # identity + out.append(('summand', sec, i, s, p)) + if len(ss) > 1: + o = (f, t, ss) + L2 = L[:i] + L[i + 1:] + for p in slots(L2, o, i): + if p != i: + out.append(('gate', sec, i, None, p)) + return out + + +def crosses_scatter(word, o): + """o commutes with the scatter (targets ^= retained totals) and may sit in either phase under H3: it writes + neither a target nor a retained total, and reads no target""" + V = word.V + t, ss = o[1], o[2] + return not (V <= t < 2 * V) and t not in word.pin and not any(V <= s < 2 * V for s in ss) + + +def cross_candidates(word, regs=None): + """relocations that cross the scatter: (kind, section, index, source or None, destination section, index), + one per slot of the destination section reachable through commuting gates (the scatter counts as a boundary)""" + out = [] + for sec in 'AB': + L, M = (word.A, word.B) if sec == 'A' else (word.B, word.A) + for i, (f, t, ss) in enumerate(L): + if regs is not None and t not in regs and not any(x in regs for x in ss): + continue + variants = [('xsummand', s, (f, t, (s,)), + L[:i] + ([(f, t, tuple(x for x in ss if x != s))] if len(ss) > 1 else []) + L[i + 1:]) + for s in ss] + if len(ss) > 1: + variants.append(('xgate', None, (f, t, ss), L[:i] + L[i + 1:])) + for kind, s, o, L2 in variants: + if not crosses_scatter(word, o): + continue + regs_o = {o[1], *o[2]} + if sec == 'A': # walk forward to the end of A, then into B from its start + p = i + while p < len(L2) and commute(o, L2[p]): + p += 1 + if p < len(L2): + continue + q = 0 + out.append((kind, sec, i, s, 'B', q)) + while q < len(M) and commute(o, M[q]): + q += 1 + if touches(M[q - 1], regs_o): + out.append((kind, sec, i, s, 'B', q)) + else: # walk backward to the start of B, then into A from its end + p = i + while p > 0 and commute(o, L2[p - 1]): + p -= 1 + if p > 0: + continue + q = len(M) + out.append((kind, sec, i, s, 'A', q)) + while q > 0 and commute(o, M[q - 1]): + q -= 1 + if touches(M[q], regs_o): + out.append((kind, sec, i, s, 'A', q)) + return out + + +def apply(word, cand): + if cand[0] in ('xsummand', 'xgate'): + kind, sec, i, s, dst, q = cand + L, M = (word.A, word.B) if sec == 'A' else (word.B, word.A) + f, t, ss = L[i] + if kind == 'xsummand': + o = (f, t, (s,)) + L2 = L[:i] + ([(f, t, tuple(x for x in ss if x != s))] if len(ss) > 1 else []) + L[i + 1:] + else: + o = (f, t, ss) + L2 = L[:i] + L[i + 1:] + M2 = M[:q] + [o] + M[q:] + return (L2, M2) if sec == 'A' else (M2, L2) + kind, sec, i, s, p = cand + L = getattr(word, sec) + f, t, ss = L[i] + if kind == 'summand': + o = (f, t, (s,)) + L2 = L[:i] + ([(f, t, tuple(x for x in ss if x != s))] if len(ss) > 1 else []) + L[i + 1:] + else: + o = (f, t, ss) + L2 = L[:i] + L[i + 1:] + L2 = L2[:p] + [o] + L2[p:] + return (L2, word.B) if sec == 'A' else (word.A, L2) + + +_W = None + + +def _init(path, z): + global _W, _Z + _W = R.Word(R.load(path)) + _Z = z + + +def _eval(batch): + res = [] + for cand in batch: + A, B = apply(_W, cand) + o = R.optimum(_W, A, B, _Z) + res.append((cand, None if o is None else (o['cost'], o['profile'], o['free'], o['components'], + o['enumerated']))) + return res + + +def main(): + path = sys.argv[1] + c = Fraction(sys.argv[2]) + z = float(c) + jobs = int(sys.argv[sys.argv.index('--jobs') + 1]) if '--jobs' in sys.argv else os.cpu_count() + outp = sys.argv[sys.argv.index('--out') + 1] if '--out' in sys.argv else None + t0 = time.time() + word = R.Word(R.load(path)) + base = R.optimum(word, word.A, word.B, z) + assert base['profile'] == R.fixed_profile(word, word.A, word.B), 'base word is not frame-optimal in this model' + cands = candidates(word) + cross_candidates(word) + batches = [cands[k:k + 64] for k in range(0, len(cands), 64)] + results = [] + with Pool(jobs, initializer=_init, initargs=(path, z)) as pool: + for part in pool.imap(_eval, batches): + results.extend(part) + legal = [(cand, r) for cand, r in results if r is not None] + deltas = sorted(((r[0] - base['cost'], cand, r[1]) for cand, r in legal), key=lambda x: (x[0], x[1])) + improving = [d for d in deltas if d[0] < -1e-9] + same = [d for d in deltas if abs(d[0]) <= 1e-9] + kinds = {} + for cand, r in results: + k = (cand[0], cand[1]) + e = kinds.setdefault('%s/%s' % k, dict(candidates=0, legal=0, improving=0, same_cost=0)) + e['candidates'] += 1 + if r is not None: + e['legal'] += 1 + d = r[0] - base['cost'] + e['improving'] += d < -1e-9 + e['same_cost'] += abs(d) <= 1e-9 + report = dict( + word=os.path.basename(path), c=str(c), base_profile=base['profile'], base_cost=base['cost'], + base_free_gates=base['free'], base_components=base['components'], + candidates=len(cands), legal=len(legal), illegal=len(cands) - len(legal), + improving=len(improving), same_cost=len(same), by_kind=kinds, + best=[dict(delta=d, move=list(cand), profile=prof) for d, cand, prof in deltas[:20]], + smallest_nonzero_loss=min((d for d, _, _ in deltas if d > 1e-9), default=None), + seconds=round(time.time() - t0, 1)) + if '--detail' in sys.argv: + report['detail'] = [dict(kind=cand[0], sec=cand[1], i=cand[2], s=cand[3], + dst=cand[4] if len(cand) == 6 else cand[1], p=cand[-1], + profile=None if r is None else r[1]) for cand, r in results] + js = json.dumps(report, indent=1, default=str) + if outp: + open(outp, 'w').write(js + '\n') + print(js) + + +if __name__ == '__main__': + main() diff --git a/research/bit589-transport-reframe/steinberg.py b/research/bit589-transport-reframe/steinberg.py new file mode 100644 index 0000000000..5ca05f8a67 --- /dev/null +++ b/research/bit589-transport-reframe/steinberg.py @@ -0,0 +1,167 @@ +"""Exhaustive Steinberg 3 -> 2 rewrites (PR548's mechanism, re-run greedily by PR589's tuner) with exact reframing. + +Over F2, for single-source gates b: bt ^= bs and e reading or writing b's operands, + case 1 (e: et ^= bt reads b's target): b ; e = e ; b ; c with c: et ^= bs, + case 2 (e: bs ^= es writes b's source): b ; e = e ; b ; c with c: bt ^= es, +so when e can be brought next to b and c can be brought next to them through commuting gates (the conditions of +PR589's tune.find_triples), the three gates b, e, c are replaced by e ; b at b's place. Every rewritten word is checked +by an exact F2 replay of D, A, scatter, B and the rebuilt literal-reverse C on all columns, and then gets the exact +optimum over all frame assignments (reframe.optimum). Single-source gates within one phase only. + +Usage: steinberg.py WORD.json.gz C [--out FILE] [--independent] [--control] + --independent: recompute every optimum with independent_check.py's implementation and require agreement. + --control: expand PR589's phase A by one inverse rewrite (e ; b -> b ; e ; c on an adjacent pair, c relocated to its + farthest commuting slot; seeded choice); the triple search on it must recover W's phase A exactly. +Prepared with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0. +""" +import json +import os +import random +import sys +from collections import Counter, defaultdict +from fractions import Fraction + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import reframe as R +import search as S + + +def f2_ok(word, A, B): + """exact F2 endpoint of D, A, scatter, B, C (C = literal reverse of the z-destination gates of A then B)""" + w = word.w + V = word.V + N = word.N + val = [1 << i for i in range(N)] + for f, t, ss in w['D']: + for s in ss: + val[t] ^= val[s] + for f, t, ss in A: + for s in ss: + val[t] ^= val[s] + snap = [val[q] for q in w['ret']] + for t, ks in enumerate(w['scatter']): + for k in ks: + val[V + t] ^= snap[k] + for f, t, ss in B: + for s in ss: + val[t] ^= val[s] + for f, t, ss in reversed([g for g in A + B if g[1] < V or g[1] >= 2 * V]): + for s in ss: + val[t] ^= val[s] + return all(val[r] == ((1 << r) ^ (1 << (r - V)) if V <= r < 2 * V else 1 << r) for r in range(N)) + + +def triples(L): + single = [len(g[2]) == 1 for g in L] + pair, bysrc, bydst = defaultdict(list), defaultdict(list), defaultdict(list) + for k, (f, t, ss) in enumerate(L): + if single[k]: + pair[(t, ss[0])].append(k) + bysrc[ss[0]].append(k) + bydst[t].append(k) + out = [] + for pl, (fb, bt, bss) in enumerate(L): + if not single[pl]: + continue + bs = bss[0] + cands = [(1, pk, (L[pk][1], bs)) for pk in bysrc[bt] if pk > pl] + \ + [(2, pk, (bt, L[pk][2][0])) for pk in bydst[bs] if pk > pl] + for case, pk, cp in cands: + if not single[pk] or not all(S.commute(L[pk], L[j]) for j in range(pl + 1, pk)): + continue + for pq in pair.get(cp, []): + if len({pl, pk, pq}) < 3: + continue + lo, hi = min(pl, pq), max(pl, pq) + if all(S.commute(L[pq], L[j]) for j in range(lo, hi + 1) if j not in (pk, pl, pq)): + out.append((case, pl, pk, pq)) + return out + + +def rewrite(L, pl, pk, pq): + rest = [g for j, g in enumerate(L) if j not in (pl, pk, pq)] + q = pl - (pq < pl) + return rest[:q] + [L[pk], L[pl]] + rest[q:] + + +def search(word, z, indep=None): + """all rewrites of the word; with indep (an independent_check.Problem), every optimum is recomputed by the + independent implementation and must agree""" + base = R.optimum(word, word.A, word.B, z) + rows = [] + for sec in 'AB': + L = getattr(word, sec) + for case, pl, pk, pq in triples(L): + new = rewrite(L, pl, pk, pq) + A, B = (new, word.B) if sec == 'A' else (word.A, new) + assert f2_ok(word, A, B), ('rewrite changes the map', sec, pl, pk, pq) + o = R.optimum(word, A, B, z) + if indep is not None: + h = indep.optimum([(t, tuple(ss)) for f, t, ss in A], [(t, tuple(ss)) for f, t, ss in B]) + assert h == (None if o is None else o['profile']), ('implementations disagree', sec, pl, pk, pq) + rows.append(((sec, case, pl, pk, pq), None if o is None else o['profile'], + None if o is None else o['cost'] - base['cost'])) + return base, rows + + +def expand_control(word, seed=14): + """positive control for the triple finder and the rewrite. Under exact reframing every inverse expansion of this + word is neutral, so the control tests detection and exact recovery rather than a cost gain: one adjacent + single-source pair e ; b of phase A (case 1 in reverse: e: et ^= bt then b: bt ^= bs) becomes b ; e ; c with + c: et ^= bs, and c is then relocated through commuting gates to the farthest slot. The map must be unchanged, and + the 3 -> 2 search on the expanded word must list a triple whose rewrite gives back W's phase A exactly.""" + rng = random.Random(seed) + L = word.A + idx = [k for k in range(len(L) - 1) if len(L[k][2]) == 1 and len(L[k + 1][2]) == 1 + and L[k][2][0] == L[k + 1][1] and L[k][1] != L[k + 1][2][0] and L[k][1] != L[k + 1][1]] + rng.shuffle(idx) + for k in idx: + e, b = L[k], L[k + 1] + c = (e[0], e[1], (b[2][0],)) + stem = L[:k] + [b, e] + L[k + 2:] + far = max(S.slots(stem, c, k + 2), key=lambda p: abs(p - (k + 2))) + if far == k + 2: + continue + new = stem[:far] + [c] + stem[far:] + assert f2_ok(word, new, word.B), 'expansion changes the map' + return dict(pair_index=k, c_slot=far, moved_by=far - (k + 2)), new + raise SystemExit('no control expansion found') + + +def main(): + path, c = sys.argv[1], Fraction(sys.argv[2]) + z = float(c) + word = R.Word(R.load(path)) + report = {} + if '--control' in sys.argv: + info, new = expand_control(word) + tr = triples(new) + hits = [t for t in tr if rewrite(new, *t[1:]) == word.A] + o = R.optimum(word, rewrite(new, *hits[0][1:]), word.B, z) if hits else None + report = dict(info, triples_in_expanded_A=len(tr), recovering_triples=[list(t) for t in hits], + recovered_word_identical=bool(hits), + recovered_profile=None if o is None else {str(k): v for k, v in o['profile'].items()}) + else: + indep = None + if '--independent' in sys.argv: + import gzip + import independent_check as I + w = json.load(gzip.open(path, 'rt')) + w['_z'] = z + indep = I.Problem(w) + base, rows = search(word, z, indep) + out = Counter('illegal' if p is None else 'same' if p == base['profile'] else + 'better' if d < -1e-9 else 'worse' for _, p, d in rows) + report = dict(word=os.path.basename(path), c=str(c), triples=len(rows), + by_section_case=dict(Counter('%s/case%d' % (r[0][0], r[0][1]) for r in rows)), + f2_checked=len(rows), independent_agree=len(rows) if indep is not None else None, + outcome=dict(out), + profiles=[p for _, p, _ in rows if p is not None]) + js = json.dumps(report, default=str) + if '--out' in sys.argv: + open(sys.argv[sys.argv.index('--out') + 1], 'w').write(js + '\n') + print(js if '--control' in sys.argv else json.dumps({k: v for k, v in report.items() if k != 'profiles'})) + + +if __name__ == '__main__': + main() diff --git a/research/bit589-transport-reframe/verify.py b/research/bit589-transport-reframe/verify.py new file mode 100644 index 0000000000..f08a5227c6 --- /dev/null +++ b/research/bit589-transport-reframe/verify.py @@ -0,0 +1,164 @@ +"""One-command replay of the transport-and-reframe search on PR589's bit word (standard library only). + +Steps (each compared with EXPECTED.json): + 0. pins: SHA-256 of the two input words and the moment engine; + 1. depth one on PR589's word: every commuting relocation slot (within A, within B, across the scatter), exact frame + optimum, no improvement; + 2. positive control on PR555's word: the same search finds PR589's hoist and sink; + 3. independent re-implementation: same class count from every insertion index, identical outcome multisets; + 4. exact rational moment certification of every distinct depth-one profile; + 5. explicit-word control: PR555 + hoist + sink, rebuilt with optimal frames, replayed by PR589's wlib and accepted by + the unchanged xcheck_p.py interface audit, with PR589's exact local profile; + 6. negative controls: a non-commuting relocation changes the exact F2 map; a frame below its forced bound fails; + and a seeded sample of interacting pairs (seed 14) on which the primary and independent optima must agree; + 6b. Steinberg 3 -> 2 rewrites of PR589's word (PR548's mechanism): every rewrite F2-checked, exact optimum from + both implementations, none better; detection control on a word expanded by one inverse rewrite; + 7. (--pairs, about 35 min on 12 cores) the pair positive control on PR555's word (from the hoist, the best second + move is PR589's sink, reaching PR589's profile), then depth two over interacting pairs on PR589's word; every + distinct pair profile is certified exactly. +Usage: verify.py OUTDIR [--jobs N] [--pairs] +Prepared with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0. +""" +import gzip +import hashlib +import json +import os +import subprocess +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PY = [sys.executable, '-B'] +TUNED = ROOT / 'research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz' +BASE555 = ROOT / 'research/e8-bit-p111-tuned/data/bitE8mut-p111.json.gz' +MOMENT = ROOT / 'research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/moment.py' +XCHECK = ROOT / 'research/e8-bit-p111-tuned/code/xcheck_p.py' +C589 = '1733427039589844234749/1000000000000000000000000' +C555 = '1733052823330162099157/1000000000000000000000000' + + +def sha(p): + return hashlib.sha256(Path(p).read_bytes()).hexdigest() + + +def run(args, out=None): + r = subprocess.run(PY + [str(a) for a in args], capture_output=True, text=True, cwd=ROOT) + if r.returncode: + sys.stderr.write(r.stdout[-4000:] + r.stderr[-4000:]) + raise SystemExit('FAIL: ' + ' '.join(map(str, args))) + return r.stdout + + +def check(name, got, want): + if got != want: + raise SystemExit('FAIL %s: got %r expected %r' % (name, got, want)) + print('ok', name) + + +def f2_replay(w, A, B): + """exact F2 map of D, A, scatter, B, C on symbolic columns (frames ignored); True iff the word's endpoint holds""" + V = w['v'] + N = 2 * V + w['R'] + val = [1 << i for i in range(N)] + for f, t, ss in w['D'] + A: + for s in ss: + val[t] ^= val[s] + snap = [val[q] for q in w['ret']] + for t, ks in enumerate(w['scatter']): + for k in ks: + val[V + t] ^= snap[k] + full = max(range(len(w['frames'])), key=lambda f: len(w['frames'][f])) + C = [[full, t, ss] for f, t, ss in reversed([g for g in A + B if g[1] < V or g[1] >= 2 * V])] + for f, t, ss in B + C: + for s in ss: + val[t] ^= val[s] + return all(val[r] == ((1 << r) ^ (1 << (r - V)) if V <= r < 2 * V else 1 << r) for r in range(N)) + + +def negative_controls(): + sys.path.insert(0, str(HERE)) + import reframe as R + w = json.load(gzip.open(TUNED, 'rt')) + assert f2_replay(w, w['A'], w['B']) + # (a) relocate an op across an adjacent gate that reads its destination (not commuting) + A = w['A'] + k = next(k for k in range(1, len(A)) if len(A[k][2]) == 1 and A[k][1] in A[k - 1][2]) + bad = A[:k - 1] + [A[k], A[k - 1]] + A[k + 1:] + commuting_ok = f2_replay(w, bad, w['B']) + # (b) lower one forced (lo = hi) gate frame below its bound: nesting must fail + word = R.Word(R.load(str(TUNED))) + gates = list(word.A) + j = next(j for j, (f, t, ss) in enumerate(gates) if R.Lattice.dim(word.lat, f) >= 2 and len(ss) == 1) + f, t, ss = gates[j] + lower = word.lat.close(f & -f)[0] # a rank-one subframe + gates[j] = (lower, t, ss) + nesting = R.fixed_profile(word, gates, word.B) + return dict(noncommuting_index=k, noncommuting_endpoint_holds=commuting_ok, + lowered_gate=j, lowered_profile_legal=nesting is not None) + + +def main(): + out = Path(sys.argv[1]).resolve() + out.mkdir(parents=True, exist_ok=True) + jobs = sys.argv[sys.argv.index('--jobs') + 1] if '--jobs' in sys.argv else str(os.cpu_count()) + E = json.load(open(HERE / 'EXPECTED.json')) + check('pins', dict(tuned=sha(TUNED), base555=sha(BASE555), moment=sha(MOMENT), xcheck=sha(XCHECK)), E['pins']) + + run([HERE / 'search.py', TUNED, C589, '--jobs', jobs, '--detail', '--out', out / 'depth1.json']) + d1 = json.load(open(out / 'depth1.json')) + check('depth one', {k: d1[k] for k in E['depth1']}, E['depth1']) + + run([HERE / 'search.py', BASE555, C555, '--jobs', jobs, '--out', out / 'control555.json']) + c5 = json.load(open(out / 'control555.json')) + check('positive control', dict(improving=c5['improving'], + top=[[b['move'], b['profile']] for b in c5['best'][:c5['improving']]]), + E['control555']) + + ind = json.loads(run([HERE / 'independent_check.py', TUNED, out / 'depth1.json', '--jobs', jobs])) + check('independent implementation', ind, E['independent']) + + json.dump([r['profile'] for r in d1['detail'] if r['profile'] is not None], open(out / 'depth1-profiles.json', 'w')) + cert = json.loads(run([HERE / 'certify.py', out / 'depth1-profiles.json'])) + check('exact certification (depth one)', cert, E['certify_depth1']) + + ex = json.loads(run([HERE / 'export.py', BASE555, C555, out / 'control-hoist-sink.json.gz', + json.dumps(E['explicit_control']['moves'])])) + check('explicit control profile', ex['profile'], E['explicit_control']['profile']) + xc = run([XCHECK, out / 'control-hoist-sink.json.gz']) + check('explicit control xcheck_p', xc.strip().splitlines()[-1], E['explicit_control']['xcheck_last_line']) + + check('negative controls', negative_controls(), E['negative_controls']) + + st = json.loads(run([HERE / 'steinberg.py', TUNED, C589, '--independent'])) + check('Steinberg 3->2 rewrites', st, E['steinberg']) + sc = json.loads(run([HERE / 'steinberg.py', TUNED, C589, '--control'])) + check('Steinberg detection control', sc, E['steinberg_control']) + + ps = E['pair_sample'] + sample = json.loads(run([HERE / 'pair_sample_check.py', TUNED, C589, str(ps['pairs']), str(ps['seed']), + '--jobs', jobs])) + check('seeded pair cross-check', sample, ps) + + if '--pairs' in sys.argv: + pc = E['pair_control555'] + run([HERE / 'pairs.py', BASE555, C555, '--jobs', '1', '--first', json.dumps(pc['first']), + '--out', out / 'pair-control555.json']) + q = json.load(open(out / 'pair-control555.json')) + check('pair positive control', dict(improving_pairs=q['improving_pairs'], best_m2=q['best'][0]['m2'], + best_profile=q['best'][0]['profile']), + {k: pc[k] for k in ('improving_pairs', 'best_m2', 'best_profile')}) + run([HERE / 'pairs.py', TUNED, C589, '--jobs', jobs, '--out', out / 'pairs.json']) + p = json.load(open(out / 'pairs.json')) + check('depth two', {k: p[k] for k in E['depth2']}, E['depth2']) + json.dump([pr for pr, n in p['profiles']], open(out / 'pair-profiles.json', 'w')) + cert2 = json.loads(run([HERE / 'certify.py', out / 'pair-profiles.json'])) + check('exact certification (depth two)', cert2, E['certify_depth2']) + print('PASS_BIT589_TRANSPORT_REFRAME classes=%d legal=%d improving=0 control_rediscovered=2 ' + 'independent_mismatches=0 certified=%d steinberg=%d pair_sample_agree=%d%s no_new_kappa' % ( + d1['candidates'], d1['legal'], cert['certified_below'], st['triples'], sample['agree'], + ' pairs=%d' % E['depth2']['legal_pairs'] if '--pairs' in sys.argv else '')) + + +if __name__ == '__main__': + main()