"""Exact checks of the constants c_Z used by the RS-theta and Directed Steiner Tree proofs.

RS-theta (prop:rst-certs, prop:rst-rate).  For i = 0, 1 the program runs verify(cert_final_i.json)
of verify_cert.py, which checks the certificate and returns c_{Z_i} = min_{z in Z_i} fin(z),
fin(A, B, C) = A + B + C/2, as an exact rational.  It checks c_{Z_0} >= 0.6212, c_{Z_1} >= 0.6293
(the values in the table of prop:rst-certs) and hence c_{Z_i} >= 0.62 (used in prop:rst-rate).

Directed Steiner Tree (prop:fa-dst-certs, thm:fa-dst).  From dst_certificates.json it reads the
weights lambda_j and the certificates (y_j, e1_j, e2_j, Z_j) as exact rationals, exactly as
dst_certificate_verify.py does, and checks that the lambda_j are nonnegative and sum to 1, and that
c_{Z_j} e2_j >= 0.40, 0.41, 0.011 (the table of prop:fa-dst-certs), hence >= 1/100 (used in the proof
of thm:fa-dst), where c_{Z_j} = min_{z in Z_j} z_1.

All arithmetic is exact (fractions.Fraction); no floating-point value enters a comparison.
Usage: python3 cz_bounds.py   (paths relative to this script; under a second)
"""
import json
import os
from fractions import Fraction as F

from verify_cert import verify

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

for i, bound in [(0, "0.6212"), (1, "0.6293")]:
    with open(os.path.join(HERE, f"cert_final_{i}.json")) as fh:
        good, info = verify(json.load(fh))
    c = info["c"] if good else None
    res = good and c >= F(bound) and c >= F("0.62")
    ok &= res
    print(f"RS-theta certificate {i}: verified {good}; c_Z = {c} = {float(c):.10f}...; "
          f">= {bound} and >= 0.62: {res}")

with open(os.path.join(HERE, "dst_certificates.json")) as fh:
    data = json.load(fh)
lam = [F(s) for s in data["lambda"]]
res = len(lam) == len(data["certificates"]) and all(l >= 0 for l in lam) and sum(lam) == 1
ok &= res
print(f"DST weights lambda_j: {len(lam)}, nonnegative and summing to 1: {res}")
for j, (cert, bound) in enumerate(zip(data["certificates"], ["0.40", "0.41", "0.011"])):
    e2 = F(cert["e2"])
    cz = min(F(a) for a, b in cert["Z"])
    prod = cz * e2
    res = prod >= F(bound) and prod >= F(1, 100)
    ok &= res
    print(f"DST certificate {j}: c_Z = {float(cz):.10f}..., c_Z e2 = {float(prod):.10f}... "
          f"(exact rational); >= {bound} and >= 1/100: {res}")

print("ALL OK" if ok else "FAILED")
assert ok