check_final_one_profile.py

"""Finite semantic audit of global rectangle reuse; no native timing claim."""
from dataclasses import dataclass
from itertools import product
import json
from check_rectangle_deficit import Token, extend, debit, count, frame_count
from check_frozen_row_composition import B, insert, lookup

@dataclass(frozen=True)
class State:
    names: object = B
    targets: object = B
    pairs: object = B
    nv: object = None
    nt: object = None
    debt: object = None

def add(s,v,w):
    row=lookup(s.pairs,v) or B
    fresh_v=not bool(lookup(s.names,v))
    fresh_w=not bool(lookup(s.targets,w))
    fresh_pair=not bool(lookup(row,w))
    nv,nt,debt=s.nv,s.nt,s.debt
    if fresh_v:
        debt=extend(debt,nt); nv=Token(nv)
    if fresh_w:
        debt=extend(debt,nv); nt=Token(nt)
    if fresh_pair: debt=debit(debt)
    return State(insert(s.names,v,True),insert(s.targets,w,True),
                 insert(s.pairs,v,insert(row,w,True)),nv,nt,debt)

def inspect(s,edges):
    vs={v for v,w in edges}; ws={w for v,w in edges}
    assert count(s.nv)==len(vs) and count(s.nt)==len(ws)
    assert frame_count(s.debt)==len(vs)*len(ws)-len(edges)
    rows={frozenset(w for x,w in edges if x==v) for v in vs}
    assert (s.debt is None)==(len(rows)<=1)

counts=dict(sequences=0,prefixes=0,snapshots=0,answers=0,radial_prefixes=0)
universe=list(product(('0','01'),('1','10')))
for length in range(7):
    for seq in product(universe,repeat=length):
        s=State(); es=set(); history=[]
        for v,w in seq:
            history.append((s,frozenset(es)));s=add(s,v,w);es.add((v,w))
            inspect(s,es);counts['prefixes']+=1
        for old,oldes in history:
            inspect(old,oldes);counts['snapshots']+=1
        counts['sequences']+=1
# Exhaust all 3-by-3 relations, all left subsets, plus absent and prefix names.
vs=('0','00','1');ws=('0','01','1');pairs=list(product(vs,ws))
for mask in range(1<<len(pairs)):
    es={e for j,e in enumerate(pairs) if mask>>j&1};s=State()
    for e in sorted(es):s=add(s,*e)
    inspect(s,es)
    for lm in range(16):
        selected={v for j,v in enumerate(vs+('001',)) if lm>>j&1}
        flag=any(lookup(s.names,v) for v in selected)
        for b in ws+('001',):
            candidate=bool(flag and lookup(s.targets,b))
            actual=any((v,b) in es for v in selected)
            # The checked language rejects invalid right blocks irrespective of pins.
            assert ((s.debt is None) and not candidate)==((len({frozenset(w for x,w in es if x==v) for v in {x for x,w in es}})<=1) and not actual)
            counts['answers']+=1
# Unbounded-prefix-diversity family (finite samples), then common final levels.
for m in range(1,7):
    s=State();es=set();names=['0'*(j+1)+'1' for j in range(m)]
    for j,v in enumerate(names):
        w='0'*(j+1);s=add(s,v,w);es.add((v,w));inspect(s,es);counts['radial_prefixes']+=1
    profiles={frozenset(len(w) for x,w in es if x==v) for v in names}
    assert len(profiles)==m
    for v in names:
        for n in range(1,m+1):
            for bs in product('01',repeat=n):
                w=''.join(bs);s=add(s,v,w);es.add((v,w));inspect(s,es);counts['radial_prefixes']+=1
    assert s.debt is None
# Arbitrarily unequal names and direct short final query; duplicates preserve debt.
s=State();es=set()
for e in [('0'*257,'1'),('0'*257,'00'),('1','1'),('1','1'),('1','00')]:
    s=add(s,*e);es.add(e);inspect(s,es)
assert s.debt is None
# Labeled marginal counts do not decide two-profile membership.
a=((0,0,0,1),(0,0,0,1),(1,1,1,0))
b=((0,0,0,1),(0,0,1,0),(1,1,0,1))
def marg(x):return tuple(map(sum,x)),tuple(map(sum,zip(*x)))
assert marg(a)==marg(b) and len(set(a))==2 and len(set(b))==3
counts['marginal_collision']=1
# Exact rational Gram determinant versus independent cardinality diversity.
from fractions import Fraction

def determinant(a):
    a=[[Fraction(x) for x in row] for row in a]; out=Fraction(1)
    for i in range(len(a)):
        pivot=next((j for j in range(i,len(a)) if a[j][i]),None)
        if pivot is None:return 0
        if pivot!=i:a[i],a[pivot]=a[pivot],a[i];out=-out
        q=a[i][i];out*=q
        for j in range(i+1,len(a)):
            z=a[j][i]/q
            for l in range(i+1,len(a)):a[j][l]-=z*a[i][l]
    return out
counts['moment_cases']=0
for length in range(5):
    for cs in product(range(1,7),repeat=length):
        for k in (1,2,3):
            moments=[sum(c**j for c in cs) for j in range(2*k+1)]
            det=determinant([[moments[i+j] for j in range(k+1)] for i in range(k+1)])
            assert (det==0)==(len(set(cs))<=k) and det>=0
            counts['moment_cases']+=1
# Complete levels uniquely encode their occupied-length set in literal size.
sizes={sum(2**n for n in range(1,7) if mask>>(n-1)&1):mask for mask in range(64)}
assert len(sizes)==64
counts['radial_cardinality_encodings']=64
counts['native_timing_evidence']=False
print(json.dumps(counts,sort_keys=True))