#!/usr/bin/env python3
"""Independent verifier of the co-performance corpus (extensions/co-performance.md).

Written from the extension's text. It shares no code with wai-rs, which generates the corpus,
and never runs it. It checks Ed25519 signatures with ../claim-conformance/_ed25519.py, WAI's
strict rule (SPEC §7 *Signatures*) written from RFC 8032 with the standard library. Each room
is verified by the live-rooms corpus's own second implementation, live_rooms_verify.py
(live-rooms §9), written from its text alone. Everything else is here:

- the co-performance policy (§3): its layout, rules, signature and chain;
- the statements (§4), who signs each, and the two grant attributes;
- intents, what played, the pinned rules and the fidelity statement (§5);
- schedules, turns and pairs, handovers, the floor, latency budgets and marks (§6);
- windows, inputs, moderation of inputs, the commitment, the three rules, the selection and
  its credits (§7);
- verification (§9), with the reasons read from the extension's §10 table.

For every room it requires the outcome, reason and place, and everything else the corpus
states; of the corpus, that every reason of §10 appears in it and that no other file is there.
Then it mutates copies of the corpus, one defect each, and requires every copy to fail; and it
drops each of its own checks in turn and requires the corpus to catch the weakened verifier.

    python3 co_performance_verify.py <live-conformance/coperformance>

Exit status 0 only if every room verifies, every mutated copy fails and every weakened verifier
is caught. Python 3.8 or later; standard library only.
"""

import copy
import hashlib
import json
import os
import struct
import sys

HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, HERE)
sys.path.insert(0, os.path.join(HERE, "..", "claim-conformance"))
import live_events_verify as LEV  # noqa: E402
import live_rooms_verify as LRV  # noqa: E402
import _ed25519 as ED  # noqa: E402

Refuse = LEV.Refuse
EXTENSION = os.path.join(HERE, "..", "extensions", "co-performance.md")

ZERO = bytes(32)
POLICY_MAGIC = b"WPP1"
POLICY_DOMAIN = b"wai:co-performance-policy" + b"\x01"     # §3.2: 26 bytes
SEED_DOMAIN = b"wai:co-performance-seed" + b"\x01"         # §7.2: 24 bytes
DRAW_DOMAIN = b"wai:co-performance-draw" + b"\x01"         # §7.6: 24 bytes
COMMIT_DOMAIN = b"wai:co-performance-commit" + b"\x01"     # §7.5: 26 bytes
VOTERS_DOMAIN = b"wai:co-performance-voters" + b"\x01"     # §7.8: 26 bytes
OPTION_DOMAIN = b"wai:co-performance-option" + b"\x01"     # §7.8: 26 bytes
INTENT, FIDELITY, SCHEDULE, HANDOVER, MARK = b"WPI1", b"WPF1", b"WPT1", b"WPH1", b"WPM1"
WINDOW, INPUT, COMMIT, SELECTION = b"WPW1", b"WPA1", b"WPK1", b"WPS1"
MAGICS = (INTENT, FIDELITY, SCHEDULE, HANDOVER, MARK, WINDOW, INPUT, COMMIT, SELECTION)   # §4.1
META, CHAT, REACTION, CAPTION, DECISION = 0x01, 0x03, 0x04, 0x0A, 0x0B
JOIN, LEAVE, EXCHANGE = 0x10, 0x11, 0x14
DIRECT = 2                                                   # live-rooms §3.3, bit 1
FORMS = {1: "object", 2: "notes", 3: "text", 4: "camera"}
REFUSE_MODE, MARK_MODE = 1, 2
OUT_OF_TURN, LATE = 1, 2
PLURALITY, REACTIONS, DRAW = 1, 2, 3
RULES = {1: "plurality", 2: "reactions", 3: "draw"}
PROMPT, SKETCH, VOTE, MOVEMENT = 1, 2, 3, 4
AUTHOR, DIRECT_STEP = 1, 2


# A check named here is left out: the verifier weakened on purpose, to show the corpus catches it.
SKIP = set()


def need(name, ok, reason, at):
    """Refuse with `reason` at `at` unless `ok`, or unless the check `name` is left out."""
    if not ok and name not in SKIP:
        raise Stop(reason, at)


class Stop(Exception):
    def __init__(self, reason, at):
        super().__init__(reason)
        self.reason, self.at = reason, at


def sha(*parts):
    h = hashlib.sha256()
    for p in parts:
        h.update(p)
    return h.digest()


def reasons_table():
    """§10's reasons, from the text."""
    with open(EXTENSION, encoding="utf-8") as f:
        text = f.read()
    at = text.index("\n## 10. Reasons")
    end = text.index("\n## ", at + 1)
    return [line.split("`")[1] for line in text[at:end].splitlines() if line.startswith("| `")]


REASONS = reasons_table()


# ---------------------------------------------------------------- reading

class Bad(Exception):
    """A statement that does not read (§4.2)."""


class R:
    """Reads fields in order; running out is Bad."""

    def __init__(self, b):
        self.b, self.p = b, 0

    def take(self, n):
        if self.p + n > len(self.b):
            raise Bad()
        s = self.b[self.p:self.p + n]
        self.p += n
        return s

    def u8(self):
        return self.take(1)[0]

    def u16(self):
        return struct.unpack("<H", self.take(2))[0]

    def u32(self):
        return struct.unpack("<I", self.take(4))[0]

    def i32(self):
        return struct.unpack("<i", self.take(4))[0]

    def u64(self):
        return struct.unpack("<Q", self.take(8))[0]

    def text(self):
        raw = self.take(self.u16())
        try:
            raw.decode("utf-8")
        except UnicodeDecodeError:
            raise Bad()
        return raw

    def done(self):
        return self.p == len(self.b)


def read_policy(b):
    """§3.1, §3.3."""
    if len(b) < 4:
        raise Refuse("truncated")
    if b[:4] != POLICY_MAGIC:
        raise Refuse("malformed")
    if len(b) < 5:
        raise Refuse("truncated")
    if b[4] != 1:
        raise Refuse("unknown_version")
    r = LEV.Reader(b, "truncated")
    r.take(5)
    p = {"room": r.take(32), "prev": r.take(32), "effective": r.u64(), "horizon_ms": r.u32(), "window_ms": r.u32(),
         "time_tol_us": r.u32(), "angle_tol_mdeg": r.u32(), "modes": r.u8()}
    n = r.p
    p["sig"] = r.take(64)
    if not r.done():
        raise Refuse("malformed")
    if (p["horizon_ms"] == 0 or p["window_ms"] == 0 or p["modes"] not in (1, 2, 3)) and "policy-rules" not in SKIP:
        raise Refuse("co_policy_malformed")
    p["body"] = b[:n]
    p["digest"] = sha(p["body"])
    return p


def notes(r):
    """§5.2: a notes body."""
    n = r.u8()
    if not 1 <= n <= 64:
        raise Bad()
    out = []
    for _ in range(n):
        x = {"onset": r.u32(), "duration": r.u32(), "pitch": r.u8(), "velocity": r.u8()}
        if x["duration"] == 0 or x["pitch"] > 127 or not 1 <= x["velocity"] <= 127:
            raise Bad()
        out.append(x)
    keys = [(x["onset"], x["pitch"]) for x in out]
    if any(a >= b for a, b in zip(keys, keys[1:])):
        raise Bad()
    return out


def camera(r):
    """§5.2: a camera body."""
    c = {"pan": r.i32(), "tilt": r.i32(), "zoom": r.u32()}
    if not (-180000 <= c["pan"] <= 180000 and -90000 <= c["tilt"] <= 90000 and c["zoom"] > 0):
        raise Bad()
    return c


def whole(f, b):
    """A symbolic payload read whole as a form's body, or None (§5.5)."""
    r = R(b)
    try:
        x = f(r)
    except Bad:
        return None
    return x if r.done() else None


def read_statement(b):
    """§4.1, §4.2 and each section's layout and value rules: the statement, or Bad."""
    r = R(b)
    m = r.take(4)
    if r.u8() != 1:
        raise Bad()
    s = {"magic": m}
    if m == INTENT:
        s.update(track=r.take(32), at=r.u64(), span=r.u32(), form=r.u8())
        if s["form"] == 1:
            s["planned"] = r.take(32)
        elif s["form"] == 2:
            s["notes"] = notes(r)
        elif s["form"] == 3:
            s["text"] = r.text()
            if not 1 <= len(s["text"]) <= 500:
                raise Bad()
        elif s["form"] == 4:
            s["camera"] = camera(r)
        else:
            raise Bad()
        if s["span"] == 0 or (s["track"] == ZERO) != (s["form"] == 3):
            raise Bad()
        if s["form"] == 2 and any(x["onset"] >= s["span"] for x in s["notes"]):
            raise Bad()
    elif m == FIDELITY:
        s["through"] = r.u64()
        s["entries"] = []
        for _ in range(r.u8()):
            s["entries"].append((r.take(32), (r.u32(), r.u32(), r.u32(), r.u32())))
        ks = [p for p, _ in s["entries"]]
        if any(a >= b for a, b in zip(ks, ks[1:])):
            raise Bad()
    elif m == SCHEDULE:
        s.update(t0=r.u64(), frm=r.u64(), mode=r.u8(), beat_us=r.u32(), bpb=r.u8())
        s["segments"] = []
        for _ in range(r.u8()):
            g = {"start": r.u64(), "length": r.u32(), "turns": r.u16(), "pairs": r.u8()}
            g["holders"] = [r.take(32) for _ in range(r.u8())]
            s["segments"].append(g)
        if not schedule_ok(s):
            raise Bad()
    elif m == HANDOVER:
        s.update(at=r.u64(), to=r.take(32))
    elif m == MARK:
        s.update(track=r.take(32), group=r.u64(), object=r.u64(), flags=r.u8())
        if s["flags"] == 0 or s["flags"] & ~3:
            raise Bad()
    elif m == WINDOW:
        s.update(rule=r.u8(), types=r.u8(), options=r.u8(), k=r.u8(), close=r.u64(), seed_commit=r.take(32), question=r.text())
        if s["rule"] == PLURALITY:
            ok = s["types"] == 4 and 2 <= s["options"] <= 32
        elif s["rule"] in (REACTIONS, DRAW):
            ok = s["types"] != 0 and s["types"] & 0b0100 == 0 and s["types"] < 16 and s["options"] == 0
        else:
            ok = False
        if not (ok and 1 <= s["k"] <= 8 and len(s["question"]) <= 500 and (s["rule"] == DRAW or s["seed_commit"] == ZERO)):
            raise Bad()
    elif m == INPUT:
        s.update(window=r.take(32), type=r.u8())
        if s["type"] == PROMPT:
            s["prompt"] = r.text()
            if not 1 <= len(s["prompt"]) <= 500:
                raise Bad()
        elif s["type"] in (SKETCH, MOVEMENT):
            s["object"] = r.take(32)
        elif s["type"] == VOTE:
            s["option"] = r.u8()
        else:
            raise Bad()
    elif m == COMMIT:
        s.update(window=r.take(32), count=r.u32(), root=r.take(32))
    elif m == SELECTION:
        s.update(rule=r.u8())
        if s["rule"] not in (1, 2, 3):
            raise Bad()
        s.update(window=r.take(32), commit=r.take(32), seed=r.take(32))
        n = r.u8()
        s["picks"] = list(r.take(n)) if s["rule"] == PLURALITY else [r.take(32) for _ in range(n)]
        s["credits"] = []
        for _ in range(r.u8()):
            c = (r.u8(), r.take(32), r.take(32), r.u32())
            if c[0] not in (1, 2):
                raise Bad()
            s["credits"].append(c)
    else:
        raise Bad()
    if not r.done():
        raise Bad()
    return s


def turn_length(s, g):
    """§6.1: L, in µs."""
    return g["length"] if s["beat_us"] == 0 else g["length"] * s["bpb"] * s["beat_us"]


def schedule_ok(s):
    """§6.1's rules that the record alone fixes."""
    if s["mode"] not in (1, 2) or (s["beat_us"] == 0) != (s["bpb"] == 0) or s["bpb"] > 32:
        return False
    if not 1 <= len(s["segments"]) <= 4:
        return False
    floor = s["frm"]
    for g in s["segments"]:
        if not (1 <= g["turns"] <= 1024 and g["pairs"] in (0, 1) and 1 <= len(g["holders"]) <= 4):
            return False
        L = turn_length(s, g)
        end = g["start"] + g["turns"] * L
        if L == 0 or L >= 1 << 64 or end >= 1 << 64 or g["start"] < floor:
            return False
        if len(set(g["holders"])) != len(g["holders"]):
            return False
        if g["pairs"] == 1 and (g["turns"] % 2 or len(g["holders"]) < 2):
            return False
        floor = end
    return True


def turn_at(s, x):
    """§6.2: (segment, turn, start, end) running at x, or None."""
    for i, g in enumerate(s["segments"]):
        L = turn_length(s, g)
        if g["start"] <= x < g["start"] + g["turns"] * L:
            n = (x - g["start"]) // L
            return i, n, g["start"] + n * L, g["start"] + (n + 1) * L
    return None


def decimal(v):
    """§4.4: 1 to 6 digits, the first not 0."""
    if not (1 <= len(v) <= 6 and v[0] != "0" and all("0" <= c <= "9" for c in v)):
        return None
    return int(v)


# ---------------------------------------------------------------- §9 verification

class Room:
    def __init__(self, d, grants, held, objects, payloads):
        self.d, self.grants, self.held, self.objects, self.payloads = d, grants, held, objects, payloads
        self.life = []
        for h in held:
            if LRV.is_room_key(d, h["ev"]["principal"]) and h["ev"]["kind"] in (JOIN, LEAVE, EXCHANGE):
                x = LRV.read_detail(h["ev"]["kind"], h["p"]["detail"])
                g = x["grant"] if h["ev"]["kind"] == JOIN else x["new"] if h["ev"]["kind"] == EXCHANGE else None
                self.life.append((h["ev"]["t"], h["p"]["subject"], g))
        self.schedules, self.handovers, self.intents, self.windows, self.marks, self.inputs = [], [], [], [], [], []

    def grant_at(self, p, x):
        """§9.1: the grant in effect for an object."""
        g = None
        for t, q, gg in self.life:
            if q == p and t <= x:
                g = gg
        return g

    def restricted(self, target, before):
        """§7.4."""
        last = None
        for h in self.held[:before]:
            if h["ev"]["kind"] == DECISION and h["p"]["target"] == target:
                last = h["p"]["verdict"]
        return last in (2, 3)

    def schedule_at(self, x):
        cur = None
        for s in self.schedules:
            if s["frm"] <= x:
                cur = s
        return cur

    def holder(self, s, seg, n, x):
        """§6.3: the holder of a turn at x."""
        g = s["segments"][seg]
        best = None
        for h in self.handovers:
            if h["schedule"] is s and h["seg"] == seg and h["turn"] == n and h["at"] <= x:
                if best is None or (h["at"], h["idx"]) > (best["at"], best["idx"]):
                    best = h
        return best["to"] if best else g["holders"][n % len(g["holders"])]

    def floor(self, p, x):
        """§6.4: (floor, mode)."""
        s = self.schedule_at(x)
        t = turn_at(s, x) if s else None
        if t is None or p not in s["segments"][t[0]]["holders"]:
            return "open", None
        return ("in_turn" if self.holder(s, t[0], t[1], x) == p else "out_of_turn"), s["mode"]

    def played(self, it, as_of=None):
        """§5.4, §5.5: (outcome, what played)."""
        author, w = self.held[it["idx"]]["ev"]["principal"], it["window_us"]
        if it["form"] == 3:
            limit = as_of[0] if as_of else len(self.held)
            best = None
            for k, h in enumerate(self.held[:limit]):
                if h["ev"]["principal"] == author and h["ev"]["kind"] in (CHAT, CAPTION) and abs(h["ev"]["t"] - it["at"]) <= w:
                    if best is None or abs(h["ev"]["t"] - it["at"]) < best[0]:
                        best = (abs(h["ev"]["t"] - it["at"]), k)
            if best is None:
                return "missed", None
            h = self.held[best[1]]
            return ("kept" if h["p"]["text"].encode("utf-8") == it["text"] else "diverged"), {"event": h["digest"].hex()}
        best = None
        for n, o in enumerate(self.objects):
            if o["principal"] != author or o["track"] != it["track"] or abs(o["due"] - it["at"]) > w:
                continue
            if as_of and o["arrival"] > as_of[1]:
                continue
            if best is None or abs(o["due"] - it["at"]) < best[0]:
                best = (abs(o["due"] - it["at"]), n)
        if best is None:
            return "missed", None
        o = self.objects[best[1]]
        place = {"track": o["track"].hex(), "group": o["group"], "object": o["object"]}
        if it["form"] == 1:
            return ("kept" if o["digest"] == it["planned"] else "diverged"), place
        need("payload", o["digest"] in self.payloads, "payload_missing", self.at(it["idx"]))
        b = self.payloads.get(o["digest"], b"")
        if it["form"] == 2:
            got, want, tol = whole(notes, b), it["notes"], it["tol"]
            ok = got is not None and len(got) == len(want) and all(
                a["pitch"] == c["pitch"] and abs((it["at"] + a["onset"]) - (o["due"] + c["onset"])) <= tol
                and abs(a["duration"] - c["duration"]) <= tol for a, c in zip(want, got))
        else:
            got, want, tol = whole(camera, b), it["camera"], it["angle"]
            ok = (got is not None and abs(got["pan"] - want["pan"]) <= tol and abs(got["tilt"] - want["tilt"]) <= tol
                  and got["zoom"] == want["zoom"])
        return ("kept" if ok else "diverged"), place

    def fidelity(self, intents, as_of=None):
        by = {}
        for it in intents:
            out, _ = self.played(it, as_of)
            e = by.setdefault(self.held[it["idx"]]["ev"]["principal"], [0, 0, 0, 0])
            e[0] += 1
            e[{"kept": 1, "diverged": 2, "missed": 3}[out]] += 1
        return [(p, tuple(by[p])) for p in sorted(by)]

    def at(self, k):
        return ["record", self.held[k]["c"], self.held[k]["i"]]

    def eligible(self, w, ck):
        """§7.5."""
        return [k for k, s in self.inputs if k < ck and s["window"] == w["digest"]
                and self.held[k]["ev"]["t"] < w["close"] and not self.restricted(self.held[k]["digest"], ck)]

    def plurality(self, w, eligible):
        """§7.6 rule 1: (counts, voters per option, picks)."""
        last = {}
        for k in eligible:
            s = dict(self.inputs)[k]
            if s["type"] == VOTE:
                last[self.held[k]["ev"]["principal"]] = s["option"]
        voters = [sorted(p for p, o in last.items() if o == i) for i in range(w["options"])]
        counts = [len(v) for v in voters]
        order = sorted((i for i in range(w["options"]) if counts[i] > 0), key=lambda i: (-counts[i], i))
        return counts, voters, order[:w["k"]]

    def scores(self, w, eligible, ck):
        """§7.6 rule 2: each eligible input's score, in the merged order."""
        out = []
        for k in eligible:
            x = self.held[k]["digest"]
            last = {}
            for j, h in enumerate(self.held[:ck]):
                if h["ev"]["kind"] == REACTION and h["p"]["target"] == x and h["ev"]["t"] < w["close"]:
                    last[h["ev"]["principal"]] = j
            out.append((x, sum(1 for j in last.values()
                               if not self.held[j]["p"]["remove"] and not self.restricted(self.held[j]["digest"], ck)), k))
        return out


# Each room's live-rooms verification, by its inputs: it does not depend on SKIP.
ROOMS = {}


def verify(v):
    """§9: a dict of what the corpus states for the room."""
    descriptor = bytes.fromhex(v["descriptor"])
    grants = [bytes.fromhex(g) for g in v["grants"]]
    chains = [[bytes.fromhex(r) for r in c] for c in v["chains"]]
    key = json.dumps([v["descriptor"], v["grants"], v["key_log"], v["chains"]])
    if key not in ROOMS:
        ROOMS[key] = LRV.verify_room(descriptor, grants, v["key_log"], chains)       # step 1
    room = ROOMS[key]
    if room["outcome"] == "refuse":
        return {"outcome": "refuse", "reason": room["reason"], "at": ["room"] + room["at"]}
    d = LRV.read_descriptor(descriptor)
    held_grants, _ = LRV.check_grants(d, grants)
    try:
        return run(v, d, held_grants, chains, room)
    except Stop as e:
        return {"outcome": "refuse", "reason": e.reason, "at": e.at}


def run(v, d, held_grants, chains, room):
    gapped = room["outcome"] == "gap"
    policies = []                                                                     # step 2
    for i, h in enumerate(v["policies"]):
        try:
            p = read_policy(bytes.fromhex(h))
        except Refuse as e:
            raise Stop(e.reason, ["policy", i])
        if p["room"] != d["room"]:
            raise Stop("wrong_room", ["policy", i])
        bad = ED.verify(d["authority"], POLICY_DOMAIN + p["body"], p["sig"])
        need("policy-signature", not bad, bad, ["policy", i])
        linked = (p["prev"] == ZERO and p["effective"] == 0) if not policies else (
            p["prev"] == policies[-1]["digest"] and p["effective"] > policies[-1]["effective"])
        need("policy-link", linked, "co_policy_unlinked", ["policy", i])
        policies.append(p)
    attrs = {}                                                                        # step 3
    for i, g in enumerate(held_grants):
        a = {}
        for key, val in LRV.read_attrs(g["attrs"]):
            if key == "audience_input":
                n = decimal(val)
                need("attributes", n is not None and 1 <= n <= 255, "co_attr_malformed", ["grant", i])
                a["audience_input"] = n or 255
            elif key == "latency_budget_ms":
                n = decimal(val)
                need("attributes", n is not None and 1 <= n <= 600000, "co_attr_malformed", ["grant", i])
                a["budget"] = n or int(val)
        attrs[g["digest"]] = a
    by_digest = {g["digest"]: g for g in held_grants}
    held, seen = [], set()
    for c, i, under in room["order"]:
        ev = LEV.read_record(chains[c][i])
        if ev["digest"] in seen:
            continue
        seen.add(ev["digest"])
        p = LEV.read_payload(ev["kind"], ev["payload"], 1 << 20)
        held.append({"c": c, "i": i, "ev": ev, "p": p, "digest": ev["digest"], "under": bytes.fromhex(under) if under else None})
    objects = [{"principal": bytes.fromhex(o["principal"]), "track": bytes.fromhex(o["track"]), "group": o["group"],
                "object": o["object"], "digest": bytes.fromhex(o["digest"]), "arrival": o["arrival"], "due": o["due"]}
               for o in v["objects"]]
    payloads = {sha(bytes.fromhex(b)): bytes.fromhex(b) for b in v["payloads"]}
    rm = Room(d, by_digest, held, objects, payloads)
    for k, h in enumerate(held):                                                      # step 4
        if h["ev"]["kind"] == META and h["ev"]["payload"][:4] in MAGICS:
            statement(rm, policies, attrs, k, gapped)
    intents = []                                                                      # step 5
    for it in rm.intents:
        out, played = rm.played(it)
        intents.append({"digest": held[it["idx"]]["digest"].hex(), "principal": held[it["idx"]]["ev"]["principal"].hex(),
                        "form": FORMS[it["form"]], "at": it["at"], "outcome": out, "played": played})
    fidelity = [{"principal": p.hex(), "announced": e[0], "kept": e[1], "diverged": e[2], "missed": e[3]}
                for p, e in rm.fidelity(rm.intents)]
    floor = []                                                                        # step 6
    for n, o in enumerate(objects):
        f, mode = rm.floor(o["principal"], o["arrival"])
        marks = 0
        for _, m in rm.marks:
            if (m["track"], m["group"], m["object"]) == (o["track"], o["group"], o["object"]):
                marks |= m["flags"]
        lateness = max(0, o["arrival"] - o["due"])
        g = rm.grant_at(o["principal"], o["arrival"])
        budget = attrs.get(g, {}).get("budget") if g else None
        late = budget is not None and lateness > budget * 1000
        need("refuse", not (f == "out_of_turn" and mode == REFUSE_MODE), "turn_violated", ["object", n])
        need("mark-out-of-turn", not (f == "out_of_turn" and mode == MARK_MODE and not marks & OUT_OF_TURN), "turn_unmarked", ["object", n])
        need("mark-late", not (late and not marks & LATE), "late_unflagged", ["object", n])
        floor.append({"floor": f, "mode": {1: "refuse", 2: "mark"}.get(mode), "late": late, "lateness": lateness, "marks": marks})
    for k, m in rm.marks:                                                             # step 7
        hit = [x for o, x in zip(objects, floor) if (o["track"], o["group"], o["object"]) == (m["track"], m["group"], m["object"])]
        bad = not hit or (m["flags"] & OUT_OF_TURN and hit[0]["floor"] != "out_of_turn") or (m["flags"] & LATE and not hit[0]["late"])
        need("marks-founded", not bad, "mark_unfounded", rm.at(k))
    schedules = []
    for s in rm.schedules:
        turns = []
        for si, g in enumerate(s["segments"]):
            L = turn_length(s, g)
            for n in range(g["turns"]):
                role = "solo" if g["pairs"] == 0 else ("call" if n % 2 == 0 else "response")
                turns.append({"segment": si, "index": n, "start": g["start"] + n * L, "end": g["start"] + (n + 1) * L,
                              "holder": g["holders"][n % len(g["holders"])].hex(), "role": role})
        schedules.append({"digest": s["digest"].hex(), "mode": {1: "refuse", 2: "mark"}[s["mode"]], "from": s["frm"], "turns": turns})
    handovers = [{"digest": h["digest"].hex(), "at": h["at"], "to": h["to"].hex(), "schedule": h["schedule"]["digest"].hex(),
                  "segment": h["seg"], "turn": h["turn"]} for h in rm.handovers]
    windows = []
    for w in rm.windows:
        tally = scores = None
        if w["commit"] is not None and w["rule"] == PLURALITY:
            tally = rm.plurality(w, w["eligible"])[0]
        if w["commit"] is not None and w["rule"] == REACTIONS:
            scores = [{"input": x.hex(), "score": n} for x, n, _ in rm.scores(w, w["eligible"], w["commit"][0])]
        sel = w["selection"]
        windows.append({
            "digest": w["digest"].hex(), "rule": RULES[w["rule"]], "close": w["close"],
            "eligible": [held[k]["digest"].hex() for k in w["eligible"]],
            "commit": w["commit"][1].hex() if w["commit"] else None,
            "picks": None if sel is None else [x if isinstance(x, int) else x.hex() for x in sel["picks"]],
            "credits": [] if sel is None else [{"step": "author" if c[0] == AUTHOR else "direct", "party": c[1].hex(),
                                                "ref": c[2].hex(), "count": c[3]} for c in sel["credits"]],
            "tally": tally, "scores": scores})
    out = {"outcome": "gap" if gapped else "accept"}
    if gapped:
        out["reason"] = "delivery_gap"
        out["gaps"] = room["gaps"]
    out.update({"room": d["room"].hex(), "policy_digests": [p["digest"].hex() for p in policies], "intents": intents,
                "fidelity": fidelity, "schedules": schedules, "handovers": handovers, "floor": floor, "windows": windows})
    return out


def statement(rm, policies, attrs, k, gapped):
    """§9.2 step 4 over one statement."""
    h = rm.held[k]
    at, t, author = rm.at(k), h["ev"]["t"], h["ev"]["principal"]
    try:
        s = read_statement(h["ev"]["payload"])
    except Bad:
        raise Stop("co_statement_malformed", at)
    m = s["magic"]
    need("statement-context", not ((m == SCHEDULE and s["t0"] != rm.d["t0"]) or (m == WINDOW and s["close"] <= t)
                                   or (m == FIDELITY and s["through"] > t)), "co_statement_malformed", at)
    pol = None                                                                        # §3.4
    for p in policies:
        if p["effective"] <= t:
            pol = p
    need("no-policy", pol is not None, "co_no_policy", at)
    if pol is None:
        pol = {"horizon_ms": 1 << 40, "window_ms": 1 << 40, "time_tol_us": 1 << 40, "angle_tol_mdeg": 1 << 40, "modes": 3}
    room_key = LRV.is_room_key(rm.d, author)                                          # §4.3
    grant = rm.grants.get(h["under"]) if h["under"] else None
    direct = room_key or (grant is not None and grant["powers"] & DIRECT != 0)
    need("authors", not ((m in (SCHEDULE, WINDOW) and not direct) or (m in (FIDELITY, MARK, COMMIT, SELECTION) and not room_key)),
         "co_not_permitted", at)
    s["idx"], s["digest"] = k, h["digest"]
    if m == INTENT:                                                                   # §5.3
        need("ahead", s["at"] > t, "intent_not_ahead", at)
        need("horizon", s["at"] + s["span"] - t <= pol["horizon_ms"] * 1000, "intent_beyond_horizon", at)
        s["window_us"], s["tol"], s["angle"] = pol["window_ms"] * 1000, pol["time_tol_us"], pol["angle_tol_mdeg"]
        rm.intents.append(s)
    elif m == FIDELITY:                                                               # §5.6
        if not gapped:
            covered = [it for it in rm.intents if it["at"] + it["window_us"] <= s["through"]]
            need("fidelity", rm.fidelity(covered, (k, t)) == s["entries"], "fidelity_mismatch", at)
    elif m == SCHEDULE:                                                               # §6.1
        need("retroactive", s["frm"] >= t, "schedule_retroactive", at)
        need("modes", pol["modes"] >> (s["mode"] - 1) & 1, "mode_not_allowed", at)
        rm.schedules.append(s)
    elif m == HANDOVER:                                                               # §6.3
        need("handover-turn", s["at"] >= t, "handover_invalid", at)
        sch = rm.schedule_at(s["at"])
        turn = turn_at(sch, s["at"]) if sch else None
        need("handover-turn", turn is not None and s["to"] in sch["segments"][turn[0]]["holders"], "handover_invalid", at)
        if turn is not None:
            need("handover-author", direct or rm.holder(sch, turn[0], turn[1], s["at"]) == author, "handover_not_holder", at)
            s.update(schedule=sch, seg=turn[0], turn=turn[1])
            rm.handovers.append(s)
    elif m == MARK:
        rm.marks.append((k, s))
    elif m == WINDOW:
        s.update(commit=None, eligible=[], selection=None)
        rm.windows.append(s)
    elif m == INPUT:                                                                  # §7.3
        limit = None if room_key or grant is None else attrs.get(grant["digest"], {}).get("audience_input")
        need("audience-power", limit is not None, "input_not_permitted", at)
        w = next((x for x in rm.windows if x["digest"] == s["window"]), None)
        need("window-known", w is not None, "window_unknown", at)
        if w is not None:
            need("input-type", w["types"] >> (s["type"] - 1) & 1 and not (s["type"] == VOTE and s["option"] >= w["options"]),
                 "input_type_mismatch", at)
        sent = sum(1 for j, x in rm.inputs if x["window"] == s["window"] and rm.held[j]["ev"]["principal"] == author)
        need("input-limit", sent + 1 <= (limit or 255), "input_over_limit", at)
        rm.inputs.append((k, s))
    elif m == COMMIT:                                                                 # §7.5
        w = next((x for x in rm.windows if x["digest"] == s["window"]), None)
        if w is None:
            raise Stop("window_unknown", at)
        need("commit-early", t >= w["close"], "commit_early", at)
        need("repeated", w["commit"] is None, "statement_repeated", at)
        eligible = rm.eligible(w, k)
        root = sha(COMMIT_DOMAIN, w["digest"], struct.pack("<I", len(eligible)), *[rm.held[j]["digest"] for j in eligible])
        need("commit-recompute", gapped or (s["count"] == len(eligible) and s["root"] == root), "commit_mismatch", at)
        w["commit"], w["eligible"] = (k, h["digest"]), eligible
    elif m == SELECTION:                                                              # §7.7
        w = next((x for x in rm.windows if x["digest"] == s["window"]), None)
        if w is None:
            raise Stop("window_unknown", at)
        need("repeated", w["selection"] is None, "statement_repeated", at)
        if w["commit"] is None:
            raise Stop("selection_uncommitted", at)
        need("committed", s["commit"] == w["commit"][1], "selection_uncommitted", at)
        if w["rule"] == DRAW:
            need("seed", sha(SEED_DOMAIN, s["seed"]) == w["seed_commit"], "seed_mismatch", at)
        else:
            need("statement-context", s["seed"] == ZERO, "co_statement_malformed", at)
        if not gapped:
            ck = w["commit"][0]
            if s["rule"] != PLURALITY:
                for x in s["picks"]:
                    need("late-pick", not any(rm.held[j]["digest"] == x and y["window"] == w["digest"] and rm.held[j]["ev"]["t"] >= w["close"]
                                              for j, y in rm.inputs), "input_late", at)
            if w["rule"] == PLURALITY:
                _, voters, picks = rm.plurality(w, w["eligible"])
                credits = [(DIRECT_STEP, sha(VOTERS_DOMAIN, *voters[o]), sha(OPTION_DOMAIN, w["digest"], bytes([o])), len(voters[o]))
                           for o in picks]
            else:
                if w["rule"] == REACTIONS:
                    ranked = sorted(rm.scores(w, w["eligible"], ck), key=lambda x: (-x[1], x[2]))
                    picks = [x for x, _, _ in ranked[:w["k"]]]
                else:
                    picks = sorted((rm.held[j]["digest"] for j in w["eligible"]),
                                   key=lambda x: (sha(DRAW_DOMAIN, s["seed"], x), x))[:w["k"]]
                authors = {rm.held[j]["digest"]: rm.held[j]["ev"]["principal"] for j in w["eligible"]}
                credits = [(AUTHOR, authors[x], x, 1) for x in picks]
            need("rule", s["rule"] == w["rule"] and s["picks"] == picks, "selection_mismatch", at)
            for n, c in enumerate(credits):
                need("credits", n < len(s["credits"]), "input_uncredited", at)
                need("credits", n >= len(s["credits"]) or s["credits"][n] == c, "credit_mismatch", at)
            need("credits", len(s["credits"]) <= len(credits), "credit_mismatch", at)
        w["selection"] = s


# ---------------------------------------------------------------- the corpus

def check(doc, quiet=False):
    """Every room against what the corpus states: the failures."""
    fails = []
    for v in doc.get("vectors", []):
        try:
            got = verify(v)
        except Exception as e:  # a crash on a mutated copy is a failure to read it
            got, bad = None, ["the room does not verify: %s: %s" % (type(e).__name__, e)]
        else:
            bad = [k for k in got if v.get(k) != got[k]] + [k for k in ("outcome", "reason", "at") if k in v and k not in got]
        if not quiet:
            what = "?" if got is None else got["outcome"] + (" " + got["reason"] if got["outcome"] == "refuse" else "")
            print(("PASS" if not bad else "FAIL") + " room %s: %s" % (v.get("name"), what))
        fails += ["room %s: %s differs from the corpus" % (v.get("name"), k) for k in bad]
    return fails


def flip(h, at):
    b = bytearray(bytes.fromhex(h))
    b[at] ^= 0x01
    return b.hex()


def mutations(doc):
    """Copies of the corpus, each with one defect a conforming verifier must catch."""
    vn = {v["name"]: k for k, v in enumerate(doc["vectors"])}
    jam, aud = vn["jam"], vn["audience"]

    def mutate(label, f):
        d = copy.deepcopy(doc)
        f(d["vectors"])
        return label, d

    def drop_record(vs, name, chain, index):
        del vs[vn[name]]["chains"][chain][index]

    def set_arrival(vs, i, x):
        vs[jam]["objects"][i]["arrival"] = x

    return [
        mutate("a byte of the jam's policy signature", lambda vs: vs[jam]["policies"].__setitem__(0, flip(vs[jam]["policies"][0], -3))),
        mutate("the jam's policy withheld", lambda vs: vs[jam].update(policies=[])),
        mutate("the AI participant's fidelity stated with the divergence kept",
               lambda vs: next(f for f in vs[jam]["fidelity"] if f["diverged"] == 1).update(kept=5, diverged=0)),
        mutate("the diverged intent stated kept", lambda vs: next(i for i in vs[jam]["intents"] if i["outcome"] == "diverged").update(outcome="kept")),
        mutate("the out-of-turn object stated in turn", lambda vs: next(o for o in vs[jam]["floor"] if o["floor"] == "out_of_turn").update(floor="in_turn")),
        mutate("the late object stated on time", lambda vs: next(o for o in vs[jam]["floor"] if o["late"]).update(late=False)),
        mutate("the late object given an on-time arrival", lambda vs: set_arrival(vs, 3, 11_010_000)),
        mutate("the out-of-turn object given an arrival in its own turn", lambda vs: set_arrival(vs, 4, 11_500_000)),
        mutate("the notes payload withheld", lambda vs: vs[jam].update(payloads=vs[jam]["payloads"][1:])),
        mutate("the clock's mark of the out-of-turn object dropped", lambda vs: drop_record(vs, "jam", 0, 4)),
        mutate("the handover stated to another turn", lambda vs: vs[jam]["handovers"][0].update(turn=1)),
        mutate("the second schedule stated as marking", lambda vs: vs[jam]["schedules"][1].update(mode="mark")),
        mutate("the reactions window's picks stated in another order", lambda vs: vs[aud]["windows"][1]["picks"].reverse()),
        mutate("a credit dropped from the stated selection", lambda vs: vs[aud]["windows"][1]["credits"].pop()),
        mutate("the plurality's tally stated with the late vote", lambda vs: vs[aud]["windows"][0]["tally"].__setitem__(0, 2)),
        mutate("the denied prompt stated eligible", lambda vs: vs[aud]["windows"][1]["eligible"].insert(2, vs[aud]["windows"][1]["eligible"][1])),
        mutate("a member's vote record dropped", lambda vs: drop_record(vs, "audience", 2, 0)),
        mutate("a refused room stated with another reason", lambda vs: vs[vn["selection_counts_a_late_input"]].update(reason="selection_mismatch")),
        mutate("a refused room stated at another place", lambda vs: vs[vn["late_unflagged"]].update(at=["object", 4])),
    ]


CHECKS = {
    "policy-rules": "§3.3: the policy's rules",
    "policy-signature": "§3.2: the policy's signature",
    "policy-link": "§3.4: the policy's chain",
    "no-policy": "§3.4: a policy in effect",
    "attributes": "§4.4: the attributes' syntax",
    "statement-context": "§5.6, §6.1, §7.2, §7.7 step 2: the rules a statement's context fixes",
    "authors": "§4.3: who signs",
    "ahead": "§5.3 rule 1: an intent ahead of its instant",
    "horizon": "§5.3 rule 2: an intent's horizon",
    "payload": "§5.4: the played object's payload",
    "fidelity": "§5.6: the fidelity statement recomputed",
    "retroactive": "§6.1: no schedule changes the past",
    "modes": "§6.1: the modes the policy allows",
    "handover-turn": "§6.3: a handover's turn",
    "handover-author": "§6.3: a handover's author",
    "refuse": "§6.5: no out-of-turn object forwarded under refuse",
    "mark-out-of-turn": "§6.5: an out-of-turn object marked under mark",
    "mark-late": "§6.6: a late object marked",
    "marks-founded": "§6.7: a mark founded",
    "audience-power": "§7.3 step 1: the audience-input power",
    "window-known": "§7.3 step 2: an input's window",
    "input-type": "§7.3 step 3: an input's type",
    "input-limit": "§7.3 step 4: the inputs a grant may send",
    "repeated": "§7.5, §7.7 step 1: one commitment and one selection",
    "commit-early": "§7.5: a commitment after the close",
    "commit-recompute": "§7.5: the commitment recomputed",
    "committed": "§7.7 step 1: the selection's commitment",
    "seed": "§7.7 step 2: the draw's seed",
    "late-pick": "§7.7 step 3: no input after the close",
    "rule": "§7.7 step 4: the picks recomputed",
    "credits": "§7.7 step 5: the credits",
}


def main(corpus_dir):
    fails = []
    st = ED._self_test()
    print(("PASS" if not st else "FAIL") + " Ed25519 strict rule self-test " + ",".join(st))
    fails += ["ed25519 self-test"] if st else []
    ok_table = len(REASONS) == 31 and len(set(REASONS)) == 31
    print(("PASS" if ok_table else "FAIL") + " §10 read from the extension: %d reasons" % len(REASONS))
    fails += [] if ok_table else ["the extension's §10 does not read"]
    with open(os.path.join(corpus_dir, "vectors.json"), encoding="utf-8") as f:
        doc = json.load(f)
    fails += check(doc)
    extra = sorted(set(os.listdir(corpus_dir)) - {"vectors.json", "README.md"})
    print(("PASS" if not extra else "FAIL") + " no file but vectors.json and README.md")
    fails += ["an extra file: %s" % n for n in extra]
    seen = {v.get("reason") for v in doc["vectors"]}
    missing = [r for r in REASONS if r not in seen]
    print(("PASS" if not missing else "FAIL") + " every reason of §10 appears in the corpus")
    fails += ["no room gives %s" % r for r in missing]
    for label, d in mutations(doc):
        # Only the rooms the defect changed: the others are the corpus's, checked above.
        changed = {"vectors": [v for v, o in zip(d["vectors"], doc["vectors"]) if v != o]}
        caught = check(changed, quiet=True) if changed["vectors"] else []
        print(("PASS" if caught else "FAIL") + " mutated copy fails: %s%s" % (label, " (%s)" % caught[0][:100] if caught else ""))
        if not caught:
            fails.append("a mutated copy verifies: %s" % label)
    for name, what in CHECKS.items():
        SKIP.clear()
        SKIP.add(name)
        caught = check(doc, quiet=True)
        SKIP.clear()
        print(("PASS" if caught else "FAIL") + " a verifier without %s fails the corpus%s" % (what, " (%s)" % caught[0][:70] if caught else ""))
        if not caught:
            fails.append("the corpus does not catch a verifier without %s" % what)
    for f in fails:
        print("FAIL " + f)
    print(("PASS" if not fails else "FAIL") + " co-performance corpus: %d rooms" % len(doc["vectors"]))
    return 1 if fails else 0


if __name__ == "__main__":
    if len(sys.argv) != 2:
        print("usage: co_performance_verify.py <live-conformance/coperformance>", file=sys.stderr)
        sys.exit(2)
    sys.exit(main(sys.argv[1]))