#!/usr/bin/env python3
"""Drive AH004-CELL-COVER-v1 (producer + verifier) on an instance it did not author.

The instance is my interior_singleton: box [-1,1], eta=0, target B, one bad point at theta=1/2.
The author's kernel claims completeness for the one-parameter predicate implication, so the
expected answer for this pair is COUNTEREXAMPLE at theta=1/2 — not TRANSFER_VALID.

Also checks, on the same pair, that their verifier refuses a cover that keeps only the point
strata (a point-only producer), and reports the author's own two fixtures for comparison.
"""
import json
from copy import deepcopy
from fractions import Fraction as Q

import cell_cover
from cell_cover import build, inspect, partition
from cover_fixtures import interior_tie, open_transfer_loss
from graph_model import parse
from verify_cover import verify

BOX = [["-1", "1"]]


def action(name, base, bit, keep, c, v):
    return {"name": name, "base": base, "bit": bit, "keep": keep,
            "c": str(c), "v": [str(x) for x in v], "next": []}


def graph(actions):
    return {"root": "root", "target": "B", "eta": "0", "box": BOX,
            "nodes": [{"name": "root", "actions": actions}]}


def source():
    return graph([action("K0", "K", 0, True, Q(-1, 2), (1,)),
                  action("K1", "K", 1, True, Q(1, 2), (-1,)),
                  action("O0", "O", 0, False, Q(-2), (0,)),
                  action("O1", "O", 1, False, Q(0), (0,))])


def abstract():
    raw = source()
    for a in raw["nodes"][0]["actions"]:
        if a["name"] == "O1":
            a["c"] = "-1"
    return raw


def point_only_cover(s, t):
    """A producer that walks the cut list and never builds an open-cell proof."""
    ps, pt = parse(s), parse(t)
    cuts, _cells = partition(ps, pt, 10000)
    rows = []
    for x in cuts:
        src, dst = inspect(ps, x), inspect(pt, x)
        if src["type"] == "safe_set":
            side, proof = "source_safe", src
        elif dst["type"] == "safe_set":
            side, proof = "source_safe", src      # wrongly approves: source is bad here
        else:
            side, proof = "abstract_bad", dst
        rows.append({"kind": "point", "lo": str(x), "hi": str(x),
                     "representative": str(x), "side": side, "proof": proof})
    return {"schema": cell_cover.SCHEMA, "kind": "COVER", "source_hash": ps.hash,
            "abstract_hash": pt.hash, "target": s["target"], "domain": ["-1", "1"],
            "cuts": [str(c) for c in cuts], "cells": rows}


def main() -> int:
    s, t = source(), abstract()
    checks = []

    def note(name, ok, detail):
        checks.append({"check": name, "ok": bool(ok), "detail": detail})

    out = build(deepcopy(s), deepcopy(t))
    status = out["status"]
    cert = out.get("certificate") or {}
    theta = cert.get("theta")
    note("their complete producer reports a counterexample, not a valid transfer",
         status == "COUNTEREXAMPLE", f"status={status} theta={theta}")
    note("the counterexample is at the interior singleton theta=1/2",
         theta is not None and Q(theta) == Q(1, 2), f"theta={theta}")

    v = verify(deepcopy(s), deepcopy(t), cert) if status == "COUNTEREXAMPLE" else {}
    note("their verifier accepts the counterexample certificate",
         v.get("status") == "COUNTEREXAMPLE_VALID" and Q(v.get("theta")) == Q(1, 2),
         json.dumps(v)[:200])
    note("the source-bad witness is the path ((root, O1),) at that one theta",
         cert.get("source_bad", {}).get("path") == [["root", "O1"]],
         json.dumps(cert.get("source_bad"))[:160])
    note("the abstract-safe witness is a closed safe set containing the root",
         cert.get("abstract_safe", {}).get("type") == "safe_set"
         and "root" in cert.get("abstract_safe", {}).get("nodes", []),
         json.dumps(cert.get("abstract_safe"))[:160])

    fake = point_only_cover(deepcopy(s), deepcopy(t))
    r = verify(deepcopy(s), deepcopy(t), fake)
    note("their verifier refuses a cover built only from point strata",
         r.get("status") == "UNKNOWN", json.dumps(r)[:200])
    note("the refusal names the cell list, not a digest",
         "cell" in json.dumps(r).lower(), json.dumps(r)[:200])

    # The point-only producer's own claim, if its cells were accepted as a full cover.
    note("the point-only cell list really is short of a complete cover",
         len(fake["cells"]) != 2 * len(fake["cuts"]) - 1,
         f"{len(fake['cells'])} cells for {len(fake['cuts'])} cuts")

    for name, maker in (("interior_tie (author's)", interior_tie),
                        ("open_transfer_loss (author's)", open_transfer_loss)):
        a, b = maker()
        res = build(a, b)
        got = (res.get("certificate") or {}).get("theta", res.get("reason", ""))
        note(f"{name}: their producer answers {res['status']} at {got}",
             res["status"] in ("TRANSFER_VALID", "COUNTEREXAMPLE"),
             json.dumps(str(got))[:120])

    result = {"fixture": "interior-singleton vs AH004-CELL-COVER-v1", "checks": checks,
              "passed": sum(1 for c in checks if c["ok"]), "total": len(checks)}
    print(json.dumps(result, indent=2))
    return 0 if all(c["ok"] for c in checks) else 1


if __name__ == "__main__":
    raise SystemExit(main())