#!/usr/bin/env python3
import sys,json,importlib.util,numpy as np
from pathlib import Path

HERE=Path(__file__).resolve().parent
dep=Path("/mnt/data/UESFCM_Lebesgue_Cycle_17_Verify_Hierarchical_F3.py")
if not dep.exists():
    dep=HERE/"UESFCM_Lebesgue_Cycle_17_Verify_Hierarchical_F3.py"
spec=importlib.util.spec_from_file_location("hv",str(dep))
hv=importlib.util.module_from_spec(spec)
spec.loader.exec_module(hv)
v=hv.v

def build_trie(leaves):
    root={}
    for leaf in leaves:
        node=root
        for ch in leaf["path"]:
            if "_type" in node:
                raise RuntimeError("leaf is prefix of another")
            node=node.setdefault(ch,{})
        if node:
            raise RuntimeError("duplicate/prefix conflict")
        node["_type"]=leaf["type"]
    return root

def verify_tree(tree, TH, ETA):
    trie=build_trie(tree["leaves"])
    stack=[(
        trie,
        np.array(tree["root_center"],float),
        np.array(tree["root_halfwidth"],float)
    )]
    leaves=internals=area=notf=0
    minsl=float("inf")

    while stack:
        node,c,h=stack.pop()
        if "_type" in node:
            if len(node)!=1:
                raise RuntimeError("leaf has children")
            typ=node["_type"]
            leaves+=1
            if typ=="N":
                if not (v.d3_upper(c,h)<v.S_F3):
                    raise RuntimeError("bad NOT-F3 leaf")
                notf+=1
            elif typ=="A":
                lb=v.box_lower(c,h)
                slack=(lb-ETA)-TH
                if slack<=0:
                    raise RuntimeError(f"bad area leaf slack={slack}")
                area+=1
                minsl=min(minsl,slack)
            else:
                raise RuntimeError("unknown leaf type")
        else:
            if set(node.keys())!={"0","1"}:
                raise RuntimeError("incomplete binary coverage")
            internals+=1
            c1,c2=v.split_box(c,h)
            stack.append((node["1"],c2[0],c2[1]))
            stack.append((node["0"],c1[0],c1[1]))
    return dict(
        leaves=leaves,
        internal_nodes=internals,
        area_leaves=area,
        not_f3_leaves=notf,
        minimum_verified_slack=minsl
    )

def main(path):
    C=json.load(open(path,encoding="utf-8"))
    TH=float(C["constants"]["THRESHOLD"])
    ETA=float(C["constants"]["ETA_SAFE"])
    outs=[]
    for tree in C["trees"]:
        out=verify_tree(tree,TH,ETA)
        out["local_index"]=tree["local_index"]
        outs.append(out)

    total_nodes=sum(o["leaves"]+o["internal_nodes"] for o in outs)
    minsl=min(o["minimum_verified_slack"] for o in outs if o["area_leaves"])
    print("PASS")
    print("roots =", [o["local_index"] for o in outs])
    print("total verified nodes =", total_nodes)
    print("minimum verified slack =", minsl)
    for o in outs:
        print(o)

if __name__=="__main__":
    main(sys.argv[1])