#!/usr/bin/env python3
"""Exact finite placement and static Chord models; standard library only.
Print JSON to stdout. Explicit checks run in ordinary and -O modes.
No networking, configuration writes or production migration is performed.
"""
import sys
sys.dont_write_bytecode=True
from bisect import bisect_left
from collections import Counter
from itertools import combinations,permutations,product
from random import Random
from fractions import Fraction
import json

def require(v,msg):
    if not v:raise ValueError(msg)
def check(v,msg):
    if not v:raise AssertionError(msg)
class Ring:
    def __init__(self,M,tokens):
        require(type(M) is int and M>=2,'integer space at least two')
        require(bool(tokens),'nonempty token configuration')
        require(all(type(x) is int and 0<=x<M and isinstance(owner,str) and owner for x,owner in tokens),'coordinate and physical owner')
        require(len({x for x,_ in tokens})==len(tokens),'distinct token coordinates')
        self.M=M;items=sorted(tokens);self.positions=tuple(x for x,_ in items);self.owners=tuple(o for _,o in items)
    def token(self,k):
        require(type(k) is int and 0<=k<self.M,'key coordinate')
        i=bisect_left(self.positions,k)%len(self.positions)
        return self.positions[i],self.owners[i]
    def owner(self,k):return self.token(k)[1]
    def physical_counts(self):return dict(sorted(Counter(self.owner(k) for k in range(self.M)).items()))
    def movement(self,other,keys):
        require(other.M==self.M,'same coordinate space')
        return [dict(key=k,before=self.owner(k),after=other.owner(k)) for k in keys if self.owner(k)!=other.owner(k)]

def hrw_rank(scores,members):
    require(bool(members) and len(set(members))==len(members),'nonempty distinct members')
    require(all(isinstance(v,str) and v in scores and type(scores[v]) is int for v in members),'stable name and integer score')
    return sorted(members,key=lambda v:(-scores[v],v))
def hrw_top(scores,members,r):
    require(type(r) is int and 0<=r<=len(members),'candidate count')
    return hrw_rank(scores,members)[:r]

def delta(a,b,M):return (b-a)%M
def build_network(m,nodes):
    require(type(m) is int and m>=1,'positive identifier width')
    M=1<<m;require(bool(nodes) and len(set(nodes))==len(nodes),'nonempty distinct members')
    require(all(type(v) is int and 0<=v<M for v in nodes),'member coordinate')
    ordered=sorted(nodes)
    def successor(k):return ordered[bisect_left(ordered,k)%len(ordered)]
    return {u:dict(successor=successor((u+1)%M),fingers=[successor((u+(1<<i))%M) for i in range(m)]) for u in ordered}

def chord_lookup(m,network,start,key,budget=1000,unreachable=()):
    """Each decision reads only network[current]. Other records are read only
    after simulated message delivery. O(sum(1+local finger length)) local work
    and full candidate trace; no global member sorting or successor oracle.
    Returns owner identity, not the stored value.
    """
    require(type(m) is int and m>=1,'positive identifier width')
    M=1<<m;require(type(key) is int and 0<=key<M,'key coordinate')
    require(type(start) is int and 0<=start<M,'start coordinate')
    require(type(budget) is int and budget>=0,'nonnegative hop budget')
    unavailable=set(unreachable);current=start;trace=[]
    for _ in range(budget):
        if current in unavailable or current not in network:
            return dict(status='UNKNOWN',reason='destination_unavailable',trace=trace,unresolved=current)
        local=network[current];s=local['successor'];row=dict(node=current,successor=s,candidates=[])
        if key==current:
            row['reason']='equal_node';trace.append(row);return dict(status='FOUND',owner=current,trace=trace)
        if s==current:
            row['reason']='singleton_under_correct_successor_contract';trace.append(row);return dict(status='FOUND',owner=current,trace=trace)
        if 0<delta(current,key,M)<=delta(current,s,M):
            row['reason']='correct_successor_brackets_key';trace.append(row);return dict(status='FOUND',owner=s,trace=trace)
        best=s;distance=delta(current,s,M)
        # Correct successor lies strictly before key in this branch.
        for f in local['fingers']:
            d=delta(current,f,M);ok=0<d<delta(current,key,M)
            row['candidates'].append(dict(finger=f,distance=d,eligible=ok))
            if ok and d>distance:best=f;distance=d
        row.update(reason='forward',next=best);trace.append(row);current=best
    return dict(status='UNKNOWN',reason='hop_budget',trace=trace,unresolved=current)

SCORES={
 'alpha':dict(zip('ABCDE',[90,20,70,40,75])),
 'beta':dict(zip('ABCDE',[30,80,60,20,81])),
 'gamma':dict(zip('ABCDE',[10,50,95,40,10])),
 'delta':dict(zip('ABCDE',[70,60,20,85,90])),
 'epsilon':dict(zip('ABCDE',[40,30,60,55,59])),
 'zeta':dict(zip('ABCDE',[65,65,10,50,65]))}

def literal_successor(nodes,key,M):return min(nodes,key=lambda v:((v-key)%M))
def independent_path_check(nodes,m,key,result):
    M=1<<m;check(result['status']=='FOUND' and result['owner']==literal_successor(nodes,key,M),'local lookup equals independent circular minimization')
    owner=result['owner'];predecessor=min(nodes,key=lambda v:((key-v-1)%M))
    for row in result['trace']:
        if row['reason']=='forward':
            u=row['node'];v=row['next']
            check(0<delta(u,v,M)<delta(u,key,M),'strict key interval progress')
            D=delta(u,predecessor,M);check(delta(v,predecessor,M)*2<D or delta(v,predecessor,M)==0,'full finger distance to predecessor halves')
    check(len(result['trace'])<=m+1,'m-bit deterministic bound')

def main():
    rng=Random(10102026)
    old=Ring(32,[(1,'A'),(8,'B'),(16,'C'),(24,'D')]);joined=Ring(32,[(1,'A'),(8,'B'),(12,'E'),(16,'C'),(24,'D')]);removed=Ring(32,[(1,'A'),(12,'E'),(16,'C'),(24,'D')]);virtual=Ring(32,[(1,'A'),(17,'A'),(5,'C'),(21,'C'),(9,'B'),(25,'B'),(13,'D'),(29,'D')])
    join_moves=old.movement(joined,range(32));leave_moves=joined.movement(removed,range(32))
    check([x['key'] for x in join_moves]==[9,10,11,12],'ring joining example')
    check([x['key'] for x in leave_moves]==list(range(2,9)),'ring leaving example')
    check(old.physical_counts()=={'A':9,'B':7,'C':8,'D':8} and virtual.physical_counts()==dict.fromkeys('ABCD',8),'physical ownership counts')
    hrw={k:dict(old=hrw_rank(s,list('ABCD')),joined=hrw_rank(s,list('ABCDE')),removed=hrw_rank(s,list('ABD'))) for k,s in SCORES.items()}
    check([k for k,v in hrw.items() if v['old'][0]!=v['joined'][0]]==['beta','delta'],'HRW newcomer wins only two')
    check([k for k,v in hrw.items() if v['old'][0]!=v['removed'][0]]==['gamma','epsilon'],'HRW removed winner only two')
    check(hrw['zeta']['joined'][0]=='A','stable tie order')
    network=build_network(5,[1,4,8,14,21,28]);queries=[]
    for start,key in [(4,31),(1,27),(28,0),(14,14),(8,3)]:
        z=chord_lookup(5,network,start,key);independent_path_check(list(network),5,key,z);queries.append(dict(start=start,key=key,result=z))
    gap_case=chord_lookup(5,build_network(5,[0,1,16]),0,15)
    check([x['node'] for x in gap_case['trace']]==[0,1] and gap_case['owner']==16 and delta(1,15,32)*2>delta(0,15,32),'distance to key need not halve')
    slow={u:dict(successor=x['successor'],fingers=[x['successor']]) for u,x in network.items()};slow_query=chord_lookup(5,slow,4,31)
    check([x['node'] for x in slow_query['trace']]==[4,8,14,21,28] and slow_query['owner']==1,'correct successors retain correctness')
    bad={u:dict(successor=x['successor'],fingers=x['fingers'][:]) for u,x in network.items()};bad[28]['successor']=4
    bad_answer=chord_lookup(5,bad,28,0);check(bad_answer['owner']==4 and literal_successor(list(network),0,32)==1,'incorrect successor violates premise')
    timeout=chord_lookup(5,network,4,31,unreachable=[21]);limited=chord_lookup(5,network,4,31,budget=1)
    check(timeout['status']==limited['status']=='UNKNOWN','unavailable/budget not success')
    # Exhaustive small ring configurations and all permitted single insert/remove.
    ring_updates=0
    for M in range(2,10):
        for mask in range(1,1<<M):
            nodes=[i for i in range(M) if mask>>i&1];r=Ring(M,[(i,str(i)) for i in nodes])
            for key in range(M):check(r.token(key)[0]==literal_successor(nodes,key,M),'ring lower bound versus circular oracle')
            for x in range(M):
                if x not in nodes:
                    z=Ring(M,[(i,str(i)) for i in nodes+[x]])
                    check(all(z.owner(k)==r.owner(k) or z.owner(k)==str(x) for k in range(M)),'no old-to-old joining movement');ring_updates+=1
                elif len(nodes)>1:
                    z=Ring(M,[(i,str(i)) for i in nodes if i!=x])
                    check(all(r.owner(k)==str(x) or z.owner(k)==r.owner(k) for k in range(M)),'only removed owner moves');ring_updates+=1
    # All rankings, all member subsets, insertion/removal, and finite score ties.
    rank_cases=top_cases=0
    names=list('ABCDE')
    for order in permutations(names):
        scores={v:5-i for i,v in enumerate(order)}
        for mask in range(1,1<<5):
            V=[v for i,v in enumerate(names) if mask>>i&1];rank=hrw_rank(scores,V)
            check(rank==[v for v in order if v in V],'ranking restricts global permutation')
            for x in names:
                if x not in V:
                    W=hrw_rank(scores,V+[x]);check(W[0]==rank[0] or W[0]==x,'HRW insertion stability')
                    for t in range(1,len(V)+1):check(set(W[:t])-{x}<=set(rank[:t]),'top-r insertion survivor containment');top_cases+=1
                elif len(V)>1:
                    W=hrw_rank(scores,[v for v in V if v!=x]);check(rank[0]==x or W[0]==rank[0],'HRW deletion stability')
            rank_cases+=1
    tie_cases=0
    for values in product(range(3),repeat=4):
        s=dict(zip('ABCD',values));expected=sorted(s,key=lambda v:(-s[v],v))
        for V in permutations('ABCD'):check(hrw_rank(s,list(V))==expected,'membership input order independence');tie_cases+=1
    # All subsets for m<=3, plus 1200 distinct m=4 subsets; all sources/keys.
    lookup_cases=configurations=0
    for m in range(1,5):
        M=1<<m
        masks=range(1,1<<M) if m<=3 else rng.sample(range(1,1<<M),1200)
        for mask in masks:
            nodes=[u for u in range(M) if mask>>u&1];net=build_network(m,nodes);configurations+=1
            for u in nodes:
                for k in range(M):independent_path_check(nodes,m,k,chord_lookup(m,net,u,k));lookup_cases+=1
    degraded=0
    for _ in range(1200):
        m=6;nodes=sorted(rng.sample(range(64),rng.randrange(1,20)));net=build_network(m,nodes)
        for u in nodes:net[u]['fingers']=[rng.choice(nodes) for _ in range(rng.randrange(7))]
        u=rng.choice(nodes);k=rng.randrange(64);z=chord_lookup(m,net,u,k,budget=len(nodes)+1)
        check(z['status']=='FOUND' and z['owner']==literal_successor(nodes,k,64) and len(z['trace'])<=len(nodes),'arbitrary live shortcuts with correct successor');degraded+=1
    # Exact rational integral for the raw multiplier counterexample.
    scaled_win=Fraction(1,4)+Fraction(1,2);check(scaled_win==Fraction(3,4) and scaled_win!=Fraction(2,3),'raw score scaling is not proportional weighting')
    # Configuration change alone never copies stored data.
    storage={'C':{10:'v10'},'E':{}};check(joined.owner(10)=='E' and 10 not in storage['E'],'new mapping not completed transfer')
    invalid=0
    for f in [lambda:Ring(8,[]),lambda:Ring(8,[(1,'A'),(1,'B')]),lambda:hrw_top({'A':1},['A'],2),lambda:build_network(2,[1,1])]:
        try:f()
        except ValueError:invalid+=1
        else:raise AssertionError('invalid configuration accepted')
    record=dict(status='PASS',checks=dict(ring_single_updates=ring_updates,ranking_member_cases=rank_cases,top_r_insertions=top_cases,finite_score_tie_orders=tie_cases,static_ring_configurations=configurations,all_source_key_lookups=lookup_cases,degraded_finger_histories=degraded,invalid_inputs=invalid),examples=dict(ring_before=old.physical_counts(),ring_joined=joined.physical_counts(),ring_removed=removed.physical_counts(),join_moves=join_moves,leave_moves=leave_moves,virtual_counts=virtual.physical_counts(),hrw=hrw,network=network,queries=queries,key_distance_counterexample=gap_case,slow_successor_lookup=slow_query,wrong_successor=bad_answer,unavailable=timeout,budget=limited,scaled_uniform_win=str(scaled_win)),scope='Finite static placement/lookup and deliberate premise failures. No membership repair, state transfer, consistency protocol, hash-independence test or deployment certification.')
    print(json.dumps(record,ensure_ascii=False,indent=2))
if __name__=='__main__':main()