"""The constructor on tapes that are not recipes.

Two statements are checked. First, the decoding loop of P halts on an arbitrary
tape exactly when a tag byte in {0, 128} is reached, counting the stale input
register as the tag once the tape is exhausted, and its output on every such
tape is the extension of delta computed by selfrep.decode_any. Second, the
program P_e obtained by inserting one end-of-tape guard after the tag read
halts on every tape, agrees with P on recipes, and runs in at most
643 |tau| + 9 steps.
"""
import json
import os
import random
import sys

sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
from selfrep import (HOST_PATH, M_STAR, P, P_TOTAL, decode, decode_any, describe,
                     describe_literal, memory_image, run_reference, tau_star)

REPO = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
M_E = memory_image(P_TOTAL)
M_PP = memory_image(P)


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 budget(tape: bytes) -> int:
    """The bound proved for P_e: at most |tau| passes that consume a tape byte,
    each of at most 5*127 + 8 steps, and one final pass of at most nine."""
    return 643 * len(tape) + 9


def tapes():
    rng = random.Random(777)
    out = [(b"", "empty")]
    for t in (0, 1, 2, 127, 128, 129, 200, 255):
        out.append((bytes([t]), f"a single byte {t}"))
        out.append((bytes([t, 0x41]), f"byte {t} then a payload byte"))
    out.append((b"\x05\x01", "a literal token truncated after one payload byte"))
    out.append((b"\x7f", "a literal tag with no payload at all"))
    out.append((b"\xff", "a repeat tag with no payload"))
    out.append((b"\x80\x41\x41", "the reserved tag 128"))
    sigma = open(HOST_PATH, "rb").read()
    r = describe(sigma)
    out.append((r, "a real recipe"))
    out.append((r[:-1], "that recipe with its end token removed"))
    out.append((r[:5000], "a truncated recipe"))
    out.append((tau_star(sigma, M_STAR), "tau*"))
    for _ in range(600):
        n = rng.randrange(0, 60)
        alpha = rng.choice([2, 3, 130, 256])
        out.append((bytes(rng.randrange(alpha) for _ in range(n)), "random"))
    for _ in range(200):
        f = bytes(rng.randrange(rng.choice([2, 256])) for _ in range(rng.randrange(0, 80)))
        enc = rng.choice((describe, describe_literal))
        r = enc(f)
        k = rng.randrange(0, len(r) + 1)
        out.append((r[:k], "a prefix of a recipe"))
    return out


def main() -> int:
    out = {}
    ok = True
    cases = tapes()

    # P: the halting characterization, and the output when it halts.
    diverge = halt = 0
    bad = []
    for tape, label in cases:
        want, halts = decode_any(tape, guard=False)
        cap = budget(tape) * 4
        try:
            got, steps = run_reference(M_PP, tape, max_steps=cap)
        except Exception as exc:                     # pragma: no cover
            bad.append((label, repr(exc)))
            continue
        ran_out = steps >= cap
        if halts:
            halt += 1
            if ran_out or got != want:
                bad.append((label, "halting case wrong"))
        else:
            diverge += 1
            if not ran_out or not got.startswith(want):
                bad.append((label, "divergent case wrong"))
    print(f"  P on {len(cases)} tapes: {halt} halt, {diverge} do not; the "
          f"characterization and the emitted bytes agree in every case: "
          f"{'yes' if not bad else f'NO {bad[:3]}'}")
    ok &= not bad
    out["P_cases"] = len(cases)
    out["P_halting"] = halt
    out["P_divergent"] = diverge
    out["P_failures"] = len(bad)

    # P_e: total, and within the proved bound.
    ebad = []
    worst = 0.0
    for tape, label in cases:
        want, halts = decode_any(tape, guard=True)
        assert halts
        cap = budget(tape)
        got, steps = run_reference(M_E, tape, max_steps=cap + 1)
        if steps > cap or got != want:
            ebad.append((label, steps, cap))
        worst = max(worst, steps / cap)
    print(f"  P_e on the same {len(cases)} tapes: halts on every one, output "
          f"equals the extended decoding, and the step bound 643|tau| + 9 "
          f"holds: {'yes' if not ebad else f'NO {ebad[:3]}'}")
    print(f"  the worst case observed reaches {worst * 100:.0f} per cent of the "
          f"bound")
    ok &= not ebad
    out["Pe_failures"] = len(ebad)
    out["Pe_bound_slack"] = 1 / worst if worst else None

    # P_e agrees with P on recipes.
    rng = random.Random(31337)
    agree = 0
    abad = 0
    for _ in range(300):
        f = bytes(rng.randrange(rng.choice([2, 5, 256]))
                  for _ in range(rng.randrange(0, 400)))
        for enc in (describe, describe_literal):
            r = enc(f)
            a, _ = run_reference(M_PP, r)
            b, _ = run_reference(M_E, r)
            agree += 1
            if not (a == b == f):
                abad += 1
    print(f"  P and P_e emit the same bytes on {agree} recipes, equal to the "
          f"described string: {'yes' if abad == 0 else f'NO ({abad})'}")
    ok &= abad == 0
    out["recipe_agreement"] = agree
    out["recipe_disagreements"] = abad

    # the self-description still goes through, on the total program
    sigma = open(HOST_PATH, "rb").read()
    o, n = run_reference(M_E, describe(sigma))
    same = o == sigma
    print(f"  P_e emits sigma(N_host) from its recipe in {n:,} steps: "
          f"{'exact' if same else 'FAILED'}")
    ok &= same
    out["Pe_selfdescription_steps"] = n
    out["Pe_selfdescription_exact"] = same
    out["Pe_instructions"] = len(P_TOTAL)

    json.dump(out, open(runs_path("paper_total.json"), "w"), indent=1)
    return 0 if ok else 1


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