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

Written from the extension's text. It shares no code with wai-rs, which generates the corpus,
and never runs it. It takes from the second implementations of the texts this extension
builds on what they define: group and object receipts from the JWP corpus's
(`../jwp-conformance/jwp_verify.py`, jwp-receipts §2.2, §3), a claim's steps 1 to 5 from the
claim corpus's (`../claim-conformance/claim_verify.py`, jwp-receipts §3.1, with the two
classes' bodies and rules), and key logs, anchoring and confirmation from the key-discovery
corpus's (`../signer-conformance/signer_verify.py`, jwp-receipts §7). Everything this
extension adds is written here:

- §4.3 and §5.3: a transmission and a reconciliation against the group and its objects,
  with the root over the received leaves computed from jwp-receipts §2.2;
- §6: the verdict over a group — the declarations, the reconciliations counted, set aside
  and joined, the counts, the status, a sink's own bearer, and statements offered;
- §7: the upper bound on a receiver's share;
- §8: confirmation with no return path, where a log that arrives on the bearer anchors
  nothing.

For every case it requires the outcome the corpus states, field for field; for the cases
`same_receipt` names, one group and its object receipts byte for byte with one verdict on
every bearer class; that every reason of §10's table appears in the corpus; 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 bearer_verify.py <live-conformance/bearers>

Exit status 0 only if every case verifies, every mutated copy fails and every weakened
verifier is caught. Python 3.8 or later; the `cryptography` package, which the claim and
key-discovery verifiers import.
"""

import copy
import json
import os
import re
import sys

HERE = os.path.dirname(os.path.abspath(__file__))
for d in ("claim-conformance", "jwp-conformance", "signer-conformance"):
    sys.path.insert(0, os.path.join(HERE, "..", d))
import claim_verify as CV  # noqa: E402
import jwp_verify as JV  # noqa: E402
import signer_verify as SV  # noqa: E402

EXTENSION = os.path.join(HERE, "..", "extensions", "bearer-receipts.md")
BEARERS = ("bidirectional", "multicast", "unidirectional")

# A weakened run drops one of these checks (see `weakened`); None checks everything.
DROPPED = None


def drops(name):
    return DROPPED == name


def reasons_table():
    """§10's codes, in order."""
    text = open(EXTENSION, encoding="utf-8").read()
    at = text.index("\n## 10. Reasons")
    end = text.find("\n## ", at + 1)
    rows = text[at:end if end >= 0 else len(text)].splitlines()
    return [r.split("`")[1] for r in rows if r.startswith("| `")]


# ------------------------------------------------------------------ jwp-receipts §2.2

def merkle_root(leaves):
    """§2.2: pairs hashed level by level, an odd level's last leaf duplicated; no leaf, zeros."""
    if not leaves:
        return bytes(32)
    level = list(leaves)
    while len(level) > 1:
        if len(level) % 2:
            level.append(level[-1])
        level = [JV.node(level[i], level[i + 1]) for i in range(0, len(level), 2)]
    return level[0]


def received(b):
    """§5.1: object i is bit 0x80 >> (i mod 8) of byte i div 8."""
    bits = bytes.fromhex(b["received"])
    return [i for i in range(8 * len(bits)) if bits[i // 8] & (0x80 >> (i % 8))]


def need(ok, reason):
    if not ok:
        raise CV.Reject(6, reason)


# ------------------------------------------------------------------ §4.3, §5.3: step 6

def check_transmission(c, g):
    """§4.3 against a group that passed jwp-receipts §3 steps 1 and 2."""
    need(drops("subject") or JV.link(g).hex() == c["subject"], "transmission_subject_mismatch")
    need(drops("signer") or g["signer_pubkey"] == c["signer_pubkey"], "transmission_signer_mismatch")


def check_reconciliation(c, g, objects):
    """§5.3 against a group that passed §3 steps 1 and 2, and the object receipts held
    under it, of which those that pass §3 step 5 are used."""
    b = c["body"]
    need(drops("subject") or JV.link(g).hex() == c["subject"], "reconciliation_subject_mismatch")
    need(drops("by_publisher") or c["signer_pubkey"] != g["signer_pubkey"], "reconciliation_by_publisher")
    need(b["leaf_count"] == g["leaf_count"], "reconciliation_leaf_count_mismatch")
    idx = received(b)
    if len(idx) == g["leaf_count"]:
        root = bytes.fromhex(g["root_hash"])
    else:
        leaves = []
        for i in idx:
            o = next((o for o in objects if o["object_id"] == i and included(o, g)), None)
            if o is None and drops("objects_held"):
                continue
            need(o is not None, "reconciliation_objects_not_held")
            leaves.append(JV.leaf(o))
        root = merkle_root(leaves)
    need(drops("root") or root.hex() == b["received_root"], "reconciliation_root_mismatch")


def included(o, g):
    try:
        JV.inclusion(o, g)
        return True
    except JV.Refuse:
        return False


# ------------------------------------------------------------------ §6: the verdict

def bound(j, n):
    """§7: ⌈j / max(1, n)⌉."""
    n = max(1, n)
    return j // n if drops("ceiling") else (j + n - 1) // n


def verdict(case):
    raw = case["group"]
    try:
        g = JV.read_group(raw)
        JV.verify_group(g)
    except JV.Refuse as r:
        return {"outcome": "refuse", "reason": r.reason}

    # Step 2: the objects, the same on every bearer.
    objs, overdicts = [], []
    for o in case["objects"]:
        try:
            ob = JV.read_object(o["receipt"])
        except JV.Refuse as r:
            overdicts.append("reject reason=" + r.reason)
            continue
        objs.append(ob)
        try:
            if o["envelope"] is None:
                JV.inclusion(ob, g)
                overdicts.append("inclusion-verified")
            else:
                JV.accept(ob, g, bytes.fromhex(o["envelope"]))
                overdicts.append("delivered-verified")
        except JV.Refuse as r:
            overdicts.append("reject reason=" + r.reason)

    # Step 3: each claim, §3.1 steps 1-5, then step 6.
    held, claims, accepted = {}, [], []
    for wire in case["claims"]:
        try:
            c = CV.verify_claim(wire)
        except CV.Reject as r:
            claims.append(f"reject step={r.step} reason={r.reason}")
            accepted.append(None)
            continue
        previous = held.get(c["signer_pubkey"])
        held[c["signer_pubkey"]] = c
        try:
            CV.check_chain(c, previous)
            if c["class"] == "transmission":
                check_transmission(c, g)
            elif c["class"] == "reconciliation":
                check_reconciliation(c, g, objs)
            else:
                raise CV.Reject(6, "context_mismatch")
        except CV.Reject as r:
            claims.append(f"reject step={r.step} reason={r.reason}")
            accepted.append(None)
            continue
        claims.append("declared")
        accepted.append(c)

    # Step 4: the declarations, by instance.
    by_id = {}
    for i, c in enumerate(accepted):
        if c is not None and c["class"] == "transmission":
            by_id.setdefault(c["body"]["bearer_id"], []).append(i)
    standing, contradicted = {}, set()
    for bid, idx in by_id.items():
        bodies = [accepted[i]["body"] for i in idx]
        if drops("contradiction") or all(b == bodies[0] for b in bodies):
            standing[bid] = bodies[0]
        else:
            contradicted.add(bid)
            for i in idx:
                claims[i] = "set-aside reason=bearer_contradicted"

    # Step 5: the reconciliations.
    count_only = case["count_only"]
    bits, counted = {}, set()
    n = g["leaf_count"]
    for i, c in enumerate(accepted):
        if c is None or c["class"] != "reconciliation":
            continue
        b, key = c["body"], c["signer_pubkey"]
        d = standing.get(b["bearer_id"])
        aside = None
        if b["bearer_id"] in contradicted:
            aside = "bearer_contradicted"
        elif d is None and not drops("undeclared"):
            aside = "bearer_not_declared"
        elif d is not None and d["bearer"] != b["bearer"]:
            aside = "bearer_contradicted"
        elif count_only is not None and key not in count_only:
            aside = "sink_not_confirmed"
        if aside:
            claims[i] = "set-aside reason=" + aside
            continue
        if (key, b["bearer_id"]) in counted and not drops("duplicate"):
            claims[i] = "joined reason=reconciliation_duplicate_sink"
        else:
            claims[i] = "counted"
        counted.add((key, b["bearer_id"]))
        mine = bits.setdefault(key if not drops("duplicate") else (key, i), set())
        mine.update(received(b))

    # Step 6.
    sinks = len(bits)
    whole = sum(1 for s in bits.values() if len(s) == n or (drops("whole") and s))
    received_by = [sum(1 for s in bits.values() if j in s) for j in range(n)]
    lines = []
    for bid in sorted(standing):
        d = standing[bid]
        k = len({key for key, x in counted if x == bid})
        e = d["energy"]
        lines.append({
            "bearer_id": bid,
            "bearer": d["bearer"],
            "sinks": k,
            "energy": None if e is None else {"joules_micro": e["joules_micro"], "energy_provenance": e["energy_provenance"]},
            "per_receiver_upper_bound": None if e is None else bound(e["joules_micro"], k),
        })
    status = "reconciled" if sinks else "transmitted" if standing else "published"

    # §6.5.
    sink = None
    if case["sink"] is not None:
        sb, sid = case["sink"]["bearer"], case["sink"]["bearer_id"]
        if sid in contradicted:
            sink = "bearer_contradicted"
        elif sid not in standing:
            sink = "bearer_not_declared"
        else:
            sink = "declared" if standing[sid]["bearer"] == sb else "bearer_contradicted"
    # §6.4.
    assertion = None
    a = case["assertion"]
    if a is not None:
        if a["status"] == "transmitted":
            assertion = "holds" if any(l["bearer"] == a["bearer"] for l in lines) else "bearer_not_declared"
        elif whole == 0 and not drops("delivered"):
            assertion = "delivery_not_reconciled"
        elif whole < a["sinks"]:
            assertion = "delivery_exceeds_reconciled"
        else:
            assertion = "holds"
    return {"outcome": "verdict", "objects": overdicts, "claims": claims, "status": status, "sinks": sinks,
            "whole": whole, "received_by": received_by, "bearers": lines, "sink": sink, "assertion": assertion}


# ------------------------------------------------------------------ §8: no return path

def offline(case):
    item = case["item"]
    if "claim" in item:
        try:
            c = CV.verify_claim(item["claim"])
        except CV.Reject as r:
            return {"outcome": "refuse", "reason": f"reject step={r.step} reason={r.reason}"}
        pub, sid, time = bytes.fromhex(c["signer_pubkey"]), c["signer_id"], c["issued_at"]
        auth, figure = SV.claim_authorities(c), SV.figure_authorities(c)
    else:
        try:
            g = JV.read_group(item["group"])
            JV.verify_group(g)
            objs = [JV.read_object(o) for o in item["objects"]]
            for o in objs:
                JV.inclusion(o, g)
        except JV.Refuse as r:
            return {"outcome": "refuse", "reason": "refuse reason=" + r.reason}
        # §7.5 of jwp-receipts: the group's own class, where its payload is labelled, and each
        # labelled object's.
        classes = [g["cls"]["label"]] if g["labelled"] and g["cls"] is not None else []
        classes += [o["class"]["label"] for o in objs if o["labelled"] and o["class"] is not None]
        pub, sid, time = bytes.fromhex(g["signer_pubkey"]), g["signer_id"], g["group_end"]
        auth, figure = SV.item_authorities("group", classes), None
    revisions, anchors, outcomes = [], [], [None] * len(case["logs"])
    for i, l in enumerate(case["logs"]):
        if l["via"] != "pinned":
            continue
        out = SV.anchor_log(l["origin"], l["log"], "pinned", None)
        if out[0] == "anchored":
            revisions += SV.read_log(l["origin"], l["log"])
            anchors.append({"origin": l["origin"], "revision": out[1], "path": "pinned", "pinned_revision": out[3]})
            outcomes[i] = "anchored"
        else:
            outcomes[i] = "not-anchored reason=" + out[1]
    for i, l in enumerate(case["logs"]):
        if l["via"] != "bearer":
            continue
        try:
            revs = SV.read_log(l["origin"], l["log"])
        except SV.Stop as s:
            outcomes[i] = "unread reason=" + s.reason
            continue
        revisions += revs
        anchored = any(a["origin"] == l["origin"] for a in anchors)
        if drops("anchor_on_bearer") and not anchored:
            h = SV.rev_hash(revs[-1])
            anchors.append({"origin": l["origin"], "revision": h, "path": "pinned", "pinned_revision": h})
            anchored = True
        outcomes[i] = "held" if anchored else "anchor_on_bearer"
    conf = SV.confirm(pub, sid, auth, time, revisions, anchors, None)
    fig = None if figure is None else SV.confirm(pub, sid, figure, time, revisions, anchors, None)
    return {"outcome": "confirm", "logs": outcomes, "confirmation": conf, "figure": fig}


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

def strings(v, out):
    if isinstance(v, str):
        out.append(v)
    elif isinstance(v, list):
        for x in v:
            strings(x, out)
    elif isinstance(v, dict):
        for x in v.values():
            strings(x, out)


def check(doc, quiet=False):
    """The failures of a corpus document: each case's outcome, the one receipt on every
    bearer, and every reason of §10."""
    fails = []
    for c in doc["cases"]:
        try:
            got = verdict(c)
        except (KeyError, TypeError, ValueError, IndexError, AttributeError) as e:
            got = {"error": repr(e)}
        if got != c["outcome"]:
            fails.append(c["name"])
            if not quiet:
                print(f"FAIL {c['name']}\n  stated {json.dumps(c['outcome'])}\n  got    {json.dumps(got)}")
    for c in doc["offline"]:
        try:
            got = offline(c)
        except (KeyError, TypeError, ValueError, IndexError, AttributeError, SV.Stop) as e:
            got = {"error": repr(e)}
        if got != c["outcome"]:
            fails.append(c["name"])
            if not quiet:
                print(f"FAIL {c['name']}\n  stated {json.dumps(c['outcome'])}\n  got    {json.dumps(got)}")
    same = [next((c for c in doc["cases"] if c["name"] == n), None) for n in doc["same_receipt"]]
    if None in same or {c["sink"]["bearer"] for c in same if c} != set(BEARERS):
        fails.append("same_receipt does not name a case on every bearer class")
    else:
        for a, b in zip(same, same[1:]):
            if (a["group"], [o["receipt"] for o in a["objects"]]) != (b["group"], [o["receipt"] for o in b["objects"]]) \
                    or a["outcome"]["objects"] != b["outcome"]["objects"]:
                fails.append(f"{a['name']} and {b['name']} do not carry one receipt with one verdict")
    stated = []
    for c in doc["cases"] + doc["offline"]:
        strings(c["outcome"], stated)
    for code in reasons_table():
        if not any(s == code or s.endswith("reason=" + code) for s in stated):
            fails.append("no case gives " + code)
    return fails


def mutations(doc):
    """Copies of the corpus, one defect each, every one of which must fail."""
    def case(d, name):
        return next(c for c in d["cases"] + d["offline"] if c["name"] == name)

    def m_root(d):
        c = case(d, "reconciled_by_three_sinks")
        w = json.loads(c["claims"][3])
        w["body"]["received_root"] = "00" * 32
        c["claims"][3] = json.dumps(w, separators=(",", ":"), sort_keys=True)

    def m_bound(d):
        case(d, "bound_rounds_up")["outcome"]["bearers"][0]["per_receiver_upper_bound"] -= 1

    def m_status(d):
        case(d, "transmitted_presented_as_delivered")["outcome"]["status"] = "reconciled"

    def m_delivered(d):
        case(d, "transmitted_presented_as_delivered")["outcome"]["assertion"] = "holds"

    def m_same(d):
        case(d, "same_receipt_multicast")["objects"][0]["receipt"]["origin"] = "elsewhere"

    def m_drop_claim(d):
        case(d, "reconciled_by_three_sinks")["claims"].pop()

    def m_via(d):
        case(d, "offline_anchor_on_the_bearer")["logs"][0]["via"] = "pinned"

    def m_duplicate(d):
        case(d, "duplicate_sink_joined")["outcome"]["claims"][2] = "counted"

    def m_unmetered(d):
        case(d, "unmetered_transmission_has_no_bound")["outcome"]["bearers"][0]["per_receiver_upper_bound"] = 0

    def m_sink(d):
        case(d, "sink_bearer_contradicted")["sink"]["bearer"] = "multicast"

    def m_reason_gone(d):
        c = case(d, "reconciliation_by_the_publisher")
        d["cases"].remove(c)

    return [m_root, m_bound, m_status, m_delivered, m_same, m_drop_claim, m_via, m_duplicate, m_unmetered, m_sink,
            m_reason_gone]


WEAKENINGS = ["subject", "signer", "by_publisher", "objects_held", "root", "contradiction", "undeclared", "duplicate",
              "whole", "ceiling", "delivered", "anchor_on_bearer"]


def main(argv):
    global DROPPED
    if len(argv) != 2:
        print(__doc__)
        return 2
    path = os.path.join(argv[1], "vectors.json")
    doc = json.load(open(path, encoding="utf-8"))
    extra = sorted(set(os.listdir(argv[1])) - {"vectors.json", "README.md"})
    fails = check(doc)
    if extra:
        fails.append(f"files the corpus does not hold: {extra}")
    print(f"{len(doc['cases'])} cases, {len(doc['offline'])} offline cases: {len(fails)} failure(s)")
    caught = 0
    for m in mutations(doc):
        d = copy.deepcopy(doc)
        m(d)
        if check(d, quiet=True):
            caught += 1
        else:
            fails.append(f"mutation {m.__name__} was not caught")
    print(f"{caught} of {len(mutations(doc))} mutated copies fail")
    weak = 0
    for w in WEAKENINGS:
        DROPPED = w
        if check(doc, quiet=True):
            weak += 1
        else:
            fails.append(f"a verifier without its {w} check passes the corpus")
    DROPPED = None
    print(f"{weak} of {len(WEAKENINGS)} weakened verifiers are caught")
    for f in fails:
        print("FAIL", f)
    return 1 if fails else 0


if __name__ == "__main__":
    sys.exit(main(sys.argv))