"""fwide.py -- the record run against the dam's bar past the tau table:
is E/F at most 10 at every t in 4..10^4?

QUESTION. The dam's bar F(t) = max{P+ : tau(P) <= t} is the least
nondecreasing slack every escape from the void pays (dambar.py), but
tau's table to 10^4 fixes it only to t = 1822, where E/F is at most
6.9715. Widened until tau passes 10^4, so that F is fixed at every
t in 4..10^4 (E's range), is the record run's envelope E within 10 F there?

DESIGN. cgreedy.feasible and its striking rule, run over the primes to
a wider bound, the table stopping at the first P with tau(P) > 10^4.
widen() replaces cgreedy's module globals PR, PM1 and X in this
process, after cgreedy.tau_table has been read at its own bound; every
later call into cgreedy reads the wider lists.
E, U and B as envelope.py and choosy.py build them, t <= 10^4.
(1) F <= U, U(t) = max{p(s) : s a prime power <= t}: tau(P) <= t gives
beta(P) <= t by the floor tau >= beta, and beta(P) divides no p - 1 with
p <= P, so P+ <= p(beta(P)) <= U(t). So B <= F <= U.
(2) tau is nondecreasing in P, so once a tabled P has tau(P) > t, F(t)
is final: stopping at tau > 10^4 fixes every t in 4..10^4.
(3) E/F < E/t, since F(t) > t: E/F can spike only where E jumps and F
has not.

PREDICTIONS (frozen before the code).
P1 (forced) the widened table equals cgreedy.tau_table at every
   P <= 10^4.
P2 (proved) B <= F <= U at every fixed t.
P3 (forced) F <= E at every fixed t <= 10^4.
P4 (a guess, 50%) E/F <= 10 at every fixed t <= 10^4.
P5 (a guess, 55%) the largest E/F sits past t = 1822.

THE PRINT. "fixed to <end>" first; then the largest E/F over the fixed
t in 4..10^4 with its t, E and F; then "KILL: E/F ABOVE 10 at <ts>" or
"E/F AT MOST 10 TO <end>". KILL of "the record run is within a
constant of the dam's bar" at any E/F above 10.

CONTROLS, read first. C1 is P1. C2 F(7) = 13, F(13) = 23 and F equals
dambar.f_table at every t <= 1822. C3 the kill's reading flags E
planted at 10.5 F at one fixed t, and only there. C4 P2's test flags F
raised to U + 1 at one fixed t.

FINDINGS (from the printed run; the controls passed first). The widened
table reads 14172 primes to P = 153757, where tau = 11003 first passes
10^4, so F is fixed at every t in 4..10^4 (9997 t), F(10^4) = 153757.
P1 holds (1229 primes, 0 differ); C2 F = dambar's F on 4..1822. P2
holds: B <= F <= U at every fixed t. P3 holds: F <= E at every fixed t.
P4 holds, the kill silent: E/F AT MOST 10 TO 10000, largest 7.6829 at
t = 1997 (E 87869, F 11437), so P5 holds (past 1822). E/F over the
fixed t >= 100: least 1.1026 at 107, median 3.8921; 2.3397 at 10^4. E/t
is largest at 3833, 60.0003, where F/t is 9.9121; F/t climbs to 17.9980
at 8543 and is 15.3757 at 10^4, so E/F falls at the top. U/F is
largest at 5227, 10.4560.
Readings added after the first run: the witness state's m0 equals tau
at the last three tau jumps (P = 81349, 121697, 153757; 7825 to 14057
primes), 12 jumps past 9973; the dam ratio rho(P) = P+/tau(P) on the
widened table is largest at P = 153749, 17.9980, and tau(P)/P there is
0.0556. The skipping run (choosy.py's arm B) against F: E_B/F largest
7.6829 at t = 1997 too, where both runs pay 87869 = p(1997), each
holding 1997 with no seat 1 mod 1997 before 87869 (the anchor holds
the tide at most 1997 until one enters): the record run seats 1997 at
move 96 (moves counted from 0) from tide 167, the skipping run at move 56 from tide 499, the
anchor p(499) of a held 499, and each seats 87869 from tide 1997
(moves 1714 and 134; that line added after the first run); E_B = F last at
24, 227, 228; min(E, E_B) above
2 F at 8610 fixed t, 3 F at 5368, 4 F at 2474, 5 F at 882.
So the record run stays within 7.6829 of the dam's bar at every
t in 4..10^4: a rule to 10^4, no constant proved.
RUN RECORD. Rehearsal at --x 20000: 6/6, table 1.1 s, 3.5 s, 80.2 MB.
First full run: 6/6, 36.8 s, 86.6 MB. With the readings, C4's test cut
to its flag (its first clause was implied): 6/6, 38.6 s, 87.6 MB. With
the skipping run: 6/6, 38.4 s, 87.9 MB. With the 1997 line: 6/6,
38.4 s, 89.6 MB. From its shipped place: 6/6, 38.2 s, 89.0 MB.

    python fwide.py [--x PMAX]     (PMAX caps the primes read: a
                                    rehearsal; the default reads on until
                                    tau passes 10^4)
"""

import os
import sys
import time

os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
import cgreedy  # noqa: E402
import envelope as ev  # noqa: E402
import choosy  # noqa: E402
import dambar  # noqa: E402

T = ev.T
PMAX = 600_000                    # under envelope's sieve, N = 700000
CHECKS = []


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


def widen(pmax):
    """cgreedy's primes and p - 1 maps, widened to pmax + 200."""
    cgreedy.PR = [p for p in ev.PRIMES if p <= pmax + 200]
    cgreedy.PM1 = {p: ev.fac(p - 1) for p in cgreedy.PR}
    cgreedy.X = pmax


def tau_wide(pmax, stop):
    """{P: (tau(P),)} for the primes P <= pmax, ending at the first P
    with tau(P) > stop; cgreedy.tau_table's loop without witnesses."""
    pps = [t for t in cgreedy.prime_powers(pmax + 1) if t > 4]
    tau, i, out, t0 = 4, 0, {}, time.time()
    for P in cgreedy.PR:
        if P > pmax:
            break
        while i < len(pps):
            if cgreedy.feasible(pps[i], P) is None:
                break
            tau = pps[i]
            i += 1
        out[P] = (tau,)
        if len(out) % 2000 == 0:
            print(f"    P = {P}: tau {tau} ({time.time() - t0:.1f} s)",
                  flush=True)
        if tau > stop:
            break
    return out


def main():
    pmax = PMAX
    if "--x" in sys.argv:
        pmax = int(sys.argv[sys.argv.index("--x") + 1])
    t0 = time.time()
    orig = cgreedy.tau_table()
    F0 = dambar.f_table(orig)
    widen(pmax)
    tab = tau_wide(pmax, T)
    F = dambar.f_table(tab)
    fixed = [t for t in range(4, T + 1) if F[t] is not None]
    Plast = max(tab)
    print(f"widened table: {len(tab)} primes to P = {Plast}, tau(P) = "
          f"{tab[Plast][0]}; fixed to {fixed[-1]} "
          f"({time.time() - t0:.1f} s)")
    B, _ = choosy.bars()
    epairs, _, _, _ = ev.record_run()
    E = ev.hull([(m, R) for m, R, _ in epairs])
    U = ev.hull([(s, ev.p_of(s)) for s, _, _ in ev.prime_powers(T)])

    def over(Ex):
        return [t for t in fixed if Ex[t] > 10 * F[t]]

    def p2_bad(Fx):
        return [t for t in fixed if not B[t] <= Fx[t] <= U[t]]

    print("CONTROLS")
    diff = [P for P in orig if orig[P][0] != tab[P][0]]
    check("C1 = P1 the widened table equals cgreedy.tau_table at every "
          f"P <= {max(orig)}", not diff and all(P in tab for P in orig),
          f"{len(orig)} primes, {len(diff)} differ {diff[:3]}")
    f0 = [t for t in range(4, T + 1) if F0[t] is not None]
    off = [t for t in f0 if F[t] != F0[t]]
    check("C2 F(7) = 13, F(13) = 23 and F = dambar's F on its fixed "
          f"range 4..{f0[-1]}", F[7] == 13 and F[13] == 23 and not off,
          f"F(7) = {F[7]}, F(13) = {F[13]}, {len(off)} differ")
    tp = fixed[(2 * len(fixed)) // 3]
    plant = list(E)
    plant[tp] = int(10.5 * F[tp])
    got = over(plant)
    check("C3 the kill's reading flags E planted at 10.5 F at one fixed t",
          tp in got and (set(got) - {tp}) == set(over(E)),
          f"t = {tp}, F = {F[tp]}")
    plant = list(F)
    plant[tp] = U[tp] + 1
    check("C4 P2's test flags F raised to U + 1 at one fixed t",
          tp in p2_bad(plant),
          f"t = {tp}, U = {U[tp]}")
    if not all(ok for _, ok in CHECKS):
        print("CONTROL FAILED: nothing below is read.")
        raise SystemExit(1)

    print("THE BARS")
    print(f"  fixed to {fixed[-1]} ({len(fixed)} t in 4..{T})")
    bad = p2_bad(F)
    check("P2 B <= F <= U at every fixed t", not bad,
          f"{len(bad)} off {bad[:3]}")
    under = [t for t in fixed if E[t] < F[t]]
    check(f"P3 F <= E at every fixed t <= {T}", not under,
          f"{len(under)} off {under[:3]}")

    print("READINGS")
    # added after the first run: the engine past cgreedy's range, read
    # at the last three tau jumps by its witness state's m0
    jumps = [P for P in sorted(tab) if P > max(orig) and
             tab[P][0] != tab[cgreedy.PR[cgreedy.PR.index(P) - 1]][0]]
    for P in jumps[-3:]:
        tau = tab[P][0]
        mf = {l: 1 for l in cgreedy.feasible(tau, P)}
        mf.update({p: 1 for p in cgreedy.PR if tau <= p <= P})
        print(f"  witness at P = {P}: m0 {cgreedy.m0(mf)}, tau {tau}"
              f" ({len(mf)} primes)")
    print(f"  tau jumps past {max(orig)}: {len(jumps)}")
    # added after the first run: the dam ratio rho(P) = P+/tau(P) on the
    # widened table, P below its last (whose tau passed 10^4)
    tp = sorted(tab)[:-1]
    rho = [(cgreedy.next_prime(P) / tab[P][0], P) for P in tp]
    for lo in (0, 9973):
        m = max(x for x in rho if x[1] > lo)
        print(f"  largest rho past {lo}: {m[0]:.4f} at P = {m[1]}")
    print(f"  tau(P)/P at P = {tp[-1]}: {tab[tp[-1]][0] / tp[-1]:.4f}")
    for t in (1000, 1822, 2048, 4096, 5000, 8192, T):
        if F[t] is not None:
            print(f"  t = {t}: B {B[t]}, F {F[t]}, E {E[t]}, U {U[t]}, "
                  f"F/t {F[t] / t:.4f}, E/F {E[t] / F[t]:.4f}")
    r = sorted((E[t] / F[t], t) for t in fixed if t >= 100)
    print(f"  E/F over the fixed t >= 100: least {r[0][0]:.4f} at "
          f"{r[0][1]}, median {r[len(r) // 2][0]:.4f}")
    tm = max(fixed, key=lambda t: F[t] / t)
    print(f"  largest F/t: {F[tm] / tm:.4f} at t = {tm}")
    tm = max(fixed, key=lambda t: U[t] / F[t])
    print(f"  largest U/F: {U[tm] / F[tm]:.4f} at t = {tm}")
    tm = max(fixed, key=lambda t: E[t] / t)
    print(f"  largest E/t: {E[tm] / tm:.4f} at t = {tm} (F/t there "
          f"{F[tm] / tm:.4f})")

    # added after the first run: the skipping run (choosy.py arm B)
    # against F over the whole fixed range
    pairs, _ = choosy.run("B")
    EB = ev.hull(pairs)
    tm = max(fixed, key=lambda t: EB[t] / F[t])
    print(f"  E_B/F over the fixed t: largest {EB[tm] / F[tm]:.4f} at t = "
          f"{tm}; equal at {[t for t in fixed if EB[t] == F[t]][-3:]} last")
    for c in (2, 3, 4, 5):
        w = [t for t in fixed if min(E[t], EB[t]) > c * F[t]]
        print(f"  min(E, E_B) > {c} F at {len(w)} fixed t")
    # added after the first run: how each run pays p(1997) at 1997
    for name, run in (("record", [(m, R) for m, R, _ in epairs]),
                      ("skipping", pairs)):
        seats = [R for _, R in run]
        i, j = seats.index(1997), seats.index(87869)
        anch = [R for R in seats[:j] if R % 1997 == 1]
        print(f"  {name} run: 1997 seated at move {i} from tide "
              f"{run[i][0]}, 87869 at move {j} from tide {run[j][0]}; "
              f"seats = 1 mod 1997 before it: {anch}")

    print("THE PRINT")
    print(f"  fixed to {fixed[-1]}")
    tm = max(fixed, key=lambda t: E[t] / F[t])
    print(f"  largest E/F over the fixed t: {E[tm] / F[tm]:.4f} at t = "
          f"{tm} (E {E[tm]}, F {F[tm]}); P5 past 1822: {tm > 1822}")
    hi = over(E)
    print("  " + (f"KILL: E/F ABOVE 10 at {len(hi)} t, first {hi[:5]}"
                  if hi else f"E/F AT MOST 10 TO {fixed[-1]}"))
    print(f"{sum(ok for _, ok in CHECKS)}/{len(CHECKS)} checks passed, "
          f"{time.time() - t0:.1f} s")
    raise SystemExit(0 if all(ok for _, ok in CHECKS) else 1)


if __name__ == "__main__":
    main()