"""The recipe codec on every short string and at every boundary of the format.

Checked for both encoders: the round trip, the length bound of the completeness
lemma, and that the reserved tag 128 is never emitted. The boundaries covered
are the 127-byte literal cap and the run lengths that map to the extreme repeat
tags, together with exhaustive coverage at small lengths.
"""
import itertools
import json
import os
import random
import sys

sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
from selfrep import describe, describe_literal, decode

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 bound(n: int) -> int:
    return n + -(-n // 127) + 1


def tags(tape: bytes):
    i, out = 0, []
    while True:
        t = tape[i]
        out.append(t)
        i += 1
        if t == 0:
            return out
        i += t if t <= 127 else 1


class Audit:
    def __init__(self):
        self.n = 0
        self.roundtrip = []
        self.overlong = []
        self.not_tight = []
        self.tag128 = []

    def check(self, b: bytes) -> None:
        self.n += 1
        for enc in (describe, describe_literal):
            r = enc(b)
            if decode(r) != b:
                self.roundtrip.append((enc.__name__, len(b)))
            if len(r) > bound(len(b)):
                self.overlong.append((enc.__name__, len(b), len(r)))
        if len(describe_literal(b)) != bound(len(b)):
            self.not_tight.append(len(b))
        if 128 in tags(describe(b)):
            self.tag128.append(len(b))

    @property
    def ok(self) -> bool:
        return not (self.roundtrip or self.overlong or self.not_tight or self.tag128)


def main() -> int:
    a = Audit()
    for n in range(0, 15):
        for t in itertools.product((0, 1), repeat=n):
            a.check(bytes(t))
    binary = a.n
    for n in range(0, 10):
        for t in itertools.product((0, 1, 2), repeat=n):
            a.check(bytes(t))
    ternary = a.n - binary
    print(f"  exhaustive: {binary:,} binary strings to length 14, "
          f"{ternary:,} ternary to length 9")

    edges = (list(range(0, 12))
             + [126, 127, 128, 129, 130, 251, 252, 253, 254, 255, 256, 257,
                380, 381, 382, 508, 509, 510])
    before = a.n
    for L in edges:
        a.check(bytes([0x41]) * L)
        a.check(bytes([0x00]) * L)
        a.check(bytes([0xFF]) * L)
        a.check(bytes(range(256))[:L] if L <= 256 else bytes(range(256)) * (L // 256))
        a.check(bytes([0x41] * L + [0x42]))
        a.check(bytes([0x42] + [0x41] * L))
        a.check(bytes([0x41] * L + [0x42] * L))
        a.check(bytes(([0x41] * 4 + [0x42]) * max(1, L)))
        a.check(bytes(([0x41] * 3 + [0x42]) * max(1, L)))
    print(f"  boundaries: {a.n - before:,} strings straddling the literal cap, "
          f"the extreme repeat tags, and the run/literal transitions")

    rng = random.Random(11)
    before = a.n
    for _ in range(4000):
        n = rng.randrange(0, 900)
        alpha = rng.choice([2, 3, 7, 256])
        a.check(bytes(rng.randrange(alpha) for _ in range(n)))
    for _ in range(1500):
        n = rng.randrange(0, 900)
        out = bytearray()
        while len(out) < n:
            out += bytes([rng.randrange(256)]) * rng.choice([1, 2, 3, 4, 5, 126, 127, 128, 253])
        a.check(bytes(out[:n]))
    print(f"  random and run-structured: {a.n - before:,} strings")

    print(f"  total {a.n:,}: round-trip exact, neither encoder exceeds "
          f"|f| + ceil(|f|/127) + 1, the literal encoder attains it, "
          f"tag 128 never emitted: {'yes' if a.ok else 'NO'}")
    if not a.ok:
        print("   roundtrip:", a.roundtrip[:5])
        print("   overlong:", a.overlong[:5])
        print("   not tight:", a.not_tight[:5])
        print("   tag128:", a.tag128[:5])
    json.dump({"strings": a.n, "roundtrip_failures": len(a.roundtrip),
               "bound_failures": len(a.overlong),
               "literal_not_tight": len(a.not_tight),
               "tag128_emitted": len(a.tag128)},
              open(runs_path("paper_codec.json"), "w"), indent=1)
    return 0 if a.ok else 1


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