"""The device against Definition 2.8 of the paper.

Definition 2.8 specifies one device application on the
post-instruction state (x, tau, h, omega):

  (i)   if y[c_wr] = 1 then omega' = omega . y[R_out] and x'[R_out] = 0,
        otherwise omega' = omega;
  (ii)  if y[c_rd] = 1 and h < |tau| then x'[R_in] = tau[h], x'[c_eot] = 0,
        h' = h + 1; if y[c_rd] = 1 and h = |tau| then x'[c_eot] = 1 and h' = h;
        if y[c_rd] = 0 then h' = h;
  (iii) if y[c_rw] = 1 then h' = 0;
  (iv)  finally x'[c_rd] = x'[c_rw] = x'[c_wr] = 0.

The clauses are transcribed here independently of selfrep.Tape and the two are
compared over the whole cross product of request values, head positions and
tapes. The sweep covers non-unit values, so it also decides whether a request
fires on the value 1 alone.
"""
import itertools
import json
import os
import sys

sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
from selfrep import Tape, C_WR, C_EOT, C_RW, C_RD, R_IN, R_OUT

REPO = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))


def runs_path(name: str) -> str:
    d = os.path.join(REPO, "paper", "runs")
    os.makedirs(d, exist_ok=True)
    return os.path.join(d, name)


def spec(mem, tau, h, omega):
    """Definition 2.8, clause by clause, on (mem, h, omega)."""
    m = list(mem)
    w = list(omega)
    if m[C_WR] == 1:                                   # (i)
        w.append(m[R_OUT])
        m[R_OUT] = 0
    hp = h
    if m[C_RD] == 1:                                   # (ii)
        if h < len(tau):
            m[R_IN] = tau[h]
            m[C_EOT] = 0
            hp = h + 1
        else:
            m[C_EOT] = 1
    if m[C_RW] == 1:                                   # (iii)
        hp = 0
    m[C_WR] = m[C_RD] = m[C_RW] = 0                    # (iv)
    return m, hp, w


def main() -> int:
    tapes = [b"", b"\x07", b"\x01\x02", bytes(range(5)), bytes(range(64))]
    vals = (0, 1, 2, 3, 127, 128, 255)
    bad, n = [], 0
    for tau in tapes:
        heads = sorted({0, 1, max(0, len(tau) - 1), len(tau)})
        for h in heads:
            for wr, rd, rw in itertools.product(vals, repeat=3):
                for eot, rin, rout in ((0, 0, 0), (1, 9, 200), (0, 255, 1), (1, 1, 255)):
                    mem = [0] * 256
                    mem[C_WR], mem[C_RD], mem[C_RW] = wr, rd, rw
                    mem[C_EOT], mem[R_IN], mem[R_OUT] = eot, rin, rout
                    mem[0x10] = 0xAB                    # an ordinary cell, must not move
                    want_mem, want_h, want_out = spec(mem, tau, h, b"")

                    dev = Tape(tau)
                    dev.h = h
                    got_mem = list(mem)
                    dev.apply(got_mem)
                    n += 1
                    if (got_mem != want_mem or dev.h != want_h
                            or bytes(dev.out) != bytes(want_out)):
                        bad.append({"tau": len(tau), "h": h, "wr": wr, "rd": rd,
                                    "rw": rw, "eot": eot,
                                    "spec": (want_mem[C_EOT], want_mem[R_IN],
                                             want_mem[R_OUT], want_h, list(want_out)),
                                    "impl": (got_mem[C_EOT], got_mem[R_IN],
                                             got_mem[R_OUT], dev.h, list(dev.out))})
    print(f"  device applications compared: {n:,}")
    print(f"  implementation agrees with Definition 2.8 on every one: "
          f"{'yes' if not bad else f'NO ({len(bad)} disagreements)'}")
    for b in bad[:5]:
        print("   ", b)

    # A request fires on the value 1 and on no other value. The head starts off
    # zero so that a rewind is observable; without that a rewind of a head
    # already at 0 changes nothing and the test would not see it fire.
    fires = []
    for cell in (C_WR, C_RD, C_RW):
        for v in range(256):
            mem = [0] * 256
            mem[cell] = v
            mem[R_OUT] = 0x5A
            dev = Tape(b"\x11\x22")
            dev.h = 1
            before = (dev.h, len(dev.out))
            dev.apply(mem)
            acted = (dev.h, len(dev.out)) != before or mem[R_IN] != 0 or mem[C_EOT] != 0
            if acted != (v == 1):
                fires.append((cell, v, acted))
    print(f"  each request fires exactly on the value 1, over all 256 cell values: "
          f"{'yes' if not fires else f'NO {fires[:5]}'}")

    ok = not bad and not fires
    json.dump({"applications": n, "disagreements": len(bad),
               "value_trigger_failures": len(fires)},
              open(runs_path("paper_device.json"), "w"), indent=1)
    return 0 if ok else 1


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