diff --git a/research/helper-donor-kernel-search/README.md b/research/helper-donor-kernel-search/README.md new file mode 100644 index 0000000000..a11e14d976 --- /dev/null +++ b/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. diff --git a/research/helper-donor-kernel-search/inputs/K4-BASE-WORD.json.gz b/research/helper-donor-kernel-search/inputs/K4-BASE-WORD.json.gz new file mode 100644 index 0000000000..eacf8c773c Binary files /dev/null and b/research/helper-donor-kernel-search/inputs/K4-BASE-WORD.json.gz differ diff --git a/research/helper-donor-kernel-search/inputs/K4-EXTRA-WORD.json.gz b/research/helper-donor-kernel-search/inputs/K4-EXTRA-WORD.json.gz new file mode 100644 index 0000000000..4d464f55a2 Binary files /dev/null and b/research/helper-donor-kernel-search/inputs/K4-EXTRA-WORD.json.gz differ diff --git a/research/helper-donor-kernel-search/inputs/PR1218-BASE-WORD.json.gz b/research/helper-donor-kernel-search/inputs/PR1218-BASE-WORD.json.gz new file mode 100644 index 0000000000..ba44a29122 Binary files /dev/null and b/research/helper-donor-kernel-search/inputs/PR1218-BASE-WORD.json.gz differ diff --git a/research/helper-donor-kernel-search/search.py b/research/helper-donor-kernel-search/search.py new file mode 100644 index 0000000000..1db09fc95c --- /dev/null +++ b/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; ; 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=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= 1000, (name, n) + print(name, 'write instances', n, 'gains 0') + print('PASS_HELPER_DONOR_KERNEL_SEARCH_CONTROLS') +if __name__ == '__main__': + main()