verify_flat_segment_growth.py

#!/usr/bin/env python3
"""Finite controls for flat-segment capacity; not formal theorem verification."""
import json
from itertools import product

# All sets of available unary lengths with initial lengths 0..h, through k
# new Cons nodes. A new node length is an available length plus one.
chain_cases=0
for h in range(1,5):
    states={frozenset(range(h+1))}
    for k in range(7):
        for state in states:
            assert max(state)<=h+k
            chain_cases+=1
        states={state|{x+1} for state in states for x in state}

witnesses=[]
for s,n in product(range(1,6),range(1,13)):
    # Sharing: s identical output roots, only n newly allocated Cons nodes.
    old=list(range(n+1)); new=list(range(n+1,2*n+1))
    out=[old[-1]+len(new)]*s
    assert sum(out)==2*s*n and len(new)==n
    assert max(out)-max(old)==n
    witnesses.append((s,n))

thresholds=[]
for s,h,A in product(range(1,6),range(1,6),range(5)):
    t=next(t for t in range(1,40) if 2**t>s*(h+A*t))
    assert all(2**u<=s*(h+A*u) for u in range(t))
    thresholds.append({'s':s,'h':h,'A':A,'first_capacity_violation':t})

# Finite word-level descriptor histories. Literal strings stand for proper
# list contents. This does not simulate all heaps or prove allocation bounds.
history_cases=0;overflow_cases=0
for s in range(1,4):
    states={()}
    for depth in range(5):
        nextstates=set(states)
        for d in states:
            w=''.join(d)
            if d:
                tail=d[0][1:]
                p=((tail,)+d[1:]) if tail else d[1:]
                assert ''.join(p)==w[1:]
            else:p=()
            nextstates.add(p)
            for c in 'ab':
                p=((c+d[0],)+d[1:]) if d else (c,)
                assert ''.join(p)==c+w
                nextstates.add(p)
            # Empty, singleton a/b, and retained current descriptor operands.
            for e in ((),('a',),('b',),d):
                if len(d)+len(e)<=s:
                    out=d+e
                    assert ''.join(out)==w+''.join(e)
                    nextstates.add(out)
                else:overflow_cases+=1
            assert len(d)<=s and all(d)
            history_cases+=1
        states=nextstates
print(json.dumps({
    'scope':'Unary available-length enumeration h=1..4 through 6 Cons allocations; sharp sharing witnesses s=1..5,n=1..12; first arithmetic violations s,h=1..5,A=0..4; word-level push/pop/guarded concat states through five rounds for s=1..3. No exhaustive heap/controller search or proof-assistant verification.',
    'chain_states_checked':chain_cases,'sharp_witnesses':len(witnesses),
    'descriptor_states_checked':history_cases,'overflow_controls':overflow_cases,
    'first_violation_examples':[x for x in thresholds if x['h']==1 and x['A']==2],
    'threshold_parameter_cases':len(thresholds)
},indent=2))