verify_visible_checkpoint_erasure.py

#!/usr/bin/env python3
"""Finite tests of bounded hidden blocks and saved caller restoration.

All words through a specified depth and all requests at those words are checked.
This is not proof-assistant verification or exhaustive infinite-state checking.
"""
from collections import deque
from dataclasses import dataclass
from pathlib import Path
import json


@dataclass
class Machine:
    alphabet: str
    hidden: str
    start: object
    delta: dict
    output: dict

    def run(self, word, start=None):
        q = self.start if start is None else start
        for g in word:
            if (q, g) not in self.delta:
                return None
            q = self.delta[q, g]
        return q


def gap_bound(m):
    seen, queue = {m.start}, deque([m.start])
    while queue:
        q = queue.popleft()
        for g in m.alphabet:
            r = m.delta.get((q, g))
            if r is not None and r not in seen:
                seen.add(r)
                queue.append(r)
    color, longest = {}, {}
    def visit(q):
        if color.get(q) == 1:
            raise ValueError('hidden cycle')
        if color.get(q) == 2:
            return longest[q]
        color[q] = 1
        longest[q] = max([0] + [1 + visit(m.delta[q, h])
                               for h in m.hidden if (q, h) in m.delta])
        color[q] = 2
        return longest[q]
    try:
        return max(visit(q) for q in seen)
    except ValueError:
        return None


@dataclass(frozen=True)
class Frame:
    label: str
    saved_p: object
    saved_w: str
    prev: object


@dataclass(frozen=True)
class State:
    p: object
    w: str
    root: object


def step(m, state, op, mutate=False):
    sign, g = op
    p, w, root = state.p, state.w, state.root
    q = m.run(w, p)  # finite table lookup in the implementation
    assert q is not None
    if sign == '+':
        r = m.delta.get((q, g))
        if r is None:
            return None
        if g in m.hidden:
            return State(p, w + g, root), 0
        return State(r, '', Frame(g, p, w, root)), 1
    if g in m.hidden:
        if not w.endswith(g):
            return None
        return State(p, w[:-1], root), 0
    if w or root is None or root.label != g:
        return None
    return State(root.saved_p, '' if mutate else root.saved_w, root.prev), 0


def encode(m, word):
    state = State(m.start, '', None)
    for g in word:
        result = step(m, state, '+' + g)
        assert result is not None
        state = result[0]
    return state


def decode(state):
    pieces = [state.w]
    frame = state.root
    while frame is not None:
        pieces.append(frame.label)
        pieces.append(frame.saved_w)
        frame = frame.prev
    return ''.join(reversed(pieces))


def raw_step(m, word, op):
    sign, g = op
    if sign == '+':
        return word + g if m.run(word + g) is not None else None
    return word[:-1] if word.endswith(g) else None


def bounded_two():
    delta, output = {}, {}
    for length in range(3):
        for parity in range(2):
            q = (length, parity)
            output[q] = parity
            delta[q, 'A'] = (0, parity)
            if length < 2:
                delta[q, 'X'] = (length + 1, 1 - parity)
                delta[q, 'Y'] = (length + 1, parity)
    return Machine('AXY', 'XY', (0, 0), delta, output)


def alternating():
    delta, output = {}, {}
    for phase in range(2):
        for parity in range(2):
            q = (phase, parity)
            output[q] = parity
            if phase == 0:
                delta[q, 'A'] = (1, parity)
            else:
                delta[q, 'X'] = (0, 1 - parity)
    return Machine('AX', 'X', (0, 0), delta, output)


def finite_hidden():
    return Machine('XY', 'XY', 0,
                   {(n, h): n + 1 for n in range(3) for h in 'XY'},
                   {n: n % 2 for n in range(4)})


def evidence(name, m, depth, expected):
    assert gap_bound(m) == expected
    words, queue = [''], deque([''])
    while queue:
        w = queue.popleft()
        if len(w) == depth:
            continue
        for g in m.alphabet:
            if m.run(w + g) is not None:
                words.append(w + g)
                queue.append(w + g)
    operations = enabled = disabled = visible_restorations = 0
    for word in words:
        state = encode(m, word)
        assert decode(state) == word
        assert m.output[m.run(state.w, state.p)] == m.output[m.run(word)]
        for sign in '+-':
            for g in m.alphabet:
                op = sign + g
                expected_word = raw_step(m, word, op)
                actual = step(m, state, op)
                assert (actual is None) == (expected_word is None)
                operations += 1
                if actual is None:
                    disabled += 1
                    continue
                enabled += 1
                target, allocations = actual
                assert target == encode(m, expected_word)
                assert decode(target) == expected_word
                assert allocations == int(sign == '+' and g not in m.hidden)
                if g in m.hidden:
                    assert target.root is state.root
                if sign == '-' and g not in m.hidden:
                    visible_restorations += 1
                    assert target.root is state.root.prev
                if sign == '+':
                    back = step(m, target, '-' + g)
                    assert back is not None and back[0] == state
    return {'case': name, 'exact_hidden_bound': expected,
            'enumerated_word_depth': depth, 'legal_words_checked': len(words),
            'request_cases': operations, 'enabled': enabled, 'disabled': disabled,
            'visible_restorations': visible_restorations,
            'scope': 'All legal words through this depth; all requests there, including one-step targets beyond depth; canonical restoration and root/allocation invariants.'}


def main():
    positive = [evidence('alternating_with_parity', alternating(), 16, 1),
                evidence('two_hidden_labels_gap_two_with_parity', bounded_two(), 8, 2),
                evidence('no_visible_frames_finite_depth_three', finite_hidden(), 4, 3),
                evidence('all_visible_unbounded',
                         Machine('AB', '', 0, {(0, 'A'): 0, (0, 'B'): 0}, {0: 0}), 8, 0)]
    negatives = [Machine('X', 'X', 0, {(0, 'X'): 0}, {0: 0}),
                 Machine('AX', 'X', 0, {(0, 'A'): 1, (1, 'X'): 1}, {0: 0, 1: 0})]
    assert all(gap_bound(m) is None for m in negatives)
    m = alternating()
    state = encode(m, 'AXA')
    wrong = step(m, state, '-A', mutate=True)[0]
    assert decode(wrong) == 'A' and decode(wrong) != 'AX'
    anchored = negatives[1]
    left = raw_step(anchored, 'AX', '-X')
    right = raw_step(anchored, 'AXXX', '-X')
    assert raw_step(anchored, left, '-A') is not None
    assert raw_step(anchored, right, '-A') is None
    result = {'positive_cases': positive,
              'hidden_cycle_cases_rejected': ['X_star', 'epsilon_union_A_X_star'],
              'checkpoint_mutation': {'source': 'AXA', 'request': '-A',
                                      'expected': 'AX', 'mutant': decode(wrong)},
              'parity_boundary_witness': {'stacks': ['AX', 'AXXX'],
                                         'experiment': ['-X', '-A']},
              'verification_status': 'Finite corroboration only. Written unbounded proof is separate; no proof assistant or general controller synthesis.'}
    Path(__file__).with_name('visible-checkpoint-erasure-output.json').write_text(
        json.dumps(result, indent=2) + '\n')
    print(json.dumps(result, indent=2))


if __name__ == '__main__':
    main()