check_ordered_suffix.py

#!/usr/bin/env python3
"""Finite semantics audit; tuple deque/FIFO and integer reader lag are models.
Linked unit gaps and linked endpoint digits expose the actual cursor steps.
Native complexity follows from the written proof and imported strict primitives,
not Python tuple cost. Integer set/min operations below belong to test oracles.
"""
from dataclasses import dataclass, replace
from itertools import product
from random import Random
import json
from check_sparse_age_minimum import Unit, depth, numeral, decode, release, step, idle


def units(n):
    p=None
    for _ in range(n): p=Unit(p)
    return p


@dataclass(frozen=True)
class Entry:
    gap: object
    endpoint: object


def sequence(hist):
    p=0; seq=()
    for x in sorted(k for k,c in hist.items() if c):
        seq+=(Entry(units(x-p),numeral(x)),); p=x
    return seq


def inspect(seq):
    p=0; result=[]
    for e in seq:
        g=depth(e.gap); assert g>0
        p+=g; assert p==decode(e.endpoint); result.append(p)
    return tuple(result)


def splice(seq,hist,old,n):
    suffix=seq; prefix=(); acc=None; gap=suffix[0].gap if suffix else None
    old_cursor=units(old); retained=False
    for d in range(1,n+1):
        at_old=old_cursor is not None and old_cursor.tail is None
        old_cursor=old_cursor.tail if old_cursor is not None else None
        acc=Unit(acc); retained=False
        if suffix:
            assert gap is not None
            gap=gap.tail
            if gap is None:
                # hist[d] models the paid, parallel current histogram cursor.
                if not(at_old and hist[d]==1):
                    prefix+=(Entry(acc,suffix[0].endpoint),); acc=None; retained=True
                suffix=suffix[1:]; gap=suffix[0].gap if suffix else None
    if n<=old: return seq
    if not retained:
        assert acc is not None
        prefix+=(Entry(acc,numeral(n)),)  # models input-paid position numeral
    if suffix:
        assert gap is not None
        suffix=(replace(suffix[0],gap=gap),)+suffix[1:]
    return prefix+suffix


@dataclass(frozen=True)
class Row:
    lower: object
    upper: object


@dataclass(frozen=True)
class Compare:
    row: Row
    index: int  # fixed finite palette position, not an endpoint number
    left: object
    right: object


@dataclass(frozen=True)
class Lane:
    minimum: object=None
    queue: tuple=()
    active: object=None


def enqueue(lanes,row):
    return (replace(lanes[0],minimum=release(lanes[0].minimum,row.lower)),)+tuple(
        replace(s,queue=s.queue+(row,)) for s in lanes[1:])


def lane_step(s,palette,j):
    s=replace(s,minimum=step(s.minimum))
    if j==0: return s
    c=s.active
    if c is None:
        if not s.queue: return s
        row=s.queue[0]
        return replace(s,queue=s.queue[1:],active=Compare(row,0,palette[0],row.upper))
    a,b=c.left,c.right
    unequal=(a is None)!=(b is None) or (a is not None and b is not None and a.bit!=b.bit)
    if unequal:
        if c.index+1==j:
            return replace(s,active=None,minimum=release(s.minimum,c.row.lower))
        i=c.index+1
        return replace(s,active=Compare(c.row,i,palette[i],c.row.upper))
    if a is None: return replace(s,active=None)
    return replace(s,active=replace(c,left=a.tail,right=b.tail))


def quiet(s): return not s.queue and s.active is None and idle(s.minimum)


def serve(lanes,palette,count):
    for _ in range(count):
        if all(quiet(s) for s in lanes): break
        lanes=tuple(lane_step(s,palette,j) for j,s in enumerate(lanes))
    return lanes


def answers(lanes,maxima,rows,stop):
    palette=tuple(numeral(x) for x in maxima); m=len(maxima)
    positions=[0]*m; values=[None]*m
    for n in range(1,stop+1):
        lanes=serve(lanes,palette,1024*m)
        for j,s in enumerate(lanes):
            if values[j] is None and quiet(s) and s.minimum is not None:
                values[j]=decode(s.minimum.best)
            if values[j] is not None: positions[j]=min(n,positions[j]+4)
        # Range/lag arithmetic models the fixed unary readers, not a native op.
        got=any((0 if j==0 else maxima[j-1])<n<=maxima[j] and values[j] is not None
                and positions[j]==n and values[j]<=n for j in range(m))
        assert got==any(b<=n<=h for b,h in rows),(maxima,rows,n,got)
    return stop


def main():
    rng=Random(196); splices=forks=prefixes=debt_checks=0
    for counts in product(range(3),repeat=5):
        hist={i+1:c for i,c in enumerate(counts) if c}; seq=sequence(hist)
        for old in (0,)+tuple(hist):
            for n in range(1,8):
                before=inspect(seq); got=splice(seq,hist,old,n); new=dict(hist)
                if n>old:
                    if old: new[old]-=1
                    new[n]=new.get(n,0)+1
                assert inspect(got)==tuple(sorted(x for x,c in new.items() if c))
                assert inspect(seq)==before; splices+=1
    for M in (100,10000):
        hist={1:1,2:1,M:1}; seq=sequence(hist)
        assert inspect(splice(seq,hist,1,2))==(2,M)
        assert inspect(splice(seq,hist,1,3))==(2,3,M)
        assert inspect(seq)==(1,2,M); splices+=2
    for trial in range(75):
        m=1+trial%5; maxima=sorted(rng.sample(range(1,160),m))
        palette=tuple(numeral(x) for x in maxima); lanes=tuple(Lane() for _ in maxima)
        rows=[]; saved=[]
        for i in range(1,36):
            lanes=serve(lanes,palette,64*m*i.bit_length())
            h=rng.choice(maxima); b=rng.randrange(1,h+1)
            lanes=enqueue(lanes,Row(numeral(b),numeral(h))); rows.append((b,h))
            if i%7==0: saved.append((lanes,tuple(rows)))
        for state,selected in saved:
            prefixes+=answers(state,maxima,selected,maxima[-1]+2)
            done=serve(state,palette,100000); assert all(quiet(s) for s in done)
            for j,s in enumerate(done):
                bs=[b for b,h in selected if j==0 or h>maxima[j-1]]
                assert (s.minimum is None)==(not bs)
                if bs: assert decode(s.minimum.best)==min(bs)
            forks+=1
    M=(1<<1800)+1
    for maxima,rows in [([2,M,M+2],[(1,2),(7,M),(9,M+2)]),
                        ([1,3,M],[(2,3),(4,M)]),([M,M+2,M+4],[(1,M+4),(2,M)])]:
        lanes=tuple(Lane() for _ in maxima)
        for b,h in rows: lanes=enqueue(lanes,Row(numeral(b),numeral(h)))
        prefixes+=answers(lanes,maxima,rows,40)
    for maxima in ([1,3,7],[31,63,127],[3,5,9,17]):
        palette=tuple(numeral(x) for x in maxima); lanes=tuple(Lane() for _ in maxima); rows=[]
        for i in range(1,55):
            lanes=serve(lanes,palette,2*i.bit_length())
            h=rng.choice(maxima); b=rng.randrange(1,h+1)
            lanes=enqueue(lanes,Row(numeral(b),numeral(h))); rows.append((b,h))
            for j in range(1,len(maxima)):
                bs=[b for b,h in rows if h>maxima[j-1]]
                k=max(4,maxima[j-1].bit_length(),min(bs).bit_length() if bs else 0)
                D=sum(x.bit_length()+2 for x in maxima[:j])+2*k
                bound=D+sum((1<<d)*max(0,D-2*d) for d in range(1,D//2+1))
                s=lanes[j]; count=0
                while not quiet(s): s=lane_step(s,palette,j); count+=1
                assert count<=bound,(maxima,j,i,count,bound); debt_checks+=1
    for k in range(4,513):
        assert 4*k<=16*(1<<(k-4)); assert 64-15*k<=16
    print(json.dumps(dict(occupied_sequence_updates=splices,retained_receipt_forks=forks,
        query_prefix_answers=prefixes,combined_debt_checks=debt_checks,deadline_inequalities=509,
        scope='semantic deque/FIFO, histogram, setup and reader models; linked gap/digit audit'),indent=2))


if __name__=='__main__': main()