verify_residual_allocation.py

#!/usr/bin/env python3
"""Finite addition-DAG exploration. The unbounded bound is proved in the note."""
import hashlib
import json
from pathlib import Path

states = {frozenset({0, 1})}
rows = []
for budget in range(5):
    maximum = max(max(s) for s in states)
    assert maximum == 2**budget
    rows.append({"fresh_Cat_budget": budget, "distinct_available_length_sets": len(states),
                 "maximum_length": maximum})
    # Each new Cat can reference any two old or earlier fresh roots, including
    # the same root twice. Sets identify length-equivalent states only.
    states = {s | {x+y} for s in states for x in s for y in s}

# A concrete persistent heap word model verifies the special input family.
for n in range(17):
    heap = ["", "a", "b"]
    root = "a"
    for _ in range(n):
        root += "b"
        heap.append(root)
    assert root == "a" + "b"*n
    assert max([1] + [len(w) for w in heap if "a" not in w]) == 1

length = 1
for _ in range(3):
    length += length
assert length == 8  # Rejects a proposed linear allocation lower bound.

print(json.dumps({
    "scope": "Finite length-state exploration through four fresh binary concatenations and heap examples n=0..16; not formal verification or an unbounded lower-bound proof.",
    "checker_sha256": hashlib.sha256(Path(__file__).read_bytes()).hexdigest(),
    "addition_DAG_checks": rows,
    "sharing_control": "Three fresh Cat(x,x) nodes represent b^8 from B; linear copying is not necessary.",
    "extra_old_root_control": "An old b^n raises M to at least n and permits zero-allocation return.",
}, indent=2))