"""Exact verification (Python Fractions) of an antinorm certificate.

Checks, with K' = {A >= 0, A+B >= 0, A+B+C >= 0} (cumulative order):
  0. every z in Z is a nonnegative rational vector with A > 0; 0 < e2 < 1; e1, y > 0;
  (a) for every pair (i, j): T(z_i o z_j - sum_k mu_k z_k) >= 0 with mu a rational
      probability vector (from the stored float combination, rationalised and
      renormalised exactly);
  (b) for m = 0..m0: T(Init(m) - e1 e2^m sum mu z) >= 0, and
      T((y/2, 0, 0) - e1 e2^(m0+1) sum mu z) >= 0  (covers every m > m0, since
      Init(m) >=_K' (y/2,0,0) and e1 e2^m <= e1 e2^(m0+1));
  c = min_z fin(z) > 0.
Conclusion (Lemma F): W_{F,m}(y) >= c e1^s e2^M for every tree F (s vertices) and
every m: V(F) -> Z_{>=0} with sum m = M.
"""
import json, sys
from fractions import Fraction as Fr

def merge(P, Q):
    A, B, C = P; a, b, c = Q
    return (A * (2 * a + b + c), B * (a + b + c / 2) + C * a, C * (b + c / 2))

def Tc(P):
    return (P[0], P[0] + P[1], P[0] + P[1] + P[2])

def ratmu(lst):
    mu = [(k, Fr(v).limit_denominator(10 ** 15)) for k, v in lst]
    s = sum(v for _, v in mu)
    return [(k, v / s) for k, v in mu]

def dominated(p, mu, Z, scale=Fr(1)):
    w = [sum(v * Z[k][d] for k, v in mu) * scale for d in range(3)]
    diff = Tc(tuple(p[d] - w[d] for d in range(3)))
    return all(x >= 0 for x in diff)

def verify(cert):
    y = Fr(*cert['y']); e1 = Fr(*cert['e1']); e2 = Fr(*cert['e2']); m0 = cert['m0']
    Z = [tuple(Fr(*v) for v in z) for z in cert['Z']]
    assert y > 0 and e1 > 0 and 0 < e2 < 1
    assert all(all(v >= 0 for v in z) and z[0] > 0 for z in Z)
    n = len(Z)
    for i in range(n):
        for j in range(n):
            p = merge(Z[i], Z[j])
            mu = ratmu(cert['combos'][f"{i},{j}"])
            assert all(v >= 0 for _, v in mu)
            if not dominated(p, mu, Z):
                return False, f"pair {i},{j}"
    for m in range(m0 + 1):
        p = (y / 2, Fr(0), Fr(1, 2 ** m))
        mu = ratmu(cert['inits'][str(m)])
        if not dominated(p, mu, Z, scale=e1 * e2 ** m):
            return False, f"init {m}"
    p = (y / 2, Fr(0), Fr(0))
    mu = ratmu(cert['inits']['inf'])
    if not dominated(p, mu, Z, scale=e1 * e2 ** (m0 + 1)):
        return False, "init inf"
    c = min(z[0] + z[1] + z[2] / 2 for z in Z)
    assert c > 0
    return True, dict(y=y, e1=e1, e2=e2, c=c, npts=n)

if __name__ == '__main__':
    for f in sys.argv[1:]:
        ok, info = verify(json.load(open(f)))
        print(f, "VERIFIED" if ok else "FAILED", info if not ok else {k: (float(v) if not isinstance(v, int) else v) for k, v in info.items()})