"""Finite natural-number descent certificates; not a universal halting decider.
Standard library, stdout only, explicit checks also under -O. A size-change
matrix is a supplied sound summary, not an automatic arithmetic proof.
Graph closures contain NONEMPTY call words and are not pruned by subsumption.
All functions use finite input lists/maps; arbitrary integer bit costs are extra.
A pool step budget raises an explicit resource error; it does not prove divergence.
"""
from dataclasses import dataclass
from collections import deque,Counter
import json

def require(ok,msg):
 if not ok:raise ValueError(msg)
def nat(x):return type(x) is int and x>=0

def multiset_step(old,new):
 require(type(old) in (tuple,list) and type(new) in (tuple,list),'finite occurrence lists')
 require(all(nat(x) for seq in (old,new) for x in seq),'natural-number elements')
 a,b=sorted(old),sorted(new);i=j=0;common=[];removed=[];added=[]
 while i<len(a) and j<len(b):
  if a[i]==b[j]:common.append(a[i]);i+=1;j+=1
  elif a[i]<b[j]:removed.append(a[i]);i+=1
  else:added.append(b[j]);j+=1
 removed.extend(a[i:]);added.extend(b[j:]);ok=bool(removed) and (not added or removed[-1]>added[-1])
 return dict(descends=ok,common=common,removed=removed,added=added,max_difference=max(removed[-1:] + added[-1:],default=None))

def verify_multiset(old,new,c):
 try:
  parts=(old,new,c['common'],c['removed'],c['added'])
  if not all(type(part) in (tuple,list) and all(nat(x) for x in part) for part in parts):return False
  bound=max(c['removed'],default=-1)
  return (Counter(old)==Counter(c['common'])+Counter(c['removed']) and Counter(new)==Counter(c['common'])+Counter(c['added']) and bound>=0 and all(y<bound for y in c['added']))
 except (KeyError,TypeError):return False

def pool_run(initial,policy='largest',limit=100000,trace=False):
 require(type(initial) in (list,tuple) and all(nat(x) for x in initial),'finite natural tasks');require(policy in ('largest','smallest'),'selection policy');require(nat(limit),'step budget')
 pool=list(enumerate(initial));fresh=len(pool);steps=0;peak=len(pool);records=[]
 while pool:
  require(steps<limit,'resource budget exhausted; not a nontermination certificate')
  i=min(range(len(pool)),key=lambda i:((-pool[i][1] if policy=='largest' else pool[i][1]),pool[i][0]));identifier,n=pool[i];before=[x for _,x in pool];pool.pop(i);children=[]
  if n:
   for _ in range(n+1):children.append((fresh,n-1));fresh+=1
  pool.extend(children);after=[x for _,x in pool];proof=multiset_step(before,after);require(proof['descends'] and verify_multiset(before,after,proof),'rewrite descent')
  steps+=1;peak=max(peak,len(pool))
  if trace:records.append(dict(step=steps,selected=[identifier,n],children=children,remaining=pool.copy(),certificate=proof))
 return dict(steps=steps,peak=peak,created=fresh,trace=records)

@dataclass(frozen=True)
class Graph:
 source:str
 target:str
 labels:tuple

class SCT:
 """0 absent; 1 weak source>=target; 2 strict source>target. No pruning."""
 def __init__(self,arities):
  require(type(arities) is dict and all(type(f) is str and f and nat(n) for f,n in arities.items()),'finite procedure signature')
  self.arities=arities.copy()
 def graph(self,source,target,labels):
  require(source in self.arities and target in self.arities,'known procedures');a,b=self.arities[source],self.arities[target];labels=tuple(labels)
  require(len(labels)==a*b and all(type(x) is int and x in (0,1,2) for x in labels),'typed size-change matrix')
  return Graph(source,target,labels)
 def compose(self,g,h):
  require(g.target==h.source,'matching intermediate procedure');a,b,c=(self.arities[g.source],self.arities[g.target],self.arities[h.target]);out=[]
  for i in range(a):
   for k in range(c):
    level=0
    for j in range(b):
     left,right=g.labels[i*b+j],h.labels[j*c+k]
     if left and right:level=max(level,left,right)
    out.append(level)
  return Graph(g.source,h.target,tuple(out))
 def closure(self,raw):
  graphs=[];derivations=[];index={};todo=deque();compositions=0
  def add(g,reason):
   if g in index:return index[g]
   i=len(graphs);index[g]=i;graphs.append(g);derivations.append(reason);todo.append(i);return i
  for i,g in enumerate(raw):
   require(self.graph(g.source,g.target,g.labels)==g,'well-formed supplied graph');add(g,dict(base=i))
  while todo:
   i=todo.popleft()
   for j in range(len(graphs)):
    for left,right in [(i,j),(j,i)]:
     g,h=graphs[left],graphs[right]
     if g.target==h.source:
      compositions+=1;add(self.compose(g,h),dict(left=left,right=right))
  idempotents=[];bad=[]
  for i,g in enumerate(graphs):
   if g.source==g.target and self.compose(g,g)==g:
    k=self.arities[g.source];strict=[j for j in range(k) if g.labels[j*k+j]==2];idempotents.append(dict(graph=i,strict_diagonal=strict))
    if not strict:bad.append(i)
  return dict(passed=not bad,graphs=graphs,derivations=derivations,idempotents=idempotents,bad=bad,compositions=compositions)
 def verify_certificate(self,raw,result):
  require(len(result['graphs'])==len(result['derivations']),'one derivation per graph');seen=[]
  for i,(g,d) in enumerate(zip(result['graphs'],result['derivations'])):
   self.graph(g.source,g.target,g.labels)
   if 'base' in d:
    require(type(d['base']) is int and 0<=d['base']<len(raw),'base index');expect=raw[d['base']]
   else:
    require(0<=d['left']<i and 0<=d['right']<i,'acyclic derivation references');expect=self.compose(seen[d['left']],seen[d['right']])
   require(expect==g,'composition certificate');seen.append(g)
  universe=set(seen);require(len(universe)==len(seen) and all(g in universe for g in raw),'unique closure includes inputs')
  for g in seen:
   for h in seen:
    if g.target==h.source:require(self.compose(g,h) in universe,'closure completeness')
  idem=[];bad=[]
  for i,g in enumerate(seen):
   if g.source==g.target and self.compose(g,g)==g:
    n=self.arities[g.source];strict=[j for j in range(n) if g.labels[j*n+j]==2];idem.append(dict(graph=i,strict_diagonal=strict))
    if not strict:bad.append(i)
  require(result['idempotents']==idem and result['bad']==bad and result['passed']==(not bad),'exact idempotent judgment')
  return True
 def word(self,result,index):
  # Optional output-sensitive expansion, iterative even for deep proof DAGs.
  stack=[index];out=[]
  while stack:
   d=result['derivations'][stack.pop()]
   if 'base' in d:out.append(d['base'])
   else:stack.extend([d['right'],d['left']])
  return out

def actual_swap(x,y):
 require(nat(x) and nat(y),'natural arguments');trace=[(x,y)]
 while x:
  x,y=y,x-1;trace.append((x,y))
 return trace

def serial(result):
 return {k:([dict(source=g.source,target=g.target,labels=g.labels) for g in v] if k=='graphs' else v) for k,v in result.items()}

def rejections_and_regressions():
 rejected=[]
 def rejects(name,fn):
  try:fn()
  except (ValueError,KeyError,TypeError):rejected.append(name);return
  raise RuntimeError('missing rejection: '+name)
 for name,a,b in [('negative task',[-1],[]),('bool task',[True],[]),('nonlist task',range(3),[])]:rejects(name,lambda a=a,b=b:multiset_step(a,b))
 require(multiset_step((2,),[1,1])['descends'],'mixed finite sequence types')
 require(not verify_multiset([2],[1],dict(common=[],removed=[],added=[1])),'empty removed certificate rejected')
 rejects('pool budget',lambda:pool_run([3],limit=1));rejects('arity type',lambda:SCT({'f':True}))
 s=SCT({'f':2});rejects('matrix size',lambda:s.graph('f','f',[2]));rejects('matrix label',lambda:s.graph('f','f',[3,0,0,0]));rejects('unknown procedure',lambda:s.graph('f','g',[]))
 g=s.graph('f','f',[0,2,1,0]);res=s.closure([g]);truncated=res.copy();truncated['graphs']=res['graphs'][:1];truncated['derivations']=res['derivations'][:1]
 rejects('incomplete closure',lambda:s.verify_certificate([g],truncated))
 tampered=res.copy();tampered['passed']=False;rejects('wrong verdict',lambda:s.verify_certificate([g],tampered))
 future=res.copy();future['derivations']=[res['derivations'][0],dict(left=2,right=0),res['derivations'][2]];rejects('future parent reference',lambda:s.verify_certificate([g],future))
 # Weak reflexive/transitive-chain graph: subsuming its stronger square loses
 # the only idempotent graph if an implementation tests only retained nodes.
 t=SCT({'h':3});chain=t.graph('h','h',[1,1,0,0,1,1,0,0,1]);closed=t.closure([chain]);require(not closed['passed'] and t.compose(chain,chain)!=chain,'unpruned weak-chain counterexample');t.verify_certificate([chain],closed)
 for n in range(5):
  expected=1
  for j in range(1,n+1):expected=1+(j+1)*expected
  for policy in ('largest','smallest'):require(pool_run([n],policy)['steps']==expected,'exact expansion tree count')
 return dict(rejections=rejected,weak_chain_closure=serial(closed),mixed_sequences=True,empty_removed_rejected=True)

def main():
 big=pool_run([3,1],'largest',trace=True);small=pool_run([3,1],'smallest',trace=True);require(big['steps']==small['steps']==44,'unfolded task count')
 s=SCT({'f':2});swap=s.graph('f','f',[0,2,1,0]);positive=s.closure([swap]);s.verify_certificate([swap],positive);require(positive['passed'] and len(positive['graphs'])==3,'rotating descent closure')
 a=s.graph('f','f',[2,0,0,0]);b=s.graph('f','f',[0,0,0,2]);negative=s.closure([a,b]);s.verify_certificate([a,b],negative);require(not negative['passed'],'disconnected strict threads')
 weak=s.graph('f','f',[1,0,0,0]);lossy=s.closure([weak]);require(not lossy['passed'],'weakening loses proof, not actual termination')
 empty=SCT({'f':0,'g':0});acyclic=empty.closure([empty.graph('f','g',[])]);cyclic=empty.closure([empty.graph('f','g',[]),empty.graph('g','f',[])]);require(acyclic['passed'] and not cyclic['passed'],'nonempty paths only, zero arity cycles')
 require(not multiset_step([1],[1,0])['descends'],'strict growth counterexample')
 out=dict(status='PASS',checks=rejections_and_regressions(),task_pool=dict(largest=big,smallest=small),swap=dict(trace=actual_swap(2,5),certificate=serial(positive)),split_strict=dict(certificate=serial(negative),bad_words=[s.word(negative,i) for i in negative['bad']],concrete_cycle=[[1,1],[0,2],[1,1]]),lossy=serial(lossy),zero_arity=dict(acyclic=serial(acyclic),cyclic=serial(cyclic)))
 print(json.dumps(out,indent=2))
if __name__=='__main__':main()