"""Independent upper-bound checker. Imports nothing from the solver or oracle
modules: it rebuilds P(n,5) from the definition, replays every stored
chronology in results/upper_bound_witnesses.jsonl force by force (checking
that the source is black, the target white, and the target is the unique
white neighbour of the source), and checks that the final set is V.
Also replays the uniform 12-vertex construction of P7 for 13 <= n <= NMAX.
Writes results/upper_bound_verification.json. Exit code 1 on any failure.
"""
import json
import os
import sys

ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
os.chdir(ROOT)


def petersen_adj(n, k):
    adj = {}
    for i in range(n):
        for a, b in ((("u", i), ("u", (i + 1) % n)), (("u", i), ("v", i)), (("v", i), ("v", (i + k) % n))):
            adj.setdefault(a, set()).add(b)
            adj.setdefault(b, set()).add(a)
    return adj


def parse(lbl):
    return (lbl[0], int(lbl[1:]))


def replay(adj, S, chron):
    black = set(S)
    for idx, (b, w) in enumerate(chron):
        if b not in black or w in black:
            return False, idx
        white = [x for x in adj[b] if x not in black]
        if white != [w]:
            return False, idx
        black.add(w)
    return len(black) == len(adj), None


def p7_chronology(n):
    S = [("u", i) for i in range(12)]
    ch = [(("u", i), ("v", i)) for i in range(1, 11)] + [(("v", 5), ("v", 0)), (("v", 6), ("v", 11))]
    for j in range(12, n):
        ch.append((("u", j - 1), ("u", j)))
        ch.append((("v", j - 5), ("v", j)))
    return S, ch


if __name__ == "__main__":
    nmax = int(sys.argv[1]) if len(sys.argv) > 1 else 60
    report = {"witnesses": [], "P7": []}
    ok_all = True
    path = "results/upper_bound_witnesses.jsonl"
    seen = set()
    if os.path.exists(path):
        for line in open(path):
            w = json.loads(line)
            n = w["n"]
            adj = petersen_adj(n, w["k"])
            S = [parse(s) for s in w["S"]]
            chron = [(parse(a), parse(b)) for a, b in w["chronology"]]
            ok, bad = replay(adj, S, chron)
            ok = ok and len(set(S)) == w["size"] == len(S)
            report["witnesses"].append({"n": n, "size": w["size"], "replay_ok": ok, "first_bad_force": bad, "source": w.get("source")})
            ok_all &= ok
    for n in range(13, nmax + 1):
        adj = petersen_adj(n, 5)
        S, ch = p7_chronology(n)
        ok, bad = replay(adj, S, ch)
        report["P7"].append({"n": n, "replay_ok": ok, "forces": len(ch)})
        ok_all &= ok
    # n = 12: outer layer then spokes
    adj = petersen_adj(12, 5)
    ok, bad = replay(adj, [("u", i) for i in range(12)], [(("u", i), ("v", i)) for i in range(12)])
    report["P7"].insert(0, {"n": 12, "replay_ok": ok, "forces": 12})
    ok_all &= ok
    report["all_ok"] = ok_all
    with open("results/upper_bound_verification.json", "w") as f:
        json.dump(report, f, indent=1)
    print("witness replays: %d, P7 replays: %d, all ok: %s" % (len(report["witnesses"]), len(report["P7"]), ok_all))
    sys.exit(0 if ok_all else 1)