"""Verify the saved exact rational Bernstein certificate without its producer."""
from fractions import Fraction as F
from math import comb
from pathlib import Path
import hashlib,json

path=Path(__file__).with_name('complete-certificate.json')
data=json.loads(path.read_text())
def values(c,box):
    na=max(i for i,j in c);nb=max(j for i,j in c);a,b,u,v=box;p={}
    for (i,j),cc in c.items():
      for k in range(i+1):
       for l in range(j+1):
        p[k,l]=p.get((k,l),F(0))+cc*comb(i,k)*a**(i-k)*(b-a)**k*comb(j,l)*u**(j-l)*(v-u)**l
    return [sum((p.get((k,l),F(0))*F(comb(i,k),comb(na,k))*F(comb(j,l),comb(nb,l))
                 for k in range(i+1) for l in range(j+1)),F(0))
            for i in range(na+1) for j in range(nb+1)]
def check(c,box,tree):
    if 'min' in tree:
        assert min(values(c,box))==F(tree['min'])>0
        return 1
    a,b,u,v=box
    children=((a,(a+b)/2,u,v),((a+b)/2,b,u,v)) if tree['axis']==0 else ((a,b,u,(u+v)/2),(a,b,(u+v)/2,v))
    return check(c,children[0],tree['left'])+check(c,children[1],tree['right'])
leaves=0
for rec in data['certificates']:
    box=tuple(F(v) for v in rec['box'])
    for part in ['numerator','denominator']:
        p=rec[part];c={(i,j):F(v) for i,j,v in p['coefficients']}
        n=check(c,box,p['tree']);assert n==p['leaves'];leaves+=n
assert all(F(v)>0 for v in data['positive_constants'].values())
assert F(data['theta'])==F(8733821,10000000)
assert F(87402,100000)-F(data['theta'])==F(6379,10000000)>F(1,100000)
receipt={'status':'PASS_SAVED_RATIONAL_INEQUALITIES_ONLY','conditions':len(data['certificates']),
         'leaves':leaves,'positive_constants':len(data['positive_constants']),
         'certificate_sha256':hashlib.sha256(path.read_bytes()).hexdigest(),
         'new_mixed_moment_proved':False,'new_endpoint_proved':False}
Path(__file__).with_name('complete-verification.json').write_text(json.dumps(receipt,indent=2)+'\n')
print(json.dumps(receipt))