#!/usr/bin/env python3
"""Independent arbitrary-precision check of the L=128 box-SOS witness."""
from pathlib import Path
from fractions import Fraction
x=(Path(__file__).parent/'box-sos-l128.txt').read_text().split();at=0
def get(w=None):
 global at
 z=x[at];at+=1
 if w is not None:assert z==w,(z,w)
 return z
get('AP_BOX_SOS_LOWER_V1');get('L');L=int(get());get('denom');D=int(get());get('factor_scale');R=int(get())
get('diag');a=[int(get()) for _ in range(L)]
def ae(i0,j0):
 i,j=i0+1,j0+1
 return int(j+1<=2*i<=j+L)+int(i+1<=2*j<=i+L)
H=[[2*D*ae(i,j) for j in range(L)]for i in range(L)]
for i in range(L):H[i][i]+=2*a[i]
get('triangles');nt=int(get());ls=0
for _ in range(nt):
 typ,i,j,k,m=map(int,[get(),get(),get(),get(),get()]);assert 0<=typ<4 and 0<=i<j<k<L and m>=0;ls+=m
 signs=([1,1,1] if typ==0 else [1,-1,-1] if typ==1 else [-1,1,-1] if typ==2 else [-1,-1,1])
 for (u,v),s in zip(((i,j),(i,k),(j,k)),signs):H[u][v]-=m*s;H[v][u]-=m*s
get('factor');P=[[0]*L for _ in range(L)]
for i in range(L):
 for j in range(i+1):P[i][j]=int(get())
get('claimed_multiplier_sum');S=int(get());get('claimed_q_bound');qn,qd=int(get()),int(get());get('claimed_delta_bound');bn,bd=int(get()),int(get());assert at==len(x) and S==sum(a)+ls
marg=[]
for i in range(L):
 radius=0
 for j in range(L):
  dot=sum(P[i][k]*P[j][k] for k in range(min(i,j)+1))
  q=R*R*H[i][j]-2*D*dot
  if i==j:dia=q
  else:radius+=abs(q)
 marg.append(dia-radius)
assert min(marg)>=0
q=Fraction(-S,D);delta=Fraction(1,16)-Fraction(1,8*L)+q/Fraction(8*L*L)
assert q==Fraction(qn,qd) and delta==Fraction(bn,bd)>Fraction(1675,32768)
# Bell inequalities are multi-affine; verify all four on all 8 cube vertices.
for typ in range(4):
 signs=([1,1,1] if typ==0 else [1,-1,-1] if typ==1 else [-1,1,-1] if typ==2 else [-1,-1,1])
 for u in (-1,1):
  for v in (-1,1):
   for w in (-1,1):assert 1+signs[0]*u*v+signs[1]*u*w+signs[2]*v*w>=0
print(f'box-SOS cross-check PASS: min margin {min(marg)}, bound {delta}')
