"""Board qldpc-open (site key qldpcopen): weight-6 CSS codes ranked by the exact efficiency k d^2 / n inside a size
bracket n <= n_max. SPEC_v2_final s3 with review_final_fable Q1-Q4.

Artifact {"n": n, "HX": [[q, ...], ...], "HZ": [[q, ...], ...], "d": d, "logical": {"type": "X" or "Z", "support": [q, ...]}}.
Validity: 1 <= n <= n_max; 1 <= d <= min(n, d_max); rows are nonempty strictly increasing qubit lists, none repeated
within HX or within HZ, at most max_rows_factor * n rows in total; row weight <= 6; qubit degree (rows of HX and HZ
together containing it) <= 6; HX HZ^T = 0 (mod 2); k = n - rank HX - rank HZ >= 1.
Witness (checked before any search): logical.support is strictly increasing with exactly d entries; an X witness v has
HZ v = 0 and v not in rowspan HX (a Z witness: swap X and Z). So it is a nontrivial logical of weight d and d >= the
true distance min(d_X, d_Z).
Lower bound: the exhaustive search of qldpc.py (imported, unchanged) proves that no nontrivial X or Z logical of weight
<= d - 1 exists (see qldpc.py for the proof of the search and its cover-bound cut). Nontriviality is tested against a
full basis of the conjugate logicals (the whole logical quotient). Schedule (Q1): limits w = 1 .. min(d - 1, 10), both
types at each limit, then w = d - 1 once if d - 1 > 10; w = d - 1 alone is exhaustive, the small limits only find
exaggerated distances early. Together with the witness, d = min(d_X, d_Z) exactly. For d = 1 there is nothing to search.
If the search finds a nontrivial logical of weight < d the artifact is rejected and the reason names it.
Budget: nodes (every DFS entry, both types, all limits) are summed against the instance's node_limit, checked after
every search call (a call cannot be stopped from outside, but a call that ends over the limit gives error whatever it
found, so the verdict is the one of a search stopped at the limit); CPU time (time.process_time) against cpu_seconds
(QARENA_CPU) minus 60 s, polled inside the search. Either limit gives status error, never an accept. The search runs
serially over every root, so no root's work can be missing.
Score: efficiency = k d^2 / n as a reduced fraction {"num", "den"} (lowercase hex) (max), then n (min), then the
largest qubit degree maxdeg (min).
"""
import os
import time
from fractions import Fraction

from common import Reject, exact_keys, want_int, want_list, is_int, load_instance, rank, rref, reduce, popcount, short
from qldpc import parse_rows, logical_basis, search


def parse_support(x, n, d):
    s = want_list(x, "logical.support")
    if len(s) != d:
        raise Reject(f"logical.support must list exactly d = {d} qubits, got {len(s)}")
    prev = -1
    for q in s:
        if not is_int(q) or not 0 <= q < n:
            raise Reject(f"logical.support contains {short(q)}, not a qubit index in [0, {n})")
        if q <= prev:
            raise Reject("logical.support must be strictly increasing")
        prev = q
    return sum(1 << q for q in s)


def schedule(d):
    """Search limits (Q1): 1 .. min(d - 1, 10), then d - 1 once."""
    ws = list(range(1, min(d - 1, 10) + 1))
    if d - 1 > 10:
        ws.append(d - 1)
    return ws


def verify(inst, art, time_budget=None, node_limit=None):
    I = load_instance("qldpcopen", inst)
    n_max, d_max, max_w, max_deg = I["n_max"], I["d_max"], I["max_weight"], I["max_degree"]
    node_limit = I["node_limit"] if node_limit is None else node_limit
    cpu = float(os.environ.get("QARENA_CPU") or I["cpu_seconds"])
    deadline = time.process_time() + (cpu - 60 if time_budget is None else time_budget)
    exact_keys(art, ["n", "HX", "HZ", "d", "logical"])
    n = want_int(art["n"], 1, n_max, f"n (instance {inst} allows n <= {n_max})")
    d = want_int(art["d"], 1, min(n, d_max), f"d (at most min(n, {d_max}))")
    max_rows = I["max_rows_factor"] * n
    HXl = want_list(art["HX"], "HX", max_len=max_rows)
    HZl = want_list(art["HZ"], "HZ", max_len=max_rows)
    if len(HXl) + len(HZl) > max_rows:
        raise Reject(f"more than {max_rows} rows in HX and HZ together")
    lg = art["logical"]
    if not isinstance(lg, dict):
        raise Reject("logical must be an object")
    exact_keys(lg, ["type", "support"], where="logical")
    if not isinstance(lg["type"], str) or lg["type"] not in ("X", "Z"):
        raise Reject(f"logical.type must be \"X\" or \"Z\", got {short(lg['type'])}")
    kind = lg["type"]
    v = parse_support(lg["support"], n, d)
    HX = parse_rows(HXl, n, "HX", max_w)
    HZ = parse_rows(HZl, n, "HZ", max_w)
    deg = [0] * n
    for r in HX + HZ:
        while r:
            low = r & -r
            deg[low.bit_length() - 1] += 1
            r ^= low
    maxdeg = max(deg)
    if maxdeg > max_deg:
        raise Reject(f"qubit {deg.index(maxdeg)} lies in {maxdeg} checks > {max_deg}")
    for i, a in enumerate(HX):
        for j, b in enumerate(HZ):
            if popcount(a & b) & 1:
                raise Reject(f"HX[{i}] and HZ[{j}] anticommute")
    rx, rz = rank(HX), rank(HZ)
    k = n - rx - rz
    if k < 1:
        raise Reject(f"k = {k}: no logical qubits")
    # the witness first (Q4c): a nontrivial logical of weight exactly d
    checks, stabs = (HZ, HX) if kind == "X" else (HX, HZ)
    for i, c in enumerate(checks):
        if popcount(c & v) & 1:
            raise Reject(f"logical ({kind}, weight {d}) has odd overlap with {'HZ' if kind == 'X' else 'HX'}[{i}]: "
                         f"it is not a logical operator")
    if reduce(v, rref(stabs)) == 0:
        raise Reject(f"logical ({kind}, weight {d}) is a product of {'HX' if kind == 'X' else 'HZ'} rows (a stabilizer), "
                     f"not a nontrivial logical")
    # lower bound: no nontrivial logical of weight < d of either type
    zbar = logical_basis(HZ, HX, n)   # Z logicals: ker HX mod rowspace HZ
    xbar = logical_basis(HX, HZ, n)   # X logicals: ker HZ mod rowspace HX
    assert len(zbar) == k and len(xbar) == k
    types = (("X", HZ, zbar, HX), ("Z", HX, xbar, HZ))
    nodes = {"X": 0, "Z": 0}
    ws = schedule(d)
    t0 = time.process_time()
    try:
        for w in ws:
            for t, chk, lgs, st in types:
                x, cnt = search(chk, lgs, n, w, deadline)
                nodes[t] += cnt
                if nodes["X"] + nodes["Z"] > node_limit:
                    return error(f"distance search exceeded the node limit {node_limit}", n, k, d, nodes)
                if x is not None:
                    return reject_witness(t, x, n, d, chk, st)
    except TimeoutError:
        return error("distance search did not finish within the CPU time limit", n, k, d, nodes)
    eff = Fraction(k * d * d, n)
    return {"status": "accepted",
            "score": {"efficiency": {"num": format(eff.numerator, "x"), "den": format(eff.denominator, "x")},
                      "k": k, "d": d, "n": n, "maxdeg": maxdeg},
            "detail": {"n": n, "k": k, "d": d, "rank_HX": rx, "rank_HZ": rz, "max_qubit_degree": maxdeg,
                       "max_check_weight": max((popcount(r) for r in HX + HZ), default=0),
                       "efficiency": f"{eff.numerator}/{eff.denominator}",
                       "distance": (f"exactly {d}: the {kind} witness has weight {d}, and an exhaustive search found no "
                                    f"nontrivial X or Z logical of weight <= {d - 1}" if d > 1 else
                                    "exactly 1: the witness has weight 1"),
                       "search_limits": ws, "search_nodes": nodes,
                       "search_cpu_seconds": round(time.process_time() - t0, 2)}}


def error(reason, n, k, d, nodes):
    return {"status": "error", "detail": {"reason": reason + " (not ranked)", "n": n, "k": k, "d": d, "search_nodes": nodes}}


def reject_witness(kind, x, n, d, checks, stabs):
    # independent recheck of the found vector before reporting it
    assert all(popcount(c & x) % 2 == 0 for c in checks)
    assert reduce(x, rref(stabs)) != 0
    qs = [q for q in range(n) if x >> q & 1]
    assert len(qs) < d
    raise Reject(f"distance below the claimed d = {d}: nontrivial {kind} logical of weight {len(qs)} on qubits {qs}")