diff --git a/research/p104-free-cohort-split/DISCOVERY.json b/research/p104-free-cohort-split/DISCOVERY.json new file mode 100644 index 0000000000..ea770b5739 --- /dev/null +++ b/research/p104-free-cohort-split/DISCOVERY.json @@ -0,0 +1,37 @@ +{ + "source_head": "e59520bb11b0df5ac33f062f55397d78a491e7af", + "source_canonical_sha256": "3454c4900245ed1814ceeff79a741a45160eb3a93cf8d15f891fe2a67ba036fc", + "domain": "All currently contact-free paths individually preserving the exact nonzero paid-rank Counter; helper boundary(3,127); no cardinality limit. Rational prefix and suffix basis-vector pairings with retained smooth alphabet nominations.", + "windows": 10537, + "prefix_systems": 23070, + "saved_states": 3789, + "nonzero_pairings": 1, + "nominations": 1, + "used_roles": [ + 1463, + 1243, + 509 + ], + "source_cut": 37929, + "chart": 734, + "command": "python3 -B discover.py /tmp/source7112.json.gz /tmp/hits.json 3 127", + "limitations": [ + "Finite nominations, not global optimality or exhaustive alphabet/basis exclusion.", + "The verifier trusts the explicit witness only after whole-word checks; floating scores in search do not establish the claim." + ], + "prior_rounds": "Earlier at-most-two-retiming, neutral A2, owned reconstruction, and component/cleanup rounds are preserved locally and publicly labelled local-only; their scripts/results are not this package evidence.", + "overlap": { + "open_prs_fetched": "2026-11-10T17:00:01.314420+00:00", + "open_prs": 414, + "discussions_fetched": "2026-11-10T17:01:16.267941+00:00", + "discussions": 7021, + "complete_pagination": true, + "local_notes": 10178, + "query": [ + "coordinated helper retiming", + "zero-cost cohort", + "neutral retiming" + ], + "caveat": "No text matches is not proof of novelty; #7113 and #7114 heads read live." + } +} diff --git a/research/p104-free-cohort-split/ENVIRONMENT.json b/research/p104-free-cohort-split/ENVIRONMENT.json new file mode 100644 index 0000000000..9f00540816 --- /dev/null +++ b/research/p104-free-cohort-split/ENVIRONMENT.json @@ -0,0 +1,14 @@ +{ + "initial_python": "3.14.7", + "initial_platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "registered_replay": { + "python": "3.12.16", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "result": "PASS, exact frozen receipt" + }, + "dependencies": "Python standard library", + "interpreter_origin": "Official Astral python-build-standalone release20261026; isolated /tmp installation", + "interpreter_archive_sha256": "fbf4afef53c2a6b72bb741bc06d5671a9dfaf87bd84e5aa73ac9b3d0d589f14e", + "hosted_ci": "Not yet run; canonical base has known current-CI-navigation planning failure before scientific replay.", + "completed_utc": "2026-11-10T17:11:54.939971+00:00" +} diff --git a/research/p104-free-cohort-split/INPUTS.json b/research/p104-free-cohort-split/INPUTS.json new file mode 100644 index 0000000000..bdf9177a1e --- /dev/null +++ b/research/p104-free-cohort-split/INPUTS.json @@ -0,0 +1,141 @@ +{ + "source_head": "e59520bb11b0df5ac33f062f55397d78a491e7af", + "source_pr": 7112, + "archive_sha256": "00e2659f1725a3f1824e3d80bf1bfcba29202a7d5e6d303fb2ff7f8304e95a9a", + "source_canonical_sha256": "3454c4900245ed1814ceeff79a741a45160eb3a93cf8d15f891fe2a67ba036fc", + "files": [ + { + "path": "research/p104-smooth-swap-split/DISCOVERY.json", + "mode": "100644", + "git_blob": "fe67a5dbb7b0ff55ec201eee5db16a86d1a98c10", + "size": 872, + "sha256": "4a544b21a210af3e3b2ce248ebea58d4d4851bc8a84d474feddca6895c292270" + }, + { + "path": "research/p104-smooth-swap-split/ENVIRONMENT.json", + "mode": "100644", + "git_blob": "0d7dff9cd479ccf06d966f10a7d89a512aed8d13", + "size": 408, + "sha256": "2860fca96aa0434c503be638f7db9f0474577f29271313d05159ccfdb60ff62e" + }, + { + "path": "research/p104-smooth-swap-split/INPUTS.json", + "mode": "100644", + "git_blob": "22243b7749bc81f70b21f9fb1a6b2ed60c1b3768", + "size": 2147, + "sha256": "ecf2d1cdfd0a095fe391a00198fd2aac707d613ef8fee8bb3289146ec0f95ca8" + }, + { + "path": "research/p104-smooth-swap-split/README.md", + "mode": "100644", + "git_blob": "a4b45d077c0debc54659296ffbfef5d1e1472b78", + "size": 9291, + "sha256": "d71258b6b9587d64d97485a903a83fd3fa3a16e996894b7f01be2abc30a7667d" + }, + { + "path": "research/p104-smooth-swap-split/REPLAY.txt", + "mode": "100644", + "git_blob": "fe270e54f395015e40e177c795b2bf5024014772", + "size": 1237, + "sha256": "18e20cd5002ec58dbe54b14c91c6907ea2cad4a4c2de42a76da8fc18fa05bc3c" + }, + { + "path": "research/p104-smooth-swap-split/RESULT.json", + "mode": "100644", + "git_blob": "6d984a86455bcbd77bcee9d2922ac7d713b15284", + "size": 73115, + "sha256": "7b808ff32d9803084aaaf820cd172ddc9001c7aebbd17e0324e779abeff91b30" + }, + { + "path": "research/p104-smooth-swap-split/SOURCES.json", + "mode": "100644", + "git_blob": "c4150ae39789502a4adf89e8f5235995d458a72e", + "size": 856, + "sha256": "8b58a30ae55396b8d108de4ee2c7c6ac75dc1096948c9ac3796c20b21b1c9372" + }, + { + "path": "research/p104-smooth-swap-split/TASK.json", + "mode": "100644", + "git_blob": "924cd11aa76899764d8ddd0fcce06bf020db0672", + "size": 10462, + "sha256": "2a168ac27695bd06326a56904cbb06566311126816c2e3d3687c9b59eee76b87" + }, + { + "path": "research/p104-smooth-swap-split/VALIDATION.md", + "mode": "100644", + "git_blob": "94c6b092d27fd099fcdfacc416d7d69e0e1eca24", + "size": 1528, + "sha256": "99e51e4f98b5667be452db9c472189468e4f6e421077507789271838ef4ce018" + }, + { + "path": "research/p104-smooth-swap-split/VERIFY.json", + "mode": "100644", + "git_blob": "f1330ca857a907ebbed0ec2bfffa277a07a223d2", + "size": 664, + "sha256": "5d726a2ab788428741b57356f29c68435b49bf607c271b45b8d6d607efd99c7a" + }, + { + "path": "research/p104-smooth-swap-split/WITNESS.json", + "mode": "100644", + "git_blob": "3e9f2081de7cec8292493a6ab46e933c015d4771", + "size": 9943, + "sha256": "1f032109f14f975e2294dc33cde421ae949e2c1764f5b93fbee1027b1998a7aa" + }, + { + "path": "research/p104-smooth-swap-split/WORD.json.gz", + "mode": "100644", + "git_blob": "856952b2aabfef84bf2c1fe37320f4b6d6bc4491", + "size": 355352, + "sha256": "fe0b1dc3049a6b72760a705af2e698e0e9998e969e19862a696eba63434eb233" + }, + { + "path": "research/p104-smooth-swap-split/construct.py", + "mode": "100644", + "git_blob": "502faa905eeac1dbaa676319966fc7fc8f7d6e65", + "size": 452, + "sha256": "f29033d9de506fd57524493b439e6b64f6076dc1a913dadf7cfdf29bf8e2c305" + }, + { + "path": "research/p104-smooth-swap-split/derive_grid.py", + "mode": "100644", + "git_blob": "f8cb37f00bcd197d77bbb205dae3c1a40c0aa680", + "size": 1510, + "sha256": "ceb7a44ef19d72a16db7b43c65c85910d965499d1715436011de32af5d39dbb0" + }, + { + "path": "research/p104-smooth-swap-split/inputs/pr7110.tar", + "mode": "100644", + "git_blob": "f615a25ada40f42cff2b65c519856b5722c77f0e", + "size": 1105920, + "sha256": "b116bd277bcb1560fc1f15e33ce300b487c769564cece55d7821b072085097a8" + }, + { + "path": "research/p104-smooth-swap-split/source.py", + "mode": "100644", + "git_blob": "1b2bdc34174a6cb1efdd6d61c2184f04aad05f1d", + "size": 5041, + "sha256": "5a0751b23559b2e11d7f139fdec43eee3036bca5f3dae4624151caa8e6f6d734" + }, + { + "path": "research/p104-smooth-swap-split/split.py", + "mode": "100644", + "git_blob": "5407e8959b8723464aee68eea6ffcf2ee75cc3b7", + "size": 6432, + "sha256": "3d529d78994504ad591a3afade4dab094751c1c221edbab10165290314cf0894" + }, + { + "path": "research/p104-smooth-swap-split/support.py", + "mode": "100644", + "git_blob": "192cd38d27e4b732981b98730459a041dcfb52e7", + "size": 606, + "sha256": "f3e6eeb879480715c5c32c1a390a63c57d26ea1c9a9cbdb89b83ca34260e47f6" + }, + { + "path": "research/p104-smooth-swap-split/verify.py", + "mode": "100644", + "git_blob": "69b56996c102490f9a2027ed0f35ee13a7abdadf", + "size": 12296, + "sha256": "f8ab680573b587620bfd4d871a7c2bc5db5346e6784b5856b7380ccc4bfc1cb0" + } + ] +} diff --git a/research/p104-free-cohort-split/README.md b/research/p104-free-cohort-split/README.md new file mode 100644 index 0000000000..7226175a2e --- /dev/null +++ b/research/p104-free-cohort-split/README.md @@ -0,0 +1,71 @@ +# Three-role neutral cohort: conditional κ .003638315828316 + +This exact successor of [#7112](https://github.com/CrocSwap/integer-mult-bounds/pull/7112) improves its conditional claim by **.000000898708375**, to **.003638315828316**. It also exceeds the concurrent caller improvement [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113), .00363797977, by **.000000336058316**. Three coordinated contact-free MOVE retimings expose one additional independent helper split, rank 9 → rank 3 + rank 6. Each retimed role preserves its complete paid histogram; all 690 new scalar instructions are charged. The source and caller are pinned to #7112, head `e59520bb11b0df5ac33f062f55397d78a491e7af`. + +## Construction and changed premise + +Earlier retiming searches admitted at most two moved roles. This construction needs three roles together at chart 734, dimension 3, before zero-based source event 37929: + +| Role | Original MOVE event | Path | Placement relative to split | +|---|---:|---|---| +| 1463 | 38145 | 3 → 734 | before | +| 1243 | 37722 | 734 → 738 | after | +| 509 | 39073 | 3 → 734 | before | + +All three original and replacement paths cost exactly one rank 3 MOVE. `construct.prepare` checks the entire contact-free interval, every removed event, absence of scalar reads/writes and INIT/CLEAR, nested frames, ownership flags, and exact nonzero paid-rank Counter equality for each role. It moves each role into the common cut chart and restores its required outgoing chart before its next contact. Distinct roles have no shared scalar operation in these intervals, so the relocations commute. The verifier rejects omission of each of the three retimings individually. A synthetic rank 1+8 → rank 3+6 retiming is rejected even though both paths have the same rank sum: paid histograms must agree. + +At the aligned cut, with helper pivot 509, + +``` +a = e1463 - 2 e509, +b = -e1463/3 - 2 e1243/3 - 2 e509/3 + 2 e806/3. +``` + +The complete exact boundary vectors c and d are in `WITNESS.json`. They use only independent helpers whose initial/final charts are (3,127), dimensions (0,9). For the entire prefix P and suffix S, including all public and owned coefficients, `split.check_cut` proves aP=c, Sb=d and ab=cd=1. Every cut operand is at 734. No input helper is assumed zero or identified with another helper. + +The credited independent-helper construction chooses G with row 509=c and Gd=e509, and J with row 509=a and Jb=e509. It emits G⁻¹, the prepared prefix, J, the renamed J⁻¹ and suffix, then the renamed G. Pivot 509 now ends at 734; fresh independent helper 1484 starts at 734 and ends at 127. G isolates the retained arbitrary input at the cut. Substituting the new arbitrary input changes the suffix along b, hence the final boundary along d, which G isolates to the renamed output. All other outputs agree. Owned labels shift by one and retain all logical lifetimes. The existing smooth-swap basis rule from #7112 is retained; here both pivot entries are already nonzero. + +G has 340 instructions and J has 5. Including inverses adds **686 ADDs and 4 SCALEs**, with no net change in MOVE count. The emitted word has 72,833 events, 1,485 public fields and 1,085 independent helpers. Owned labels 51, lifetimes 54, peak 43, rises 23 and ascent mass 56 remain unchanged. Canonical word SHA256 is `ae30929ff3b5f6b49a5edac78e2164acfbf809113d0b9f03249ef940dd7b2491`. + +## Complete invoice and bounds + +Per LOCAL, ΔP={} and ΔT={3:+1,6:+1,9:−1}. Across 18 LOCALs, the concave margin improves by **18(3^p+6^p−9^p)>0** for every 0peak:peak=mass;witness=[i,kind] + for i,e in enumerate(word['program']): + op,r=e[:2] + if op in('INIT','CLEAR'):rows[r]={} + elif op=='SCALE': + rows[r]={k:Q(e[2])*v for k,v in rows[r].items()};observe(rows[r],i,'scale') + elif op in('ADD','COPY'): + if op=='COPY':assert not rows[r] + product={k:Q(e[3])*v for k,v in rows[e[2]].items()};observe(product,i,'product') + row=rows[r].copy() + for k,v in product.items(): + value=row.get(k,Q(0))+v + if value:row[k]=value + else:row.pop(k,None) + rows[r]=row;observe(row,i,'stored') + odd=denom;frac=0 + while odd%2==0:odd//=2;frac+=1 + return dict(odd_scale=odd,fractional_bits=frac,unscaled_maximum_mass=str(peak),scaled_maximum_mass=str(peak*odd),mass_witness=witness,coefficient_visits=visits),rows +if __name__=='__main__': + w=json.load(gzip.open(sys.argv[1],'rt'));result,rows=derive(w) + Path(sys.argv[2]).write_text(json.dumps(result,indent=2)+'\n');print(result) diff --git a/research/p104-free-cohort-split/discover.py b/research/p104-free-cohort-split/discover.py new file mode 100644 index 0000000000..d8b7d1b34d --- /dev/null +++ b/research/p104-free-cohort-split/discover.py @@ -0,0 +1,167 @@ +"""Successor discovery on exact #7112: explicit boundary group, any finite histogram-neutral contact-free cohort; native 2,3,5-smooth scalar alphabet. +Parameterized boundary-group ranks by OpenAI Codex for dillona; retains predecessor authors below. + +Optional finite discovery; the verifier does not trust this search. + +Helper kernel/basis methods: Ali Romman. Paid main-path retiming extension: +Jerry Chen / @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +Floating point only screens candidates; accepted constructions receive exact +whole-word, phase, invoice and complete conditional-parameter verification. +""" +import gzip,json,sys,time +from pathlib import Path +from fractions import Fraction as Q +from math import lcm +from collections import defaultdict,Counter +sys.path.insert(0,str(Path(__file__).resolve().parent)) +from support import L +add,span=L.add,L.span +from split import basis + +def pure_combinations(rows, roles, group): + """Eliminate coordinates outside the group; retain field coefficients.""" + pivots, output = {}, [] + for role in roles: + outside = {k:v for k,v in rows[role].items() if k not in group} + inside = {k:v for k,v in rows[role].items() if k in group} + coefficients = {role:Q(1)} + while outside: + pivot = min(outside) + if pivot not in pivots: + scale = 1/outside[pivot] + pivots[pivot] = [{k:v*scale for k,v in row.items()} + for row in (outside, inside, coefficients)] + break + scale = -outside[pivot] + for target, source in zip((outside, inside, coefficients), pivots[pivot]): + add(target, source, scale) + if not outside and inside: + output.append((inside, coefficients)) + return output + + +def smooth_program(program): + for event in program: + q=Q(event[-2]) + if abs(q)+1 >= 2**16:return False + tests=[q.denominator] + if event[0]=='SCALE':tests.append(abs(q.numerator)) + for x in tests: + if not x:return False + for prime in (2,3,5): + while x%prime==0:x//=prime + if x!=1:return False + return True + + + +def encode(value): + if isinstance(value,Q):return str(value) + if isinstance(value,dict):return {str(k):encode(v)for k,v in value.items()} + if isinstance(value,(tuple,list)):return [encode(x)for x in value] + return value + +HERE=Path(__file__).parent +w=json.loads(gzip.decompress((Path(sys.argv[1])).read_bytes())) +n=w['public'];N=n+w['owned_fields'];main=set(w['live'])|{r+112 for r in w['live']}|set(w['hosted']['X2'])|set(w['hosted']['Y2']) +U,V=map(int,sys.argv[3:5]);group={r for r in range(n)if r not in main and(w['initial'][r],w['final'][r])==(U,V)} +spans=[span(b)for b in w['frames']];dims=list(map(len,w['frames'])) +contacts=defaultdict(list);moves=defaultdict(list) +for i,e in enumerate(w['program']): + if e[0]=='MOVE':moves[e[1]].append(i) + else: + contacts[e[1]].append(i) + if e[0]in('ADD','COPY'):contacts[e[2]].append(i) +t=1-.003637417119941 +windows=[];starts=defaultdict(list);ends=defaultdict(list) +for r in range(N): + touches=[-1]+contacts[r]+[len(w['program'])] + for lo,hi in zip(touches,touches[1:]): + mi=[i for i in moves[r]if lo=maxgain-1e-12:continue + h=dict(role=r,lo=lo+1,hi=hi,frame=f,old=a,new=b,moves=mi,old_paid=paid,new_paid=[d1,d2],cost=cost,private=r>=n) + idx=len(windows);windows.append(h);starts[lo+1].append(idx);ends[hi+1].append(idx) +print('windows',len(windows),flush=True) +rows=[{r:Q(1)}if r=gain-1e-12:continue + accepted_cost[len(used)]+=1 + def odd_other(n): + for prime in (2,3,5): + while n%prime==0:n//=prime + return n + gauge=lcm(*(odd_other(q.denominator)for row in (a,c)for q in row.values())) + selected=None + for alpha in sorted({1,gauge}): + aa={r:q*alpha for r,q in a.items()};cc={r:q*alpha for r,q in c.items()} + bb={r:q/alpha for r,q in b.items()};dd={r:q/alpha for r,q in d.items()} + if smooth_program(basis(cc,dd,p,U)+basis(aa,bb,p,f)): + selected=(aa,bb,cc,dd);break + if selected is None: + rejected_alphabet[len(used)]+=1;continue + aa,bb,cc,dd=selected + key=(f,p,tuple(sorted(c.items())),tuple(sorted(d.items())),tuple(sorted(a.items())),tuple(sorted(b.items()))) + if key in seen:continue + seen.add(key);hits.append(dict(frame=f,pivot=p,cut=cut,ranks=[dims[f]-dims[U],dims[V]-dims[f]],gain=gain-cost,paths=[windows[idx]for idx in used],a=aa,b=bb,c=cc,d=dd)) + if cut: + e=w['program'][cut-1];op,r=e[:2] + if op in('INIT','CLEAR'):cols[r]={} + elif op=='SCALE':cols[r]={k:v*Q(e[2])for k,v in cols[r].items()} + elif op in('ADD','COPY'): + add(cols[e[2]],cols[r],Q(e[3])) + if op=='COPY':cols[r]={} + if cut%5000==0:print('reverse',cut,'pairs',pairs,'hits',len(hits),'sec',round(time.time()-start,2),flush=True) +hits.sort(key=lambda h:-h['gain']) +(Path(sys.argv[2])).write_text(json.dumps(encode(hits),indent=2)+'\n') +print('paired',pairs,'hits',len(hits),'seconds',time.time()-start,'cost_pass',dict(accepted_cost),'alphabet_reject',dict(rejected_alphabet),flush=True) +for h in hits[:10]:print({k:v for k,v in encode(h).items()if k not in('a','b','c','d')},flush=True) diff --git a/research/p104-free-cohort-split/inputs/pr7112.tar b/research/p104-free-cohort-split/inputs/pr7112.tar new file mode 100644 index 0000000000..aeced196c3 Binary files /dev/null and b/research/p104-free-cohort-split/inputs/pr7112.tar differ diff --git a/research/p104-free-cohort-split/source.py b/research/p104-free-cohort-split/source.py new file mode 100644 index 0000000000..82cb6ef60e --- /dev/null +++ b/research/p104-free-cohort-split/source.py @@ -0,0 +1,79 @@ +"""Authenticate exact #7112 closure and reconstruct every predecessor edit. +Prepared for dillona with substantial OpenAI Codex assistance. Apache-2.0. +""" +from contextlib import contextmanager +from hashlib import sha256, sha1 +from pathlib import Path +import contextlib, gzip, importlib.util, io, json, sys, tarfile, tempfile +HERE = Path(__file__).resolve().parent + +def need(ok, why): + if not ok: raise ValueError(why) + +def read(path): + raw = Path(path).read_bytes() + return json.loads(gzip.decompress(raw) if raw[:2] == b'\x1f\x8b' else raw) + +def canonical(obj): return json.dumps(obj, sort_keys=True, separators=(',', ':')).encode() + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + out = importlib.util.module_from_spec(spec); sys.modules[name] = out + spec.loader.exec_module(out) + return out + +def extract(archive, root, pins=None): + root.mkdir(parents=True, exist_ok=True); seen = set() + with tarfile.open(archive) as tar: + for member in tar: + if member.isdir(): continue + path = root/member.name + need(member.isfile() and path.resolve().is_relative_to(root.resolve()) and path not in seen, + 'Unique safe regular archive member') + raw = tar.extractfile(member).read() + if pins is not None: + need(member.name in pins, 'Listed source member') + pin = pins[member.name] + need(len(raw) == pin['size'] and sha256(raw).hexdigest() == pin['sha256'] and + sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == pin['git_blob'], + 'Exact source Git blob and SHA256') + path.parent.mkdir(parents=True, exist_ok=True); path.write_bytes(raw); seen.add(path) + if pins is not None: need(seen == {root/p for p in pins}, 'Complete listed source closure') + sums = root/'SHA256SUMS' + if sums.exists(): + for line in sums.read_text().splitlines(): + digest, name = line.split(None, 1); path = root/name.lstrip('*') + need(path.resolve().is_relative_to(root.resolve()) and sha256(path.read_bytes()).hexdigest() == digest, + 'Nested source checksum') + +@contextmanager +def sources(): + pins=read(HERE/'INPUTS.json'); archive=HERE/'inputs/pr7112.tar' + need(sha256(archive.read_bytes()).hexdigest()==pins['archive_sha256'],'Frozen outer archive') + old_path=list(sys.path) + with tempfile.TemporaryDirectory(prefix='p104-7112-') as tmp: + root=Path(tmp);extract(archive,root,{x['path']:x for x in pins['files']}) + parent=root/'research/p104-smooth-swap-split' + parent_source=load('cohort_parent_source',parent/'source.py') + with parent_source.sources() as (vendor,previous,rank9,bundle,word): + saved={name:sys.modules.get(name) for name in ('support','split')} + try: + load('support',parent/'support.py');load('split',parent/'split.py') + emitter=load('cohort_parent_construct',parent/'construct.py') + word=emitter.construct(word,read(parent/'WITNESS.json')) + finally: + for name,module in saved.items(): + if module is None:sys.modules.pop(name,None) + else:sys.modules[name]=module + need(canonical(word)==gzip.decompress((parent/'WORD.json.gz').read_bytes()),'Entire reconstructed #7112') + need(sha256(canonical(word)).hexdigest()==pins['source_canonical_sha256'],'Pinned #7112 canonical word') + try:yield vendor,previous,rank9,bundle,parent,word + finally:sys.path[:]=old_path + +if __name__ == '__main__': + import argparse + parser = argparse.ArgumentParser(); parser.add_argument('--output', type=Path, required=True) + args = parser.parse_args() + with sources() as source: + raw = canonical(source[-1]) + with args.output.open('xb') as out: out.write(gzip.compress(raw, mtime=0)) diff --git a/research/p104-free-cohort-split/split.py b/research/p104-free-cohort-split/split.py new file mode 100644 index 0000000000..5407e8959b --- /dev/null +++ b/research/p104-free-cohort-split/split.py @@ -0,0 +1,154 @@ +"""Split independent helper jobs with three scalar basis changes. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +Adapted for arbitrary counted owned-field inventory by @CubeJerry with OpenAI assistance. +Successor: OpenAI Codex for dillona excludes both hosted main planes from helper groups. +The source word and caller retain the credits in README.md. +Successor: dillona/OpenAI Codex choose a small smooth swap entry when pivot is zero. +""" +from copy import deepcopy +from fractions import Fraction as Q +from support import L + + +def inverse(program): + return [[e[0], *e[1:-2], + str(1/Q(e[-2]) if e[0] == 'SCALE' else -Q(e[-2])), e[-1]] + for e in reversed(program)] + + +def basis(a, b, pivot, frame): + """Return B with row pivot equal to a and B b equal to e_pivot.""" + L.need(sum(v*b.get(k, 0) for k, v in a.items()) == 1, 'Unit basis pairing') + roles = sorted(set(a) | set(b) | {pivot}) + values, program = dict(b), [] + + def emit(event): + program.append(event) + r, q = event[1], Q(event[-2]) + if event[0] == 'SCALE': + values[r] = values.get(r, 0)*q + else: + values[r] = values.get(r, 0)+q*values.get(event[2], 0) + + def swap_score(r): + q=b[r] + def smooth(x): + for prime in (2,3,5): + while x%prime==0:x//=prime + return x==1 + return (not(smooth(abs(q.numerator)) and smooth(q.denominator)), + abs(q.numerator).bit_length()+q.denominator.bit_length(),r) + j = pivot if b.get(pivot) else min((r for r in roles if b.get(r)),key=swap_score) + if j != pivot: + for event in [['ADD', pivot, j, '1', frame], + ['ADD', j, pivot, '-1', frame], + ['ADD', pivot, j, '1', frame], + ['SCALE', j, '-1', frame]]: + emit(event) + if values[pivot] != 1: + emit(['SCALE', pivot, str(1/values[pivot]), frame]) + for r in roles: + if r != pivot and values.get(r): + emit(['ADD', r, pivot, str(-values[r]), frame]) + L.need(all(values.get(r, 0) == int(r == pivot) for r in roles), 'Basis column') + inverse_rows = {r: {r: Q(1)} for r in roles} + for e in inverse(program): + if e[0] == 'SCALE': + inverse_rows[e[1]] = {k: Q(e[-2])*v for k, v in inverse_rows[e[1]].items()} + else: + L.add(inverse_rows[e[1]], inverse_rows[e[2]], Q(e[-2])) + row = {} + for r, q in a.items(): + L.add(row, inverse_rows[r], q) + L.need(row[pivot] == 1, 'Basis row coefficient') + for r in roles: + if r != pivot and row.get(r): + program.append(['ADD', pivot, r, str(row[r]), frame]) + return program + + +def check_cut(word, h): + """Check the whole prefix row and suffix column over the rationals.""" + n, cut, f, p = word['public'], h['cut_after'], h['frame'], h['pivot'] + a, b, c, d = ({int(k): Q(v) for k, v in h[s].items()} for s in ('a', 'b', 'c', 'd')) + main = set(word['live']) | {r+112 for r in word['live']} | set(word['hosted']['X2']) | set(word['hosted']['Y2']) + L.need(p < n and p not in main, 'A helper supplies the retained output role') + u, v = word['initial'][p], word['final'][p] + group = {r for r in range(n) if r not in main and + (word['initial'][r], word['final'][r]) == (u, v)} + L.need(set(c) | set(d) <= group, 'Both boundary vectors use one helper group') + L.need(L.span(word['frames'][u]) < L.span(word['frames'][f]) < L.span(word['frames'][v]), + 'Two strictly productive nested targets') + L.need(h['ranks'] == [len(word['frames'][f])-len(word['frames'][u]), + len(word['frames'][v])-len(word['frames'][f])], 'Declared split ranks') + rows = [{r: Q(1)} if r < n else {} for r in range(n+word['owned_fields'])] + current = word['initial']+[None]*word['owned_fields'] + for e in word['program'][:cut+1]: + op, r = e[:2] + if op == 'MOVE': + current[r] = e[3] + elif op in ('INIT', 'CLEAR'): + rows[r] = {} + current[r] = e[2] if op == 'INIT' else None + elif op == 'SCALE': + rows[r] = {k: Q(e[-2])*x for k, x in rows[r].items()} + elif op == 'COPY': + rows[r] = {k: Q(e[-2])*x for k, x in rows[e[2]].items()} + else: + L.add(rows[r], rows[e[2]], Q(e[-2])) + L.need(all(current[r] == f for r in set(a) | set(b) | {p}), 'One intermediate chart') + total = {} + for r, q in a.items(): + L.add(total, rows[r], q) + L.need(total == c, 'Exact prefix functional; no other input') + column = [b.get(r, Q(0)) for r in range(n+word['owned_fields'])] + for e in word['program'][cut+1:]: + op, r = e[:2] + if op in ('INIT', 'CLEAR'): + column[r] = Q(0) + elif op == 'SCALE': + column[r] *= Q(e[-2]) + elif op == 'COPY': + column[r] = Q(e[-2])*column[e[2]] + elif op == 'ADD': + column[r] += Q(e[-2])*column[e[2]] + L.need(column == [d.get(r, Q(0)) for r in range(n+word['owned_fields'])], 'Exact suffix direction; no other output') + L.need(sum(x*b.get(r, 0) for r, x in a.items()) == + sum(x*d.get(r, 0) for r, x in c.items()) == 1, 'Both independent pairings') + return a, b, c, d + + +def split(word, h): + a, b, c, d = check_cut(word, h) + n, p, f, cut = word['public'], h['pivot'], h['frame'], h['cut_after'] + u, v = word['initial'][p], word['final'][p] + + def shift_owned(event): + e = event.copy() + e[1] += int(e[1] >= n) + if e[0] in ('ADD', 'COPY'): + e[2] += int(e[2] >= n) + return e + + def use_successor(event): + e = event.copy() + if e[1] == p: + e[1] = n + if e[0] in ('ADD', 'COPY') and e[2] == p: + e[2] = n + return e + + boundary, middle = basis(c, d, p, u), basis(a, b, p, f) + out = deepcopy(word) + out['public'] = n+1 + out['initial'].append(f) + out['final'].append(v) + out['final'][p] = f + out['program'] = inverse(boundary) + out['program'] += [shift_owned(e) for e in word['program'][:cut+1]] + out['program'] += [shift_owned(e) for e in middle] + out['program'] += [use_successor(shift_owned(e)) for e in inverse(middle)] + out['program'] += [use_successor(shift_owned(e)) for e in word['program'][cut+1:]] + out['program'] += [use_successor([*e[:-1], v]) for e in boundary] + return out diff --git a/research/p104-free-cohort-split/support.py b/research/p104-free-cohort-split/support.py new file mode 100644 index 0000000000..192cd38d27 --- /dev/null +++ b/research/p104-free-cohort-split/support.py @@ -0,0 +1,18 @@ +"""Small exact sparse operations, retained from Ali Romman/CubeJerry. Apache-2.0.""" +class L: + @staticmethod + def need(ok, why): + if not ok: raise ValueError(why) + @staticmethod + def add(dst, src, q): + for k,v in tuple(src.items()): + value=dst.get(k,0)+q*v + if value: dst[k]=value + else: dst.pop(k,None) + @staticmethod + def span(basis): + out={0} + for v in basis: + L.need(type(v) is int and 00,'Complete conservative ordinary bill') + gate,price=G.exact_price(vendor,archive,before,invoice,previous) + manifest=read(vendor/'INDEPENDENT-SOURCES.json') + P=load('static_bit_binding',archive/'verify.py');P.bit_binding(I,manifest) + precision=base.precision(vendor,word,caller,gate,manifest) + need(precision['word']['odd_scale_lcm']==1125 and precision['word']['dyadic_height']==24 and precision['context_c']==1342,'Recomputed signed caller precision') + print('PASS full signed caller, ordinary bill, two exact price engines, precision and compiler gates',flush=True) + charts=chart_check(vendor,source,word) + controls={} + grid_engine=G.module('static_grid_controls',vendor/'retained/odd-native-common-grid/independent_bounds.py') + controls['insufficient_odd_grid']=rejected(lambda:grid_engine.word_run(word,375,24)) + controls['insufficient_fractional_grid']=rejected(lambda:grid_engine.word_run(word,1125,23)) + bad=deepcopy(hit);bad['a']['509']='1' + controls['wrong_prefix']=rejected(lambda:construct(source,bad)) + bad=deepcopy(hit);bad['b']['509']='2' + controls['wrong_suffix']=rejected(lambda:construct(source,bad)) + bad=deepcopy(hit);bad['frame']=246 + controls['wrong_cut_frame']=rejected(lambda:construct(source,bad)) + from split import basis + Gbasis=basis(*[{int(k):Q(v)for k,v in hit[s].items()}for s in('c','d')],hit['pivot'],3) + Jbasis=basis(*[{int(k):Q(v)for k,v in hit[s].items()}for s in('a','b')],hit['pivot'],734) + need((len(Gbasis),len(Jbasis))==(340,5),'Boundary and cut basis lengths') + prepared,spec=prepare(source,hit) + split_after=spec['cut_after'] + for name,index in [('missing_cut_correction',len(Gbasis)+split_after+1), + ('missing_successor_correction',len(Gbasis)+len(Jbasis)+split_after+1)]: + bad=deepcopy(word);bad['program'].pop(index) + controls[name]=bool(I.native(bad)['bad_inputs']) + for role in (1463,1243,509): + bad=deepcopy(hit);bad['paths']=[p for p in bad['paths'] if p['role']!=role] + controls['missing_retiming_'+str(role)]=rejected(lambda:construct(source,bad)) + bad=deepcopy(hit);bad['paths'][0]['lo']-=1 + controls['intervening_scalar_contact']=rejected(lambda:construct(source,bad)) + bad=deepcopy(hit);bad['paths'][0]['moves']=[] + controls['omitted_old_move']=rejected(lambda:construct(source,bad)) + bad=deepcopy(hit);bad['paths'].append(deepcopy(bad['paths'][0])) + controls['duplicate_retimed_role']=rejected(lambda:construct(source,bad)) + bad=deepcopy(word);bad['initial'][-1]=3 + controls['wrong_successor_frame']=rejected(lambda:I.native(bad)) + synthetic={'frames':[[],[1],[1,2,4],[1,2,4,8,16,32,64,128,256]], + 'program':[['MOVE',0,0,1,False],['MOVE',0,1,3,False]]} + charged={'frame':2,'cut':1,'paths':[dict(role=0,old=0,new=3,frame=2,lo=0,hi=2,moves=[0,1],private=False)]} + controls['changed_paid_rank_histogram']=rejected(lambda:prepare(synthetic,charged)) + need(all(controls.values()),'All split rejection controls') + physical_checks=[]; signed_routes=None + if physical: + with tempfile.TemporaryDirectory(prefix='static-physical-') as tmp: + path=Path(tmp)/'word.json.gz';path.write_bytes(gzip.compress(canonical(word),mtime=0)) + for command,args in [(vendor/'frozen/verify_host3_odd.py',[path,'1125']), + (vendor/'frozen/physical.py',[path,vendor/'frozen/clifford_exact.py','1000000009','11'])]: + subprocess.run([sys.executable,'-I','-B',str(command),*map(str,args)],check=True) + physical_checks.append(command.name) + physical_engine=G.module('static_signed_routes',rank9/'physical_child.py',( + ('cca66a7ec924bab47ccd1410968d16e071a01dc6110b5c08040bd207f753d066',sha256(canonical(word)).hexdigest()),)) + capture=io.StringIO() + with contextlib.redirect_stdout(capture):physical_engine.main(path,vendor/'data/caller.json',caller_path) + signed_routes=json.loads(capture.getvalue()) + need(signed_routes['status']=='PASS_PHYSICAL_RANK9_ALGEBRA' and signed_routes['paid_calls']==32,'Signed physical route replay') + need(1000*sum(len(row['caller_fields'])*row['ordinary_elementary_units'] for row in signed_routes['bindings'])==routes==1168000,'Actual signed route ordinary charge') + physical_checks.append('physical_child.py') + print('PASS chart columns and phase, rejection controls and finite physical replay',flush=True) + return encode(dict(status='PASS_P104_FREE_COHORT_SPLIT',source_head='e59520bb11b0df5ac33f062f55397d78a491e7af', + word_canonical_sha256=sha256(canonical(word)).hexdigest(),native=native,forward=forward_receipt,grid=grid,derived_grid=derived, + caller=symbolic,invoice=invoice,ordinary=ordinary,gate=gate,price=price,precision=precision, + charts=charts,controls=controls,physical_checks=physical_checks,signed_routes=signed_routes, + limitations=['Source-aware reuse of attributed engines, not independent human or kernel review.', + 'The five framework assumptions and complete source-specific provider/caller/tariff application remain open.', + 'Finite physical checks and source-unit bills do not constitute a complete multiplication theorem.'])) + +def main(): + p=argparse.ArgumentParser();p.add_argument('--out',type=Path);p.add_argument('--skip-physical',action='store_true');a=p.parse_args() + result=run(not a.skip_physical) + if a.out: + with a.out.open('x') as f:json.dump(result,f,sort_keys=True,indent=2);f.write('\n') + else:need(result==read(HERE/'RESULT.json'),'Every frozen receipt field') + print(result['status'],result['gate']['claim'],flush=True) +if __name__=='__main__':main()