"""Standalone re-verification of a fei_71a certificate. Imports NOTHING from solution.py,
benchmark.py, or evaluate.py — its own independent WHT + exact arithmetic, so a bug in the
search/scoring code cannot make a bad artifact pass.

It recomputes, FROM THE ARTIFACT TRUTH TABLE ALONE:
  * the integer Walsh-Hadamard spectrum a_S = 2^n ghat(S) (own butterfly),
  * balance a_0 == 0, influence I = Sum w_S|S| (exact Fraction, must equal the claim),
  * spectral entropy H (mpmath interval, LOG BASE 2, grouped by |a_S|),
  * the amplified constant  C = H/(I-1)  as a certified interval [lo, hi],
and checks the certified LOWER endpoint strictly exceeds the LIVE FEI record, cross-checking
the artifact's own claimed value. Exit 0 iff valid AND a genuine beat.

Convention (matches constants/71a.md and the MI2026b certificate):
  table[x] in {+1,-1}, TRUE=-1, bit i of x set <=> x_{i+1}=-1.  H over ALL S, base 2.

Usage:  python verify.py [path-to-artifact.json]     (default: best_artifact.json)
"""

import hashlib
import json
import os
import sys
from fractions import Fraction

import numpy as np
import mpmath
from mpmath import iv

HERE = os.path.dirname(os.path.abspath(__file__))

# Live record re-fetched 2026-07-20 (PR #124 / MI2026b, merged 2026-07-17).
LIVE_RECORD_DEC = "6.51432691393056537265062517595609726535914349523745739524537"
# The published value is the floor-truncation of MI's interval LOWER endpoint. A *proven strict*
# improvement needs our certified lower endpoint to exceed MI's certified UPPER endpoint ("...957").
RECORD_BAR_DEC = "6.514326913930565372650625175957"


def _dec_to_frac(s):
    a, b = s.split(".")
    return Fraction(int(a + b), 10 ** len(b))


LIVE_RECORD = _dec_to_frac(LIVE_RECORD_DEC)
RECORD_BAR = _dec_to_frac(RECORD_BAR_DEC)


def wht_independent(vals):
    """Iterative radix-2 WHT, int64, written independently of benchmark.py.
    Returns a with a[S] = 2^n ghat(S). Exact for n <= ~30."""
    a = np.asarray(vals, dtype=np.int64).copy()
    N = a.size
    step = 1
    while step < N:
        for start in range(0, N, step * 2):
            u = a[start:start + step].copy()
            v = a[start + step:start + 2 * step].copy()
            a[start:start + step] = u + v
            a[start + step:start + 2 * step] = u - v
        step *= 2
    return a


def _endpoint(raw):
    sign, man, exp, _ = raw
    if man == 0:
        return Fraction(0)
    val = Fraction(int(man)) * (Fraction(2) ** int(exp))
    return -val if sign else val


def main():
    path = sys.argv[1] if len(sys.argv) > 1 else os.path.join(HERE, "fei_c71_n18_artifact.json")
    if not os.path.exists(path):
        print(f"FAIL: no artifact at {path}")
        return 1
    art = json.load(open(path))
    n = int(art["n"])
    N = 1 << n
    if n > 30:
        print("FAIL: n too large for int64-exact verification")
        return 1

    # --- rebuild the truth table FROM THE HEX ALONE ---
    mask = int(art["true_hex"], 16)
    if mask >= (1 << N):
        print("FAIL: hex mask out of range for n")
        return 1
    table = [-1 if (mask >> x) & 1 else 1 for x in range(N)]

    # sha256 binding (same convention as the MI2026b cert)
    sha = hashlib.sha256(",".join(str(v) for v in table).encode()).hexdigest()
    if "sha256_table" in art and sha != art["sha256_table"]:
        print("FAIL: sha256 of rebuilt table != artifact sha256_table (artifact drift)")
        return 1

    # --- independent spectrum ---
    a = wht_independent(table)
    if int((a.astype(np.int64) ** 2).sum()) != N * N:
        print("FAIL: Parseval (Sum a_S^2 != 4^n) — WHT/table inconsistent")
        return 1
    a0 = int(a[0])
    if a0 != 0:
        print(f"FAIL: NOT balanced (a_0 = {a0} != 0) — amplification C>=H/(I-1) is INVALID")
        return 1

    # exact influence
    idx = np.arange(N, dtype=np.int64)
    pc = np.zeros(N, dtype=np.int64)
    i = 0
    while (1 << i) < N:
        pc += (idx >> i) & 1
        i += 1
    asq = a.astype(np.int64) ** 2
    I_num = int((asq * pc).sum())
    I = Fraction(I_num, N * N)
    if I <= 1:
        print(f"FAIL: I = {I} <= 1 — amplification requires I > 1")
        return 1
    claimed_I = art.get("I")
    if claimed_I is not None and Fraction(claimed_I) != I:
        print(f"FAIL: influence mismatch — recomputed {I}, artifact claims {claimed_I}")
        return 1

    # exact entropy interval (grouped by |a_S|), LOG BASE 2
    mpmath.mp.dps = 80
    iv.dps = 80
    absa = np.abs(a)
    nz = absa[absa > 0]
    vals, counts = np.unique(nz, return_counts=True)
    ln2 = iv.log(2)
    H = iv.mpf(0)
    fourn = N * N
    for v, cnt in zip(vals.tolist(), counts.tolist()):
        if v == N:                       # w_S = 1 (constant) -> 0, only if degenerate
            continue
        pref = Fraction(int(v) * int(v) * int(cnt), fourn)
        log2v = iv.log(int(v)) / ln2
        H += (iv.mpf(pref.numerator) / iv.mpf(pref.denominator)) * (iv.mpf(2 * n) - 2 * log2v)
    H_lo = _endpoint(H._mpi_[0])
    if H_lo <= 0:
        print(f"FAIL: H lower endpoint {float(H_lo)} <= 0 — need H > 0")
        return 1

    denom = I - 1
    ratio = H / (iv.mpf(denom.numerator) / iv.mpf(denom.denominator))
    lo = _endpoint(ratio._mpi_[0])
    hi = _endpoint(ratio._mpi_[1])

    # monotone (reported; NOT required for the general constant 71a)
    t = np.array(table)
    mono = True
    for j in range(n):
        b = 1 << j
        loi = idx[(idx & b) == 0]
        if np.any((t[loi] == -1) & (t[loi | b] == 1)):
            mono = False
            break

    # cross-check the artifact's own claimed lower endpoint
    claim_ok = True
    if "ratio_lo_dec" in art:
        claimed_lo = _dec_to_frac(art["ratio_lo_dec"])
        if claimed_lo > lo:
            print(f"FAIL: artifact claims lo={art['ratio_lo_dec']} but recompute gives "
                  f"lo={float(lo):.18f} (claim exceeds truth)")
            claim_ok = False

    beats = lo > RECORD_BAR
    margin = lo - RECORD_BAR

    def _dec_floor(fr, k=30):
        neg = fr < 0
        fr = -fr if neg else fr
        sc = fr * 10 ** k
        s = str(sc.numerator // sc.denominator).rjust(k + 1, "0")
        return ("-" if neg else "") + s[:-k] + "." + s[-k:]

    print(f"artifact: {path}")
    print(f"n = {n}   balanced = True   I = {I} = {float(I):.9f}   "
          f"monotone = {mono}   nonzero coeffs = {int(nz.size)}")
    print(f"H > 0: True   C = H/(I-1) certified lower endpoint (exact floor, 30 digits):")
    print(f"    {_dec_floor(lo)}")
    print(f"live record (MI2026b): {LIVE_RECORD_DEC}")
    print(f"strict bar (their hi): {RECORD_BAR_DEC}")
    print(f"beats record (strict): {beats}   margin over bar = {_dec_floor(margin, 24)}")

    if not claim_ok:
        print("RESULT: FAIL (artifact/claim drift)")
        return 1
    if not _claims_crosscheck(lo):
        print("RESULT: FAIL (claims-table drift)")
        return 1
    if beats:
        print("RESULT: PASS — valid balanced seed, certified C strictly exceeds the live record")
        return 0
    print("RESULT: valid but does NOT beat the live record (not a new record)")
    return 1


# ---- wins/ extension: cross-check the KB claims table (AGENTS.md rule) ----
def _claims_crosscheck(recomputed_lo):
    import json as _json
    root = os.path.dirname(os.path.dirname(HERE))
    claims = os.path.join(root, "knowledge", "kb", "claim.jsonl")
    if not os.path.exists(claims):
        print("claims table: not found (skip)")
        return True
    ok = True
    for line in open(claims):
        try:
            d = _json.loads(line)
        except ValueError:
            continue
        if d.get("problem") != "fei_71a":
            continue
        ours = Fraction(str(d.get("ours")))
        if ours > recomputed_lo:
            print(f"FAIL: claims table says ours={float(ours)} but artifact recomputes "
                  f"to {float(recomputed_lo)} — claim exceeds artifact")
            ok = False
        else:
            print(f"claims-table cross-check OK: claimed {float(ours):.16f} <= "
                  f"recomputed lower endpoint")
    return ok


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