#!/usr/bin/env python3
"""A one-parameter graph pair whose ONLY unsafe theta is an interior singleton.

Built against the published AH004-REDUCTION-v1 sources (digests checked separately in
verify_sources.sh): reduction.py (author's verifier), reduction_oracle.py (author's cell
enumeration), graph_model.py/verify_graph.py (unchanged upstream).

What it is for. The author's AH004-CELL-COVER-v1 scope lists "omit an interior singleton or
open interval" among its predeclared controls. This file supplies one concrete instance of that
control, and separates three sentences that are easy to conflate:

  A. "both original endpoints are covered"  -> does NOT imply coverage of the box.
  B. "the author's cell set keeps the singleton"      -> true, and checkably so.
  C. "a cell set of endpoints plus open-interval midpoints is enough" -> false, and here is
     the pair on which it prints safe.

The construction is exact rational, one parameter, target B, eta = 0:

    source   K0 = theta - 1/2,  K1 = 1/2 - theta,  O0 = -2,  O1 = 0     (both keep=True/False as named)
    abstract K0, K1, O0 unchanged;  O1 = -1

O1 is the only bad action (keep=False, target B). O1 is admissible iff every competitor is
within eta = 0 of it: K0 gives theta <= 1/2, K1 gives theta >= 1/2, O0 gives -2 <= 0 always.
So the source has a bad path at theta = 1/2 EXACTLY, and at no other theta in [-1, 1]. The
abstract's O1 sits one unit lower, so it is admissible nowhere and the abstract is safe.

Run: python3 interior_singleton.py
"""
import json
import sys
from fractions import Fraction as Q

from reduction import certificate, verify_reduction
from reduction_oracle import cells, paths

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 report():
    s, t = source(), abstract()
    out = {"fixture": "interior-singleton", "box": BOX, "eta": "0"}
    checks = []

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

    # 1. The witness itself, and both endpoints.
    bad_at_half = paths(s, (Q(1, 2),))
    note("source has a bad path at the interior midpoint 1/2", bad_at_half,
         "paths = " + repr(sorted(bad_at_half)))
    lo, hi = paths(s, (Q(-1),)), paths(s, (Q(1),))
    note("source is safe at BOTH endpoints", not lo and not hi,
         "theta=-1 -> " + repr(sorted(lo)) + " ; theta=+1 -> " + repr(sorted(hi)))

    # 2. Sweep: the unsafe set really is the singleton, not a thin interval.
    hits = []
    for k in range(-2000, 2001):
        theta = Q(k, 2000)
        if paths(s, (theta,)):
            hits.append(theta)
    note("a 4001-point sweep finds exactly one unsafe theta", hits == [Q(1, 2)],
         "hits = " + repr(hits))
    for exponent in (30, 60):
        eps = Q(1, 10 ** exponent)
        left, right = paths(s, (Q(1, 2) - eps,)), paths(s, (Q(1, 2) + eps,))
        note(f"source is safe at 1/2 -/+ 10^-{exponent}",
             not left and not right,
             f"eps={eps}: left={sorted(left)} right={sorted(right)}")

    # 3. The abstraction is safe everywhere, the witness included.
    note("abstract is safe at the witness theta", not paths(t, (Q(1, 2),)),
         "abstract paths at 1/2 = " + repr(sorted(paths(t, (Q(1, 2),)))))

    # 4. The author's verifier on this pair.
    exact = verify_reduction(s, t, certificate(s, t,
                                               {n["name"]: n["name"] for n in s["nodes"]},
                                               {n["name"]: {a["name"]: a["name"] for a in n["actions"]}
                                                for n in s["nodes"]}, "exact"))
    note("author's verify_reduction rejects the exact-mode relation", exact["status"] == "UNKNOWN",
         exact.get("reason", exact["status"]))

    # 5. The author's own cell enumeration, and two variants that are not complete.
    author_cells = [tuple(x) for x in cells(s, t)]
    note("author's cells() keeps the singleton", (Q(1, 2),) in author_cells,
         "cells = " + repr([str(x[0]) for x in author_cells]))
    endpoints_and_midpoints = [(Q(-1),), (Q(0),), (Q(1),)]
    missed = [x for x in endpoints_and_midpoints if not paths(s, x)]
    note("endpoints-plus-a-midpoint sees a safe source at every sampled theta",
         len(missed) == len(endpoints_and_midpoints),
         "sampled = " + repr([str(x[0]) for x in endpoints_and_midpoints])
         + " ; unsafe among them: " + repr([str(x[0]) for x in endpoints_and_midpoints if paths(s, x)]))

    # The variant that a naive implementation produces: keep the extrema, and the midpoints of
    # the intervals between consecutive cut points, but drop the cut points themselves.
    cuts = sorted({x[0] for x in author_cells if x[0] in (Q(-1), Q(-1, 2), Q(1, 2), Q(1))})
    variant = [Q(-1)] + [(a + b) / 2 for a, b in zip(cuts, cuts[1:])] + [Q(1)]
    variant_set = {(x,) for x in variant}
    note("a cell set of extrema plus open-interval midpoints misses the witness",
         (Q(1, 2),) not in variant_set,
         "variant = " + repr([str(x) for x in variant]))
    note("and that variant reports the source safe at every theta it samples",
         all(not paths(s, x) for x in sorted(variant_set)),
         "unsafe among variant samples: " + repr([str(x[0]) for x in sorted(variant_set) if paths(s, x)]))

    # Coverage of the box as a set: a finite union of points and open intervals covering [-1,1]
    # must carry the point itself, because no open interval around it can be closed onto it.
    open_cells = [(a, b) for a, b in zip(cuts, cuts[1:])]
    note("no open cell of the decomposition contains the witness point",
         not any(a < Q(1, 2) < b for a, b in open_cells),
         "open cells = " + repr([(str(a), str(b)) for a, b in open_cells]))

    out["checks"] = checks
    out["passed"] = sum(1 for c in checks if c["ok"])
    out["total"] = len(checks)
    return out


if __name__ == "__main__":
    result = report()
    print(json.dumps(result, indent=2, default=str))
    print(f"\n{result['passed']}/{result['total']} checks as expected")
    sys.exit(0 if result["passed"] == result["total"] else 1)