"""Independent integral checks for T715; no generator code is imported.

Usage: sage -python checks.py [rows.json] [results.json]
Input is {"rows":[{"params":{"p":1,"v":"1/4"},"number":"..."},...]}
with NumberDB decimal interval encodings. The default is offline-rows.json.
The integral is a different implementation from the series / Euler transform /
beta coefficients used to generate entries. Both use Arb arithmetic, and both
rely on the same series-to-moment identity; this is not a separate library check.
Analytic quadrature and an explicit positive tail yield a second enclosure.
"""
import json
import math
import pathlib
import sys
import time
from fractions import Fraction

import numberdb.sage as numberdb
from sage.rings.rational_field import QQ
from sage.rings.real_arb import RealBallField
from sage.rings.complex_arb import ComplexBallField
from sage.rings.real_mpfi import RealIntervalField

R = RealBallField(450)
C = ComplexBallField(450)
I = RealIntervalField(600)


def rational(text):
    f = Fraction(str(text))
    return QQ(f.numerator)/f.denominator


def decimal_bounds(text):
    text = str(text).lower()
    mantissa, _, exponent = text.partition('e')
    places = len(mantissa.split('.')[1]) if '.' in mantissa else 0
    ulp = QQ(10)**(int(exponent or 0)-places)
    center = rational(text)
    return center-ulp, center+ulp, ulp


def narrow(y):
    return bool(y.is_finite() and R(y.rad()) < R(10)**-110)


def contained(text, y):
    if not narrow(y):
        return False
    lo, hi, _ = decimal_bounds(text)
    interval = I(y)
    return bool(interval.lower() >= lo and interval.upper() <= hi)


def integral(p, v):
    """U_p(v) via the logarithmic moment after theta=theta_end exp(-t)."""
    v = rational(v)
    a = 2*R(abs(v)).sqrt()
    theta = a.arcsin() if v > 0 else a.arcsinh()
    norm = C(theta/a)/math.factorial(p-1)
    A, th = C(a), C(theta)
    def integrand(t, analytic):
        z = th*(-t).exp()
        kernel = z.sin() if v > 0 else z.sinh()
        return norm*(-t).exp()*(A/kernel).log(analytic=analytic)**(p-1)
    L = 420
    y = C.integral(integrand, 0, L, abs_tol=R(10)**-120, rel_tol=R(10)**-120)
    # log(a/kernel(theta exp(-t))) <= t+1, theta/a < 2.
    tail = 2*R(-L).exp()*sum(R(L+1)**k/math.factorial(k) for k in range(p))
    assert y.real().is_finite() and y.imag().is_finite() and y.imag().contains_zero()
    return y.real().add_error(tail)


def main(input_path, output_path):
    data = json.loads(pathlib.Path(input_path).read_text())
    records = data['rows']
    comparisons, failures = [], []
    controls = []
    start = time.time()
    for row in records:
        p = int(row['params']['p']); v = row['params']['v']
        y = integral(p,v)
        ok = contained(row['number'],y)
        center = R(rational(row['number'])); ulp = decimal_bounds(row['number'])[2]
        comparisons.append({'params':row['params'],'integral_ball':str(y),
                            'radius':str(y.rad()),'stored_contains_integral':ok,
                            'residual_in_stored_ulps':str((center-y)/R(ulp))})
        if not ok: failures.append({'params':row['params'],'reason':'stored interval does not contain the narrow integral enclosure'})
        if p==1:
            a=2*R(abs(rational(v))).sqrt()
            known=(a.arcsin() if rational(v)>0 else a.arcsinh())/a
            controls.append(bool(narrow(known) and narrow(y) and y.overlaps(known)))
        if p==2 and rational(v)==QQ(1)/4:
            controls.append(bool(y.overlaps(R.pi()*R(2).log()/2)))
        print('ROW_JSON='+json.dumps(comparisons[-1]),flush=True)
    reference=records[0]; y=integral(int(reference['params']['p']),reference['params']['v'])
    _,_,ulp=decimal_bounds(reference['number'])
    negative_controls={
        'missing_initial_term':not contained(reference['number'],y-1),
        'wrong_sign':not contained(reference['number'],-y),
        'five_last_place_units':not contained(reference['number'],y+5*R(ulp)),
        'vacuous_radius':not contained(reference['number'],y.add_error(100)),
        'nan':not contained(reference['number'],R('nan')),
    }
    result={'table':'T715','checked_entries':len(records),'total_entries':len(records),
            'failures':failures,'known_answer_control':all(controls) and len(controls)==5,
            'negative_control_rejected':all(negative_controls.values()),
            'negative_controls':negative_controls,'known_answer_controls':controls,
            'comparisons':comparisons,'seconds':time.time()-start,
            'method':'450-bit Arb analytic quadrature on [0,420] plus explicit exponential tail',
            'skill_manifest':'skill-manifest.json',
            'skill_bundle_sha256':'d6661c2f21613524889fa3a57d3c95f8330344ca62e5a856211c08a282b7dbab',
            'limitations':'Independent formula and implementation; shared Arb arithmetic and series-to-moment identity. This is builder evidence, not a critic verdict.'}
    pathlib.Path(output_path).write_text(json.dumps(result,indent=2))
    assert not failures and result['known_answer_control'] and result['negative_control_rejected']
    return result


if __name__=='__main__':
    here=pathlib.Path(__file__).parent
    inp=sys.argv[1] if len(sys.argv)>1 else here/'offline-rows.json'
    out=sys.argv[2] if len(sys.argv)>2 else here/'check-results.json'
    main(inp,out)
