check_mixed_budget_independent.py

"""Independent semantic and deadline audit; no primary checker imports.
Python data structures model semantics, not native operations.
"""
import random, copy, json
from collections import deque
rng=random.Random(660201)
counts={k:0 for k in ('point_updates','unit_budget_steps','deadline_histories','word_commits','target_bit_steps','completed_boundaries','retained_forks','block_checks')}
def mixed(bits):
    if not any(bits) or all(bits): return 0
    m=len(bits)//2
    return 1+mixed(bits[:m])+mixed(bits[m:])
def insert(bits,x):
    if bits[x]: return bits,[]
    if len(bits)==1:return (1,),[]
    m=len(bits)//2; old=int(any(bits) and not all(bits))
    if x<m:
        a,ds=insert(bits[:m],x); z=a+bits[m:]
    else:
        a,ds=insert(bits[m:],x-m); z=bits[:m]+a
    return z,ds+[int(any(z) and not all(z))-old]
for width,trials in [(8,None),(16,5000),(64,5000)]:
    cases=((tuple((mask>>i)&1 for i in range(width)),x) for mask in range(1<<width) for x in range(width)) if trials is None else ((tuple(rng.randrange(2) for _ in range(width)),rng.randrange(width)) for _ in range(trials))
    for bits,x in cases:
        out,delta=insert(bits,x)
        assert out==bits[:x]+(1,)+bits[x+1:]
        assert mixed(out)==mixed(bits)+sum(delta)
        for cap in (0,1,3,7,17):
            value=mixed(bits); slack=max(cap-value,0); debt=max(value-cap,0)
            for d in delta:
                assert d in (-1,0,1)
                if d==1:
                    if slack:slack-=1
                    else:debt+=1
                elif d==-1:
                    if debt:debt-=1
                    else:slack+=1
                value+=d
                assert value>=0 and cap-value==slack-debt and not(slack and debt)
                assert bool(debt)==(value>cap)
                counts['unit_budget_steps']+=1
            assert value==mixed(out)
        counts['point_updates']+=1
# All one-hole profiles: collapse every ancestor after final point.
for h in range(1,9):
    w=1<<h
    for x in range(w):
        bits=tuple(int(i!=x) for i in range(w)); out,ds=insert(bits,x)
        assert mixed(bits)==h and sum(ds)==-h and all(out)
        counts['point_updates']+=1
class Row:
    def __init__(self):self.words={};self.q=deque();self.active=None;self.cover=set()
    def service(self):
        if self.active is None and self.q:self.active=self.q.popleft()
        if self.active is None:return
        n,left=self.active;left-=1
        if left==0:self.cover.add(n);self.active=None
        else:self.active=(n,left)
    def word(self,n,v):
        for _ in range(n):
            for _ in range(4):self.service()
            counts['target_bit_steps']+=1
        if n not in self.words:
            self.words[n]=set();self.q.append((n,n+1))
        self.words[n].add(v)
        counts['word_commits']+=1
    def complete(self):return all(len(v)==1<<n for n,v in self.words.items())
    def quiet(self):return not self.q and self.active is None
    def gate(self,r):
        m={}
        for j in range(1,1+max(self.cover,default=1).bit_length()):
            a=1<<(j-1);bits=tuple(int(n in self.cover) for n in range(a,2*a))
            ell=j.bit_length()-1;b=1<<ell;m[b]=m.get(b,0)+mixed(bits)
        counts['block_checks']+=len(m)
        return all(v<=r*b for b,v in m.items())
for trial in range(500):
    rows=[Row() for _ in range(rng.randrange(1,5))]
    todo=[]
    for ri in range(len(rows)):
        for n in rng.sample(range(1,6),rng.randrange(1,6)):
            todo += [(ri,n,v) for v in range(1<<n)]
            todo += [(ri,n,rng.randrange(1<<n)) for _ in range(rng.randrange(8))]
    rng.shuffle(todo)
    snapshots=[]
    for ri,n,v in todo:
        rows[ri].word(n,v)
        for row in rows:
            if row.complete():
                assert row.quiet() and row.cover==set(row.words)
                counts['completed_boundaries']+=1
            row.gate(trial%4)
        if rng.randrange(16)==0:
            snapshots.append((copy.deepcopy(rows),[(set(r.cover),{n:frozenset(v) for n,v in r.words.items()}) for r in rows]))
    assert all(row.complete() and row.quiet() for row in rows)
    for snap,expected in snapshots:
        assert [(set(r.cover),{n:frozenset(v) for n,v in r.words.items()}) for r in snap]==expected
        # Continue a retained version through a valid complete row, including prior partial widths.
        for row in snap:
            for n,words in list(row.words.items()):
                for v in range(1<<n):
                    if v not in words:row.word(n,v)
            assert row.complete() and row.quiet() and row.cover==set(row.words)
        counts['retained_forks']+=1
    counts['deadline_histories']+=1
print(json.dumps({'status':'pass','counts':counts,'qualification':'Finite semantic, slack/debt and normalized service model only. No native primitive implementation or independent proof of constant C.'},indent=2))