#!/usr/bin/env python3
"""
Generate a robust certificate candidate from a standardized host instance.

Pipeline:
- Doeblin witness search on allowed edge sequences
- Avoidability detection for that word (OG4) and finite recurrence bound if unavoidable
- Rate pack computation from delta and U

Outputs:
- sources/generated/<name>_robust_certificate_generated.json
- sources/generated/<name>_summary.json
"""
from __future__ import annotations
import os, json, argparse, math, hashlib
from collections import defaultdict, deque
from typing import Dict, Any, List, Tuple

def load(p: str) -> Dict[str, Any]:
    with open(p,"r",encoding="utf-8") as f:
        return json.load(f)

def dump(p: str, obj: Dict[str, Any]) -> None:
    os.makedirs(os.path.dirname(p), exist_ok=True)
    with open(p,"w",encoding="utf-8") as f:
        json.dump(obj, f, indent=2)

def sha256_json(d: Dict[str, Any]) -> str:
    b = json.dumps(d, sort_keys=True).encode("utf-8")
    return "sha256:" + hashlib.sha256(b).hexdigest()

def mm(X: List[List[float]], Y: List[List[float]]) -> List[List[float]]:
    return [[sum(X[i][k]*Y[k][j] for k in range(len(Y))) for j in range(len(Y[0]))] for i in range(len(X))]

def identity(n: int) -> List[List[float]]:
    return [[1.0 if i==j else 0.0 for j in range(n)] for i in range(n)]

def is_strict_pos(M: List[List[float]]) -> bool:
    return all(M[i][j] > 0 for i in range(len(M)) for j in range(len(M[0])))

def min_entry(M: List[List[float]]) -> float:
    return float(min(min(r) for r in M))

def max_entry(M: List[List[float]]) -> float:
    return float(max(max(r) for r in M))

def doeblin_search(inst: Dict[str, Any], Lmax: int) -> Tuple[bool, Dict[str, Any]]:
    n=int(inst["cone_dimension"])
    templates=inst["templates"]
    edges=inst["constraint_graph"]["edges"]
    states=inst["constraint_graph"]["states"]
    out_edges=defaultdict(list)
    for e in edges:
        out_edges[e["from"]].append(e)
    q=deque((s,0,identity(n),[],[]) for s in states)
    seen=set()
    while q:
        cur,L,M,ids,syms=q.popleft()
        if L>=Lmax:
            continue
        for e in out_edges[cur]:
            T=templates[e["template"]]["matrix"]
            M2=mm(T,M)
            ids2=ids+[e["id"]]
            syms2=syms+[e["template"]]
            cur2=e["to"]
            if is_strict_pos(M2):
                return True, {"L":L+1,"edge_ids":ids2,"templates":syms2,"matrix":M2}
            pat="".join("1" if M2[i][j]>0 else "0" for i in range(n) for j in range(n))
            sig=(cur2,L+1,pat)
            if sig in seen:
                continue
            seen.add(sig)
            q.append((cur2,L+1,M2,ids2,syms2))
    return False, {}

def avoidance_check(inst: Dict[str, Any], forbidden: List[str]) -> Tuple[bool, Dict[str, Any]]:
    states=inst["constraint_graph"]["states"]
    edges=inst["constraint_graph"]["edges"]
    out_edges=defaultdict(list)
    for e in edges:
        out_edges[e["from"]].append(e)
    L=len(forbidden)
    k=L-1

    def build_suffix(suf: Tuple[str,...], sym: str) -> Tuple[str,...]:
        nxt = suf + (sym,)
        if len(nxt) <= k:
            return nxt
        return nxt[-k:]

    start=[(s, tuple()) for s in states]
    adj=defaultdict(list)
    nodes=set(start)
    q=deque(start)
    while q:
        gstate, suf=q.popleft()
        for e in out_edges[gstate]:
            sym=e["template"]
            if k==0:
                if [sym]==forbidden:
                    continue
                suf2=tuple()
            else:
                if list(suf + (sym,)) == forbidden:
                    continue
                suf2=build_suffix(suf, sym)
            node2=(e["to"], suf2)
            adj[(gstate,suf)].append((node2, e["id"], sym))
            if node2 not in nodes:
                nodes.add(node2)
                q.append(node2)

    color={}
    parent={}
    parent_edge={}
    def dfs(u):
        color[u]=1
        for v,eid,sym in adj.get(u,[]):
            if v not in color:
                parent[v]=u
                parent_edge[v]=(eid,sym)
                cyc=dfs(v)
                if cyc:
                    return cyc
            elif color[v]==1:
                cycle=[]
                cur=u
                cycle.append((eid,sym))
                while cur!=v:
                    cycle.append(parent_edge[cur])
                    cur=parent[cur]
                cycle.reverse()
                return cycle
        color[u]=2
        return None

    for s in start:
        if s not in color:
            cyc=dfs(s)
            if cyc:
                return True, {"cycle_edge_ids":[x[0] for x in cyc],"cycle_templates":[x[1] for x in cyc]}

    indeg=defaultdict(int)
    for u in nodes:
        for v,_,_ in adj.get(u,[]):
            indeg[v]+=1
    topo=deque([u for u in nodes if indeg[u]==0])
    dist={u:0 for u in nodes}
    while topo:
        u=topo.popleft()
        for v,_,_ in adj.get(u,[]):
            if dist[v] < dist[u]+1:
                dist[v]=dist[u]+1
            indeg[v]-=1
            if indeg[v]==0:
                topo.append(v)
    B=max(dist.values()) if dist else 0
    return False, {"B":int(B)}

def main()->int:
    ap=argparse.ArgumentParser()
    ap.add_argument("--root", default=".")
    ap.add_argument("--host_instance", required=True)
    ap.add_argument("--name", required=True)
    ap.add_argument("--Lmax", type=int, default=10)
    args=ap.parse_args()

    root=os.path.abspath(args.root)
    inst=load(os.path.join(root, args.host_instance.replace("/", os.sep)))

    found, wit = doeblin_search(inst, args.Lmax)

    model_hash=sha256_json(inst)
    robust={
        "model_hash": model_hash,
        "perturbation_metric": {"cost_norm":"linfty","matrix_metric":"absolute_entrywise","matrix_norm":"linfty_entrywise"},
        "calibration": {"lambda_star":0.0,"u_potential":[0.0]},
        "tight_core": {
            "tight_edges":[e["id"] for e in inst["constraint_graph"]["edges"]],
            "tight_gap_gamma": 0.0,
            "tight_lipschitz_Kc": 1.0,
            "eps_tight": 0.0,
            "tight_graph_hash":"sha256:"+hashlib.sha256("|".join(sorted(e["id"] for e in inst["constraint_graph"]["edges"])).encode("utf-8")).hexdigest(),
            "tight_scc_summary":{"scc_count":len(inst["constraint_graph"]["states"]), "aperiodic_scc_count": None, "periods":[1]},
            "degeneracy_report":{"all_edges_tight": True, "gamma_is_positive": False, "note":"Generated from standardized host instance; treated as cost-free tight graph."}
        },
        "doeblin":{
            "word": wit.get("templates",[]),
            "L": int(wit.get("L",1)) if found else 1,
            "M_bound": 0.0,
            "U_bound": 0.0,
            "delta": 0.0,
            "eps_doeblin": 0.0,
            "delta_prime_formula":"Generated candidate",
            "U_prime_formula":"Generated candidate"
        },
        "recurrence":{
            "mode":"combinatorial",
            "eps_recurrence": 0.0,
            "details":{"rc1_holds": None, "L_syn": None, "gap_bound_B": None, "og4_avoidance_cycle": None, "hypothesis_type": None, "margin": None, "note":"Generated candidate"}
        },
        "rate_pack":{
            "projective_diameter_bound": 0.0,
            "tau_unperturbed": 1.0,
            "tau_prime_formula":"Generated candidate",
            "eps_rate": 0.0,
            "kappa_prime_formula":"Generated candidate"
        },
        "eps_star":{"eps_c_star": 0.0, "eps_A_star": 0.0}
    }

    summary={"host_instance":args.host_instance,"name":args.name,"doeblin_found":found,"Lmax":args.Lmax}

    if not found:
        summary["outcome"]="OG3_candidate_no_doeblin_found_up_to_Lmax"
        robust["doeblin"]["delta"]=0.0
        robust["tight_core"]["degeneracy_report"]["note"]="No strictly positive Doeblin word found up to Lmax; candidate OG3."
    else:
        M=wit["matrix"]
        delta=min_entry(M); U=max_entry(M)
        summary["doeblin_word"]=wit["templates"]; summary["doeblin_L"]=wit["L"]
        summary["delta"]=delta; summary["U"]=U
        robust["doeblin"]["delta"]=delta; robust["doeblin"]["U_bound"]=U
        robust["doeblin"]["L"]=wit["L"]; robust["doeblin"]["word"]=wit["templates"]
        avoidable, det = avoidance_check(inst, wit["templates"])
        summary["avoidable"]=avoidable
        if avoidable:
            summary["outcome"]="OG4_candidate_avoidable"
            robust["recurrence"]["details"]["rc1_holds"]=False
            robust["recurrence"]["details"]["og4_avoidance_cycle"]=det.get("cycle_edge_ids")
            robust["tight_core"]["degeneracy_report"]["note"]="Doeblin word exists but is avoidable; candidate OG4."
        else:
            B=det.get("B",0)
            summary["outcome"]="CONTRACTION_candidate_unavoidable_word"
            summary["B"]=B
            robust["recurrence"]["details"]["rc1_holds"]=True
            robust["recurrence"]["details"]["gap_bound_B"]=B
            robust["recurrence"]["details"]["L_syn"]=wit["L"]
            Delta=2.0*math.log(U/delta)
            tau=math.tanh(Delta/4.0)
            robust["rate_pack"]["projective_diameter_bound"]=Delta
            robust["rate_pack"]["tau_unperturbed"]=tau
            robust["rate_pack"]["kappa_prime_formula"]="kappa = -log(tau)/L"
            summary["tau"]=tau
            robust["tight_core"]["degeneracy_report"]["note"]="Doeblin word exists and is unavoidable; recurrence bound computed from forbidden automaton."

    out_cert=os.path.join(root,"sources","generated",f"{args.name}_robust_certificate_generated.json")
    out_sum=os.path.join(root,"sources","generated",f"{args.name}_summary.json")
    dump(out_cert, robust)
    dump(out_sum, summary)
    print("Wrote:", os.path.relpath(out_cert, root))
    print("Wrote:", os.path.relpath(out_sum, root))
    print("Outcome:", summary.get("outcome"))
    return 0

if __name__=="__main__":
    raise SystemExit(main())
