check_receipt_repairs.py

#!/usr/bin/env python3
"""Targeted finite audit of the two Draft 2 receipt repairs.

This checks word identities through half-length 10 and an exact unbounded
bridge-chase family. It is corroboration, not a proof of the paper.
"""
from functools import lru_cache
from itertools import product
import json

ALPHABET = '01'


@lru_cache(None)
def even_palindrome(word):
    return len(word) % 2 == 0 and word == word[::-1]


def suffixes(word):
    return sorted((word[i:] for i in range(len(word) + 1)
                   if even_palindrome(word[i:])), key=len, reverse=True)


def suffix_link(palindrome):
    return max((p for p in suffixes(palindrome) if len(p) < len(palindrome)),
               key=len, default='')


def direct(palindrome, letter):
    for candidate in suffixes(palindrome):
        if len(candidate) == len(palindrome):
            continue
        cut = len(palindrome) - len(candidate)
        if palindrome[cut - 1] == letter:
            return candidate, palindrome[:cut - 1][::-1]
    return None


def bridge(palindrome):
    link = suffix_link(palindrome)
    cut = len(palindrome) - len(link)
    return link, palindrome[cut - 1], palindrome[:cut - 1][::-1]


def wrap(anchor, word):
    value = anchor
    for letter in word:
        value = letter + value + letter
    return value


def chase_depth(palindrome, letter):
    depth = 0
    while palindrome:
        link, candidate, _ = bridge(palindrome)
        if candidate == letter:
            return depth
        palindrome = link
        depth += 1
    return depth


def main():
    endpoints = {'direct': 0, 'reset': 0}
    table_entries = table_present = 0
    for half_length in range(11):
        for bits in product(ALPHABET, repeat=half_length):
            half = ''.join(bits)
            palindrome = half + half[::-1]
            for letter in ALPHABET:
                selected = direct(palindrome, letter)
                if selected is None:
                    final = wrap('', letter + palindrome)
                    endpoints['reset'] += 1
                else:
                    interior, word = selected
                    final = wrap(letter + interior + letter, word)
                    endpoints['direct'] += 1
                # Draft 2's separate endpoint fact: the final cell receipt is
                # the source palindrome, including where bridge-shadow's
                # strict proper-suffix induction has reached its boundary.
                assert suffix_link(final) == palindrome

            for outer in ALPHABET:
                fresh = outer + palindrome + outer
                link, bridge_letter, _ = bridge(fresh)
                for letter in ALPHABET:
                    actual = direct(fresh, letter)
                    actual_receipt = None if actual is None else actual[0]
                    inherited = direct(link, letter)
                    inherited_receipt = None if inherited is None else inherited[0]
                    expected = link if letter == bridge_letter else inherited_receipt
                    assert actual_receipt == expected
                    table_entries += 1
                    table_present += int(actual_receipt is not None)

    # The transition receipt remains one stored entry while the equivalent
    # suffix-link/bridge search grows without bound.
    max_depth = 128
    for depth in range(max_depth + 1):
        palindrome = '00' + ('11' + '00') * depth
        assert direct(palindrome, '0')[0] == ''
        assert chase_depth(palindrome, '0') == depth

    print(json.dumps({
        'status': 'pass',
        'mirror_prefix_endpoints': endpoints,
        'transition_table_entries': table_entries,
        'present_transition_receipts': table_present,
        'unbounded_chase_family_through_depth': max_depth,
        'scope': ('Word-level endpoint and transition-receipt recurrences through '
                  'half-length 10, plus an exact chase family; not a sequence '
                  'implementation or full recognizer proof.')
    }, indent=2))


if __name__ == '__main__':
    main()