Research source · python
check_component_directory.py
tools/research/check_component_directory.py
158 lines. Source is displayed for inspection; it is not executed by this page.
File fingerprint
SHA-256: 584c56a5fe0bc61ed65184e409cfdcfa759d7796e4cdef2c3c70268ec8feeb3c
"""Independent finite oracle for the proposed component-directory diagnostic.
Host sets and integers are mathematical oracles, not a native execution model.
"""
from functools import lru_cache
import json
def mixed(s, x):
return bool(s & x) and bool(s - x)
def trees(s):
if len(s)==1:
yield next(iter(s)); return
a=min(s); rest=sorted(s-{a})
for m in range(1<<len(rest)):
left=frozenset([a]+[v for j,v in enumerate(rest) if m>>j&1])
right=s-left
if not right: continue
for l in trees(left):
for r in trees(right): yield (l,r)
def walk(t,x):
if isinstance(t,int): return frozenset([t]),0,1
ls,lm,lc=walk(t[0],x); rs,rm,rc=walk(t[1],x)
s=ls|rs
# Splice with complementary views stops exactly at monochromatic nodes.
return s,lm+rm+int(mixed(s,x)),(1+lc+rc if mixed(s,x) else 1)
results=[]
for r in (1,2,3):
k=1<<r; universe=frozenset(range(k)); count=0; minsum=10**9; minmax=10**9
rows=[frozenset(b for b in universe if b>>i&1) for i in range(r)]
for t in trees(universe):
vals=[]
for x in rows:
_,m,c=walk(t,x)
assert c==1+2*m
vals.append(m)
assert sum(vals)>=k-1
assert max(vals)>=(k-1+r-1)//r
minsum=min(minsum,sum(vals));minmax=min(minmax,max(vals));count+=1
# Stream births with alternating owners, followed by all coordinate/complement rows.
ell=(2*r+1).bit_length(); supports=[]; rows_by_alias={}
for b in range(k):
owner=b%2
supports.append(frozenset([b]))
rows_by_alias.setdefault(owner,set()).add(b)
for i,x in enumerate(rows):
rows_by_alias[2+2*i]=set(x)
rows_by_alias[3+2*i]=set(universe-x)
assert len(rows_by_alias)<=1<<ell
assert all(not mixed(s,set(x)) for s in supports for x in rows_by_alias.values())
results.append(dict(r=r,k=k,alias_width=ell,unordered_labeled_trees=count,minimum_total_mixed=minsum,minimum_maximum_mixed=minmax))
def produce(records):
frozen=[]; active=None; owner=None; rowsets={}; snapshots=[]; births=0
for alias,target in records:
if active is not None and alias!=owner:
frozen.append(frozenset(active)); active=None; owner=None
matches=[j for j,s in enumerate(frozen) if target in s]
assert len(matches)<=1
if matches:
pass
elif active is not None:
active.add(target)
else:
active={target};owner=alias;births+=1
rowsets.setdefault(alias,set()).add(target)
supports=tuple(frozen)+((frozenset(active),) if active is not None else ())
assert sum(map(len,supports))==len(set().union(*supports))
snapshot=(supports,{a:frozenset(x) for a,x in rowsets.items()})
snapshots.append(snapshot)
if active is not None: frozen.append(frozenset(active))
return frozen,rowsets,snapshots,births
birth_records=retained_checks=schedule_triples=query_checks=0
for r in range(1,7):
k=1<<r; ell=(2*r+1).bit_length(); width=r.bit_length(); stem='0'*17
aliases=[format(a,f'0{ell}b') for a in range(2*r+2)]
names=[stem+format(b,f'0{r}b') for b in range(k)]
records=[(aliases[b%2],names[b]) for b in range(k)]
for i in range(r):
for value in (1,0):
alias=aliases[2+2*i+(1-value)]
records.extend((alias,names[b]) for b in range(k) if ((b>>i)&1)==value)
supports,rs,snapshots,births=produce(records)
assert births==k and len(supports)==k and all(len(s)==1 for s in supports)
assert len(records)==(r+1)*k
assert all(len(a)==ell and len(t)==17+r for a,t in records)
assert sum(9+len(a)+len(t) for a,t in records)==(r+1)*k*(9+ell+17+r)
# Every retained snapshot denotes exactly the incidences that existed then.
replay={}
for record,(old_supports,old_rows) in zip(records,snapshots):
a,t=record;replay.setdefault(a,set()).add(t)
assert old_rows=={a:frozenset(x) for a,x in replay.items()}
assert all(not mixed(s,x) for s in old_supports for x in old_rows.values())
retained_checks+=1
birth_records+=len(records)
universe=frozenset(names)
source_names=[format(i,f'0{width}b') for i in range(r)]
assert len(set(source_names))==r and all(0<len(u)==width for u in source_names)
for i,u in enumerate(source_names):
baseline=frozenset();pending=frozenset()
triple=[aliases[3+2*i],aliases[2+2*i],aliases[0]]
for pos,a in enumerate(triple):
old_base,old_pending=baseline,pending
baseline=baseline|pending; pending=frozenset(rs[a])
if pos==1:
assert not old_base
assert baseline==universe-rs[aliases[2+2*i]]
for q in names+['1'+n for n in names]:
assert (q in baseline or q in pending)==(q in universe)
query_checks+=1
if pos==2:
assert old_base==universe-old_pending
assert baseline==universe
assert 10+len(u)+len(a)==10+width+ell
schedule_triples+=1
# Finite graft identity with genuine partial component rows, including a singleton.
parts=[frozenset([0]),frozenset([1,2]),frozenset([3,4,5])]
all_leaves=frozenset(range(6)); graft_identities=splice_bounds=complement_equalities=0
def graft(t,ts):
return ts[t] if isinstance(t,int) else (graft(t[0],ts),graft(t[1],ts))
def directory_mu(t,x):
if isinstance(t,int): return parts[t],0
a,ma=directory_mu(t[0],x);b,mb=directory_mu(t[1],x)
return a|b,ma+mb+int(mixed(a|b,x))
def leaves(t):
return frozenset([t]) if isinstance(t,int) else leaves(t[0])|leaves(t[1])
def splice_calls(t,b,x):
s=leaves(t);bb=b&s;xx=x&s
if not bb or not xx or bb==s or xx==s: return 1
return 1+splice_calls(t[0],b,x)+splice_calls(t[1],b,x)
from itertools import product
for d in trees(frozenset(range(3))):
for ts in product(*(list(trees(s)) for s in parts)):
g=graft(d,ts)
for mask in range(64):
x=frozenset(i for i in all_leaves if mask>>i&1)
_,mu=directory_mu(d,x)
internal=sum(walk(t,x)[1] for t in ts)
mg=walk(g,x)[1]
assert mg==mu+internal
graft_identities+=1
assert splice_calls(g,all_leaves-x,x)==1+2*mg
complement_equalities+=1
for baseline in range(64):
b=frozenset(i for i in all_leaves if baseline>>i&1)
assert splice_calls(g,b,x)<=1+2*(mu+internal)
splice_bounds+=1
print(json.dumps(dict(status='passed',cases=results,ordinary_records=birth_records,retained_snapshots=retained_checks,source_selection_triples=schedule_triples,pending_query_comparisons=query_checks,graft_mixed_identities=graft_identities,graft_complement_equalities=complement_equalities,graft_splice_upperbounds=splice_bounds),indent=2))