"""Stage 5: independent replay of every stored upper-bound witness and of the
P7 chronology, with a closure routine written from scratch (no import of
code/closure_oracle.py or code/graph_constructor.py).

Checks, per witness record in results/upper_bound_witnesses.jsonl:
  * the graph is P(n,5) rebuilt here from definition D1;
  * every stored force b -> w is legal at the moment it is applied
    (b black, w white, w the unique white neighbour of b);
  * the chronology ends with all 2n vertices black;
  * |S| equals the recorded size and the recorded Z upper bound in
    results/exact_values.csv;
  * independently, cl(S) = V by the from-scratch closure.
P7: for 12 <= n <= 300, generates the chronology exactly as written in the
proof of P7 (results/derivations.md) and replays it with the same legality
checker.
Output: results/robustness/witness_replay.json
"""
import csv
import json
import os
import sys

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


def petersen(n, k):
    adj = {}
    for i in range(n):
        adj.setdefault(("u", i), set()).update({("u", (i + 1) % n), ("u", (i - 1) % n), ("v", i)})
        adj.setdefault(("v", i), set()).update({("v", (i + k) % n), ("v", (i - k) % n), ("u", i)})
    assert len(adj) == 2 * n and all(len(s) == 3 for s in adj.values())
    assert all(a in adj[b] for a in adj for b in adj[a])
    return adj


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


def replay(adj, S, chronology):
    black = set(S)
    for src, tgt in chronology:
        b, w = parse(src), parse(tgt)
        if b not in black:
            return False, "source %s not black" % src
        if w in black:
            return False, "target %s already black" % tgt
        white = [x for x in adj[b] if x not in black]
        if white != [w] and set(white) != {w}:
            return False, "force %s->%s illegal: white nbrs %s" % (src, tgt, white)
        black.add(w)
    return len(black) == len(adj), "ended with %d black of %d" % (len(black), len(adj))


def closure(adj, S):
    black = set(S)
    changed = True
    while changed:
        changed = False
        for b in list(black):
            white = [x for x in adj[b] if x not in black]
            if len(white) == 1:
                black.add(white[0])
                changed = True
    return black


def p7_chronology(n):
    chron = []
    if n == 12:
        return [("u%d" % i, "v%d" % i) for i in range(12)]
    for i in range(1, 11):
        chron.append(("u%d" % i, "v%d" % i))
    chron.append(("v5", "v0"))
    chron.append(("v6", "v11"))
    for j in range(12, n):
        chron.append(("u%d" % (j - 1), "u%d" % j))
        chron.append(("v%d" % (j - 5), "v%d" % j))
    return chron


def main():
    Z = {int(r["n"]): int(r["Z"]) for r in csv.DictReader(open("results/exact_values.csv"))}
    out = {"witnesses": [], "P7": []}
    allok = True
    for line in open("results/upper_bound_witnesses.jsonl"):
        r = json.loads(line)
        n, k = r["n"], r["k"]
        adj = petersen(n, k)
        S = [parse(x) for x in r["S"]]
        ok1, msg = replay(adj, S, r["chronology"]) if r.get("chronology") else (None, "no chronology stored")
        ok2 = closure(adj, S) == set(adj)
        # A valid forcing set smaller than the tabulated Z would refute the table; larger
        # witnesses (intermediate steps of the fort-cover descent) are legitimate.
        rec = {"n": n, "size": len(set(S)), "recorded_size": r.get("size"), "Z_table": Z.get(n), "chronology_ok": ok1,
               "chronology_msg": msg, "closure_ok": ok2, "size_matches_Z": len(set(S)) == Z.get(n),
               "size_below_Z_would_refute": len(set(S)) < Z.get(n), "source": r.get("source")}
        rec["ok"] = bool(ok2) and (ok1 is not False) and not rec["size_below_Z_would_refute"]
        allok &= rec["ok"]
        out["witnesses"].append(rec)
    out["n_with_size_Z_witness"] = sorted({w["n"] for w in out["witnesses"] if w["size_matches_Z"] and w["closure_ok"]})
    out["n_in_table_up_to_27_missing_size_Z_witness"] = [n for n in range(11, 28) if n not in out["n_with_size_Z_witness"] and Z.get(n) != 12]
    for n in range(12, 301):
        adj = petersen(n, 5)
        S = [("u", i) for i in range(12)]
        ok, msg = replay(adj, S, p7_chronology(n))
        out["P7"].append({"n": n, "ok": ok, "msg": msg})
        allok &= ok
    out["all_ok"] = allok
    out["num_witnesses"] = len(out["witnesses"])
    out["P7_range"] = [12, 300]
    json.dump(out, open("results/robustness/witness_replay.json", "w"), indent=1)
    print("witnesses:", len(out["witnesses"]), "all ok:", all(w["ok"] for w in out["witnesses"]))
    print("P7 chronology replays 12..300 all ok:", all(p["ok"] for p in out["P7"]))
    bad = [w for w in out["witnesses"] if not w["ok"]]
    for w in bad:
        print("BAD", w)
    return 0 if allok else 1


if __name__ == "__main__":
    sys.exit(main())