verify_horn_reassociation.py

#!/usr/bin/env python3
"""Finite semantic and event checks; not a pointer-machine implementation."""
import itertools,json
from verify_horn_join import Solver,leaf,join,pin,check,snapshot

def rotate(h):
    t,s=h
    assert not s.failed and s.engine is None and s.left.engine is None
    ab,c=s.left,s.right
    assert ab.z==c.z==s.z==ab.left.z==ab.right.z
    bc=Solver(s.z,left=ab.right,right=c)
    return t,Solver(s.z,left=ab.left,right=bc)

def count(s):
    return 0 if s.engine is not None else 1+count(s.left)+count(s.right)

def main():
    programs=[[],[((),0)],[((0,),1)],[((1,),0)],[((0,),None)],[((0,),2),((2,),1)]]
    rotations=extensions=0
    for ps in itertools.product(programs,repeat=3):
        a,b,c=map(leaf,ps)
        ab,_=join(a,b); h,_=join(ab,c)
        if h[1].failed: continue
        old=snapshot(h[1]); r=rotate(h);check(r)
        assert r[0] is h[0] and r[1].left is h[1].left.left
        rotations+=1
        for q in [(),(0,),(1,),(0,1)]:
            x,ex=pin(h,q);y,ey=pin(r,q)
            assert check(x)==check(y)
            if not x[1].failed:
                delta=len(x[1].z-h[1].z)
                assert ex.D==ey.D==count(h[1])*delta
            assert snapshot(h[1])==old
            extensions+=1
    rows=[]
    def tree(n,balanced):
        if n==1:return leaf([])
        k=n//2 if balanced else n-1
        return join(tree(k,balanced),tree(n-k,balanced))[0]
    for n in [2,3,4,8,16,32]:
        for balanced in [False,True]:
            h=tree(n,balanced);r,e=pin(h,(0,1))
            assert e.D==2*(n-1) and e.A==2*n
            rows.append(dict(leaves=n,balanced=balanced,D=e.D,A=e.A))
    # A's fact must not become an unconditional fact of the newly grouped BC.
    a=leaf([((),0)]);b=leaf([((0,),1)]);c=leaf([])
    ab,_=join(a,b);h,_=join(ab,c);r=rotate(h)
    bc,_=join(b,c)
    assert r[1].right.z==frozenset((0,1)) and bc[1].z==frozenset()
    print(json.dumps(dict(rotations=rotations,future_extensions=extensions,
        shape_comparisons=rows,conditional_export_negative_control=True,
        scope='Finite two-boundary-variable semantic checks; written general proof; no proof assistant or pointer-cost verification.'),indent=2))
if __name__=='__main__':main()