check_frozen_support_reuse.py

#!/usr/bin/env python3
"""Finite semantic and operation-count audit for frozen-support reuse.

The exhaustive core was independently designed during adversarial review.
Whole-record, retained-state and stress checks were added during reconciliation.
Python sets, integers and strings are oracles, not native machine operations.
No other Lab checker is imported. Run directly with Python 3.
"""
from itertools import product

def words(n): return [''.join(w) for w in product('01', repeat=n)]
def split(U):
    p=0
    while len({w[p] for w in U})==1:p+=1
    return p,{w for w in U if w[p]=='0'},{w for w in U if w[p]=='1'}
def view(U,X):
    if not X:return 0
    if X==U:return 1
    _,L,R=split(U)
    return view(L,X&L),view(R,X&R)
def mixed(t):return 0 if isinstance(t,int) else 1+mixed(t[0])+mixed(t[1])
def merge(B,X):
    if X==0:return B,1
    if X==1 or B==1:return 1,1
    if B==0:return X,1
    l,c=merge(B[0],X[0]);r,d=merge(B[1],X[1])
    return (l if isinstance(l,int) and l==r else (l,r)),1+c+d

def route(U,q):
    bs=[]
    while len(U)>1:
        p,L,R=split(U)
        if len(q)<=p:return bs,False
        b=int(q[p]);bs.append(b);U=R if b else L
    return bs,q in U

def lookup(t,bs):
    for b in bs:
        if isinstance(t,tuple):t=t[b]
    assert isinstance(t,int)
    return bool(t)

cases=queries=0
for n in range(1,4):
    W=words(n)
    for mask in range(1,2**len(W)):
        U={w for i,w in enumerate(W) if mask>>i&1}
        ul=sorted(U)
        sets=[{w for i,w in enumerate(ul) if m>>i&1} for m in range(2**len(U))]
        views=[view(U,X) for X in sets]
        for B,bv in zip(sets,views):
            for X,xv in zip(sets,views):
                out,c=merge(bv,xv)
                assert out==view(U,B|X)
                assert c<=1+2*mixed(xv)
                for q in W:
                    bs,valid=route(U,q)
                    assert (valid and (lookup(bv,bs) or lookup(xv,bs)))==(q in B|X)
                    queries+=1
                cases+=1
print({'merge_cases':cases,'queries':queries})

# Verify streaming cutoff recurrence on every nonuniform support, row and insertion.
checks=0
for n in range(1,4):
    W=words(n)
    for mask in range(1,2**len(W)):
        support={w for i,w in enumerate(W) if mask>>i&1}
        ul=sorted(support)
        for mask_x in range(2**len(ul)):
            X={w for i,w in enumerate(ul) if mask_x>>i&1}
            initial=view(support,X)
            B=1-mixed(initial)
            for w in support:
                U=set(support);local=set(X);R=S=B;frames=[];cutoff=0;depth=0
                while len(U)>1:
                    pos,L,T=split(U)
                    old=view(U,local)
                    direction=int(w[pos]);sib=L if direction else T
                    sibling=view(sib,local&sib)
                    m=isinstance(old,tuple);f=sibling==1
                    R += m-1
                    S = R if not f else S+m
                    frames.append((direction,sibling))
                    depth+=1
                    if not f:cutoff=depth
                    U=T if direction else L;local &= U
                output=1
                for direction,sibling in reversed(frames):
                    children=(sibling,output) if direction else (output,sibling)
                    output=children[0] if isinstance(children[0],int) and children[0]==children[1] else children
                assert output==view(support,X|{w})
                assert S==1-mixed(output)
                # Fullness at every view along the changed path equals cutoff exhaustion.
                subtree=output
                for i,(direction,sibling) in enumerate(frames):
                    assert (subtree==1)==(i>=cutoff)
                    if isinstance(subtree,tuple):subtree=subtree[direction]
                assert subtree==1
                checks+=1
print({'streamed_support_insertions':checks})

# Whole ordinary-record semantics; Python containers are finite oracles only.
import random
import re
RIGHT = re.compile(r"\(-01([01]+),\+1([01]+)\);")

def prepare(records, C=1):
    parsed = []
    for record in records:
        match = RIGHT.fullmatch(record)
        if not match:
            return None
        parsed.append(match.groups())
    if not parsed:
        return {}, set(), None
    anchor, first = parsed[0]
    width, alias_width = len(first), len(anchor)
    frozen = False
    support, rows = set(), {}
    for alias, target in parsed:
        if len(alias) != alias_width or len(target) != width:
            return None
        if alias != anchor:
            frozen = True
        if not frozen:
            support.add(target)
        elif target not in support:
            return None
        rows.setdefault(alias, set()).add(target)
    if any(mixed(view(support, row)) > C * alias_width for row in rows.values()):
        return None
    return rows, support, alias_width

def record(v, w):
    return f"(-01{v},+1{w});"

def literal_events(support, q):
    current = set(support)
    events = []
    for i, bit in enumerate(q):
        children = [{w for w in current if len(w) > i and w[i] == b} for b in '01']
        if all(children):
            events.append(int(bit))
        current = children[int(bit)]
    return events, q in current

rng = random.Random(214)
accepted = rejected = source_updates = retained_checks = pin_checks = 0
for trial in range(1200):
    n, ell = rng.randrange(1, 7), rng.randrange(1, 5)
    universe = words(n)
    aliases = words(ell)
    anchor = aliases[0]
    support = set(rng.sample(universe, rng.randrange(1, len(universe) + 1)))
    anchor_words = sorted(support)
    rng.shuffle(anchor_words)
    records = [record(anchor, w) for w in anchor_words]
    tail = []
    for alias in aliases[1:]:
        chosen = rng.sample(sorted(support), rng.randrange(len(support) + 1))
        tail.extend(record(alias, w) for w in chosen)
    rng.shuffle(tail)
    records.extend(tail)
    if tail:
        records.append(record(anchor, anchor_words[0]))
    prepared = prepare(records)
    if prepared is None:
        rejected += 1
        continue
    accepted += 1
    rows, U, ell = prepared
    states = {}
    history = []
    for step in range(20):
        source = format(rng.randrange(4), 'b')
        alias = rng.choice(aliases)
        baseline, pending, literal = states.get(source, (0, 0, frozenset()))
        committed, cost = merge(baseline, pending)
        assert cost <= 1 + 2 * ell
        new_row = rows.get(alias, set())
        states[source] = committed, view(U, new_row), literal | new_row
        history.append(states[source])
        source_updates += 1
        for b, p, expected in (states[source], rng.choice(history)):
            retained_checks += 1
            for q in rng.sample(universe, min(6, len(universe))) + ['0' * (n + 1), '0' * max(0, n - 1)]:
                events, valid = literal_events(U, q)
                actual = valid and (lookup(b, events) or lookup(p, events))
                assert actual == (q in expected)
                pin_checks += 1

# Structural gates, duplicate anchors, budget repair, and off-support pin control.
assert prepare([record('0', '00'), record('1', '00'), record('0', '01')]) is None
assert prepare([record('0', '00'), record('1', '00'), record('0', '00')]) is not None
assert prepare([record('0', '00'), record('11', '00')]) is None
assert prepare([record('0', '00'), record('0', '0')]) is None
assert prepare(['(-010,+100);bad']) is None
assert prepare([]) == ({}, set(), None)
U = set(words(3))
assert mixed(view(U, {'000', '010', '100', '110'})) > 1
assert prepare([record('0', w) for w in sorted(U)] +
               [record('1', w) for w in sorted(U, key=lambda w: w[-1])]) is not None
U = {'000', '111'}
events, valid = literal_events(U, '001')
assert lookup(view(U, {'000'}), events) and not valid
assert view({'00'}, {'00'}) == 1
assert view({'00', '01'}, {'00'}) == (1, 0)

stress = []
for d in range(1, 8):
    L = 2 ** d
    U = {'0' * L + w for w in words(d + 1)}
    X = {'0' * L + '0' * d + b for b in '01'}
    assert mixed(view(U, X)) == d
    for w in X:
        events, valid = literal_events(U, w)
        assert valid and len(events) == d + 1
    stress.append({'stem': L, 'alias_width': d + 1, 'mixed': d})
for D in range(1, 8):
    U = set(words(D + 2))
    X = {w for w in U if w.startswith('0')}
    assert mixed(view(U, X)) == 1
print({'ordinary_accepted': accepted, 'ordinary_rejected': rejected,
       'source_updates': source_updates, 'retained_checks': retained_checks,
       'pin_checks': pin_checks, 'common_stem_family': stress})