Tooling: exact helper-donor cold-kernel search — rediscovers #1297's kernels, census on #1305/#1324 words (no new kappa)

research/helper-donor-kernel-search/README.md

@@ -0,0 +1,86 @@
+# Exact helper-donor cold-kernel search
+
+**No new κ.** This is a reusable search tool for the helper-donor cold-kernel mechanism, plus an exhaustive
+census of that mechanism on the current frontier words.
+
+The mechanism was introduced in #1274 for pivot 531 and extended in #1286/#1297 to pivots 543, 555 and 567.
+It is the largest local gain of the X54 line: H1 −3, H3 +1 per call per kernel, about +2.6·10⁻⁷ in κ each.
+#1297 describes an "exact backward output-sensitivity relation search", but no search tool has been published.
+`search.py` is such a tool. It is standard-library code on top of #1186's exact pricer.
+
+## What it does
+
+`search.py` takes every register p and every write gate `p += k·Y` that has earlier reads of p. For each one:
+1. It deletes a nonempty subset of those early reads.
+2. It cancels p inside the write: it inserts `Y −= p/k` at a cut, and restores it with an early-cleanup tail
+   gate. Every tail position next to a tail gate touching Y or p is tried.
+3. It computes the exact change D of the whole program map, mod 2³¹−19.
+4. It looks up one donor hook whose unit injection vector satisfies `q·v = −D` for a dyadic q. A donor hook is
+   `X += p` before a gate reading X, and `X −= p` right after.
+5. It prices each surviving candidate exactly with #1186's frame solver.
+
+## Results
+
+- **Positive control:** on #1218's base word, which has no kernel yet, the search **rediscovers #1297's pivot-555
+  kernel exactly**:
+  - delete reads 466, 502 and 734;
+  - donor 620 with coefficient 2 at hook 112;
+  - cost delta −11,676, profile `{1:2355, 2:504, 3:411, 4:130, 5:82}`.
+
+  It also finds the equivalent alternative donors 585, 616, 617 and 618, matching the five alternative hooks
+  #1297 reports.
+- **Census on #1305's final words** (base and extra, the four kernels already applied). The same words are used
+  unchanged by #1324, the current best claim, κ = 0.001677380107853623:
+  - every register and every write was searched, 1,048 write instances per word;
+  - **no further single-donor kernel exists** in this family;
+  - the four pivots 531/543/555/567 were the only ones available.
+- **Negative control:** pivot 555 on the already-kernelled word yields no gain.
+
+This tells others where not to look: further local gains on these words need relations with two or more donors,
+a different cancel form, or changed interfaces.
+
+## Reproduce
+
+```sh
+# Needs research/exact-frame-toolkit from PR #1186 (head 9254a3cc) and NumPy.
+python3 -B research/helper-donor-kernel-search/verify.py --toolkit PR1186/research/exact-frame-toolkit   # ~1 min
+SHARD=0 NSH=1 python3 -B research/helper-donor-kernel-search/search.py WORD.json.gz TOOLKIT all            # new word
+```
+
+`verify.py` does the following:
+- checks the input pins;
+- reruns the positive and negative controls;
+- checks that the recorded sweep logs (`evidence/`) cover every write and contain no gain.
+
+The inputs are vendored byte-for-byte:
+
+| Input | Source |
+|---|---|
+| `K4-BASE-WORD`, `K4-EXTRA-WORD` | #1305 at `a96a5d95` (`gauge44-word`, `extra-word`), identical to #1297/#1324 |
+| `PR1218-BASE-WORD` | #1218 at `0aa14797` |
+
+## Scope
+
+- This is a finite search over the stated family. A failed search is not an impossibility theorem.
+- A candidate found by the tool is nomination data only. It still needs native replay, the leaver premise and
+  strict owner admission.
+- All inherited conditions of the incumbent remain conditions here: all-size compiler, common-label and
+  mutable-source realization, whole-call hosting, precision and tape, exact recovery, analytic transfer, and
+  bit H1–H5.
+
+## Open next questions
+
+1. **Are there two-donor relations?** *Why:* they are the natural next family once single-donor kernels are
+   exhausted. *First step:* hash the pairwise sums of the normalized injection vectors restricted to the support
+   of D. *Blocked by:* the quadratic number of hook pairs, about 7·10⁵ per write, so a sparse-support filter is
+   needed.
+2. **Do other cancel forms work?** Examples are cancel through a helper other than the write source, or a
+   restore placed in B. *First step:* add these to the cut and restore options of `search.py`. *Blocked by:*
+   none.
+
+## Credit
+
+The mechanism is Jeremy Kothe's #1274 and Rohan Arun's #1286/#1297. The pricer and frame solver are #1186, by
+Marius-Paul Dumitrean, with the lineage it credits. The words come from #1305/#1324 (jeremykothe2), #1218/#1193
+and their ancestry. Prepared by Wronskode with substantial AI assistance (Anthropic Claude, via Claude Code).
+Apache-2.0.

research/helper-donor-kernel-search/search.py

@@ -0,0 +1,85 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Exact helper-donor cold-kernel search (the #1274/#1286/#1297 mechanism) for gauge44/k8 local words.
+
+For every register p and every write gate `p += k*Y` with earlier reads of p:
+  * delete a nonempty subset of those early reads;
+  * cancel p inside the write by `Y -= p/k` at a cut (after a read of Y, or at the write) and restore it with an
+    early-cleanup tail gate `Y += p/k` at every position adjacent to a tail gate touching Y or p;
+  * compute the exact change D of the whole program map mod 2^31-19;
+  * compare D with the unit injection vector of every donor hook `X += p; <gate j reading X>; X -= p`, normalized,
+    so that one hook with a dyadic coefficient q in {+-1,+-2,+-1/2,+-4} restores the map exactly (single-donor
+    relation sum q*col = -D);
+  * price each surviving candidate with #1186's exact frame solver (harness.Pricer: exactness mod p, cone caps,
+    optimal frames). A negative delta is a profile gain.
+
+usage: SHARD=i NSH=n python -B search.py WORD.json.gz TOOLKIT_DIR all|p1,p2,...
+TOOLKIT_DIR = research/exact-frame-toolkit from PR #1186 (head 9254a3cc). Output is nomination data only;
+a gain still needs native replay and strict owner admission. Wronskode, with Claude (Anthropic) assistance."""
+import sys, itertools, time
+from fractions import Fraction as Q
+sys.path.insert(0, sys.argv[2])
+import harness as C
+PR=C.PR
+path=sys.argv[1]; pivots=sorted({e[1] for e in __import__('harness').load(path)['B']}) if sys.argv[3]=='all' else [int(x) for x in sys.argv[3].split(',')]
+P=C.Pricer(path); w=P.base; B=w['B']
+base_rows=C.seg_rows(dict(w,_npre=0))
+def diff(ed):
+    w1=C.compile_edits(w,ed); r1=C.seg_rows(dict(w1,_npre=len(ed.get('prepend',[]))))
+    out={}
+    for q in set(base_rows)|set(r1):
+        a=base_rows.get(q,{q:1}); b=r1.get(q,{q:1})
+        for k in set(a)|set(b):
+            d=(b.get(k,0)-a.get(k,0))%PR
+            if d: out[(q,k)]=d
+    return out
+def E0(): return dict(delete=[],insert=[],tail=[],prepend=[])
+inv=lambda x: pow(x,PR-2,PR)
+QS=[Q(1),Q(-1),Q(2),Q(-2),Q(1,2),Q(-1,2),Q(4),Q(-4)]
+import os
+SH=int(os.environ.get('SHARD','0'));NS=int(os.environ.get('NSH','1'))
+for p in pivots[SH::NS]:
+  for wi,we in enumerate(B):
+    if not(we[0]=='add' and we[1]==p): continue
+    Y=we[2]; k=Q(we[3],we[4])
+    early=[(i,e[1],Q(e[3],e[4])) for i,e in enumerate(B) if e[0]=='add' and e[2]==p and i<wi]
+    if not early: continue
+    pw=[i for i,e in enumerate(B) if e[1]==p and i<wi]; lo=max(pw)+1 if pw else 0  # p constant on [lo, wi)
+    yr=[i for i,e in enumerate(B) if i<wi and e[0]=='add' and e[2]==Y and i>=lo]
+    t0=time.time()
+    # unit injection vectors: insert ('add',X,p,1) at j and ('add',X,p,-1) at j+1 around a read of X (gate j: t' += d X), lo<=j<wi
+    hooks=[]
+    for j in range(lo,wi):
+        e=B[j]
+        if e[0]=='add' and e[2]!=p and e[1]!=p:
+            X=e[2]
+            ed=dict(E0(),insert=[(j,['add',X,p,1,1,[]]),(j+1,['add',X,p,-1,1,[]])])
+            v=diff(ed)
+            if v: hooks.append((j,X,v))
+    print('pivot',p,'write',wi,'Y',Y,'early',[(i,t,str(c)) for i,t,c in early],'hooks',len(hooks),'%.0fs'%(time.time()-t0),flush=True)
+    def key(v):
+        # normalize vector to a hashable with first nonzero scaled to 1
+        it=sorted(v.items()); s=inv(it[0][1]); return tuple((a,b*s%PR) for a,b in it), it[0][1]
+    hk={}
+    for j,X,v in hooks:
+        kk,lead=key(v); hk.setdefault(kk,[]).append((j,X,lead))
+    T=[w['cleanup'][i] for i,U in w['early_cleanup']]
+    tpos=sorted({0,len(T)}|{j for j,g in enumerate(T) if Y in g[1:3] or p in g[1:3]}|{j+1 for j,g in enumerate(T) if Y in g[1:3] or p in g[1:3]})
+    for cut in sorted(set([x+1 for x in yr]+[wi])):
+     for tp in tpos:
+      for dsub in itertools.chain.from_iterable(itertools.combinations(early,r) for r in range(1,len(early)+1)):
+        ed=dict(E0(),delete=[i for i,_,_ in dsub],insert=[(cut,['add',Y,p,-(1/k).numerator,(1/k).denominator,[]])],tail=[(tp,['add',Y,p,(1/k).numerator,(1/k).denominator,[]])])
+        D=diff(ed)
+        if not D: cands=[[]]
+        else:
+            negD={a:(-b)%PR for a,b in D.items()}
+            kk,lead=key(negD); cands=[]
+            for (j,X,l) in hk.get(kk,[]):
+                q=lead*inv(l)%PR
+                for qq in QS:
+                    if (qq.numerator*inv(qq.denominator%PR))%PR==q: cands.append([(j,X,qq)])
+        for cc in cands:
+            e2=dict(ed,insert=list(ed['insert']))
+            for j,X,qq in cc: e2['insert']+= [(j,['add',X,p,qq.numerator,qq.denominator,[]]),(j+1,['add',X,p,-qq.numerator,qq.denominator,[]])]
+            r=P.price(e2,timeout=90)
+            print('  cand cut',cut,'tail',tp,'del',[i for i,_,_ in dsub],'donor',[(j,X,str(qq)) for j,X,qq in cc],r.get('status'),r.get('delta'),r.get('profile'),flush=True)

research/helper-donor-kernel-search/verify.py

@@ -0,0 +1,40 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Positive control, negative control and sweep-log tally for search.py.
+
+usage: python -B verify.py --toolkit PR1186/research/exact-frame-toolkit
+  1. pins of the vendored words;
+  2. positive control: on #1218's base word (pre-kernel), pivot 555 must rediscover #1297's kernel:
+     delete reads 466/502/734, donor 620 coefficient 2 at hook 112, cost delta -11676, profile H1 -3, H3 +1;
+  3. negative control: on #1305's final base word (kernel already applied), pivot 555 yields no gain;
+  4. the recorded all-register sweeps of #1305's two words contain no gain and cover every write.
+"""
+import argparse, hashlib, os, re, subprocess, sys
+from pathlib import Path
+PKG = Path(__file__).resolve().parent
+PINS = {'inputs/K4-BASE-WORD.json.gz': 'e8e6e78ff7422275c38324499e1f33fb2ecd30de9503aef2b8f1ee80d8c4df8e',
+        'inputs/K4-EXTRA-WORD.json.gz': '7b0e9fbda32749aabc7e156d9fe09bceb0624a178628fe69e5dfea783462f905',
+        'inputs/PR1218-BASE-WORD.json.gz': '4e837da23d932fc1336ef84dd1a802b46dbcb43bcf783b1338eeb7fa260eca1e'}
+def run(word, tk, piv):
+    r = subprocess.run([sys.executable, '-B', str(PKG / 'search.py'), str(PKG / word), str(tk), piv], cwd=tk,
+                       capture_output=True, text=True, env=dict(os.environ, SHARD='0', NSH='1'), timeout=1200)
+    assert r.returncode == 0, r.stderr[-2000:]
+    return r.stdout
+def main():
+    ap = argparse.ArgumentParser(); ap.add_argument('--toolkit', type=Path, required=True); a = ap.parse_args()
+    for rel, h in PINS.items():
+        assert hashlib.sha256((PKG / rel).read_bytes()).hexdigest() == h, rel
+    out = run('inputs/PR1218-BASE-WORD.json.gz', a.toolkit.resolve(), '555')
+    hit = [l for l in out.splitlines() if "del [466, 502, 734] donor [(112, 620, '2')] ok -11676" in l]
+    assert hit and '{1: 2355, 2: 504, 3: 411, 4: 130, 5: 82}' in hit[0], 'positive control'
+    out = run('inputs/K4-BASE-WORD.json.gz', a.toolkit.resolve(), '555')
+    assert not re.search(r' ok -\d', out), 'negative control'
+    for name in ('SWEEP-K4-BASE.log', 'SWEEP-K4-EXTRA.log'):
+        log = (PKG / 'evidence' / name).read_text()
+        assert 'Traceback' not in log and not re.search(r' ok -\d', log), name
+        n = sum(1 for l in log.splitlines() if l.startswith('pivot'))
+        assert n >= 1000, (name, n)
+        print(name, 'write instances', n, 'gains 0')
+    print('PASS_HELPER_DONOR_KERNEL_SEARCH_CONTROLS')
+if __name__ == '__main__':
+    main()