#!/usr/bin/env python3
"""Run the author's published AH004-REDUCTION-v1 verifier; report what it answers.

Scope, stated before the numbers: this executes the author's own reduction.py against the
author's own fixtures. It is a second execution of their checker on another machine, not an
independent formal review, not verification of the 2105-cell corpus, not a statement about any
real system. The files executed are the published bytes, digest-checked in verify_sources.sh.

Run: python3 run_author_verifier.py
"""
import json
import sys
from copy import deepcopy
from fractions import Fraction as Q

from reduction import certificate, verify_reduction
from reduction_fixtures import (approximate, midpoint_trap, representative_left,
                                score_alias, channel_alias, shifted_fork)
from reducer import compact


def relation(s, t, mode="over"):
    return 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"]}, mode)


def verdict(s, t, mode="over"):
    v = verify_reduction(s, t, relation(s, t, mode))
    return v["status"] + ("" if v["status"] == "RELATION_VALID" else " (" + v["reason"] + ")")


def main():
    out, checks = {}, []

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

    # 1. The exact compressor on the discriminating fixtures: relation valid.
    for name, fn in (("score_alias", score_alias), ("channel_alias", channel_alias)):
        s = fn()
        t, c = compact(s)
        out[name + "/compact"] = verify_reduction(s, t, c)["status"]
        note(f"compact({name}) is accepted by the verifier",
             out[name + "/compact"] == "RELATION_VALID", out[name + "/compact"])
        # The deliberate unsound merge must be refused.
        bad, mapping = representative_left(s)
        out[name + "/representative_left"] = verify_reduction(s, bad, relation(s, bad))["status"]
        note(f"representative_left({name}) is refused",
             out[name + "/representative_left"] == "UNKNOWN",
             out[name + "/representative_left"])

    # 2. Shifted fork: a legitimate common affine shift must survive.
    s = shifted_fork()
    t, c = compact(s)
    v = verify_reduction(s, t, c)
    out["shifted_fork/compact"] = v["status"]
    note("shifted_fork compacts to a valid relation", v["status"] == "RELATION_VALID",
         v["status"] + " max_gap_distortion=" + str(v.get("max_gap_distortion")))

    # 3. Sharp tolerance: eta_bar = 2*eps keeps the bad action; anything less loses it.
    sharp = {}
    for eps in (Q(1, 10), Q(1, 10 ** 50)):
        s, t = approximate(eps)
        row = {"eta_bar=2*eps": verdict(s, t)}
        for label, eta in (("2*eps-1e-60", 2 * eps - Q(1, 10 ** 60)), ("0", Q(0))):
            u = deepcopy(t)
            u["eta"] = str(eta)
            row["eta_bar=" + label] = verdict(s, u)
        sharp[str(eps)] = row
        under = [v for k, v in row.items() if k != "eta_bar=2*eps"]
        note(f"eps={eps}: the equality case is accepted and both underinflations are refused",
             row["eta_bar=2*eps"] == "RELATION_VALID"
             and all(v.startswith("UNKNOWN") for v in under),
             json.dumps(row))
    out["sharp_tolerance"] = sharp

    # 4. midpoint_trap: the verifier refuses a reduction that agrees at the interior midpoint.
    s, t = midpoint_trap()
    out["midpoint_trap"] = verdict(s, t)
    note("midpoint_trap is refused", out["midpoint_trap"].startswith("UNKNOWN"), out["midpoint_trap"])

    # 5. The interior-singleton pair from this workspace.
    from interior_singleton import abstract, source
    s, t = source(), abstract()
    out["interior_singleton"] = verdict(s, t, "exact")
    note("interior_singleton is refused in exact mode",
         out["interior_singleton"].startswith("UNKNOWN"), out["interior_singleton"])

    # 6. The verifier cannot depend on a corpus: it imports the parser and the certificate
    #    checker and nothing else. Assert it from the module object, not from the source text.
    import reduction
    own = sorted(set(reduction.__dict__) & {"cells", "paths", "projected", "compact"})
    note("reduction.py exposes no corpus helper of its own", not own, "module-level names: " + repr(own))
    note("reduction.py has been imported without pulling the fixture generator from it",
         "reduction_fixtures" not in getattr(reduction, "__dict__", {}),
         "no direct reference to a cell corpus on the module under test")

    result = {"passed": sum(1 for c in checks if c["ok"]), "total": len(checks),
              "verdicts": out, "checks": checks,
              "scope": "Author's verifier re-executed on published bytes; not an independent "
                       "formal review and not evidence about any real system."}
    return result


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