check_interval_boundary_composition.py

#!/usr/bin/env python3
"""Reader32 semantic model. Tuple queues stand for strict persistent FIFOs.
Independent integer-set oracle; no native timing or machine implementation claim.
"""
from dataclasses import dataclass
from itertools import permutations
from collections import Counter
import random,json
C=Counter()
@dataclass(frozen=True)
class Empty: pass
@dataclass(frozen=True)
class Full: pass
@dataclass(frozen=True)
class Cut:
    frames:tuple
    fullness:tuple
    minimum:tuple
    maximum:tuple
@dataclass(frozen=True)
class Branch:
    zero:object
    one:object
    full:bool
    minimum:bool
    maximum:bool
E,F=Empty(),Full()
def tail(q):return q[1:] if q else ()
def view(t):
    if isinstance(t,Empty):return False,False,False,E,E
    if isinstance(t,Full):return True,True,True,F,F
    if isinstance(t,Branch):return t.full,t.minimum,t.maximum,t.zero,t.one
    bit,other,old_min,old_max=t.frames[0]
    rest=t.frames[1:]
    child=Cut(rest,tail(t.fullness),tail(t.minimum),tail(t.maximum)) if rest else F
    assert max(len(t.fullness),len(t.minimum),len(t.maximum))<=len(t.frames)
    flags=(not t.fullness,old_min or not t.minimum,old_max or not t.maximum)
    return flags+((other,child) if bit else (child,other))
@dataclass(frozen=True)
class Row:
    root:object=E
    components:tuple=()
    quota:tuple|None=None

def add(row,w,quota=False):
    frames,depth,fc,mc,xc=(),(),(),(),()
    cur=row.root;pred=succ=False
    for ch in w:
        bit=int(ch);_,old_min,old_max,z,o=view(cur)
        other=z if bit else o
        sf,sm,sx,_,_=view(other)
        depth=(None,)+depth
        frames+=((bit,other,old_min,old_max),)
        if not sf:fc=depth
        if bit:mc=depth;pred=sx
        else:xc=depth;succ=sm
        cur=o if bit else z
        C['path_steps']+=1
    if view(cur)[0]:C['duplicates']+=1;return row
    count=row.components
    change=1-int(pred)-int(succ)
    if change==1:count=(None,)+count
    elif change==-1:
        assert len(count)>=2
        count=count[1:]
    q=row.quota if row.quota is not None else (None,)*len(w)
    if quota and not q:C['quota_rejections']+=1;return None
    C['distinct_insertions']+=1
    return Row(Cut(frames,fc,mc,xc),count,tail(q) if quota else None)

def components(s):return sum(x-1 not in s for x in s)
def bits(x,width):return format(x,f'0{width}b')
def member(t,w):
    for b in w:
        full,_,_,z,o=view(t)
        if full:return True
        t=o if b=='1' else z
    return view(t)[0]
def audit(row,s,width):
    assert len(row.components)==components(s)
    stack=[(row.root,0,width)]
    while stack:
        t,lo,depth=stack.pop();size=1<<depth
        full,mn,mx,z,o=view(t)
        assert (full,mn,mx)==(all(i in s for i in range(lo,lo+size)),lo in s,lo+size-1 in s)
        if depth:stack.extend(((z,lo,depth-1),(o,lo+size//2,depth-1)))
        C['annotation_checks']+=1
    C['component_audits']+=1

def splice(b,r):
    # Explicit immutable-machine continuation has fixed fields; Python list models its stack.
    stack=[('visit',b,r)];out=[];calls=0
    while stack:
        action,*args=stack.pop()
        if action=='join':
            o=out.pop();z=out.pop();zf,zm,_,_,_=view(z);of,_,om,_,_=view(o)
            out.append(F if zf and of else Branch(z,o,False,zm,om));continue
        b,r=args;calls+=1
        rf,_,_,rz,ro=view(r);bf,_,_,bz,bo=view(b)
        if isinstance(r,Empty):out.append(b)
        elif rf or bf:out.append(F)
        elif isinstance(b,Empty):out.append(r)
        else:stack.extend((('join',),('visit',bo,ro),('visit',bz,rz)))
    assert len(out)==1
    C['splice_calls']+=calls
    return out[0],calls
@dataclass(frozen=True)
class Source:
    committed:object=E
    pending:object=E
    literal:frozenset=frozenset()
def select(src,row,s,width,k):
    b,calls=splice(src.committed,src.pending)
    assert calls<=1+4*k*width
    return Source(b,row.root,src.literal|s)
def query(src,w,width):
    return len(w)==width and (member(src.committed,w) or member(src.pending,w))
def check_source(src,width):
    for w in ('0'*(width-1),'0'*(width+1)):
        assert not query(src,w,width)
        C['outside_width_queries']+=1
    for x in range(1<<width):
        w=bits(x,width)
        assert query(src,w,width)==(x in src.literal)
        C['product_queries']+=1

def main():
    rng=random.Random(149);saved=[]
    for width in range(1,4):
        for mask in range(1<<(1<<width)):
            s=frozenset(x for x in range(1<<width) if mask>>x&1)
            seqs=[sorted(s),sorted(s,reverse=True)];a=list(s);rng.shuffle(a);seqs.append(a)
            for seq in seqs:
                row=Row();seen=frozenset()
                for x in seq+seq[:2]:row=add(row,bits(x,width));seen=seen|{x};audit(row,seen,width)
                saved.append((row,seen,width));C['exhaustive_set_orders']+=1
    for seq in permutations(range(8)):
        row=Row();s=set()
        for x in seq:
            row=add(row,bits(x,3));s.add(x);assert len(row.components)==components(s)
        assert view(row.root)[:3]==(True,True,True)
        C['full_cube_permutations']+=1
    for old,s,width in saved[::3]:
        x=rng.randrange(1<<width);new=add(old,bits(x,width));audit(old,s,width);audit(new,s|{x},width)
        C['retained_row_branches']+=1
    # Exact cost count on all width3 right sets with one/two intervals and arbitrary committed sets.
    width=3
    sets=[frozenset(x for x in range(8) if m>>x&1) for m in range(256)]
    rows=[]
    for s in sets:
        r=Row()
        for x in s:r=add(r,bits(x,width))
        rows.append(r)
    for s,r in zip(sets,rows):
        if components(s)>2:continue
        for bset,b in zip(sets,rows):
            merged,calls=splice(b.root,r.root)
            assert calls<=1+4*components(s)*width
            for x in range(8):assert member(merged,bits(x,width))==(x in s|bset)
            C['exhaustive_splices']+=1
    for width in range(2,8):
        k=3;rows=[]
        for _ in range(40):
            s=set()
            for _ in range(k):
                a,b=sorted((rng.randrange(1<<width),rng.randrange(1<<width)))
                s.update(range(a,b+1))
            row=Row();seq=list(s);rng.shuffle(seq)
            for x in seq:row=add(row,bits(x,width))
            audit(row,s,width);rows.append((row,frozenset(s)))
        history=[Source()]
        for _ in range(100):
            old=rng.choice(history);row,s=rng.choice(rows);new=select(old,row,s,width,k);history.append(new)
            check_source(old,width);check_source(new,width);C['retained_source_branches']+=1
    width,k=4,2;table={};raw={};bad=()
    for _ in range(3000):
        v=rng.randrange(16);x=rng.randrange(16);old=table.get(v,Row());new=add(old,bits(x,width))
        delta=int(len(new.components)>k)-int(len(old.components)>k)
        if delta==1:bad=(None,)+bad
        elif delta==-1:assert bad;bad=bad[1:]
        table[v]=new;raw.setdefault(v,set()).add(x)
        assert len(bad)==sum(components(s)>k for s in raw.values());C['global_gate_updates']+=1
    for width in range(2,10):
        row=Row()
        for x in range(0,1<<width,2):row=add(row,bits(x,width))
        assert len(row.components)==1<<(width-1)
        for x in range(1,1<<width,2):row=add(row,bits(x,width))
        assert len(row.components)==1;C['late_interval_completion_families']+=1
        quota=Row()
        for x in range(width):quota=add(quota,bits(x,width),True)
        assert add(quota,bits(0,width),True) is quota
        assert add(quota,bits(width,width),True) is None
        # One interval has unbounded dyadic cover, so bounded-prefix-cover classes do not subsume it.
        s=set(range(1,(1<<width)-1))
        def cover(lo,n):
            if all(x in s for x in range(lo,lo+n)):return 1
            if not any(x in s for x in range(lo,lo+n)):return 0
            return cover(lo,n//2)+cover(lo+n//2,n//2)
        assert components(s)==1 and cover(0,1<<width)==2*width-2
        C['strict_extension_families']+=1
    for r in range(2,7):
        width=1<<r;row=Row()
        for x in range(1,width-1):row=add(row,bits(x,width),True)
        assert len(row.components)==1 and len(row.quota)==2
        def interval_cover(lo,size):
            hi=lo+size-1
            if lo>=1 and hi<=width-2:return 1
            if hi<1 or lo>width-2:return 0
            return interval_cover(lo,size//2)+interval_cover(lo+size//2,size//2)
        assert interval_cover(0,1<<width)==2*r-2
        C['name_linear_extension_families']+=1
    print(json.dumps({'checks':dict(sorted(C.items())),'native_recognizer_implemented':False,'timing_evidence':False},indent=2))
if __name__=='__main__':main()