verify_stored_word_richness.py

#!/usr/bin/env python3
"""Finite constructive model and source provenance; no Rocq verification."""
import hashlib,json,argparse
from pathlib import Path
from itertools import product

def make(w,n):
    assert n>=1 and len(w)>=3**n
    if n==1:return ('Small',tuple(('Ground',c) for c in w))
    k=3**(n-1)
    return ('Small',(make(w[:k],n-1),make(w[k:2*k],n-1),make(w[2*k:],n-1)))
def check(t):
    if t[0]=='Ground':return 0,t[1]
    xs=[check(x) for x in t[1]]
    assert len(xs)>=3 and len({n for n,w in xs})==1
    return xs[0][0]+1,''.join(w for n,w in xs)
count=0
for N in range(3,11):
    for letters in product('ab',repeat=N):
        w=''.join(letters)
        for n in (1,2):
            if N>=3**n:
                assert check(make(w,n))==(n,w);count+=1
for n in (3,4):
    for extra in range(4):
        N=3**n+extra;w=('ab'*(N//2+1))[:N]
        assert check(make(w,n))==(n,w);count+=1
L=4;levels=(1,2);codes={}
for i,(v,n) in enumerate(zip(('X','Y'),levels),1):
    N=max(3**n,L+5)
    codes[v]='b'+'a'*(L+i+1)+'b'*(N-L-i-2)
    assert check(make(codes[v],n))==(n,codes[v])
words=[w for k in range(L+1) for w in product(('a','b','X','Y'),repeat=k)]
assert len({''.join(codes.get(c,c) for c in w) for w in words})==len(words)
# Equality-restricted variables cannot separate even arbitrarily long samples.
for N in range(1,30):
    x='a'*N; y=x;assert x==y
expected={
 'theory/Cadeque/Types.v':'4beb995bd9634c6cc275aa053e009065a7ff699e2ad7b04fd2821df97bcd9e23',
 'theory/Cadeque/Models.v':'d19612a21f4e506aedb31657393c437a07d1f2f8e5ed4ebcea4e408d6b05402f',
 'theory/Deque/Deque.v':'5ff4fd4122c4372d2b1abd5f18e039e5e80d3b12c94887b56d24b1ed233d60bb'}
p=argparse.ArgumentParser();p.add_argument('--source',type=Path);args=p.parse_args()
if args.source:
    for path,h in expected.items():assert hashlib.sha256((args.source/path).read_bytes()).hexdigest()==h
print(json.dumps({'scope':'Handwritten Small-only tree model on all binary words of lengths 3..10 at eligible levels 1,2, plus eight words at levels 3,4; all formal expressions through length 4 over a,b,X,Y separated inside levels 1,2. The equality control is a direct model assertion. Polymorphic Empty is checked by source inspection, not a runtime test. Source hashes pin inspected statements; no Rocq build or unrestricted proof verification.', 'constructed_cases':count,'separated_expressions':len(words),'source_commit':'503c5d3ff7f9a20bad1cd7a8f8d7abf4e635d3a0','source_hashes':expected},indent=2))