"""Independent, integer-only certificates, reusing run-1 auditor's parser.

Grid completeness: w=2*max(R). If two cells differ by >=2 on either
axis, the corresponding coordinate separation is strictly greater than w.
Since R_i+R_j <= w, such a pair cannot overlap. Checking the 3x3 neighboring
cells checks every possible overlap, once, including unequal radii and
negative coordinates. No floating-point operation participates.

Algebraic walls use outward-rounded integer intervals at scale 10**100.
A nonnegative LOWER slack proves containment; an interval crossing zero is
INCOMPLETE, never treated as feasible. This is a rigorous certificate of the
original algebraic inequalities, without radius repair or numerical tolerance.
"""
import hashlib
import json
import math
import re
import sys
from fractions import Fraction as F
from pathlib import Path
sys.path.insert(0, str(Path(__file__).resolve().parents[1]/'audit_geo'))
from exact import read_scaled, decimal_fraction as dec, check_circles

ROOT=Path(__file__).resolve().parent
C=Path('claims')
Q=10**100

def iv(x):
    x=F(x)*Q
    return x.numerator//x.denominator, -(-x.numerator//x.denominator)
def add(a,b): return a[0]+b[0],a[1]+b[1]
def neg(a): return -a[1],-a[0]
def sub(a,b): return add(a,neg(b))
def mul(a,b):
    p=[x*y for x in a for y in b]
    return min(p)//Q, -(-max(p)//Q)
def div(a,b): return mul(a,iv(F(1,b)))
def sqrt(a):
    assert a[0]>=0
    lo=math.isqrt(a[0]*Q); hi=math.isqrt(a[1]*Q)
    return lo,hi+(hi*hi<a[1]*Q)

S5=sqrt(iv(5)); S3=sqrt(iv(3))
rho=div(sqrt(add(iv(25),mul(iv(10),S5))),10)
A=div(sqrt(add(iv(10),mul(iv(2),S5))),4)
B=div(sub(S5,iv(1)),4)
D=div(sqrt(sub(iv(10),mul(iv(2),S5))),4)
E=div(add(S5,iv(1)),4)
NORMALS=[(iv(0),iv(-1)),(A,neg(B)),(D,E),(neg(D),E),(neg(A),neg(B))]

def pairs(rows, grid=True):
    width=2*max(r for x,y,r in rows)
    if width<=0: grid=False
    cells={}; count=0; bad=[]; minimum=None
    for i,(x,y,r) in enumerate(rows):
        if grid:
            cell=(x//width,y//width)
            js=[j for dx in (-1,0,1) for dy in (-1,0,1)
                for j in cells.get((cell[0]+dx,cell[1]+dy),[])]
        else: js=range(i)
        for j in js:
            u,v,s=rows[j]
            gap=(x-u)**2+(y-v)**2-(r+s)**2
            count+=1
            if minimum is None or gap<minimum[0]: minimum=(gap,j+1,i+1)
            if gap<0: bad.append([j+1,i+1,str(gap)])
        if grid: cells.setdefault(cell,[]).append(i)
    return dict(pair_checks=count,overlaps=bad,
                min_checked_gap=None if minimum is None else [str(minimum[0]),*minimum[1:]])

def read_container(path,kind):
    if kind!='rect': return (*read_scaled(path),None)
    lines=[l for l in path.read_text().splitlines() if l.strip() and not l.startswith('#')]
    w=F(lines[0]); rows=[[F(t) for t in l.split()] for l in lines[1:]]
    assert all(len(r)==3 for r in rows)
    scale=math.lcm(w.denominator,*(t.denominator for r in rows for t in r))
    return [[int(t*scale) for t in r] for r in rows],scale,int(w*scale)

def check(path,kind,n):
    rows,scale,w=read_container(path,kind)
    result=pairs(rows,grid=kind=='square')
    lower=[]; upper=[]
    for x,y,r in rows:
        if kind in ('square','rect'):
            W,H=(scale,scale) if kind=='square' else (w,2*scale-w)
            slacks=[iv(F(t,scale)) for t in (x-r,y-r,W-x-r,H-y-r)]
        elif kind=='circ':
            # Unit-radius disk centred at zero; r<=1 and |c|² <= (1-r)².
            slacks=[iv(F(scale-r,scale)),iv(F((scale-r)**2-x*x-y*y,scale*scale))]
        else:
            X,Y,R=(iv(F(t,scale)) for t in (x,y,r))
            if kind=='pent':
                slacks=[sub(sub(rho,add(mul(a,X),mul(b,Y))),R) for a,b in NORMALS]
            elif kind=='tri':
                # Equilateral triangle with vertices (0,0),(1,0),(1/2,sqrt(3)/2).
                slacks=[sub(Y,R),sub(sub(mul(div(S3,2),X),div(Y,2)),R),
                        sub(sub(mul(div(S3,2),sub(iv(1),X)),div(Y,2)),R)]
            else: raise ValueError(kind)
        lower.extend(z[0] for z in slacks); upper.extend(z[1] for z in slacks)
    result.update(file=str(path),kind=kind,n=n,rows=len(rows),sha256=hashlib.sha256(path.read_bytes()).hexdigest(),
        scale=str(scale),exact_sum=dec(F(sum(r for x,y,r in rows),scale)),
        positive_radii=all(r>0 for x,y,r in rows),
        wall_lower_min=dec(F(min(lower),Q)),wall_upper_min=dec(F(min(upper),Q)),
        wall_status='pass' if min(lower)>=0 else 'fail' if min(upper)<0 else 'incomplete',
        valid_width=kind!='rect' or 0<w<2*scale)
    result['feasible']=result['rows']==n and result['positive_radii'] and result['valid_width'] and result['wall_status']=='pass' and not result['overlaps']
    return result

def main():
    records=[]
    manifests={m['file']:m for m in json.loads((C/'r2/claims.json').read_text())}
    for m in json.loads((C/'claims_csqv.json').read_text()): manifests[str(C/f'csqv{m["n"]}.txt')]=m
    cont=json.loads((C/'cont/claims_cont.json').read_text())
    for key in ('certain','above_floor_uncertain'):
        for m in cont[key]: manifests[m['file']]=m
    for path in sorted(C.rglob('*.txt')):
        m=re.fullmatch(r'(?:extra_)?csqv(\d+)',path.stem)
        cm=re.fullmatch(r'c(pent|rect|circ|tri)(\d+)',path.stem)
        if not (m or cm): continue
        kind,n=('square',int(m[1])) if m else (cm[1],int(cm[2]))
        r=check(path,kind,n)
        manifest=manifests.get(str(path))
        r['manifest_present']=manifest is not None
        if manifest:
            r['manifest_hash_matches']=r['sha256']==manifest['sha256']
            r['manifest_sum_matches']=F(r['exact_sum'])==F(manifest.get('scorer_final_exact',manifest.get('score_exact')))
        records.append(r)
    first={r['n']:r for r in records if Path(r['file']).parent==C and r['file'].split('/')[-1].startswith('csqv')}
    second=[r for r in records if '/r2/' in r['file']]
    replacements=[r for r in second if r['n'] in first]
    for r in replacements: r['gain_over_first']=dec(F(r['exact_sum'])-F(first[r['n']]['exact_sum']))
    all_pair_checks=[]
    for n in (142,1681,2601):
        p=C/'r2'/f'csqv{n}.txt'; r=check_circles(p,n); g=next(x for x in second if x['n']==n)
        assert r['feasible']==g['feasible'] and r['exact_sum']==g['exact_sum']
        all_pair_checks.append(dict(n=n,pairs=r['pair_checks'],agrees=True))
    summary=dict(files=len(records),csqv=sum(r['kind']=='square' for r in records),containers=sum(r['kind']!='square' for r in records),
        first_run=len(first),second_run=len(second),new_small=sum(r['n'] not in first and r['n']<=1600 for r in second),
        new_big=sum(r['n'] not in first and r['n']>1600 for r in second),replacements=len(replacements),
        nonimproving_replacements=[r['n'] for r in replacements if F(r['gain_over_first'])<=0],
        pair_checks=sum(r['pair_checks'] for r in records),all_pairs_crosschecks=all_pair_checks,
        infeasible=[r['file'] for r in records if not r['feasible']],
        manifest_mismatches=[r['file'] for r in records if r['manifest_present'] and not (r['manifest_hash_matches'] and r['manifest_sum_matches'])])
    (ROOT/'exact.json').write_text(json.dumps(dict(summary=summary,records=records),indent=2)+'\n')
    print(json.dumps(summary,indent=2))
if __name__=='__main__': main()