"""
verify_construction.py -- test the constructive proof of Section 5.

1. Every sporadic graph has the stated count (cg.c_brute and cg.c_esu).
2. The base certificate is re-checked line by line by an independent reader
   (pure arithmetic plus "operand already established" checks).
3. For every k in [17, KALL] and for random k up to 2^RAND_BITS, the graph
   realize(k) is built; it is checked to be a simple connected graph, and its
   number of connected sets is counted by the independent C program count_c.
4. For every m in [8, 16] and every v in [m, 2^m - 1], graph_lambda(m, v) has
   exactly m vertices; for v >= 2^(m-1) it is connected; its count is v
   (C program, for m <= 16).
5. Without the sporadic graphs of order m (m = 5, 6, 7), rules (C) and (N)
   leave exactly the gaps stated in Remark 5.5 of the note.
"""

import os
import random
import subprocess
import sys

from cg import adj_from_edges, c_brute, c_esu, is_connected
from construct import SPORADIC, realize, graph_lambda, rule_gaps

HERE = os.path.dirname(os.path.abspath(__file__))
DATA = os.path.join(HERE, "..", "data")
KALL = int(sys.argv[1]) if len(sys.argv) > 1 else 70000
RAND_BITS = int(sys.argv[2]) if len(sys.argv) > 2 else 26


def check_simple(G):
    n, edges = G
    seen = set()
    for a, b in edges:
        assert 0 <= a < n and 0 <= b < n and a != b, (a, b, n)
        key = (min(a, b), max(a, b))
        assert key not in seen, ("multi-edge", key)
        seen.add(key)


def run_counter(graphs):
    lines = []
    for n, edges in graphs:
        lines.append(f"{n} {len(edges)} " + " ".join(f"{a} {b}" for a, b in edges))
    out = subprocess.run([os.path.join(HERE, "count_c")], input="\n".join(lines) + "\n",
                         capture_output=True, text=True, check=True).stdout.split()
    return [None if x == "SKIP" else int(x) for x in out]


def check_certificate():
    L = {0: {0}}
    V = {}
    T = 0
    with open(os.path.join(DATA, "base_certificate.txt")) as f:
        for line in f:
            line = line.strip()
            if not line or line.startswith("#"):
                continue
            head, der = line.split(":")
            mpart, kind, val = head.split()
            m = int(mpart[2:])
            val = int(val)
            tok = der.split()
            V.setdefault(m, set())
            L.setdefault(m, set())
            if kind == "V":
                if tok[0] == "single":
                    assert m == 1 and val == 1
                elif tok[0] == "S":
                    assert SPORADIC[val][0] == m
                elif tok[0] == "C":
                    x = int(tok[1])
                    assert x in L[m - 1] and val == 2 ** (m - 1) + x
                elif tok[0] == "N":
                    d, r, x = map(int, tok[1:])
                    assert d >= 1 and r >= 0 and d + r + 2 == m and x in L[r]
                    assert val == 2 ** (m - 1) - 2 ** r + 2 ** d + d + x
                else:
                    raise ValueError(line)
                V[m].add(val)
            else:
                if tok[0] == "V":
                    assert val in V[m]
                else:
                    a, x, y = map(int, tok[1:])
                    assert 1 <= a < m and x in V[a] and y in L[m - a] and val == x + y
                L[m].add(val)
            T += 1
    return V, L, T


def main():
    os.makedirs(DATA, exist_ok=True)
    report = []

    # 1. sporadic graphs
    for val, (n, edges, desc, hand) in sorted(SPORADIC.items()):
        adj = adj_from_edges(n, edges)
        assert is_connected(adj) and c_brute(adj) == val == c_esu(adj), val
    report.append(f"1. the {len(SPORADIC)} sporadic graphs have the stated counts (brute force and ESU)")

    # 2. certificate
    V, L, T = check_certificate()
    assert L[7] >= set(range(7, 128))
    assert V[6] >= set(range(32, 64)) and V[7] >= set(range(64, 128))
    assert V[5] >= set(range(17, 32)) - {25}
    report.append(f"2. base certificate re-checked ({T} derivation lines): Lambda_7 contains [7,127]; "
                  f"V_5 contains [17,31] minus 25; V_6 contains [32,63]; V_7 contains [64,127]")

    # 3. realize(k)
    ks = list(range(17, KALL + 1))
    rng = random.Random(12345)
    ks += [rng.randrange(KALL + 1, 2 ** RAND_BITS) for _ in range(300)]
    batch = []
    for k in ks:
        G = realize(k)
        check_simple(G)
        assert is_connected(adj_from_edges(*G)) if G[0] <= 400 else True
        batch.append((k, G))
    counts = run_counter([G for _, G in batch])
    bad = [(k, c) for (k, _), c in zip(batch, counts) if c != k]
    assert not bad, bad[:10]
    maxn = max(G[0] for _, G in batch)
    report.append(f"3. realize(k) built and counted by count_c for every k in [17,{KALL}] and 300 random k "
                  f"< 2^{RAND_BITS}: all correct (largest graph: {maxn} vertices)")

    # 4. graph_lambda for m in [8,16]
    total = 0
    for m in range(8, 17):
        graphs = []
        for v in range(m, 2 ** m):
            G = graph_lambda(m, v)
            check_simple(G)
            assert G[0] == m
            if v >= 2 ** (m - 1):
                assert is_connected(adj_from_edges(*G))
            graphs.append(G)
        counts = run_counter(graphs)
        assert counts == list(range(m, 2 ** m)), m
        total += len(graphs)
    report.append(f"4. for every m in [8,16] and every v in [m, 2^m-1], graph_lambda(m,v) has exactly m "
                  f"vertices, is connected when v >= 2^(m-1), and has count v ({total} graphs)")

    # 5. the gaps filled by the sporadic graphs (Remark 5.5)
    gaps = {m: rule_gaps(m) for m in (5, 6, 7)}
    assert gaps == {5: [19, 25], 6: [32, 35, 57], 7: [67, 90]}, gaps
    report.append("5. without the sporadic graphs of order m (but with those of smaller order), rules (C) and (N) "
                  f"leave in [17,31] (m=5): {gaps[5]}; in [32,63] (m=6): {gaps[6]}; in [64,127] (m=7): {gaps[7]}")

    with open(os.path.join(DATA, "construction_check.txt"), "w") as f:
        f.write("\n".join(report) + "\n")
    print("\n".join(report))


if __name__ == "__main__":
    main()