check_group_degree_boundary.py

#!/usr/bin/env python3
"""Finite checks of the charged binary Horn/OMv encoding and join control.
No conjecture, asymptotic lower bound, native machine, or timing claim is tested.
"""
from itertools import product
from collections import Counter
import json, random, re

RIGHT=re.compile(r'\(-01([01]+),\+1([01]+)\);')
LEFT=re.compile(r'\(-00([01]+),\+01([01]+)\);')
PINS=re.compile(r'\(\+00([01]+)\);\(-1([01]+)\);')


def names(n):
    length=max(1,(n-1).bit_length())
    return [format(i,f'0{length}b') for i in range(n)]


def encode_matrix(matrix,rng):
    ns=names(len(matrix))
    edges=[(ns[j],ns[i]) for i,row in enumerate(matrix) for j,x in enumerate(row) if x]
    rng.shuffle(edges)
    return ''.join(f'(-01{v},+1{w});' for v,w in edges),edges


def vector_records(vector,ns):
    return ''.join(f'(-000,+01{v});' for v,x in zip(ns,vector) if x)


def parse(word):
    at=0;right=[];left=[]
    while (m:=RIGHT.match(word,at)):
        right.append(m.groups());at=m.end()
    while (m:=LEFT.match(word,at)):
        left.append(m.groups());at=m.end()
    m=PINS.fullmatch(word,at)
    assert m is not None,word
    return right,left,m.groups()


def horn_sat(word):
    # Generic Horn forward propagation on literal variable names, independent of Mv.
    right,left,(a,b)=parse(word)
    implications=[('01'+v,'1'+w) for v,w in right]+[('00'+u,'01'+v) for u,v in left]
    true={'00'+a}
    while True:
        enlarged=true|{y for x,y in implications if x in true}
        if enlarged==true:break
        true=enlarged
    return '1'+b not in true


def audit(matrix,rng,stats):
    n=len(matrix);ns=names(n);length=len(ns[0]);prefix,edges=encode_matrix(matrix,rng)
    assert len(prefix)==len(edges)*(9+2*length)
    local={}
    for v,w in edges:
        assert len(v)==len(w)==length
        # Identity normalization: one actual target in each key, independent of its set.
        local.setdefault(w,{}).setdefault(w,set()).add(v)
        assert all(len({frozenset(p) for p in group.values()})==1 for group in local.values())
        stats['prefix_gates']+=1
    assert len(edges)==len(set(edges))
    for vector in product((0,1),repeat=n):
        continuation=vector_records(vector,ns)
        assert len(continuation)==sum(vector)*(11+length)
        branch=prefix+continuation
        for i,w in enumerate(ns):
            suffix=f'(+000);(-1{w});'
            assert len(suffix)==12+length
            bit=any(x and y for x,y in zip(matrix[i],vector))
            assert horn_sat(branch+suffix)==(not bit)
            stats['horn_product_comparisons']+=1
        assert branch==prefix+continuation # original prepared prefix is reused unchanged
        stats['vector_branches']+=1
    stats['matrices']+=1


def independent_join(stats):
    # One actual target, one key, normalized right degree one, equal-length row names.
    for h in range(1,7):
        ns=names(h);w='0'*len(ns[0]);subsets=list(range(1<<h))
        for x,y in product(subsets,repeat=2):
            right=''.join(f'(-01{v},+1{w});' for j,v in enumerate(ns) if x>>j&1)
            left=''.join(f'(-000,+01{v});' for j,v in enumerate(ns) if y>>j&1)
            assert horn_sat(right+left+f'(+000);(-1{w});')==((x&y)==0)
            stats['independent_join_instances']+=1
        full=(1<<h)-1
        for x in subsets:
            assert x&(full^x)==0
            for y in subsets:
                if x!=y:
                    assert (x&(full^y)) or (y&(full^x))
                    stats['fooling_pair_cross_checks']+=1
    # An unbounded-degree positive control with only one global predecessor type.
    for h in range(2,16):
        ns=names(h);matrix=[[1]*h for _ in range(h)]
        edges=[(v,w) for v in ns for w in ns]
        assert max(sum(x==v for x,w in edges) for v in ns)==h
        # Row sweeps have at most two global column types at every prefix.
        cols={}
        for v,w in edges:
            cols.setdefault(w,set()).add(v)
            assert len({frozenset(p) for p in cols.values()})<=2
        stats['unbounded_degree_positive_controls']+=1


def nested_routes(stats):
    from check_stable_row_palettes import State, step
    from check_frozen_row_composition import B, lookup, insert
    # Persistent nested tries provide selectors without a fixed-width key tuple.
    key=lambda w:w.split('11',1)[1]
    for groups in range(1,13):
        model=State({}, {}, {});D=Z=T=B;edges=set();saved=[]
        for row in ['0','10','11111111111111111']:
            for j in range(groups):
                z=format(j,'04b')
                for tag in ['00','0000','000000']:
                    w=tag+'11'+z
                    inner=lookup(D,row);inner=B if inner is None else inner
                    old_label=lookup(inner,z);old_header=lookup(Z,z)
                    if old_label is not None:
                        assert old_header.values[old_label-1]==model.headers[z].values[model.rows[row][z]]
                    new=step(model,row,w,z,2,groups,Counter());assert new is not None
                    inner=insert(inner,z,new.rows[row][z]+1)
                    D=insert(D,row,inner);Z=insert(Z,z,new.headers[z]);T=insert(T,w,new.targets[w]+1)
                    model=new;edges.add((row,w))
                    if len(saved)<3:saved.append((D,Z,T,edges.copy()))
                    stats['nested_route_updates']+=1
        for d,zs,ts,es in saved+[(D,Z,T,edges)]:
            for v in ['0','10','11111111111111111','absent']:
                for w in list({w for v,w in edges})+['001111111']:
                    z=key(w);inner=lookup(d,v)
                    label=None if inner is None else lookup(inner,z)
                    header=lookup(zs,z);target=lookup(ts,w)
                    got=label is not None and header is not None and target is not None and bool(header.values[label-1]>>(target-1)&1)
                    assert got==((v,w) in es)
                    stats['nested_incidence_queries']+=1
            stats['nested_snapshots']+=1


def main():
    stats=Counter();rng=random.Random(146)
    for n in (1,2,3):
        for bits in product((0,1),repeat=n*n):
            audit([bits[i*n:(i+1)*n] for i in range(n)],rng,stats)
    for _ in range(50):
        n=5;audit([[rng.randrange(2) for _ in range(n)] for _ in range(n)],rng,stats)
    independent_join(stats)
    nested_routes(stats)
    print(json.dumps({'checks':dict(sorted(stats.items())),
          'native_recognizer_implemented':False,'OMv_conjecture_tested':False,
          'timing_evidence':False},indent=2))

if __name__=='__main__':main()