"""RUN-055 - LESR Paper 05: contact pressure, dual multipliers and the No-Slack boundary principle.

LESR Paper 05 (2026-09-20) builds the series' duality layer. Stacking Paper 03's linearized contact constraints
over a finite mode library and finitely many active contacts gives A c + B xi >= 0; if no (c, xi) has g^T c < 0,
Farkas gives multipliers lambda >= 0 with g = A^T lambda and B^T lambda = 0 - each witness's contact pressure
balances in translation and rotation, and mu_h matches the pressure measure on the library's moments. A smooth local
No-Slack theorem: an arc with rho_h >= kappa_0 > 0 and no active constraint admits an inward cut that lowers the
area. Conditional continuum and measure versions, a support-inclusion form, a contact-pressure graph layer, a dual
gap, and (sec. 68) the claim that the finite dual can be solved now, cheaply, on the Lebesgue line's own witnesses.
It ships a dual schema, a pressure-graph schema, a sanity-check record, a verifier scaffold, a state record and
VALIDATION. It is evidence, not a canonical document. Here the alternative is checked on random finite systems, the
No-Slack theorem on a smooth body and at a corner, and the finite dual is built and solved on the kernel.

Checks
  A0 anchors      the formulas below occur in the document as written
  W1 duality      sec. 10-15: Farkas' alternative on random finite systems - exactly one of a descent and a
                  certificate; the balances; the sanity record
  W2 no-slack     sec. 33: an inward bump on a smooth arc lowers the area within its convexity cap; at a corner
                  (rho = 0) the same kind of move has delta A = 0 (RUN-050), so the hypothesis rho >= kappa_0 is needed
  W3 kernel       sec. 5-11, 49, 68: the finite system on the kernel's hull - contacts sampled on each witness's
                  sectors and edges, Fourier modes, all witness motions free - at a generic placement, at q-dagger and
                  at the polish Z: the certificate, its residuals and its size; the gradient at the generic placement;
                  what coarse sampling and a free rotation gauge do at 16 modes
  W4 records      the schemas and the state against the sections that carry them
  W5 scaffold     the verifier scaffold, read after this rebuild and never run
  P1 package      the VALIDATION record against the bytes and the archive

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

import numpy as np
from scipy.optimize import linprog

import gate
import run046_uesfcm_cycles_07_09 as r46
from corpus import SOURCES, TREE, source_bytes, walk_sources
from run052_lesr_paper02 import QDAG
from run053_lesr_paper03 import ZPOL, structure

FOLDER = "main.zip!/LESR_Skew_Field_Variational/"
PKG = FOLDER + "LESR_Paper05_Package_v0.1.zip!/"
DOC = PKG + "LESR_Paper05_Contact_Pressure_Dual_Multipliers_and_No_Slack_Boundary_v0.1.md"
DUAL = PKG + "LESR_Paper05_Dual_Pressure_Schema_v0.1.json"
PGRAPH = PKG + "LESR_Paper05_Contact_Pressure_Graph_Schema_v0.1.json"
CHECKS_JSON = PKG + "LESR_Paper05_Sanity_Checks.json"
SCAFFOLD = PKG + "LESR_Paper05_Dual_Pressure_Verifier_Scaffold.py"
STATE = PKG + "LESR_State_Paper05_v0.1.json"
VALIDATION = PKG + "LESR_Paper05_VALIDATION.json"
PAPER06 = FOLDER + "LESR_Paper06_Package_v0.1.zip!/LESR_Paper06_Actual_Lebesgue_Shape_State_and_First_Closure_Graph_v0.1.md"
LOG = TREE / "data" / "gate-logs" / "run055-lesr-paper05.json"
MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json"
CACHE = TREE / "data" / "cache" / "run055-searches.json"     # data/cache is not committed
GENERIC = [QDAG[0] + 0.002, QDAG[1] + 0.001, QDAG[2] + 0.05, QDAG[3] - 0.001, QDAG[4] + 0.002]   # RUN-053's generic placement
WITNESS = [0] + [1] * 6 + [2] * 10          # the disc, B3's six pieces, B5's ten


def load_inputs():
    blobs = {n: source_bytes(n) for n in SOURCES}
    want = (DOC, DUAL, PGRAPH, CHECKS_JSON, SCAFFOLD, STATE, VALIDATION)
    got = {leaf.id: d for leaf, d in walk_sources(blobs, keep=lambda l: l.id in want + (PAPER06,)) if d is not None}
    rows = {row[0]: row for row in json.loads(MANIFEST.read_text(encoding="utf-8"))["leaves"]}
    return {"text": got[DOC].decode("utf-8"), "dual": json.loads(got[DUAL]), "pgraph": json.loads(got[PGRAPH]), "sanity": json.loads(got[CHECKS_JSON]),
            "scaffold": got[SCAFFOLD].decode("utf-8"), "state": json.loads(got[STATE]), "validation": json.loads(got[VALIDATION]),
            "bytes": {k: got[k] for k in want}, "manifest_rows": {k: rows[k] for k in want}, "paper06": got[PAPER06].decode("utf-8")}


# ---------------------------------------------------------------- the finite alternative

def solve_primal(A, B, g, fixed=()):
    """min g^T c over |c| <= 1, |xi| <= 10, A c + B xi >= 0 (sec. 9); fixed: placement columns held at 0"""
    N, P = A.shape[1], B.shape[1]
    bounds = [(-1, 1)] * N + [(-10, 10)] * P
    for j in fixed:
        bounds[N + j] = (0, 0)
    res = linprog(np.concatenate([g, np.zeros(P)]), A_ub=-np.hstack([A, B]), b_ub=np.zeros(A.shape[0]), bounds=bounds, method="highs")
    return float(res.fun)


def solve_dual(A, B, g, drop=()):
    """lambda >= 0 with A^T lambda = g, B^T lambda = 0 (sec. 10-11), by the dual simplex, which returns a basic
    solution; drop: placement columns whose balance is not required (a gauge-fixed motion). Returns the residuals
    and the number of nonzero multipliers, or None"""
    keep = [j for j in range(B.shape[1]) if j not in drop]
    E = np.vstack([A.T, B[:, keep].T])
    res = linprog(np.zeros(A.shape[0]), A_eq=E, b_eq=np.concatenate([g, np.zeros(len(keep))]), bounds=[(0, None)] * A.shape[0], method="highs-ds")
    if res.status != 0:
        return None
    lam = res.x
    return {"shape": float(np.max(np.abs(A.T @ lam - g))), "balance": float(np.max(np.abs(B.T @ lam)[keep])) if keep else 0.0,
            "nonzero": int(np.sum(lam > 1e-12)), "equations": E.shape[0]}


def farkas_scan(trials=300, seed=55):
    """random systems (rows 8-40, modes 3-12, placement columns 3-9): half built with a certificate (g = A^T lam0,
    B made orthogonal to lam0 >= 0), half with g random. For each, the primal's least g^T c and the dual's
    feasibility: exactly one holds"""
    rng = np.random.default_rng(seed)
    both = neither = with_cert = with_descent = 0
    worst = 0.0
    for t in range(trials):
        r, N, P = int(rng.integers(8, 41)), int(rng.integers(3, 13)), int(rng.integers(3, 10))
        A, B = rng.normal(size=(r, N)), rng.normal(size=(r, P))
        if t % 2 == 0:
            lam0 = np.abs(rng.normal(size=r)) * (rng.random(r) < 0.6)
            B -= np.outer(lam0, lam0 @ B) / max(float(lam0 @ lam0), 1e-300)
            g = A.T @ lam0
        else:
            g = rng.normal(size=N)
        descent = solve_primal(A, B, g) < -1e-9
        cert = solve_dual(A, B, g)
        ok = cert is not None and cert["shape"] < 1e-8 and cert["balance"] < 1e-8
        if ok:
            worst = max(worst, cert["shape"], cert["balance"])
        both += descent and ok
        neither += (not descent) and (not ok)
        with_cert += ok
        with_descent += descent
    theta = [0.0, 2 * math.pi / 3, 4 * math.pi / 3]
    three = float(np.hypot(sum(math.cos(x) for x in theta), sum(math.sin(x) for x in theta)))
    return {"both": both, "neither": neither, "certificates": with_cert, "descents": with_descent, "residual": worst, "three": three}


# ---------------------------------------------------------------- the No-Slack arc

def noslack_scan(N=1 << 16):
    """sec. 33 on h = 1 + 0.05 cos 3t + 0.02 sin 2t (rho > 0): phi = -bump on I = (-0.4, 0.4), C-infinity with
    compact support. Its convexity cap 1/max((L phi)^- / rho), its delta A = int phi rho < 0, and the exact quadratic
    A(eps) - A(0) at the cap and at half of it. At a corner, where rho = 0 on I, RUN-050's admissible inward move has
    delta A = 0 and lowers the area only at second order: the hypothesis rho >= kappa_0 > 0 is what makes delta A < 0"""
    th = 2 * np.pi * (np.arange(N) - N // 2) / N
    rho = 1 - 0.05 * 8 * np.cos(3 * th) - 0.02 * 3 * np.sin(2 * th)
    x = th / 0.4
    inside = np.abs(x) < 1
    bump = np.zeros(N)
    bump[inside] = np.exp(-1 / (1 - x[inside] ** 2))
    phi = -bump
    d2 = (np.roll(phi, -1) - 2 * phi + np.roll(phi, 1)) / (2 * np.pi / N) ** 2
    d1 = (np.roll(phi, -1) - np.roll(phi, 1)) / (2 * (2 * np.pi / N))
    Lphi = phi + d2
    q = np.where(Lphi < 0, -Lphi / rho, 0.0)
    cap = 1.0 / float(np.max(q))
    dt = 2 * np.pi / N
    dA = float(np.sum(phi * rho) * dt)
    d2A = float(np.sum(phi ** 2 - d1 ** 2) * dt)
    change = [e * dA + e * e * d2A / 2 for e in (cap, cap / 2)]
    return {"kappa0": float(rho.min()), "cap": cap, "dA": dA, "d2A": d2A, "change": change, "support": [float(th[inside].min()), float(th[inside].max())]}


# ---------------------------------------------------------------- the kernel's finite system

def modes(M):
    return [lambda t: np.ones_like(np.asarray(t, dtype=float))] + [f for m in range(1, M + 1) for f in ((lambda t, m=m: np.cos(m * np.asarray(t))), (lambda t, m=m: np.sin(m * np.asarray(t))))]


def kernel_system(v, M, per=4, fixed_count=None):
    """sec. 5-8 on the kernel's hull at v. Contacts: on each segment its owner, sampled at spacing pi / (per M) (or a
    fixed count per segment), and at each edge normal every piece that touches there. A_ak = phi_k(theta_a); B's
    three columns per witness (disc, B3, B5) are (h'_W, -cos, -sin), h'_W = (p - t_W).u' for the contact piece's
    centre p and the witness's reference point; g_k = int phi_k d mu_h (densities by Gauss-Legendre, edges' atoms)"""
    st = structure(v)
    C, rho, S, atoms = st["C"], st["rho"], st["S"], st["atoms"]
    refs = [np.zeros(2), np.array([v[0], v[1]]), np.array([v[3], v[4]])]
    rows = []
    for a, b, k in S:
        n = fixed_count if fixed_count else max(2, int(math.ceil((b - a) / (math.pi / (per * M)))) + 1)
        rows += [(a + (b - a) * j / (n - 1), k) for j in range(n)]
    rows += [(x, j) for x, m, k, k2, act in atoms for j in act]
    F = modes(M)
    A = np.array([[float(f(t)) for f in F] for t, _ in rows])
    B = np.zeros((len(rows), 9))
    for r, (t, k) in enumerate(rows):
        i = WITNESS[k]
        B[r, 3 * i:3 * i + 3] = [float((C[k] - refs[i]) @ np.array([-math.sin(t), math.cos(t)])), -math.cos(t), -math.sin(t)]
    xg, wg = np.polynomial.legendre.leggauss(40)
    g = np.zeros(len(F))
    for a, b, k in S:
        if rho[k] > 0:
            tt = (a + b) / 2 + (b - a) / 2 * xg
            g += rho[k] * (b - a) / 2 * np.array([float(np.sum(wg * f(tt))) for f in F])
    for x, m, k, k2, act in atoms:
        g += m * np.array([float(f(x)) for f in F])
    return A, B, g


def kernel_scan():
    """the certificate at three placements for M = 4, 8 with every witness motion free (the paper's model); at the
    generic placement also M = 16 - with B3's turn free, at two contact densities, and with it fixed (the rotation
    gauge); at Z, M = 16 with six contacts per segment; the generic placement's gradient"""
    out = {"certificates": {}}
    for name, v in (("generic", GENERIC), ("qdag", QDAG), ("z", ZPOL)):
        for M in (4, 8):
            A, B, g = kernel_system(v, M)
            out["certificates"][f"{name}-{M}"] = {"primal": solve_primal(A, B, g), "dual": solve_dual(A, B, g), "perimeter": float(g[0])}
    m16 = {}
    for per in (4, 16):
        A, B, g = kernel_system(GENERIC, 16, per)
        m16[f"free-{per}"] = solve_primal(A, B, g, fixed=(0,))
    A, B, g = kernel_system(GENERIC, 16, 4)
    m16["fixed"] = {"primal": solve_primal(A, B, g, fixed=(0, 3)), "dual": solve_dual(A, B, g, drop=(0, 3))}
    out["m16"] = m16
    A, B, g = kernel_system(ZPOL, 16, fixed_count=6)
    out["coarse"] = solve_primal(A, B, g)
    Ar = r46.area
    E = np.eye(5)
    grad = [(Ar([GENERIC[j] + 1e-7 * E[i][j] for j in range(5)]) - Ar([GENERIC[j] - 1e-7 * E[i][j] for j in range(5)])) / 2e-7 for i in range(5)]
    out["gradient"] = float(np.linalg.norm(grad))
    out["perimeter"] = r46.hull(GENERIC)[1]
    return out


# ---------------------------------------------------------------- the cache

def _key(name, fn, extra=""):
    import run008_round05_saturation_gate as r8
    import run009_round06_witness_exchange as r9
    import run052_lesr_paper02 as r52
    import run053_lesr_paper03 as r53
    digest = hashlib.sha256(inspect.getsource(fn).encode())
    for helper in HELPERS[name]:
        digest.update(inspect.getsource(helper).encode())
    for path in (r8.__file__, r9.__file__, r52.__file__, r53.__file__):
        digest.update(open(path, "rb").read())
    digest.update(extra.encode())
    return digest.hexdigest()


HELPERS = {"farkas": (solve_primal, solve_dual), "noslack": (), "kernel": (solve_primal, solve_dual, modes, kernel_system, r46.area, r46.hull)}


def searches():
    cached = json.loads(CACHE.read_text(encoding="utf-8")) if CACHE.exists() else {}
    out = {}
    for name, fn in (("farkas", farkas_scan), ("noslack", noslack_scan), ("kernel", kernel_scan)):
        key = _key(name, fn)
        if cached.get(name, {}).get("key") != key:
            cached[name] = {"key": key, "value": json.loads(json.dumps(fn()))}
            CACHE.parent.mkdir(parents=True, exist_ok=True)
            CACHE.write_text(json.dumps(cached, indent=1) + "\n", encoding="utf-8")
        out[name] = cached[name]["value"]
    return out


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

ANCHORS = {
    "A0": [r"Ac+B\xi\ge0.", r"A_{a,k}=\phi_k(\theta_{ij}).", r"g=A^T\lambda,", r"B^T\lambda=0.", r"\sum_j\lambda_{ij}u_{\theta_{ij}}=0.",
           r"\sum_j\lambda_{ij}h'_{W_i}(\theta_{ij}-\psi_i)=0.", r"\Lambda=\sum_{i,j}\lambda_{ij}\delta_{\theta_{ij}}.",
           r"\rho_h(\theta)=h+h''\ge\kappa_0>0", r"A[h+\varepsilon\phi]<A[h].", r"\operatorname{supp}\mu_h\subseteq",
           r"\lambda_{ij}C_{ij}=0.", r"`PROVED—FINITEPOLYHEDRALDUALITY`", r"\text{finite-modestationarity具有finitedualwitnesscertificate}."],
}
STATE_MAP = {"finite contact-pressure KKT theorem": (11, "Theorem—FiniteContact-PressureCertificate"), "shape/placement matrix decomposition": (5, "MatrixForm"),
             "witness translation pressure balance": (13, "WitnessTranslationBalance"), "witness rotation pressure balance": (15, "WitnessRotationBalance"),
             "discrete contact-pressure measure": (19, "DiscreteContact-PressureMeasure"), "finite-mode moment matching": (20, "Moment-MatchingInterpretation"),
             "conditional continuum pressure-measure framework": (29, "ContactPressureMeasure"), "smooth local No-Slack Arc theorem": (33, "Theorem—LocalNo-SlackArcPrinciple"),
             "measure-version No-Slack principle": (34, "Measure-VersionNo-SlackPrinciple"), "dual support inclusion principle": (35, "SupportInclusionForm"),
             "contact-pressure graph layer": (24, "ContactPressureGraph"), "dual residual and dual-gap metric": (45, "Mode-TruncatedDualResidual"),
             "binding-contact orbit priority": (60, "BindingOrbit"), "primal-dual expansion loop": (72, "這形成新的Primal–DualExpansionLoop")}
DISCLAIMERS = {"unconditional existence of continuum KKT measure for the full Lebesgue universal-cover problem": "不作無條件existenceclaim",
               "mu_h equals contact pressure when other geometric constraints are active": "只在其他geometricconstraintslocallyinactive時成立",
               "finite-mode moment closure implies full measure equality": "finite-modestationarity不是",
               "all active contacts are binding contacts": "activecontact不一定重要"}
CLAIMS = {
    "farkas_claim": {"exclusive": True, "exhaustive": True, "certificates": 213, "descents": 87, "residual": True, "three": [True, True]},
    "noslack_claim": {"kappa0": 0.5476, "cap": 0.0159, "dA": -0.114, "d2A": -0.971, "decrease": True, "support": [-0.4, 0.4]},
    "kernel_claim": {"certificates": {f"{p}-{m}": [True, True, True] for p in ("generic", "qdag", "z") for m in (4, 8)}, "gradient": 0.39,
                     "m16_free": [-0.00062, -0.00022], "m16_fixed": [True, True], "coarse": -0.11, "perimeter": True},
    "records_claim": {"dual_conditions": True, "graph_layer": ["WITNESS_PRESSURE_STATE", "BOUNDARY_PRESSURE_STATE", "UNSUPPORTED_BOUNDARY", "DUALLY_SUPPORTED"],
                      "contact_states": True, "compiler_outputs": ["DESCENT_FOUND", "DUAL_CERTIFIED", "UNSUPPORTED_BOUNDARY", "MORE_MODES_REQUIRED",
                                                                   "MORE_WITNESSES_REQUIRED", "NONSMOOTH_CONTACT", "TOPOLOGY_TRANSITION"],
                      "unmapped": [], "completed": 14, "disclaimed": [True] * 4, "next": [True, False]},
    "scaffold_facts": {"lines": 72, "defs": ["matvec_transpose", "max_abs", "verify_dual", "translation_balance", "rotation_balance"],
                       "classes": ["DualCertificate"], "solver": False, "complementarity": False, "negative_tolerance": True},
    "package_claim": {"digests": [True] * 6, "utf8": True, "delimiters": ["PASS", []], "manifest": True},
}


def sig(x, n=2):
    return float(f"{x:.{n - 1}e}")


def a0_anchors(w):
    text = gate.squash(w["text"])
    return [f"anchor not found: {a[:60]}" for a in ANCHORS["A0"] if a not in text]


def w1_duality(w):
    s, rec = w["search"]["farkas"], w["sanity"]["three_equal_contacts_translation_balance"]
    got = {"exclusive": s["both"] == 0, "exhaustive": s["neither"] == 0, "certificates": s["certificates"], "descents": s["descents"],
           "residual": s["residual"] < 1e-8, "three": [s["three"] < 1e-15, abs(rec["norm"] - s["three"]) < 1e-15]}
    w["w1"] = got
    return [] if got == w["farkas_claim"] else [f"the duality: {got}"]


def w2_noslack(w):
    s = w["search"]["noslack"]
    got = {"kappa0": round(s["kappa0"], 4), "cap": sig(s["cap"], 3), "dA": sig(s["dA"], 3), "d2A": sig(s["d2A"], 3),
           "decrease": all(c < 0 for c in s["change"]), "support": [round(x, 3) for x in s["support"]]}
    w["w2"] = got
    return [] if got == w["noslack_claim"] else [f"the no-slack arc: {got}"]


def w3_kernel(w):
    s = w["search"]["kernel"]
    certs = {}
    for k, c in s["certificates"].items():
        d = c["dual"]
        certs[k] = [c["primal"] > -1e-9, d is not None and d["shape"] < 1e-9 and d["balance"] < 1e-9, d is not None and d["nonzero"] <= d["equations"]]
    m = s["m16"]
    got = {"certificates": certs, "gradient": sig(s["gradient"], 3), "m16_free": [sig(m["free-4"]), sig(m["free-16"])],
           "m16_fixed": [m["fixed"]["primal"] > -1e-9, m["fixed"]["dual"] is not None], "coarse": sig(s["coarse"]),
           "perimeter": abs(s["certificates"]["generic-4"]["perimeter"] - s["perimeter"]) < 1e-9}
    w["w3"] = got
    return [] if got == w["kernel_claim"] else [f"the kernel: {got}"]


def w4_records(w):
    du, pg, st, raw, text = w["dual"], w["pgraph"], w["state"], w["text"], gate.squash(w["text"])
    outputs = re.search(r"輸出：[\s]*```text[\s]*(.*?)```", raw, re.S)
    got = {"dual_conditions": du["finite_model"]["dual_conditions"] == ["lambda >= 0", "g = A^T lambda", "B^T lambda = 0"],
           "graph_layer": [x for x in du["graph_layer"] if x.replace("_", "\\_") in raw or x in raw],
           "contact_states": [s.replace("_", "") for s in pg["contact_states"]] == ["VIOLATED", "SLACK", "ACTIVENONBINDING", "BINDING"]
           and all(x in text for x in ("##Violated", "##Slack", "##ActivebutNonbinding", "##Binding")),
           "compiler_outputs": outputs.group(1).split() if outputs else None,
           "unmapped": [x for x in st["completed"] if x not in STATE_MAP or f"#{STATE_MAP[x][0]}.{STATE_MAP[x][1]}" not in text],
           "completed": len(st["completed"]), "disclaimed": [x in DISCLAIMERS and DISCLAIMERS[x] in text for x in st["not_claimed"]],
           "next": [st["next"] == "Paper 06 — " + du["next_paper"], du["next_paper"] in w["paper06"][:300]]}
    w["w4"] = got
    return [] if got == w["records_claim"] else [f"the records: {got}"]


def w5_scaffold(w):
    """the scaffold, read: it verifies a supplied certificate; whether it solves for one, checks sec. 48's
    complementarity (lambda = 0 off the active constraints), or accepts multipliers down to -tol"""
    code = w["scaffold"]
    got = {"lines": code.count("\n"), "defs": re.findall(r"^def (\w+)", code, re.M), "classes": re.findall(r"^class (\w+)", code, re.M),
           "solver": bool(re.search(r"linprog|nnls|simplex|highs|cvxpy", code)), "complementarity": bool(re.search(r"inactive|complement", code, re.I)),
           "negative_tolerance": "x < -tol" in code}
    w["w5"] = got
    return [] if got == w["scaffold_facts"] else [f"the scaffold: {got}"]


def p1_package(w):
    v, B = w["validation"], w["bytes"]
    sha = lambda b: hashlib.sha256(b).hexdigest()
    body = B[DOC].decode("utf-8")
    got = {"digests": [v["paper_sha256"] == sha(B[DOC]), v["dual_schema_sha256"] == sha(B[DUAL]), v["scaffold_sha256"] == sha(B[SCAFFOLD]),
                       v["graph_schema_sha256"] == sha(B[PGRAPH]), v["checks_sha256"] == sha(B[CHECKS_JSON]), v["state_sha256"] == sha(B[STATE])],
           "utf8": v["utf8"] is True, "delimiters": [v["math_delimiters"], sorted(set(re.findall(r"\\\(|\\\)|\\\[|\\\]", body)))],
           "manifest": all(w["manifest_rows"][k][2] == sha(b) for k, b in B.items())}
    w["p1"] = got
    return [] if got == w["package_claim"] else [f"the package: {got}"]


CHECKS = {"A0": a0_anchors, "W1": w1_duality, "W2": w2_noslack, "W3": w3_kernel, "W4": w4_records, "W5": w5_scaffold, "P1": p1_package}
DEPENDS = {"A0": {"text"}, "W1": {"search", "sanity", "farkas_claim"}, "W2": {"search", "noslack_claim"}, "W3": {"search", "kernel_claim"},
           "W4": {"dual", "pgraph", "state", "text", "paper06", "records_claim"}, "W5": {"scaffold", "scaffold_facts"},
           "P1": {"validation", "bytes", "manifest_rows", "package_claim"}}


def drill_cases(base):
    def edit(obj, fn):
        x = copy.deepcopy(obj)
        fn(x)
        return x

    text, s = base["text"], base["search"]
    return [
        ("K0-unmodified", "control", {}, set()),
        ("K1-crlf", "control", {"text": text.replace("\n", "\r\n"), "scaffold": base["scaffold"].replace("\n", "\r\n")}, set()),
        ("K2-validation-keys-sorted", "control", {"validation": json.loads(json.dumps(base["validation"], sort_keys=True))}, set()),
        ("M1-theorem-label", "mutation", {"text": text.replace("`PROVED — FINITE POLYHEDRAL DUALITY`", "`CONJECTURE`", 1)}, {"A0"}),
        ("M2-both-alternatives", "mutation", {"search": edit(s, lambda x: x["farkas"].update(both=1))}, {"W1"}),
        ("M3-sanity-norm", "mutation", {"sanity": edit(base["sanity"], lambda x: x["three_equal_contacts_translation_balance"].update(norm=0.1))}, {"W1"}),
        ("M4-no-decrease", "mutation", {"search": edit(s, lambda x: x["noslack"].update(change=[1e-6, -1e-6]))}, {"W2"}),
        ("M5-first-variation-sign", "mutation", {"search": edit(s, lambda x: x["noslack"].update(dA=0.114))}, {"W2"}),
        ("M6-no-certificate", "mutation", {"search": edit(s, lambda x: x["kernel"]["certificates"]["generic-8"].update(dual=None))}, {"W3"}),
        ("M7-flat-gradient", "mutation", {"search": edit(s, lambda x: x["kernel"].update(gradient=0.0))}, {"W3"}),
        ("M8-schema-conditions", "mutation", {"dual": edit(base["dual"], lambda x: x["finite_model"]["dual_conditions"].pop())}, {"W4"}),
        ("M9-state-not-claimed", "mutation", {"state": edit(base["state"], lambda x: x["not_claimed"].append("every contact binds"))}, {"W4"}),
        ("M10-scaffold-complementarity", "mutation", {"scaffold": base["scaffold"] + "\ndef complementarity(lam, inactive):\n    return all(lam[i] == 0 for i in inactive)\n"}, {"W5"}),
        ("M11-scaffold-sign", "mutation", {"scaffold": base["scaffold"].replace("x < -tol", "x < 0", 1)}, {"W5"}),
        ("M12-validation-digest", "mutation", {"validation": {**base["validation"], "dual_schema_sha256": "0" * 64}}, {"P1"}),
        ("M13-sanity-bytes", "mutation", {"bytes": {**base["bytes"], CHECKS_JSON: base["bytes"][CHECKS_JSON] + b" "}}, {"P1"}),
    ]


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--drill", action="store_true")
    ap.add_argument("--blind", metavar="CID")
    args = ap.parse_args()
    base = {**load_inputs(), "search": searches()}

    def build():
        return {**copy.deepcopy(base), **copy.deepcopy(CLAIMS)}

    if args.blind:
        CHECKS[args.blind] = lambda w: []
        args.drill = True
    w = build()
    results = {}
    for c, fn in CHECKS.items():
        try:
            results[c] = fn(w)
        except KeyError as e:
            results[c] = [f"claim missing: {e}"]
    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", "p1"):
        print(key, "=", json.dumps(w.get(key), default=str, ensure_ascii=False))
    if not args.drill:
        return
    cases = drill_cases(base)
    if args.blind:
        cases = [c for c in cases if args.blind in c[3]]
    d = gate.run_drill(build, CHECKS, DEPENDS, cases)
    summary = gate.summarize(d, CHECKS)
    print(gate.report_drill(summary))
    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-055", "subject": "LESR Paper 05: contact pressure, dual multipliers and the No-Slack boundary", "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", "p1")}, "drill": summary}
    LOG.write_text(json.dumps(log, ensure_ascii=False, indent=1, default=str) + "\n", encoding="utf-8")


if __name__ == "__main__":
    main()