"""[Ancillary helper module, imported by rsc-verify.py.]"""
"""Exact (Fraction) verification of an 8-dim antinorm certificate for the closure tree model.
Certificate JSON fields: y, p, e1, e2 (fraction pairs), m0, Z (list of 8-vectors of fraction pairs),
combos {"i,j": [[k, w], ...]}, inits {"m": [[k,w],...], "inf": ...},
exposure: list of {"m": m, "j": j, "stages": [Y_1, ..., Y_j] (point lists), "combos": [per stage dict]}.
Checks:
 (K) the poset cone K (covers R2>R1>R0, R2>O01>O00, O01>O1>O2; all e_s >= 0) is merge-invariant
     against all unit vectors on the other side, and final is K-monotone;
 (Z) every z >= 0; c = min final(z) > 0;
 (a) for all ordered pairs: T(z_i o z_j) >= T(sum_k w_k z_k) with sum w >= 1;
 (b) Init(m,0)/(e1 e2^m) for m <= m0 and (y/2, p/2, 0..0)/(e1 e2^(m0+1)) dominate combinations with sum >= 1;
 (c) exposure stages: Y_0 = {D_m Init(m)/(e1 e2^m)}; every x o z (x in Y_{i-1}, z in Z) dominates a convex
     combination of Y_i (i < j) or (i = j) a combination of Z with weight sum >= 1.
Conclusion: every completed message of a tree in the closure model with these exposure rules lies in
e1^s e2^M R, hence W_TM' >= c e1^s e2^M."""
import json, sys, itertools
from fractions import Fraction as Fr
from multiprocessing import Pool

NAMES = ['A', 'R0', 'R1', 'R2', 'O00', 'O01', 'O1', 'O2']
IDX = {n: i for i, n in enumerate(NAMES)}
COVERS = [('R2', 'R1'), ('R1', 'R0'), ('R2', 'O01'), ('O01', 'O00'), ('O01', 'O1'), ('O1', 'O2')]

def upsets():
    U = []
    for mask in range(1, 1 << 8):
        S = {s for s in range(8) if mask >> s & 1}
        if all((IDX[b] in S) for (b, w) in COVERS if IDX[w] in S):
            U.append(sorted(S))
    return U
UPS = upsets()

def Tc(P):
    return [sum(P[s] for s in U) for U in UPS]

def merge(P, Q, q):
    A, R0, R1, R2, O00, O01, O1, O2 = P
    a, r0, r1, r2, o00, o01, o1, o2 = Q
    kS = 2 * a + 2 * r1 + 2 * r2 + o00 + o01 + q * (o1 + o2)
    sR, uR = 2 * a, 2 * r2 + o00 + o01 + o1 + q * o2
    sO, xO, uO = a, r2, o00 / 2 + o01 + o1 + q * o2
    return [A * kS, R0 * uR, R1 * uR + R0 * sR, R2 * (uR + sR) + R1 * sR,
            O00 * uO, O01 * (uO + xO) + O00 * xO, O1 * (uO + xO) + (O00 + O01) * sO, O2 * (uO + xO + sO) + O1 * sO]

def final(P, q):
    return P[0] + P[3] + P[4] / 2 + P[5] + P[6] + q * P[7]

def F(v): return Fr(v[0], v[1])

def ratw(lst, den=10 ** 12):
    return [(k, Fr(w).limit_denominator(den)) for k, w in lst if w > 0]

def dominated(P, comb, pts, need=Fr(1)):
    """T(P) >= T(sum w_k pts_k) and sum w >= need."""
    if sum(w for _, w in comb) < need: return False
    S = [sum(w * pts[k][d] for k, w in comb) for d in range(8)]
    TP, TS = Tc(P), Tc(S)
    return all(a >= b for a, b in zip(TP, TS))

def check_cone(q):
    E = [[Fr(int(i == j)) for j in range(8)] for i in range(8)]
    gens = [[E[IDX[b]][d] - E[IDX[w]][d] for d in range(8)] for b, w in COVERS] + E
    fin_ok = all(final(g, q) >= 0 for g in gens)
    for g in gens:
        for e in E:
            if any(x < 0 for x in Tc(merge(g, e, q))): return False
            if any(x < 0 for x in Tc(merge(e, g, q))): return False
    return fin_ok

_G = {}
def _init_worker(Z, q):
    _G['Z'] = Z; _G['q'] = q

def _check_rows(args):
    rows, combos = args
    Z, q = _G['Z'], _G['q']
    for (i, j), comb in zip(rows, combos):
        if not dominated(merge(Z[i], Z[j], q), ratw(comb), Z):
            return (i, j)
    return None

def verify(cert, procs=14):
    y, p, e1, e2 = F(cert['y']), F(cert['p']), F(cert['e1']), F(cert['e2'])
    q = 1 - p
    assert 0 < p <= Fr(1, 2) and y > 0 and e1 > 0 and 0 < e2 < 1
    assert check_cone(q), "cone"
    Z = [[F(v) for v in z] for z in cert['Z']]
    assert all(all(v >= 0 for v in z) for z in Z)
    c = min(final(z, q) for z in Z); assert c > 0
    n = len(Z)
    keys = [(i, j) for i in range(n) for j in range(n)]
    combos = cert['combos']
    tasks = []
    B = 2000
    for s in range(0, len(keys), B):
        ks = keys[s:s + B]
        tasks.append((ks, [combos[f"{i},{j}"] for i, j in ks]))
    with Pool(procs, initializer=_init_worker, initargs=(Z, q)) as pool:
        for r in pool.imap_unordered(_check_rows, tasks):
            if r is not None:
                return False, f"pair {r}"
    m0 = cert['m0']
    for m in range(m0 + 1):
        P = [q ** 0 * y / 2, p / 2, 0, 0, Fr(1, 2 ** m), 0, 0, 0]
        P = [x / (e1 * e2 ** m) for x in P]
        if not dominated(P, ratw(cert['inits'][str(m)]), Z): return False, f"init {m}"
    P = [x / (e1 * e2 ** (m0 + 1)) for x in [y / 2, p / 2, 0, 0, 0, 0, 0, 0]]
    if not dominated(P, ratw(cert['inits']['inf']), Z): return False, "init inf"
    for ex in cert.get('exposure', []):
        m, j = ex['m'], ex['j']
        Y0 = [[x / (e1 * e2 ** m) for x in [q ** m * y / 2, q ** m * p / 2, 0, 0, Fr(1, 2 ** m), 0, 0, 0]]]
        stages = [Y0] + [[[F(v) for v in z] for z in Y] for Y in ex['stages']]
        if j == 0:
            if not dominated(Y0[0], ratw(ex['combos'][0]['0']), Z): return False, f"exposure m={m} j=0"
            continue
        for i in range(1, j + 1):
            prev = stages[i - 1]
            target = stages[i] if i < j else Z
            need = Fr(1) if i == j else Fr(1)
            cmb = ex['combos'][i - 1]
            for a in range(len(prev)):
                for b in range(n):
                    if not dominated(merge(prev[a], Z[b], q), ratw(cmb[f"{a},{b}"]), target, need):
                        return False, f"exposure m={m} stage {i} ({a},{b})"
    return True, dict(y=y, p=p, e1=e1, e2=e2, c=c, npts=n)

if __name__ == '__main__':
    import math
    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()})