"""
fanscan.py -- a product unit reading two produced streams, scanned
under a real reader: the fan-in leftover set against the tile lemma.

QUESTION. graphs.py prices a tree of product units by the narrowed
reader's programme: a product unit reading U and V through hulls inset
by eta_U and eta_V is alive at delay L when

    v = (w - 1) - (Lam w - tau_V eta_U - tau_U eta_V)/b^L >= 0,

Lam = tau_U + tau_V, tau the streams' largest magnitudes (the bound
|u1 v1 - u2 v2| <= tau_V h_U + tau_U h_V over hulls of widths h_U and
h_V). That is a derivation. Does a real reader agree: the producers'
narrowed tiles as the hulls, the tile lemma's zone test on the
product's exact image?

THE INSTRUMENT. A stream is (lo, hi, alpha, beta): its level-n hulls are
its tiles narrowed by alpha below and beta above,
[(q - M- + alpha)/b^n, (q + M+ - beta)/b^n], each intersected with its
parent's hull, the level-0 hull clipped to the stream's range [lo, hi].
A fresh stream is (-M-, M+, 0, 0): its hulls are its boxes. A narrowed
producer keeps its value inside every committed prefix's narrowed tile
(chains.py's inset law: a reader into tiles narrowed by alpha and beta
reads x y at L1 if alpha + beta <= S(L1)), so these hulls hold every
fibre: a scan finding no kill over them finds none over the fibres.
The product's image over two hulls is the interval of its four corner
products, exact on a rectangle. It KILLS at depth n and delay L iff it
strictly contains a zone of the output's level n - L tiles
(manystream.py's Cell.kills), the tiles narrowed by (a, c) for a
head's own check. Exact integers over one denominator, int64 under an
asserted bound. The scan is exhaustive over every pair of hulls at
depths L + 1 to N, the output level n - L at least 1 (so an L = 1 row
reads depths 2 to 4, an L = 2 row depths 3 and 4); a miss to depth N
is an observation at that depth, not a proof of life.

HAND VALUES (re-derived before the code). (4, 2, 2): x y's floor 2,
S(2) = 2/9, room 2/9 a side, insets 1/9 a side; z.U at L = 1 has
v = 0 exactly, at zero insets v = -1/27. (8, 3, 5): heads at L1* = 2,
S(2) = 23/196, insets 23/392 a side (rooms 6/49 below, 10/49 above);
the root (x y)(x' y'), Lam = 50/49, at L = 1 has v = +0.0120, at zero
insets v = -1/343.

CONTROLS (frozen before the code). K0: (x y).z at (4, 2, 2), the
produced stream first: L = 1 at the head's insets reads no kill to
N = 4, L = 0 kills. K1: z.(x y), the produced stream second, which
K0 leaves unread: the same. KH: the heads at (8, 3, 5), x y at
L = 2 into tiles narrowed by 23/392 a side, no kill to N = 4; at L = 1
a kill. KP: P's root at (8, 3, 5) at its floor, L = 2, zero insets,
two produced inputs, v = 1/7 - (400/343)/64 > 0: no kill to N = 4.

PREDICTION AND KILL (frozen). P's root at (8, 3, 5), L = 1, both heads
at their insets: no kill to N = 4; at L = 0 a kill; at zero insets
printed, no prediction. KILL: P's L = 1 row prints a kill depth.

FINDINGS (every number a print of the run below).
  K0 and K1 pass: at (4, 2, 2) the threshold-miss gain reads no kill
  to depth 4 at L = 1 in either order, and dies at depth 1 at L = 0.
  At zero insets L = 1 kills at depth 4 in both orders over the
  hulls (a kill over hulls, not a real producer's death): the scan
  resolves the deficit v = -1/27, the inset the gain's whole cause. A
  planted break, run on a scratch copy and not part of this run (the
  second hull built at zero inset), fails K1 alone: z.(x y) at L = 1
  kills at depth 4, K0 untouched.
  KH passes: x y at (8, 3, 5) into tiles narrowed 23/392 a side reads
  no kill at L = 2 and kills at depth 2 at L = 1.
  KP passes: the root at its floor with zero insets reads no kill at
  depths 3 and 4. Planted breaks, each on a scratch copy and not part
  of this run: an output level one too high fails KP with K0, K1 and
  KH; hulls widened 1/4 above fail K0 and K1, and a zone test eager by
  1/64 fails K0, K1 and KH, both leaving KP passing, its margin
  v = 0.1246 of w - 1 = 1/7.
  P: the root (x y)(x' y') at L = 1, both heads at their insets,
  reads no kill to depth 4; the kill misses. At L = 0 it kills at
  depth 1, and at L = 1 over zero-inset hulls at depth 4: the scan
  resolves the 1/343 deficit too. So the leftover's live verdict at
  (8, 3, 5), the
  tree reading at 3 against the naive 4, holds under a real reader to
  depth 4, and the gain is the insets'.

RUN RECORD. 5/5 checks, 1.0 s, peak commit 24.6 MB under a memory
guard.
"""
import os
import sys
import time
from fractions import Fraction as Fr
from math import lcm

os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
import numpy as np  # noqa: E402

import manystream as ms  # noqa: E402

CHECKS = []
BOUND = 2 ** 62


def check(name, ok, detail=""):
    CHECKS.append(bool(ok))
    tail = f"  ({detail})" if detail else ""
    print(f"  {'PASS' if ok else 'FAIL'}  {name}{tail}")


def fresh(cell):
    return (-cell.Mm, cell.Mp, Fr(0), Fr(0))


def xy(cell, alpha, beta):
    return (-cell.Mm * cell.Mp, cell.Mh ** 2, Fr(alpha), Fr(beta))


def hulls(cell, stream, N):
    """{n: sorted distinct hulls at level n}, n = 1..N, as Fractions."""
    lo, hi, al, be = stream
    b = cell.b
    D = range(-cell.am, cell.ap + 1)
    level = {(0, (max(lo, -cell.Mm + al), min(hi, cell.Mp - be)))}
    out = {}
    for n in range(1, N + 1):
        s = Fr(1, b ** n)
        new = set()
        for p, (plo, phi) in level:
            for e in D:
                q = b * p + e
                a = max((q - cell.Mm + al) * s, plo)
                c = min((q + cell.Mp - be) * s, phi)
                if a <= c:
                    new.add((q, (a, c)))
        level = new
        out[n] = sorted({h for _, h in level})
    return out


def scan(cell, U, V, L, N, out=(0, 0)):
    """Least depth n <= N at which some image of u v over a U hull and a
    V hull kills at delay L (output tiles narrowed by out), or None."""
    b = cell.b
    a_o, c_o = Fr(out[0]), Fr(out[1])
    den = lcm(*[x.denominator for x in (*U, *V, a_o, c_o, cell.Mm, cell.Mp)])
    hu, hv = hulls(cell, U, N), hulls(cell, V, N)
    for n in range(1, N + 1):
        if n - L < 1:
            continue
        Dn = den * b ** n
        ul = np.array([int(h[0] * Dn) for h in hu[n]], dtype=np.int64)
        uh = np.array([int(h[1] * Dn) for h in hu[n]], dtype=np.int64)
        vl = np.array([int(h[0] * Dn) for h in hv[n]], dtype=np.int64)
        vh = np.array([int(h[1] * Dn) for h in hv[n]], dtype=np.int64)
        # image at level n - L, scaled: value * b^(n-L)... in units of
        # b^-(n-L): img * b^(n - L) = P / Dn^2 * b^(n - L). With
        # K = Dn^2 * den, floor(lo + M- - a) < hi - M+ + c becomes
        # floor(X / K) * K < Y, X = P_lo b^(n-L) den + (M- - a) K.
        K = Dn * Dn * den
        sh = b ** (n - L) * den
        mlo = int((cell.Mm - a_o) * K)
        mhi = int((cell.Mp - c_o) * K)
        big = max(int(np.abs(np.concatenate([ul, uh, vl, vh])).max()), 1)
        assert big * big * sh + max(abs(mlo), abs(mhi)) < BOUND, "int64"
        for x0, x1 in zip(ul, uh):
            c = np.stack([x0 * vl, x0 * vh, x1 * vl, x1 * vh])
            X = c.min(axis=0) * sh + mlo
            Y = c.max(axis=0) * sh - mhi
            if np.any((X // K) * K < Y):
                return n
    return None


def show(label, got):
    print(f"    {label:58s} {'none' if got is None else got}")
    return got


def main():
    t0 = time.time()
    N = 4
    print("K0, K1  (4, 2, 2): the threshold-miss gain, both orders")
    c = ms.Cell(4, 2, 2)
    U, U0, z = xy(c, Fr(1, 9), Fr(1, 9)), xy(c, 0, 0), fresh(c)
    k0a = show("(x y).z  L = 1, insets 1/9", scan(c, U, z, 1, N))
    k0b = show("(x y).z  L = 0, insets 1/9", scan(c, U, z, 0, N))
    k0c = show("(x y).z  L = 1, zero insets", scan(c, U0, z, 1, N))
    k1a = show("z.(x y)  L = 1, insets 1/9", scan(c, z, U, 1, N))
    k1b = show("z.(x y)  L = 0, insets 1/9", scan(c, z, U, 0, N))
    k1c = show("z.(x y)  L = 1, zero insets", scan(c, z, U0, 1, N))
    check("K0 the produced stream first: L = 1 lives, L = 0 dies",
          k0a is None and k0b is not None)
    check("K1 the produced stream second: the same",
          k1a is None and k1b is not None)

    print("KH  (8, 3, 5): the heads into narrowed tiles")
    c = ms.Cell(8, 3, 5)
    e = Fr(23, 392)
    x = fresh(c)
    kha = show("x y  L = 2 into tiles narrowed 23/392 a side",
               scan(c, x, x, 2, N, out=(e, e)))
    khb = show("x y  L = 1 into tiles narrowed 23/392 a side",
               scan(c, x, x, 1, N, out=(e, e)))
    check("KH the head reads at L1* = 2 narrowed, not at 1",
          kha is None and khb is not None)

    print("P  (8, 3, 5): (x y)(x' y'), both heads narrowed")
    H, H0 = xy(c, e, e), xy(c, 0, 0)
    pa = show("root L = 1, insets 23/392", scan(c, H, H, 1, N))
    pb = show("root L = 0, insets 23/392", scan(c, H, H, 0, N))
    pc = show("root L = 1, zero insets", scan(c, H0, H0, 1, N))
    pd = show("root L = 2, zero insets", scan(c, H0, H0, 2, N))
    check("KP P's root at its floor, zero insets, lives", pd is None)
    print(f"  KILL {'FIRES' if pa is not None else 'misses'}: "
          f"P's L = 1 row {'kills' if pa is not None else 'reads none'} "
          f"to N = {N}")
    check("P's break: the root one delay lower dies", pb is not None)
    del k0c, k1c, pc
    print(f"{sum(CHECKS)}/{len(CHECKS)} checks, {time.time() - t0:.1f} s")
    return 0 if all(CHECKS) else 1


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