"""The figures the crystallized paper adds up, counts or quotes, which no single gate log holds.

    python code/paper_figures.py          (from lebesgue-verification-xuanheng/; needs data/source/)

Writes data/paper-figures.json. It runs nothing of the programme and recomputes no mathematics; it only
reads what the 68 runs already wrote, and the archive. Its entries are of three kinds and never mixed:

  sums        a sum, a difference, a reciprocal or a sign change of fields of the gate logs; each entry
              names the fields it reads and asserts what it relies on (every leaf certified, no failure).
  counts      counts over the inventory of the 68 reports (crystal/data/inventory.json, by SHA-256), over
              the drill records of the gate logs, and over the input manifest.
  quoted_from_programme
              figures the paper cites from the programme's own documents, as the document writes them,
              with the document, its SHA-256 and the line. Nothing here recomputed them; the shared
              checker counts them apart from recomputed evidence.

Re-run in the recorded environment, the file is byte-identical.
"""
import hashlib
import json
import platform
import re
import sys
from decimal import Decimal
from importlib import metadata
from pathlib import Path

TREE = Path(__file__).resolve().parents[1]
LOGS = TREE / "data" / "gate-logs"
OUT = TREE / "data" / "paper-figures.json"
INVENTORY = TREE / "crystal" / "data" / "inventory.json"
MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json"
sys.path.insert(0, str(TREE / "code"))
import corpus  # noqa: E402


def log(prefix):
    (path,) = LOGS.glob(f"{prefix}-*.json")
    return json.loads(path.read_text(encoding="utf-8"))


def field(prefix, *keys):
    v = log(prefix)
    for k in keys:
        v = v[k]
    return v


def path_of(prefix, *keys):
    return f"{prefix} " + ".".join(str(k) for k in keys)


def certified_sum(parts):
    """parts: [(prefix, keys to a record)]; a record is {area, certified, failures} or a list
    [area, certified, failures, escalated, least]. The sum is of certified leaves, and every leaf must be."""
    total, read = 0, []
    for prefix, keys in parts:
        r = field(prefix, *keys)
        area, cert, fail = (r["area"], r["certified"], r["failures"]) if isinstance(r, dict) else r[:3]
        assert cert == area and fail == 0, (prefix, keys, r)
        total += cert
        read.append(path_of(prefix, *keys))
    return {"value": total, "rule": "sum of certified area leaves; each record has every leaf certified and no failure",
            "reads": read}


def sums():
    s = {}
    s["f3_erosion_area_leaves"] = certified_sum([("run047", ("w4", "c10")), ("run047", ("w4", "c11"))])
    s["root6217_cycles_12_14_area_leaves"] = certified_sum(
        [("run048", ("w4", c)) for c in ("c12", "c13", "c14")])
    s["root6217_cycles_15_17_area_leaves"] = certified_sum(
        [("run049", ("w4", "exact")), ("run049", ("w5", "h131", "exact")), ("run049", ("w5", "h129", "exact"))])
    s["root6217_area_leaves"] = {
        "value": s["root6217_cycles_12_14_area_leaves"]["value"] + s["root6217_cycles_15_17_area_leaves"]["value"],
        "rule": "sum of the two entries above", "reads": ["root6217_cycles_12_14_area_leaves", "root6217_cycles_15_17_area_leaves"]}
    roots = [field("run047", "w1", c) for c in ("c10", "c11")]
    assert all(ok for _, ok in roots)
    s["f3_roots_closed"] = {"value": sum(n for n, _ in roots), "rule": "sum of the root counts of the two erosion certificates",
                            "reads": [path_of("run047", "w1", c) for c in ("c10", "c11")]}
    verts = [field("run037", "w1", c, "vertices")[1] for c in ("47", "48")]
    s["rhcert_stored_vertices"] = {"value": sum(verts), "rule": "sum of the stored vertices of the cell 47 and cell 48 certificates",
                                   "reads": [path_of("run037", "w1", c, "vertices") for c in ("47", "48")]}
    barrier = Decimal(str(field("run049", "w2", "exact")))
    a3 = Decimal(str(find_key(log("run061"), "A3plus")))
    s["barrier_above_A3plus"] = {"value": float(barrier - a3), "rule": "difference, in decimal arithmetic",
                                 "reads": [path_of("run049", "w2", "exact"), "run061 A3plus"]}
    abar = Decimal(find_key(log("run002"), "upper"))
    s["anchored_cover_radius"] = {"value": float(2 * abar), "as_decimal": str(2 * abar),
                                  "rule": "R = 2 times the published upper bound, in decimal arithmetic", "reads": ["run002 upper"]}
    m = field("run057", "w3", "margin_72")
    assert m < 0
    s["subgradient_shortfall_72"] = {"value": -m, "rule": "the negated (negative) margin over 72 directions",
                                     "reads": [path_of("run057", "w3", "margin_72")]}
    r = field("run005", "k5_ratios")
    big = max(r, key=int)
    s["smoothing_bound_over_moment_bound"] = {"value": 1 / r[big], "rule": "reciprocal of the ratio at the largest N logged",
                                              "reads": [path_of("run005", "k5_ratios", big)]}
    return s


def find_key(v, key):
    """the one value under `key` anywhere in a log; refuses if there are several different ones"""
    found = []

    def walk(x):
        if isinstance(x, dict):
            for k, y in x.items():
                if k == key and not isinstance(y, (dict, list)):
                    found.append(y)
                walk(y)
        elif isinstance(x, list):
            for y in x:
                walk(y)
    walk(v)
    assert found and len(set(map(str, found))) == 1, (key, found)
    return found[0]


def counts():
    raw = INVENTORY.read_bytes()
    inv = json.loads(raw)
    items = [i for r in inv for i in r["items"]]

    def first(i):
        a = i.get("audit")
        return re.match(r"relabelled from '([^']+)'", a).group(1) if a else i["strength"]

    def tally(keyf, xs):
        out = {}
        for x in xs:
            out[keyf(x)] = out.get(keyf(x), 0) + 1
        return dict(sorted(out.items()))
    moved = [i for i in items if i.get("audit")]
    inventory = {
        "file": "crystal/data/inventory.json", "sha256": hashlib.sha256(raw).hexdigest(),
        "runs": len(inv), "items": len(items),
        "correction_rows": sum(len(r["corrections"]) for r in inv),
        "open_item_rows": sum(len(r["open_items"]) for r in inv),
        "by_strength": tally(lambda i: i["strength"], items),
        "by_strength_before_audit": tally(first, items),
        "moved_by_audit": len(moved),
        "moves": [{"from": a, "to": b, "items": n} for (a, b), n in
                  sorted(tally(lambda i: (first(i), i["strength"]), moved).items())],
    }
    drill = {"runs": 0, "checks": 0, "plants": 0, "caught_by_named_checks": 0, "controls": 0,
             "controls_undisturbed": 0, "must_stay_green": 0, "must_stay_green_held": 0}
    for p in sorted(LOGS.glob("run*.json")):
        g = json.loads(p.read_text(encoding="utf-8"))
        d = g.get("drill")
        if not isinstance(d, dict) or "plants" not in d:
            continue
        drill["runs"] += 1
        drill["checks"] += len(g.get("checks") or ())
        drill["plants"] += d.get("plants") or 0
        drill["caught_by_named_checks"] += d.get("plants_caught_by_named_checks") or 0
        drill["controls"] += d.get("controls") or 0
        drill["controls_undisturbed"] += d.get("controls_undisturbed") or 0
        drill["must_stay_green"] += d.get("must_stay_green_assertions") or 0
        drill["must_stay_green_held"] += d.get("must_stay_green_held") or 0
    man = json.loads(MANIFEST.read_text(encoding="utf-8"))
    size = sum(leaf[1] for leaf in man["leaves"])
    archive = {"leaves": len(man["leaves"]), "bytes": size, "megabytes": round(size / 10**6, 1),
               "rule": "decimal megabytes, one place"}
    return {"inventory": inventory, "drill": drill, "archive": archive}


def parameters():
    src = (TREE / "code" / "run030_round27_interval_replay.py").read_text(encoding="utf-8")
    bits = int(re.search(r"^P = (\d+)$", src, re.M).group(1))
    assert re.search(r"^ONE = 1 << P$", src, re.M)
    return {"integer_interval_bits": {"value": bits, "reads": "code/run030_round27_interval_replay.py: ONE = 1 << P",
                                      "used_by": ["run030", "run031", "run045", "run047"]}}


def environment():
    def series(v):
        return ".".join(v.split(".")[:2])
    full = {"python": platform.python_version(), **{m: metadata.version(m) for m in ("mpmath", "numpy", "sympy")}}
    return {"about": "the interpreter and libraries this file was written with", "versions": full,
            "series": {k: series(v) for k, v in full.items()}}


# what the paper quotes from the programme: (figure, document file name, text as the document writes it)
QUOTES = [
    ("tight reference A_ref (Cycle 16)", "UESFCM_Lebesgue_Cycle_16_Tight_Reference_and_Local_Secant_v0.1.md", "0.8349865"),
    ("stated slack of the tight reference (Cycle 16)", "UESFCM_Lebesgue_Cycle_16_Tight_Reference_and_Local_Secant_v0.1.md",
     "6.5385446698911637e-08"),
    ("separator constant s_7 (Cycle 03)", "UESFCM_Lebesgue_Cycle_03_Orbit_Localization_and_Scalar_Closure_v0.1.md", "0.00938484"),
    ("least centre area of the global pilot (Round 16)", "AMRAL_Lebesgue_Finite_Closure_Round_16_Global_Pilot_v0.1.md",
     "0.8356828349502634"),
    ("area inflation bound beta as used (Round 04 package)", "AMRAL_LUC_FC_Round_04_VALIDATION.json", "0.9063953966591665"),
    ("lens growth coefficient (BCODR LUC 04)", "BCODR_LUC_04_True_Overlap_Germ_Tangent_Decomposition_v0.1.md", "0.747599042164318"),
    ("far-branch gradient g_3, whose negative is the multiplier eta_3 by the document's g_3 + eta_3 = 0 (LESR Paper 07)",
     "LESR_Paper07_Root6217_Barrier_Shape_Reconstruction_v0.1.md", "-0.122791062735083228947666632271676747712689174"),
    ("the document's equation for the multiplier (LESR Paper 07)", "LESR_Paper07_Root6217_Barrier_Shape_Reconstruction_v0.1.md",
     r"g_3+\eta_3=0"),
    ("A_ref - m(0) (LESR Paper 08)", "LESR_Paper08_Positive_Rotation_Certificate_Reduction_v0.1.md", r"3.8944077590\times10^{-7}"),
]


def quotes():
    names = {name for _, name, _ in QUOTES}
    blobs = {n: corpus.source_bytes(n) for n in corpus.SOURCES}
    assert not corpus.check_pins(blobs), corpus.check_pins(blobs)
    docs = {}
    for leaf, data in corpus.walk_sources(blobs, keep=lambda leaf: leaf.name in names):
        if data is not None:
            assert leaf.name not in docs, f"two leaves named {leaf.name}"
            docs[leaf.name] = (leaf, data.decode("utf-8"))
    out = []
    for figure, name, text in QUOTES:
        leaf, body = docs[name]
        hits = [(n, line) for n, line in enumerate(body.splitlines(), 1) if text in line]
        assert hits, (name, text)
        n, line = hits[0]
        i = line.index(text)
        q = {"as_written": text, "line": line[max(0, i - 100):i + len(text) + 60].strip()}
        sci = re.fullmatch(r"(-?\d+\.\d+)\\times10\^\{(-?\d+)\}", text)
        if sci:
            q["reads_as"] = f"{sci.group(1)}e{sci.group(2)}"        # the same figure in e-notation
        out.append({"figure": figure, "document": leaf.id, "document_sha256": leaf.sha256, "at": f"L{n}",
                    "quoted_from_programme": q})
    # the document's own equation g_3 + eta_3 = 0 turns its g_3 into the multiplier the paper names
    g3 = next(x for x in out if x["figure"].startswith("far-branch gradient g_3"))
    assert any(x["quoted_from_programme"]["as_written"] == r"g_3+\eta_3=0" for x in out)
    g3["quoted_from_programme"]["implies"] = {"eta_3": g3["quoted_from_programme"]["as_written"].lstrip("-")}
    return out


def main():
    figures = {"schema": "lebesgue-paper-figures.v1",
               "about": "figures of the crystallized paper that no single gate log holds; see code/paper_figures.py",
               "sums": sums(), **counts(), "parameters": parameters(), "environment": environment(),
               "quotes": quotes()}
    OUT.write_text(json.dumps(figures, ensure_ascii=False, indent=1) + "\n", encoding="utf-8", newline="\n")
    print("wrote", OUT.relative_to(TREE).as_posix())
    for k, v in figures["sums"].items():
        print(f"  {k:40} {v['value']}")
    print("  inventory", {k: figures["inventory"][k] for k in ("runs", "items", "correction_rows", "moved_by_audit")})
    print("  drill", figures["drill"])
    print("  archive", figures["archive"])
    print("  quotes", len(figures["quotes"]))


if __name__ == "__main__":
    main()