"""RUN-013 - Round 10: the reference dry run, replayed.

Round 10 runs Round 08's grammar end to end on a tiny base neighbourhood of the seed:
four base leaves, each lifted by B7 over its whole root, emitted as one-bit DFS
streams and replayed by the package's verifier. Here the streams are decoded, their
boxes regenerated, every leaf bounded again with the exact common core, the package's
own 96-direction bound rebuilt and the four streams re-emitted from it byte for byte,
and the trees re-emitted with the exact bound to see what the sampling costs.

Checks
  A0 anchors      the numbers below occur in Round 10 as written
  W1 domain       sec. 1-3: the base centre is Round 07's seed with phi_5 normalised; the
                  four base leaves, none of which the base can prune; B7's root
  W2 streams      sec. 8-9, 14: the .bin streams decode (MSB first, DFS pre-order, 1 = split);
                  counts, depths, N = 2L - 1, zero padding, SHA-256
  W3 replay       sec. 4-5, 9-11: the boxes regenerated (argmin delta_7, ties to the earlier
                  of phi, x, y; the lower child first); every leaf's exact common core
                  clears 0.835; the other tie-break and child order fail
  W4 emission     sec. 5, 7, 15: the text's bound (contact points of each core in 96
                  directions, the inscribed 96-gon) rebuilt; the worst verified slacks; the
                  four streams re-emitted byte for byte
  W5 cost         the four trees re-emitted with the exact core bound instead
  P1 package      manifest and verification summary against the text and each other
  P2 package      the package's self-description of its files matches the archive
  R1 registry     Round 10's judgments reviewed, first-used statuses defined

Usage: python code/run013_round10_reference_dry_run.py [--drill] [--blind CID]
"""
import argparse
import hashlib
import inspect
import json
import math
import re

import numpy as np
from scipy.spatial import ConvexHull

import gate
import registry
from corpus import SOURCES, TREE, source_bytes, walk_sources
from run009_round06_witness_exchange import hull_pieces, placed_disc
from run010_round07_minimizer_atlas import d_star, t_text
from run011_round08_conditional_lift import motion_delta, placed_vertices
from run012_round09_adaptive_atlas import base_pieces, core_pieces, piece_arrays, support_matrix

PKG = "main.zip!/AMRAL_LUC_FC_Round_10_Package_v0.1.zip!/"
CERT = PKG + "AMRAL_LUC_FC_Round_10_reference_cert/"
DOC = PKG + "AMRAL_Lebesgue_Finite_Closure_Round_10_Reference_Dry_Run_v0.1.md"
CRYSTAL = PKG + "AMRAL_LUC_FC_State_Crystal_Round_10_v0.1.md"
VALIDATION = PKG + "AMRAL_LUC_FC_Round_10_VALIDATION.json"
EMITTER = PKG + "AMRAL_LUC_FC_Round_10_reference_emitter.py"
VERIFIER = PKG + "AMRAL_LUC_FC_Round_10_reference_verifier.py"
CERT_MANIFEST = CERT + "manifest.json"
SUMMARY = CERT + "verification_summary.json"
TREES = ("00", "01", "10", "11")
BINS = {k: CERT + f"lift_{k}.bin" for k in TREES}
ROUND07 = TREE / "data" / "external" / "round07-citations.json"
LOG = TREE / "data" / "gate-logs" / "run013-round10-reference-dry-run.json"
CACHE = TREE / "data" / "cache" / "run013-replay.json"
MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json"

T1 = 0.835
R3, R5, R7 = (1 / (2 * math.cos(math.pi / (2 * n))) for n in (3, 5, 7))

ANCHORS = {
    "W1": [r"x_3=-0.01215883209899,", r"y_3\approx-3.7082\times10^{-8},", r"\phi_5\approx2.4128951083\times10^{-5},",
           r"x_5=0.02299660691706,", r"y_5\approx-3.89698\times10^{-6}.",
           r"(4\times10^{-5},4\times10^{-5},4\times10^{-4},4\times10^{-5},4\times10^{-5}).", r"\phi_7\in[0,2\pi/7),",
           r"x_7,y_7\in[-0.19693504677116785,\+0.19693504677116785]."],
    "W2": [r"|`00`|2833|1417|21|", r"|`01`|2853|1427|21|", r"|`10`|2833|1417|21|", r"|`11`|2853|1427|21|",
           r"11372\text{liftnodes}", r"5688\text{liftleaves}", r"N=2L-1."],
    "W3": [r"\delta_7=\sqrt{h_x^2+h_y^2}+2R_7\sin\frac{h_\phi}{2}.", r"a^\star=\arg\min_a\delta_7^{(a)}."],
    "W4": [r"$$96$$個法向方向取verifiedboundarycontactpoints", r"$$96$$點inscribedpolygon",
           r"T_{\rmsearch}=0.8350002.", r"e_{\rmdry}=10^{-8}.", r"A_{\rmverify}-e_{\rmdry}\ge0.835."],
}


# ---------------------------------------------------------------- streams and boxes

def bits_of(data):
    return [(b >> (7 - i)) & 1 for b in data for i in range(8)]


def pack(bits):
    bits = list(bits) + [0] * (-len(bits) % 8)
    return bytes(int("".join(map(str, bits[i:i + 8])), 2) for i in range(0, len(bits), 8))


def parse(bits):
    """a one-bit DFS pre-order stream: (nodes, leaves, max depth, bits consumed), or None
    if the stream ends early"""
    pos, nodes, leaves, depth, stack = 0, 0, 0, 0, [0]
    while stack:
        d = stack.pop()
        if pos >= len(bits):
            return None
        b, pos, nodes, depth = bits[pos], pos + 1, nodes + 1, max(depth, d)
        if b:
            stack += [d + 1, d + 1]
        else:
            leaves += 1
    return nodes, leaves, depth, pos


def base_leaves(center, half):
    """sec. 2: halve phi_5, then x_5 in each child; leaf id = (phi_5 child, x_5 child), 0 = lower"""
    out = {}
    for i in (0, 1):
        for j in (0, 1):
            c, h = np.array(center, dtype=float), np.array(half, dtype=float)
            h[2] /= 2
            c[2] += (2 * i - 1) * h[2]
            h[3] /= 2
            c[3] += (2 * j - 1) * h[3]
            out[f"{i}{j}"] = (c, h)
    return out


def delta7(h):
    return motion_delta(h[1], h[2], h[0], R7)


def split_axis(h, order):
    """sec. 4: the axis whose halving leaves the smallest motion radius; a tie goes to the
    axis earlier in `order`"""
    best = None
    for a in order:
        c = np.array(h, dtype=float)
        c[a] /= 2
        v = delta7(c)
        if best is None or v < best[0]:
            best = (v, a)
    return best[1]


def children(c, h, a):
    hh = np.array(h, dtype=float)
    hh[a] /= 2
    lo, hi = np.array(c, dtype=float), np.array(c, dtype=float)
    lo[a] -= hh[a]
    hi[a] += hh[a]
    return (lo, hh), (hi, hh)


def replay(bits, root, rule):
    """the leaves of a stream, as (centre, half-width) boxes of (phi_7, x_7, y_7)"""
    pos, stack = 0, [root]
    while stack:
        c, h = stack.pop()
        b, pos = bits[pos], pos + 1
        if b:
            lo, hi = children(c, h, split_axis(h, rule["order"]))
            stack += [hi, lo] if rule["low_first"] else [lo, hi]       # the last pushed is read next
        else:
            yield c, h


def emit(bound, root, order, threshold, max_depth=24):
    """sec. 15: a leaf when the bound clears the search threshold, else split; None past
    the depth limit"""
    bits, stack = [], [(root[0], root[1], 0)]
    while stack:
        c, h, d = stack.pop()
        if bound(c, h) >= threshold:
            bits.append(0)
            continue
        if d >= max_depth:
            return None
        bits.append(1)
        lo, hi = children(c, h, split_axis(h, order))
        stack += [(hi[0], hi[1], d + 1), (lo[0], lo[1], d + 1)]
    return bits


# ---------------------------------------------------------------- leaf bounds

def leaf_cores(q, qh, x, g, core_radius):
    d3 = motion_delta(qh[0], qh[1], 0.0, R3)
    d5 = motion_delta(qh[3], qh[4], qh[2], R5)
    d7 = motion_delta(g[1], g[2], g[0], R7)
    return ((placed_vertices(3, 0.0, q[:2]), core_radius(d3)), (placed_vertices(5, q[2], q[3:5]), core_radius(d5)),
            (placed_vertices(7, x[0], x[1:3]), core_radius(d7)))


def exact_bound(q, qh, x, g, core_radius=lambda d: 1 - d):
    """the area of conv(D, C_3, C_5, C_7), exactly; -inf if a core is empty"""
    pieces = placed_disc()
    for V, rho in leaf_cores(q, qh, x, g, core_radius):
        if rho <= 1 / (2 * math.cos(math.pi / (2 * len(V)))):
            return -math.inf
        pieces = pieces + core_pieces(V, rho)[0]
    return hull_pieces(pieces, 2048)[0]


def contact_points(pieces, th):
    C, rho, ranged = piece_arrays(pieces)
    k = np.argmax(support_matrix(C, rho, ranged, th), axis=0)
    return C[k] + rho[k][:, None] * np.stack([np.cos(th), np.sin(th)], axis=1)


def sampled_bound(q, qh, x, g, n=96):
    """sec. 5: the hull of the inscribed n-gon of the disc and of each core's contact
    points in the same n directions"""
    th = 2 * np.pi * np.arange(n) / n
    pts = [0.5 * np.stack([np.cos(th), np.sin(th)], axis=1)]
    for V, rho in leaf_cores(q, qh, x, g, lambda d: 1 - d):
        pts.append(contact_points(core_pieces(V, rho)[0], th))
    return float(ConvexHull(np.vstack(pts)).volume)


# ---------------------------------------------------------------- the canonical replay, cached

CANON = {"order": (0, 1, 2), "low_first": True}


def _code_key(blobs, man):
    digest = hashlib.sha256(json.dumps([man["search_threshold"], man["witness"], man["base_domain"]]).encode())
    for fn in (bits_of, pack, parse, base_leaves, delta7, split_axis, children, replay, emit, leaf_cores,
               exact_bound, contact_points, sampled_bound, canonical):
        digest.update(inspect.getsource(fn).encode())
    for k in TREES:
        digest.update(blobs[k])
    return digest.hexdigest()


def canonical(world):
    """per tree: the exact bound at every leaf under the canonical rule; the sampled bound's
    worst verified slack; the streams re-emitted from the sampled and from the exact bound;
    and, for tree 00, how many leaves fail under the other tie-break and child order"""
    man = world["cert_manifest"]
    root = (np.array(man["witness"]["root_center"]), np.array(man["witness"]["root_halfwidth"]))
    leaves = base_leaves(man["base_domain"]["center"], man["base_domain"]["halfwidth"])
    out = {}
    for k in TREES:
        q, qh = leaves[k]
        bits = bits_of(world["bins"][k])
        exact = [exact_bound(q, qh, c, h) for c, h in replay(bits, root, CANON)]
        sampled = [sampled_bound(q, qh, c, h) for c, h in replay(bits, root, CANON)]
        ts = man["search_threshold"]
        re_sampled = emit(lambda c, h: sampled_bound(q, qh, c, h), root, CANON["order"], ts)
        re_exact = emit(lambda c, h: exact_bound(q, qh, c, h), root, CANON["order"], ts)
        out[k] = {"exact_worst_slack": float(min(exact) - T1), "exact_failures": int(sum(a < T1 for a in exact)),
                  "sampled_worst_area": float(min(sampled)),
                  "sampled_reemitted_hex": pack(re_sampled).hex() if re_sampled else None,
                  "exact_reemitted": parse(re_exact)[:3] if re_exact else None}
    q, qh = leaves["00"]
    bits = bits_of(world["bins"]["00"])
    out["alternatives_tree_00"] = {
        name: int(sum(exact_bound(q, qh, c, h) < T1 for c, h in replay(bits, root, rule)))
        for name, rule in (("y before x", {"order": (0, 2, 1), "low_first": True}),
                           ("higher child first", {"order": (0, 1, 2), "low_first": False}))}
    return out


_CANON, ARCHIVE_KEY = {}, []


def canonical_results(world):
    """computed once per input; kept on disk only for the archive's own inputs, so a
    drill plant never overwrites it"""
    key = _code_key(world["bins"], world["cert_manifest"])
    if key not in _CANON:
        if CACHE.exists():
            cached = json.loads(CACHE.read_text(encoding="utf-8"))
            if cached.get("key") == key:
                _CANON[key] = cached["results"]
        if key not in _CANON:
            _CANON[key] = canonical(world)
            if key in ARCHIVE_KEY:
                CACHE.parent.mkdir(parents=True, exist_ok=True)
                CACHE.write_text(json.dumps({"key": key, "results": _CANON[key]}, indent=1) + "\n", encoding="utf-8")
    return _CANON[key]


# ---------------------------------------------------------------- checks

def w1_domain(w):
    out, man = [], w["cert_manifest"]
    seed = np.array(w["round07"]["repository"]["reuleaux"]["placement"], dtype=float)
    seed[2] %= 2 * math.pi / 5
    center, half = np.array(man["base_domain"]["center"]), np.array(man["base_domain"]["halfwidth"])
    if np.max(np.abs(center - seed)) > 1e-15:
        out.append("the base centre is not Round 07's seed with phi_5 normalised")
    if list(half) != w["base_halfwidth"]:
        out.append(f"base half-widths {list(half)}, text {w['base_halfwidth']}")
    t7 = t_text(7, d_star(T1))
    if abs(t7 - w["t7"]) > 5e-13 or abs(man["witness"]["root_halfwidth"][1] - t7) > 5e-13 \
            or abs(man["witness"]["rotation_period"] - 2 * math.pi / 7) > 1e-15 \
            or abs(man["witness"]["root_center"][0] - math.pi / 7) > 1e-15:
        out.append(f"B7's root differs from Round 08's: t_7 = {t7!r}")
    pruned, rows = {}, {}
    for k, (q, qh) in base_leaves(center, half).items():
        d3, d5 = motion_delta(qh[0], qh[1], 0.0, R3), motion_delta(qh[3], qh[4], qh[2], R5)
        pieces = placed_disc() + core_pieces(placed_vertices(3, 0.0, q[:2]), 1 - d3)[0] \
            + core_pieces(placed_vertices(5, q[2], q[3:5]), 1 - d5)[0]
        core = hull_pieces(pieces, 2048)[0]
        rows[k] = {"base_area_at_centre": hull_pieces(base_pieces(q), 2048)[0], "base_core_bound": core}
        pruned[k] = core >= T1
    if pruned != w["base_pruned"]:
        out.append(f"base pruning {pruned}, recorded {w['base_pruned']}")
    root_volume = (2 * t_text(3, d_star(T1))) ** 2 * (2 * math.pi / 5) * (2 * t_text(5, d_star(T1))) ** 2
    w["w1"] = {"base_leaves": rows, "volume_fraction_of_root": float(np.prod(2 * half)) / root_volume}
    return out


def w2_streams(w):
    out, man, got = [], w["cert_manifest"], {}
    listed = {c["base_cell_id"]: c for c in man["lift_certificates"]}
    for k in TREES:
        data = w["bins"][k]
        bits = bits_of(data)
        p = parse(bits)
        if p is None:
            out.append(f"tree {k}: the stream ends early")
            continue
        nodes, leaves, depth, used = p
        got[k] = (nodes, leaves, depth)
        rest = bits[used:]
        if len(rest) >= 8 or any(rest):
            out.append(f"tree {k}: {len(rest)} bits after the tree, not all padding zeros")
        if nodes != 2 * leaves - 1:
            out.append(f"tree {k}: {nodes} nodes, {leaves} leaves")
        if tuple(w["tree_table"][k]) != got[k] or (listed[k]["nodes"], listed[k]["leaves"], listed[k]["max_depth"]) != got[k]:
            out.append(f"tree {k}: decoded {got[k]}, text {w['tree_table'][k]}, manifest "
                       f"{(listed[k]['nodes'], listed[k]['leaves'], listed[k]['max_depth'])}")
        if hashlib.sha256(data).hexdigest() != listed[k]["sha256"]:
            out.append(f"tree {k}: SHA-256 differs from the manifest")
        if depth > man["max_depth"]:
            out.append(f"tree {k}: depth {depth} beyond the manifest's limit")
    totals = (sum(v[0] for v in got.values()), sum(v[1] for v in got.values()))
    if totals != tuple(w["totals"]):
        out.append(f"totals {totals}, text {w['totals']}")
    w["w2"] = {"decoded": got, "totals": totals}
    return out


def w3_replay(w):
    out, man = [], w["cert_manifest"]
    root = (np.array(man["witness"]["root_center"]), np.array(man["witness"]["root_halfwidth"]))
    leaves = base_leaves(man["base_domain"]["center"], man["base_domain"]["halfwidth"])
    if w["replay_rule"] == CANON and w["core_radius"](0.25) == 0.75 and w["core_radius"](0.5) == 0.5:
        res = canonical_results(w)
        rows = {k: {"exact_worst_slack": res[k]["exact_worst_slack"], "exact_failures": res[k]["exact_failures"]}
                for k in TREES}
        alternatives = res["alternatives_tree_00"]
    else:                                        # a changed rule: replay directly, stopping early
        rows, alternatives = {}, None
        for k in TREES:
            q, qh = leaves[k]
            fails, worst = 0, math.inf
            for c, h in replay(bits_of(w["bins"][k]), root, w["replay_rule"]):
                a = exact_bound(q, qh, c, h, w["core_radius"])
                worst = min(worst, a - T1)
                fails += a < T1
                if fails >= 3:
                    break
            rows[k] = {"exact_worst_slack": worst, "exact_failures": fails}
            if fails:
                break
    for k, r in rows.items():
        if r["exact_failures"]:
            out.append(f"tree {k}: {r['exact_failures']} leaves below 0.835 by the exact core")
    if alternatives is not None and not all(v > 0 for v in alternatives.values()):
        out.append(f"another tie-break or child order also replays: {alternatives}")
    w["w3"] = {"trees": rows, "alternatives_tree_00_failing_leaves": alternatives}
    return out


def w4_emission(w):
    out, man = [], w["cert_manifest"]
    per = {p["base_cell_id"]: p for p in w["summary"]["per_leaf"]}
    if w["sample_n"] == 96:
        res = canonical_results(w)
        rows = {k: {"worst_verified_slack": res[k]["sampled_worst_area"] - w["pad"] - T1,
                    "reemitted": bytes.fromhex(res[k]["sampled_reemitted_hex"]) if res[k]["sampled_reemitted_hex"] else None}
                for k in TREES}
    else:                                        # a changed bound: rebuild one tree
        root = (np.array(man["witness"]["root_center"]), np.array(man["witness"]["root_halfwidth"]))
        q, qh = base_leaves(man["base_domain"]["center"], man["base_domain"]["halfwidth"])["00"]
        bits = bits_of(w["bins"]["00"])
        worst = min(sampled_bound(q, qh, c, h, w["sample_n"]) for c, h in replay(bits, root, CANON)) - w["pad"] - T1
        rows = {"00": {"worst_verified_slack": worst, "reemitted": None}}
    for k, r in rows.items():
        if abs(r["worst_verified_slack"] - per[k]["worst_verified_slack"]) > 1e-12:
            out.append(f"tree {k}: rebuilt worst verified slack {r['worst_verified_slack']!r}, "
                       f"recorded {per[k]['worst_verified_slack']!r}")
        if w["sample_n"] == 96 and r["reemitted"] != w["bins"][k]:
            out.append(f"tree {k}: the stream re-emitted from the text's bound differs from the certificate")
    w["w4"] = {k: {"worst_verified_slack": r["worst_verified_slack"],
                   "byte_identical": r["reemitted"] == w["bins"][k]} for k, r in rows.items()}
    return out


def w5_cost(w):
    out, res = [], canonical_results(w)
    rows = {}
    for k in TREES:
        ours = res[k]["exact_reemitted"]
        theirs = tuple(w["tree_table"][k])
        if ours is None:
            out.append(f"tree {k}: the exact bound does not close within depth 24")
            continue
        rows[k] = {"nodes": ours[0], "leaves": ours[1], "max_depth": ours[2], "text_leaves": theirs[1],
                   "leaf_ratio": theirs[1] / ours[1]}
        if (ours[1] < theirs[1]) != w["exact_smaller"]:
            out.append(f"tree {k}: exact-bound tree {ours[1]} leaves against the text's {theirs[1]}")
    w["w5"] = rows
    return out


def p1_package(w):
    out, man, s = [], w["cert_manifest"], w["summary"]
    if (man["target"], man["search_threshold"], man["n_sample"]) != (T1, w["t_search"], w["sample_n_text"]):
        out.append("the manifest's target, search threshold or sample count differs from the text")
    if s != w["validation"]["verification_summary"]:
        out.append("VALIDATION's copy of the verification summary differs from the certificate's")
    listed = {c["base_cell_id"]: c for c in man["lift_certificates"]}
    for p in s["per_leaf"]:
        c = listed[p["base_cell_id"]]
        if (p["nodes"], p["leaves"], p["max_depth"]) != (c["nodes"], c["leaves"], c["max_depth"]):
            out.append(f"tree {p['base_cell_id']}: summary and manifest counts differ")
        # verified slack = A - pad - T, search slack = A - T_search: they differ by T_search - T - pad
        if abs(p["worst_verified_slack"] - c["worst_search_slack"] - (w["t_search"] - T1 - p["fp_pad"])) > 1e-12:
            out.append(f"tree {p['base_cell_id']}: verified and search slacks are not {w['t_search'] - T1 - p['fp_pad']:.2e} apart")
    if (s["total_lift_nodes"], s["total_lift_leaves"]) != (sum(p["nodes"] for p in s["per_leaf"]),
                                                           sum(p["leaves"] for p in s["per_leaf"])):
        out.append("the summary's totals are not the sums of its rows")
    if s["worst_verified_slack"] != min(p["worst_verified_slack"] for p in s["per_leaf"]) or s["fp_pad"] != w["pad"]:
        out.append("the summary's worst slack or pad differs")
    if s["global_lebesgue_claim"] is not False or man["status"] != "LOCAL-DOMAIN-DRY-RUN-NOT-GLOBAL-THEOREM":
        out.append("the certificate does not mark itself local")
    return out


def p2_package(w):
    out, leaves = [], {row[0]: row for row in w["manifest"]["leaves"]}
    v = w["validation"]
    for rec, leaf_id, text in ((v["round10"], DOC, w["text"]), (v["state_crystal"], CRYSTAL, w["crystal"])):
        _, size, digest = leaves[leaf_id]
        if rec["sha256"] != digest or rec["bytes"] != size:
            out.append(f"{rec['file']}: recorded sha256/bytes differ from the archive")
        n = text.count("$$")
        if rec["double_dollar_count"] != n or rec["double_dollar_even"] != (n % 2 == 0):
            out.append(f"{rec['file']}: recorded {rec['double_dollar_count']} $$, document has {n}")
        if rec["contains_unicode_escape_sequence"] != bool(re.search(r"\\u[0-9a-fA-F]{4}", text)):
            out.append(f"{rec['file']}: unicode-escape flag differs")
        if rec["contains_bracket_math_delimiter"] != bool(re.search(r"\\[\[\]()]", text)):
            out.append(f"{rec['file']}: bracket-delimiter flag differs")
    for key, leaf_id in (("emitter_sha256", EMITTER), ("verifier_sha256", VERIFIER)):
        if v[key] != leaves[leaf_id][2]:
            out.append(f"{key}: recorded digest differs from the archive")
    return out


# ---------------------------------------------------------------- registry (Round 10)

R10_DEFINITIONS = {
    "REFERENCE-VERIFIED": ("contextual", "sec. 7, 9: an emitted certificate replayed by an independent verifier, with a "
                                         "dry-run floating pad in place of a derived error bound; below a theorem status"),
}
R10_REVIEWS = [
    ("COMPUTE-DEFERRED", "", "n/a", "n/a",
     "sec. 20's ledger heading: the full atlas, the global lift, the fallback batch, the arithmetic bound"),
    ("STILL OPEN", "GLOBAL 0.8350 CERTIFICATE", "n/a", "n/a", "sec. 23's boxed summary; read from census v3 on (RUN-003)"),
    ("VERIFIED", "REFERENCE PIPELINE", "computation", "PASS", "W2-W4: the streams replayed and re-emitted byte for byte"),
    ("LIFT-CLOSED", "2. Base atlas tree", "computation", "PASS",
     "every leaf of the four lift trees clears 0.835 by the exact core (W3); the base cannot prune any base leaf (W1)"),
    ("REJECTED", "", "reading", "PASS",
     "sec. 20: the dry run is not a global theorem; its base box is about 1e-18 of the root's volume (W1)"),
    ("BASE-PRUNED", "2. Base atlas tree", "n/a", "n/a", "a grammar token, named to say it is not used"),
    ("CONDITIONAL", "", "analytic", "PASS", "sec. 20: extended to the whole atlas, Round 08's Thm 12.1 gives a_Leb >= 0.835"),
    ("PROVED-ANALYTIC", "", "analytic", "PASS",
     "sec. 20: inherited from Round 08 (RUN-011); the split regeneration is deterministic once its tie-break and "
     "child order are fixed, which the text leaves to the code (W3)"),
    ("REFERENCE-VERIFIED", "7. Search threshold vs verify threshold", "computation", "PASS", "W3, W4"),
    ("VERIFIED-COMPUTATIONAL", "", "computation", "PASS",
     "sec. 20: 4 base leaves, 4 trees, 11372 nodes, 5688 leaves, the replay passes (W2-W4)"),
    ("VERIFIED-THEOREM-APPLICATION", "7. Search threshold vs verify threshold", "n/a", "n/a",
     "named to say the dry run does not reach it"),
]


def r1_registry(w):
    return registry.completeness(w["registry"], "R10", w["definitions"], w["reviews"])


# ---------------------------------------------------------------- world, checks, drill

CHECKS = {"A0": gate.anchors_check(ANCHORS), "W1": w1_domain, "W2": w2_streams, "W3": w3_replay, "W4": w4_emission,
          "W5": w5_cost, "P1": p1_package, "P2": p2_package, "R1": r1_registry}
DEPENDS = {"A0": {"text"}, "W1": {"cert_manifest", "round07", "base_halfwidth", "t7", "base_pruned"},
           "W2": {"bins", "cert_manifest", "tree_table", "totals"},
           "W3": {"bins", "cert_manifest", "replay_rule", "core_radius"},
           "W4": {"bins", "cert_manifest", "summary", "sample_n", "pad"}, "W5": {"bins", "cert_manifest", "tree_table", "exact_smaller"},
           "P1": {"cert_manifest", "summary", "validation", "t_search", "sample_n_text", "pad"},
           "P2": {"validation", "text", "crystal", "manifest"}, "R1": {"registry", "definitions", "reviews"}}

CLAIMS = {
    "base_halfwidth": [4e-5, 4e-5, 4e-4, 4e-5, 4e-5], "t7": 0.19693504677116785,
    "base_pruned": {k: False for k in TREES},
    "tree_table": {"00": (2833, 1417, 21), "01": (2853, 1427, 21), "10": (2833, 1417, 21), "11": (2853, 1427, 21)},
    "totals": (11372, 5688),
    "replay_rule": dict(CANON), "core_radius": lambda d: 1 - d,
    "sample_n": 96, "sample_n_text": 96, "t_search": 0.8350002, "pad": 1e-8,
    "exact_smaller": True,
}


def load_inputs():
    blobs = {n: source_bytes(n) for n in SOURCES}
    want = {DOC, CRYSTAL, VALIDATION, CERT_MANIFEST, SUMMARY, *BINS.values()}
    got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want) if d is not None}
    return (got[DOC].decode("utf-8"), got[CRYSTAL].decode("utf-8"), json.loads(got[VALIDATION]),
            json.loads(got[CERT_MANIFEST]), json.loads(got[SUMMARY]), {k: got[v] for k, v in BINS.items()},
            json.loads(MANIFEST.read_text(encoding="utf-8")))


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--drill", action="store_true")
    ap.add_argument("--blind", metavar="CID")
    args = ap.parse_args()
    text, crystal, validation, cert_manifest, summary, bins, manifest = load_inputs()
    round07 = json.loads(ROUND07.read_text(encoding="utf-8"))
    ARCHIVE_KEY.append(_code_key(bins, cert_manifest))

    def build():
        return {"text": text, "crystal": crystal, "validation": json.loads(json.dumps(validation)),
                "cert_manifest": json.loads(json.dumps(cert_manifest)), "summary": json.loads(json.dumps(summary)),
                "bins": dict(bins), "manifest": manifest, "round07": round07,
                "registry": registry.load(), "definitions": dict(R10_DEFINITIONS), "reviews": list(R10_REVIEWS),
                **{k: (dict(v) if isinstance(v, dict) else v) for k, v in CLAIMS.items()}}

    if args.blind:
        CHECKS[args.blind] = lambda w: []
        args.drill = True
    w = build()
    results = {c: fn(w) for c, fn in CHECKS.items()}
    for c, f in results.items():
        print(f"{c} {'PASS' if not f else 'FAIL'}", *(f"\n     {x}" for x in f[:6]))
    for key in ("w1", "w2", "w3", "w4", "w5"):
        print(key, w.get(key))
    if not args.drill:
        return
    table, per = CLAIMS["tree_table"], summary["per_leaf"]
    cases = [
        ("K0-unmodified", "control", {}, set()),
        ("K1-doc-crlf", "control", {"text": text.replace("\n", "\r\n")}, set()),
        ("K2-pad-written-otherwise", "control", {"pad": 0.00000001}, set()),
        ("K3-core-radius-written-otherwise", "control", {"core_radius": lambda d: (1 - 2 * d + d) / 1}, set()),
        ("M1-doc-node-count", "mutation", {"text": text.replace("| `01` | 2853 |", "| `01` | 2855 |")}, {"A0"}),
        ("M2-t7-digit", "mutation", {"t7": 0.19693504677216785}, {"W1"}),
        ("M3-leaf-claimed-base-pruned", "mutation", {"base_pruned": {**CLAIMS["base_pruned"], "10": True}}, {"W1"}),
        ("M4-table-leaves", "mutation", {"tree_table": {**table, "11": (2853, 1428, 21)}}, {"W2"}),
        ("M5-manifest-digest", "mutation", {"cert_manifest": {**cert_manifest, "lift_certificates": [
            {**c, "sha256": "0" * 64} if c["base_cell_id"] == "01" else c for c in cert_manifest["lift_certificates"]]}},
         {"W2"}),
        ("M6-core-eroded-twice", "mutation", {"core_radius": lambda d: 1 - 2 * d}, {"W3"}),
        ("M7-tie-to-y", "mutation", {"replay_rule": {"order": (0, 2, 1), "low_first": True}}, {"W3"}),
        ("M8-higher-child-first", "mutation", {"replay_rule": {"order": (0, 1, 2), "low_first": False}}, {"W3"}),
        ("M9-64-directions", "mutation", {"sample_n": 64}, {"W4"}),
        ("M10-exact-claimed-larger", "mutation", {"exact_smaller": False}, {"W5"}),
        ("M11-search-threshold", "mutation", {"t_search": 0.835002}, {"P1"}),
        ("M12-validation-summary", "mutation", {"validation": {**validation, "verification_summary": {
            **validation["verification_summary"], "total_lift_leaves": 5689}}}, {"P1"}),
        ("M13-emitter-digest", "mutation", {"validation": {**validation, "emitter_sha256": "0" * 64}}, {"P2"}),
        ("M14-review-dropped", "mutation", {"reviews": list(R10_REVIEWS[1:])}, {"R1"}),
    ]
    if args.blind:
        cases = [c for c in cases if args.blind in c[3]]
    d = gate.run_drill(build, CHECKS, DEPENDS, cases)
    summary_d = gate.summarize(d, CHECKS)
    print(gate.report_drill(summary_d))
    for x in d:
        if not x["ok"]:
            print("   DRILL FAIL", x)
    if args.blind:
        n = sum(1 for x in d if args.blind in x["expected"] and args.blind not in x["tripped"])
        print(f"blind {args.blind}: drill reported it blind in {n} cases (nothing written)")
        return
    log = {"run": "RUN-013", "subject": "Round 10: the reference dry run, replayed", "document": DOC,
           "checks": {c: {"pass": not f, "failures": f} for c, f in results.items()},
           **{k: w.get(k) for k in ("w1", "w2", "w3", "w4", "w5")}, "drill": summary_d}
    LOG.write_text(json.dumps(log, ensure_ascii=False, indent=1, default=float) + "\n", encoding="utf-8")
    if not results["R1"]:
        registry.record("R10", "RUN-013", R10_DEFINITIONS, R10_REVIEWS)
        print(f"registry: {len(R10_DEFINITIONS)} definitions, {len(R10_REVIEWS)} reviews recorded for R10")


if __name__ == "__main__":
    main()