#!/usr/bin/env python3
# -*- coding: utf-8 -*-
"""f4-stages-38.txt の検算（Python 標準ライブラリのみ・整数だけ）。
Check the 38-stage table with the standard library only, in exact integers.

  python3 check_f4_stages.py f4-stages-38.txt

確かめること / what is checked:
  (1) 倍加税：全段で a_j = 2 r_{j-1} + 1（r_0 は表の rmax、r_j = a_j + t_j）
      doubling rule at every stage
  (2) head_lo + Σ lo_j = TOTAL_LO、head_hi + Σ hi_j = TOTAL_HI（固定小数 10^100）
      the totals are the sums of the rows (fixed point, scale 10^100)
  (3) TOTAL_LO > H_HI：Walker の集合の逆数和（表の H_HI）を下界が厳密に超える
      the lower bound strictly exceeds the reciprocal sum of Walker's set
この検算は表の内部整合と大小関係だけを見る。各行の lo/hi（ブロックの逆数和の挟み込み）と
head_lo/head_hi/H の値そのものは erdos1110f4.py・erdos1111f4.py の計算に依る。
This checks only the table's internal consistency and the comparison; the per-row
brackets and the head/H values themselves come from erdos1110f4.py / erdos1111f4.py.
"""
import re, sys, math

def main(path):
    L = open(path, encoding="utf-8").read().splitlines()
    hdr = dict(re.findall(r"(\w+)=(\d+)", L[0]))
    head_lo, head_hi = int(hdr["head_lo"]), int(hdr["head_hi"])
    H_lo, H_hi = int(hdr["H_lo"]), int(hdr["H_hi"])
    r0 = int(hdr["rmax"])
    tot = dict(re.findall(r"(TOTAL_\w+)=(\d+)", "\n".join(L)))
    TL, TH = int(tot["TOTAL_LO"]), int(tot["TOTAL_HI"])
    rows = [l.split() for l in L if l.strip() and not l.startswith("#")]
    SC = 10 ** 100
    bad = 0
    prev = r0
    slo = shi = 0
    for row in rows:
        j, p, q, r, t, a, n, d, lo, hi = row
        a, t, lo, hi = int(a), int(t), int(lo), int(hi)
        if a != 2 * prev + 1:
            print(f"[NG] 段 {j}: a_j = {a} != 2 r_(j-1) + 1 = {2*prev+1}"); bad += 1
        if lo > hi:
            print(f"[NG] 段 {j}: lo > hi"); bad += 1
        prev = a + t
        slo += lo; shi += hi
    print(f"[段数 / stages] {len(rows)}")
    print(f"[倍加税 / doubling rule] {'OK' if bad == 0 else 'NG'}")
    ok_lo = head_lo + slo == TL
    ok_hi = head_hi + shi == TH
    print(f"[総和 / totals] head_lo + Σlo == TOTAL_LO: {ok_lo};  head_hi + Σhi == TOTAL_HI: {ok_hi}")
    ok_H = TL > H_hi
    print(f"[記録 / record] TOTAL_LO > H_HI: {ok_H}   (TOTAL_LO - H_HI)/10^100 = {(TL - H_hi) / SC:.5e}")
    print(f"  lower bound  = {TL // SC}.{(TL % SC) * 10**15 // SC:015d}")
    print(f"  upper bound  = {TH // SC}.{(TH % SC) * 10**15 // SC:015d}")
    print(f"  H (Walker)   = {H_hi // SC}.{(H_hi % SC) * 10**15 // SC:015d}")
    print(f"  r_0 ≈ 10^{math.log10(r0):.3f},  max element has {len(str(prev))} digits")
    allok = bad == 0 and ok_lo and ok_hi and ok_H
    print("[判定 / verdict]", "合格 / PASS" if allok else "不合格 / FAIL")
    return 0 if allok else 1

if __name__ == "__main__":
    sys.exit(main(sys.argv[1] if len(sys.argv) > 1 else "f4-stages-38.txt"))