"""Independent analytic controls and exact rational rounding invariants."""
import json
import math
import pathlib
import random
import sys
from fractions import Fraction

from flint import arb, ctx

sys.path.insert(0, "/study/code")
import verify


def rational_endpoint(value):
    mantissa, exponent = value.man_exp()
    return Fraction(int(mantissa)) * Fraction(2) ** int(exponent)


def main():
    analytic_cases = []
    # Derive these controls directly from the inverse multiplier polynomials:
    # c(lambda)=lambda/2-lambda**2/4 and c(lambda)=-1+lambda/4.
    for period, real, terms, pi_factor in [
        (1, "0", 1, Fraction(1, 4)),
        (1, "0", 8, Fraction(3, 8)),
        (2, "-1", 1, Fraction(1, 16)),
        (2, "-1", 8, Fraction(1, 16)),
    ]:
        got = verify.prove(period, real, "0", terms)
        assert got is not None
        _, area = got
        ctx.prec = 512
        exact_area = arb.pi() * pi_factor.numerator / pi_factor.denominator
        assert area.contains(exact_area)
        lower = rational_endpoint(area.lower())
        returned = verify.floor_grid(area)
        assert Fraction(returned, 2**96) <= lower
        analytic_cases.append({"period": period, "terms": terms, "known_pi_factor": str(pi_factor), "area_enclosure_contains_analytic_control": True})

    rng = random.Random(20261004)
    outward_checks = 0
    for _ in range(400):
        integer = rng.randrange(-(1 << 60), 1 << 60)
        exponent = rng.randrange(-1100, -60)
        exact = Fraction(integer) * Fraction(2) ** exponent
        ctx.prec = 256
        endpoint = arb((integer, exponent))
        assert rational_endpoint(endpoint) == exact
        lower = verify.outward(endpoint, -1)
        upper = verify.outward(endpoint, 1)
        assert math.isfinite(lower) and math.isfinite(upper)
        assert Fraction.from_float(lower) < exact < Fraction.from_float(upper)
        outward_checks += 1

    grid_checks = 0
    for _ in range(200):
        numerator = rng.randrange(1, 10**12)
        denominator = rng.randrange(1, 10**6)
        value = arb(numerator) / denominator
        floor = verify.floor_grid(value)
        lower = rational_endpoint(value.lower())
        expected = (lower.numerator * (1 << 96)) // lower.denominator
        assert floor == expected
        assert Fraction(floor, 1 << 96) <= Fraction(numerator, denominator)
        grid_checks += 1

    rejects = [
        verify.prove(2, "0", "0", 1) is None,
        verify.prove(4, "-1", "0", 1) is None,
        verify.prove(8, "-1", "0", 1) is None,
    ]
    assert all(rejects)
    result = {
        "analytic_component_controls": analytic_cases,
        "exact_dyadic_outward_rounding_checks": outward_checks,
        "exact_rational_grid_floor_checks": grid_checks,
        "wrong_period_rejections": len(rejects),
        "all_passed": True,
    }
    pathlib.Path("results/independent-controls.json").write_text(json.dumps(result, indent=2) + "\n")
    print(json.dumps(result, indent=2))


if __name__ == "__main__":
    main()