#!/usr/bin/env python3
from __future__ import annotations
from pathlib import Path
import sys

EXPECTED_CONTRACT = "OMEGA_NAUGHT/1.0"
EXPECTED_ALGEBRA = "Q(T)[lambda]/(lambda^2-T*lambda-T^2)"
EXPECTED_Q = 339949771344778
EXPECTED_S = 1000000000000000
EXPECTED_L60 = 339949771344778929576702809321279193551009905014259416689444
EXPECTED_U60 = EXPECTED_L60 + 1
REQUIRED_KEYS = ("contract", "algebra", "bits", "Q", "S", "L60", "U60")


def read_manifest(path: str) -> dict[str, str]:
    out: dict[str, str] = {}
    for raw in Path(path).read_text(encoding="utf-8").splitlines():
        line = raw.strip()
        if not line or line.startswith("#"):
            continue
        if "=" not in line:
            raise ValueError(f"bad manifest line: {raw!r}")
        k, v = line.split("=", 1)
        k, v = k.strip(), v.strip()
        if k not in REQUIRED_KEYS:
            raise ValueError(f"unknown manifest key: {k}")
        if k in out:
            raise ValueError(f"duplicate manifest key: {k}")
        out[k] = v
    missing = [k for k in REQUIRED_KEYS if k not in out]
    if missing:
        raise ValueError(f"missing manifest keys: {missing}")
    return out


class Laurent:
    """Integer Laurent polynomial in T: sum c[e] T^e."""
    def __init__(self, c: dict[int, int] | None = None):
        self.c = {e: v for e, v in (c or {}).items() if v}

    @staticmethod
    def mono(exp: int, coeff: int = 1) -> "Laurent":
        return Laurent({exp: coeff}) if coeff else Laurent()

    def __add__(self, other: "Laurent") -> "Laurent":
        d = dict(self.c)
        for e, v in other.c.items():
            d[e] = d.get(e, 0) + v
            if d[e] == 0:
                del d[e]
        return Laurent(d)

    def __neg__(self) -> "Laurent":
        return Laurent({e: -v for e, v in self.c.items()})

    def __sub__(self, other: "Laurent") -> "Laurent":
        return self + (-other)

    def __mul__(self, other: "Laurent") -> "Laurent":
        d: dict[int, int] = {}
        for e, a in self.c.items():
            for f, b in other.c.items():
                d[e + f] = d.get(e + f, 0) + a * b
        return Laurent(d)

    def shift(self, k: int) -> "Laurent":
        return Laurent({e + k: v for e, v in self.c.items()})

    def is_zero(self) -> bool:
        return not self.c

    def __eq__(self, other: object) -> bool:
        return isinstance(other, Laurent) and self.c == other.c


class K:
    """A(T)+B(T)lambda in Q(T)[lambda]/(lambda^2-Tlambda-T^2).

    For the contract checks only integer Laurent coefficients are needed.
    """
    def __init__(self, a: Laurent | None = None, b: Laurent | None = None):
        self.a = a or Laurent()
        self.b = b or Laurent()

    @staticmethod
    def one() -> "K":
        return K(Laurent.mono(0), Laurent())

    @staticmethod
    def T() -> "K":
        return K(Laurent.mono(1), Laurent())

    @staticmethod
    def Tinv() -> "K":
        return K(Laurent.mono(-1), Laurent())

    @staticmethod
    def lam() -> "K":
        return K(Laurent(), Laurent.mono(0))

    def __add__(self, other: "K") -> "K":
        return K(self.a + other.a, self.b + other.b)

    def __neg__(self) -> "K":
        return K(-self.a, -self.b)

    def __sub__(self, other: "K") -> "K":
        return self + (-other)

    def __mul__(self, other: "K") -> "K":
        # lambda^2 = T*lambda + T^2
        bd = self.b * other.b
        a = self.a * other.a + bd.shift(2)
        b = self.a * other.b + self.b * other.a + bd.shift(1)
        return K(a, b)

    def is_zero(self) -> bool:
        return self.a.is_zero() and self.b.is_zero()

    def __eq__(self, other: object) -> bool:
        return isinstance(other, K) and self.a == other.a and self.b == other.b


def check(name: str, ok: bool, results: list[tuple[str, bool]]) -> None:
    results.append((name, bool(ok)))


def main() -> int:
    manifest_path = sys.argv[1] if len(sys.argv) > 1 else "OMEGA_NAUGHT_1_0.manifest"
    m = read_manifest(manifest_path)
    results: list[tuple[str, bool]] = []

    check("manifest.contract", m.get("contract") == EXPECTED_CONTRACT, results)
    check("manifest.algebra", m.get("algebra") == EXPECTED_ALGEBRA, results)

    bits = int(m["bits"])
    Q = int(m["Q"])
    S = int(m["S"])
    L60 = int(m["L60"])
    U60 = int(m["U60"])
    check("manifest.expected_L60", L60 == EXPECTED_L60, results)
    check("manifest.expected_U60", U60 == EXPECTED_U60, results)
    check("manifest.expected_Q", Q == EXPECTED_Q, results)
    check("manifest.expected_S", S == EXPECTED_S, results)

    one, T, Ti, lam = K.one(), K.T(), K.Tinv(), K.lam()
    omega = Ti
    tau = T
    phi = lam * Ti
    mu = one - lam
    pi_k = omega - phi

    check("exact.omega_tau", omega * tau == one, results)
    check("exact.lambda_mu", lam + mu == one, results)
    check("exact.lambda_relation", (lam * lam - tau * lam - tau * tau).is_zero(), results)
    check("exact.phi_quadratic", (phi * phi - phi - one).is_zero(), results)
    check("exact.phi_pi_omega", phi + pi_k == omega, results)

    qs_decimal = f"0.{Q:015d}" if S == 10**15 and 0 <= Q < S else ""
    check("finite.qs_decimal", qs_decimal == "0.339949771344778", results)
    check("finite.ledger_adjacent", U60 - L60 == 1, results)
    check("finite.qs_below_L60", Q * 10**45 < L60, results)

    replay_ok = bits == 15
    if replay_ok:
        for d in range(1 << bits):
            y = Q * d
            f = y // S
            rho = y - S * f
            if not (0 <= rho < S):
                replay_ok = False
                break
            num = S * f + rho
            q, r = divmod(num, Q)
            if r != 0 or q != d:
                replay_ok = False
                break
    check("finite.unsigned_15bit_replay", replay_ok, results)

    scale = 10**60
    interval_ok = bits == 15
    if interval_ok:
        for d in range(1 << bits):
            qf = (Q * d) // S
            if d == 0:
                if qf != 0:
                    interval_ok = False
                    break
                continue
            lower_floor = (L60 * d) // scale
            upper = U60 * d
            uq, ur = divmod(upper, scale)
            upper_floor = uq - 1 if ur == 0 else uq
            if lower_floor != upper_floor or lower_floor != qf:
                interval_ok = False
                break
    check("finite.interval_floor_15bit", interval_ok, results)

    for name, ok in results:
        print(f"{name}={'PASS' if ok else 'FAIL'}")
    passed = all(ok for _, ok in results)
    print(f"RESULT={'PASS' if passed else 'FAIL'}")
    return 0 if passed else 1


if __name__ == "__main__":
    raise SystemExit(main())