#!/usr/bin/env python3
"""Independent verifier for the Numaro C_3a sparse-digit certificate."""

from __future__ import annotations

import json
import os
import sys
from itertools import product

import mpmath


HERE = os.path.dirname(os.path.abspath(__file__))
DEFAULT_CERT = os.path.join(HERE, "gsd_3a_cert.json")


def minimal_difference_pairs(alphabet: list[int]) -> list[tuple[int, int]]:
    pairs: list[tuple[int, int]] = []
    for delta in sorted({p - q for p in alphabet for q in alphabet}):
        candidates = [(p, q) for p in alphabet for q in alphabet if p - q == delta]
        pairs.append(min(candidates, key=lambda pair: (pair[0] + pair[1], pair)))
    return pairs


def tiny_exact_test(alphabet: list[int], base: int, rho_text: str) -> tuple[int, int, int]:
    rho = mpmath.mpf(rho_text)
    depth = 2
    cap = int(mpmath.floor(rho * depth))
    values = {
        digits[0] + digits[1] * base
        for digits in product(alphabet, repeat=depth)
        if sum(digits) <= cap
    }
    sums = {u + v for u in values for v in values}
    differences = {u - v for u in values for v in values}
    q_value = 2 * max(values) + 1
    if 0 not in values or len(differences) >= q_value:
        raise AssertionError("tiny-depth construction fails the GHR admissibility condition")
    return len(sums), len(differences), q_value


def verify(cert_path: str) -> None:
    cert = json.load(open(cert_path, encoding="utf-8"))
    alphabet = sorted({int(value) for value in cert["alphabet"]})
    base = int(cert["base"])

    if alphabet[0] != 0 or len(alphabet) != len(cert["alphabet"]):
        raise AssertionError("alphabet must be distinct and contain zero")
    if base < 2 * alphabet[-1] + 1:
        raise AssertionError("base is too small for carry-free sum and difference digits")

    iv = mpmath.iv
    iv.prec = 420
    alpha = iv.mpf(str(cert["alpha_tilt"]))
    sum_tilt = iv.mpf(str(cert["s_tilt"]))
    pairs = minimal_difference_pairs(alphabet)

    difference_weights = [iv.exp(-alpha * (p + q)) for p, q in pairs]
    z_difference = sum(difference_weights)
    probabilities = [weight / z_difference for weight in difference_weights]
    expected_p = sum(probability * p for probability, (p, _) in zip(probabilities, pairs))
    expected_q = sum(probability * q for probability, (_, q) in zip(probabilities, pairs))
    rho = max(expected_p.b, expected_q.b)
    entropy_lower = -sum(probability * iv.log(probability) for probability in probabilities)

    sum_digits = sorted({p + q for p in alphabet for q in alphabet})
    z_sum = sum(iv.exp(-sum_tilt * digit) for digit in sum_digits)
    sum_rate_upper = 2 * rho * sum_tilt + iv.log(z_sum)
    difference_rate_upper = 2 * rho * alpha + iv.log(z_difference)
    log_base = iv.log(iv.mpf(base))
    lower_bound = 1 + (entropy_lower - sum_rate_upper) / log_base

    claimed = iv.mpf(cert["claim"].split(">=")[-1].strip())
    previous = iv.mpf(str(cert["record_prev"]))
    stored_floor = iv.mpf(str(cert["L_lower_str"]))
    if not bool(lower_bound > claimed):
        raise AssertionError("rigorous interval does not clear the displayed claim")
    if not bool(lower_bound > previous):
        raise AssertionError("rigorous interval does not clear the previous record")
    if not bool(lower_bound > stored_floor):
        raise AssertionError("stored lower-bound string is not safely floor-truncated")
    if not bool(difference_rate_upper < log_base):
        raise AssertionError("difference growth does not satisfy the digit-lemma hypothesis")
    if not bool(lower_bound < iv.mpf(5) / 4):
        raise AssertionError("certificate conflicts with the digit-lemma ceiling")
    if not bool(lower_bound < iv.mpf(4) / 3):
        raise AssertionError("certificate conflicts with the proven upper bound")

    sums, differences, q_value = tiny_exact_test(alphabet, base, str(cert["rho"]))
    print(f"certificate: {cert_path}")
    print(f"alphabet size = {len(alphabet)}, max digit = {alphabet[-1]}, base = {base}")
    print(f"difference digits = {len(pairs)}, sum digits = {len(sum_digits)}")
    print(f"rho enclosure upper endpoint = {rho}")
    print(f"certified interval = {lower_bound}")
    print(f"previous record = {cert['record_prev']}")
    print(f"tiny d=2 exact test: |U+U|={sums}, |U-U|={differences}, q(U)={q_value}")
    print("RESULT: PASS - independent interval and admissibility checks")


if __name__ == "__main__":
    verify(sys.argv[1] if len(sys.argv) > 1 else DEFAULT_CERT)