"""Driver for the computer-assisted proof of  Lambda <= t0 + y0^2/2  (de Bruijn-Newman constant).

    python certify_all.py 0.174        (or 0.175)

Runs the two Arb certificates (barrier (iii) and region (ii)), writes a timestamped log, RESUMES automatically
after an interruption (region (ii) is certified y-interval by y-interval), checks that the certified y-intervals
cover [y0, sqrt(1-2 t0)] without gaps, and writes CERTIFICATE_<target>.txt with all inputs, hashes and results.
Hypothesis (i) is Platt-Trudgian (RH verified up to 3e12 >= X/2)."""
import sys, os, re, subprocess, hashlib, platform, time, json, math
HERE=os.path.dirname(os.path.abspath(__file__))
TARGETS={'0.175':dict(lam='lam_L0175.npy',t0='0.15499',y0='0.2',X='5998313329980.3135'),
         '0.174':dict(lam='lam_L0174.npy',t0='0.15399',y0='0.2',X='5998313329980.3135')}
target=sys.argv[1] if len(sys.argv)>1 else '0.174'
P=TARGETS[target]; lam=os.path.join(HERE,P['lam'])
logdir=os.path.join(HERE,'logs_'+target); os.makedirs(logdir,exist_ok=True)
def sha(f): return hashlib.sha256(open(f,'rb').read()).hexdigest()
CODEHASH=hashlib.sha256(b''.join(open(os.path.join(HERE,f),'rb').read() for f in ['cert_region_ii.py','cert_barrier.py','common.py'])).hexdigest()[:20]
def say(msg,fh=None):
    line='[%s] %s'%(time.strftime('%Y-%m-%d %H:%M:%S'),msg); print(line,flush=True)
    if fh: fh.write(line+'\n'); fh.flush()
def run(args,logfile):
    """run a certificate script, streaming its output to the console and appending it to logfile"""
    with open(logfile,'a',encoding='utf-8') as fh:
        fh.write('\n### CODEHASH %s  %s  %s\n'%(CODEHASH,time.strftime('%Y-%m-%d %H:%M:%S'),' '.join(args))); fh.flush()
        p=subprocess.Popen([sys.executable,'-u']+args,cwd=HERE,stdout=subprocess.PIPE,stderr=subprocess.STDOUT,text=True)
        for line in p.stdout:
            print(line,end='',flush=True); fh.write(line); fh.flush()
        return p.wait()
def check_codehash(logfile):
    if not os.path.exists(logfile): return
    hs=set(re.findall(r'### CODEHASH (\w+)',open(logfile,encoding='utf-8').read()))
    if hs and hs!={CODEHASH}:
        sys.exit('%s was produced by a different version of the scripts: delete the folder %s and run again'%(logfile,os.path.dirname(logfile)))
def check_real_flint():
    try:
        import flint
        return getattr(flint,'__version__','?')
    except Exception as e:
        sys.exit('python-flint is required (pip install python-flint): %s'%e)
main=open(os.path.join(logdir,'driver.log'),'a',encoding='utf-8')
if os.environ.get('CERT_MOCK')=='1': say('*** CERT_MOCK=1: test mode, the result is NOT a certificate ***',main)
fv=check_real_flint() if os.environ.get('CERT_MOCK')!='1' else 'MOCK'
import numpy
say('target Lambda <= %s : t0=%s y0=%s X=%s, weights %s (sha256 %s), code %s'%(target,P['t0'],P['y0'],P['X'],P['lam'],sha(lam)[:16],CODEHASH),main)
say('python %s, numpy %s, python-flint %s, %s'%(platform.python_version(),numpy.__version__,fv,platform.platform()),main)
# ------------------------------------------------------------ (iii) barrier
blog=os.path.join(logdir,'barrier.log'); check_codehash(blog)
done_b=os.path.exists(blog) and 'CERTIFIED (iii) [Arb]' in open(blog,encoding='utf-8').read() and 'MOCK' not in open(blog,encoding='utf-8').read()
if not done_b:
    say('running barrier certificate (iii) ...',main)
    rc=run(['cert_barrier.py',P['X'],P['t0'],P['y0']],blog)
    txt=open(blog,encoding='utf-8').read()
    if rc!=0 or 'CERTIFIED (iii) [Arb]' not in txt: say('BARRIER FAILED (exit %d) - see %s'%(rc,blog),main); sys.exit(1)
else: say('barrier already certified in %s'%blog,main)
bline=[l for l in open(blog,encoding='utf-8') if l.startswith('CERTIFIED (iii)')][-1].strip()
# ------------------------------------------------------------ (ii) region, with resume
rlog=os.path.join(logdir,'region_ii.log'); check_codehash(rlog)
ytop=math.sqrt(1-2*float(P['t0']))
pat=re.compile(r'^OK y in \[([0-9.eE+-]+),([0-9.eE+-]+)\]: (\d+) chunks, certified \|f_t0\| >= ([0-9.]+)')
def intervals():
    if not os.path.exists(rlog): return []
    txt=open(rlog,encoding='utf-8').read()
    if 'MOCK' in txt and os.environ.get('CERT_MOCK')!='1': sys.exit('region_ii.log contains MOCK output: delete it and rerun')
    out=[]
    for l in txt.splitlines():
        m=pat.match(l)
        if m: out.append((float(m.group(1)),float(m.group(2)),int(m.group(3)),float(m.group(4))))
    return out
last_cov=None; stuck=0
for attempt in range(50):
    iv=sorted(intervals())
    covered=float(P['y0']) if not iv else None
    if iv:
        # longest gap-free chain starting at y0 (printed endpoints have 5 decimals: allow overlap, demand no gap > 0)
        cur=float(P['y0']); assert abs(iv[0][0]-cur)<1e-9, 'first interval must start at y0'
        for a,b,_,_ in iv:
            if a<=cur: cur=max(cur,b)      # endpoints printed with 15 digits; consecutive intervals share the exact float
        covered=cur
    yt=re.findall(r'^YTOP_HI (\S+)',open(rlog,encoding='utf-8').read(),re.M) if os.path.exists(rlog) else []
    if yt: ytop=float(yt[-1]); assert ytop>=math.sqrt(1-2*float(P['t0']))*(1-1e-15)
    if covered>=ytop: break
    if last_cov is not None and covered<=last_cov:
        stuck+=1
        if stuck>=2: say('NO PROGRESS in two consecutive runs - stopping; see %s'%rlog,main); sys.exit(1)
    else: stuck=0
    last_cov=covered
    if iv:
        ystart=max(float(P['y0']),covered-1e-4)            # overlap of 1e-4 with the last certified interval
        h=2*max(b-a for a,b,_,_ in iv if b>=covered-1e-9)
        say('resuming region (ii) at y=%.6f (certified up to %.6f)'%(ystart,covered),main)
        args=['cert_region_ii.py',lam,P['t0'],P['y0'],P['X'],'%.6f'%ystart,'%.6f'%h]
    else:
        say('running region (ii) certificate from y0 ...',main)
        args=['cert_region_ii.py',lam,P['t0'],P['y0'],P['X']]
    rc=run(args,rlog)
    if rc!=0: say('region (ii) run stopped with exit code %d; will resume'%rc,main)
else: say('REGION (ii) NOT COMPLETED after 50 runs',main); sys.exit(1)
iv=sorted(intervals()); worst=min(d for *_,d in iv)
E=[l for l in open(rlog,encoding='utf-8') if l.startswith('eA+eB+eC0 <=')][-1].strip()
# ------------------------------------------------------------ summary
lam_bound=float(P['t0'])+float(P['y0'])**2/2
out=os.path.join(HERE,'CERTIFICATE_%s.txt'%target)
with open(out,'w',encoding='utf-8') as fh:
    fh.write('COMPUTER-ASSISTED PROOF:  Lambda <= t0 + y0^2/2 = %s + %s^2/2 = %.5f < %s\n\n'%(P['t0'],P['y0'],lam_bound,target))
    fh.write('Criterion: Polymath, Thm 1.2 (arXiv:1904.12438).\n')
    fh.write('(i)   RH verified up to 3e12 (Platt-Trudgian, arXiv:2004.09765); X/2 = %.4f < 3e12.\n'%(float(P['X'])/2))
    fh.write('(iii) %s\n'%bline)
    fh.write('(ii)  %s\n      certified y-intervals (each: all x >= X+sqrt(1-y0^2)):\n'%E)
    for a,b,c,d in iv: fh.write('        y in [%.5f, %.5f]: %2d chunks, |f_t0| >= %.5f\n'%(a,b,c,d))
    fh.write('      union covers [%s, %.6f] = [y0, sqrt(1-2 t0)];  min certified |f_t0| = %.5f\n\n'%(P['y0'],ytop,worst))
    fh.write('Inputs: X=%s t0=%s y0=%s ; weights %s sha256=%s\n'%(P['X'],P['t0'],P['y0'],P['lam'],sha(lam)))
    for f in ['cert_region_ii.py','cert_barrier.py','common.py','certify_all.py']: fh.write('        %s sha256=%s\n'%(f,sha(os.path.join(HERE,f))))
    fh.write('Software: python %s, numpy %s, python-flint %s, %s\n'%(platform.python_version(),numpy.__version__,fv,platform.platform()))
    fh.write('Logs: %s\n'%logdir)
    if fv=='MOCK': fh.write('\n*** MOCK RUN - NOT A CERTIFICATE ***\n')
say('ALL HYPOTHESES CERTIFIED: Lambda <= %.5f < %s.  Summary written to %s'%(lam_bound,target,out) if fv!='MOCK' else 'mock run finished (not a certificate)',main)