check_transfer_composition.py

#!/usr/bin/env python3
"""Finite audit for Run 09's timing, reversal, and empty-word interfaces.

The exhaustive families are deliberately small.  They test the operational
interfaces and boundary cases; the universal statements are supplied by the
Lean theorems and the mathematical composition argument in run-09.md.
"""

from __future__ import annotations

import itertools
import json
from pathlib import Path


ROOT = Path(__file__).resolve().parents[3]
LEAN = ROOT / "public/formal/persistent-stacks/lean/FPRDTransfer"
TRANSFER_HTML = ROOT / (
    "public/research-artifacts/scaffold-proof-review/history/objects/"
    "0ced5ddcec85f089dd004170f8c335a6b5fb7819009388ea7869b8a6cc2e7515.txt"
)

MOVES = (-1, 0, 1)
WORDS = [word for n in range(6) for word in itertools.product((0, 1), repeat=n)]
OFFSETS = range(-7, 8)


def direct_step(tape, head, write, move):
    tape = dict(tape)
    tape[head] = write
    return tape, head + move


def zipper_step(left, cur, right, write, move, blank=0):
    left, right = list(left), list(right)
    if move == 1:
        return [write, *left], (right[0] if right else blank), right[1:]
    if move == -1:
        return left[1:], (left[0] if left else blank), [write, *right]
    return left, write, right


def zipper_get(left, cur, right, offset, blank=0):
    if offset == 0:
        return cur
    side = right if offset > 0 else left
    index = abs(offset) - 1
    return side[index] if index < len(side) else blank


def all_tables(domain, outputs):
    for values in itertools.product(outputs, repeat=len(domain)):
        yield dict(zip(domain, values))


def source_markers():
    realtime = (LEAN / "RealtimeTransfer.lean").read_text()
    main = (LEAN / "Theorem16/Main.lean").read_text()
    normalize = (LEAN / "Theorem16/Normalize.lean").read_text()
    corollaries = (LEAN / "Theorem16/Corollaries.lean").read_text()
    html = TRANSFER_HTML.read_text()
    return {
        "machine_run_is_one_fold_step_per_letter":
            "w.foldl N.stepConfig N.initConfig" in realtime,
        "machine_to_scaffold_decision_equality":
            "theorem realtime_transfer_decides" in realtime,
        "machine_to_scaffold_tape_equality":
            "theorem realtime_transfer_tape_contents" in realtime,
        "compiled_automaton_is_distance_ok":
            "theorem realtime_transfer_wellFormed" in realtime,
        "scaffold_to_peg_reverses_once":
            "InPEG (fun word => A.decides word.reverse = true)" in main,
        "normalization_preserves_empty_and_nonempty_words":
            "theorem normalize_decides" in normalize
            and "including the empty word" in normalize,
        "transfer_corollary_has_one_reverse":
            "theorem revRT_multitape_subset_PEG" in corollaries
            and "machine.decides word.reverse = true" in corollaries,
        "epal_corollary_is_conditional_on_recognizer":
            "theorem epal₂_inPEG_of_multitape_recognizer" in corollaries
            and "hmachine" in corollaries,
        "paper_excludes_advice_and_post_input_work":
            "has no input-length advice, and performs no post-input computation" in html,
        "paper_marks_palindrome_interface_imported":
            "Classical palindrome interface (classical, imported)" in html,
    }


def audit_control_and_orientation():
    domain = tuple(itertools.product((0, 1), (0, 1)))
    outputs = tuple(itertools.product((0, 1), MOVES))
    executions = steps = empty_checks = normalization_checks = orientation_checks = 0

    for table in all_tables(domain, outputs):
        for accept_mask in range(4):
            accepts = lambda q, mask=accept_mask: bool(mask & (1 << q))
            for word in WORDS:
                q = 0
                tape, head = {}, 0
                left, cur, right = [], 0, []
                normalized = None

                if not word:
                    empty_checks += 1
                    assert accepts(q) == accepts(0)
                    assert normalized is None

                for symbol in word:
                    q_next, move = table[(q, symbol)]
                    tape, head = direct_step(tape, head, 0, move)
                    left, cur, right = zipper_step(left, cur, right, 0, move)
                    q = q_next
                    normalized = q_next
                    steps += 1
                    assert all(tape.get(head + z, 0) == zipper_get(left, cur, right, z)
                               for z in OFFSETS)

                machine_answer = accepts(q)
                stack_answer = accepts(q)
                normalized_answer = accepts(0) if normalized is None else accepts(normalized)
                peg_on_reverse = stack_answer
                assert machine_answer == stack_answer == normalized_answer == peg_on_reverse
                executions += 1
                normalization_checks += 1
                orientation_checks += 1

    return {
        "machine_tables": 6 ** 4,
        "acceptance_sets_per_table": 4,
        "words_per_machine": len(WORDS),
        "executions": executions,
        "letter_steps": steps,
        "empty_word_checks": empty_checks,
        "fresh_initial_normalization_checks": normalization_checks,
        "single_reversal_checks": orientation_checks,
    }


def audit_tape_zipper():
    domain = tuple(itertools.product((0, 1), (0, 1)))
    outputs = tuple(itertools.product((0, 1), MOVES))
    executions = steps = offset_checks = stack_actions = 0

    for table in all_tables(domain, outputs):
        for word in WORDS:
            tape, head = {}, 0
            left, cur, right = [], 0, []
            for symbol in word:
                write, move = table[(symbol, tape.get(head, 0))]
                tape, head = direct_step(tape, head, write, move)
                left, cur, right = zipper_step(left, cur, right, write, move)
                steps += 1
                stack_actions += 2
                for offset in OFFSETS:
                    assert tape.get(head + offset, 0) == zipper_get(
                        left, cur, right, offset
                    )
                    offset_checks += 1
            executions += 1

    return {
        "machine_tables": 6 ** 4,
        "words_per_machine": len(WORDS),
        "executions": executions,
        "letter_steps": steps,
        "stack_actions": stack_actions,
        "tape_offset_checks": offset_checks,
        "offset_window": [min(OFFSETS), max(OFFSETS)],
    }


def main():
    markers = source_markers()
    assert all(markers.values()), markers
    result = {
        "status": "pass",
        "scope": (
            "Exhaustive small-machine interface checks and exact source markers; "
            "the universal result is proved by the cited Lean theorems and Run 09."
        ),
        "proved_composition": {
            "machine_to_scaffold_is_letter_synchronous": True,
            "machine_to_scaffold_preserves_language_without_reversal": True,
            "scaffold_to_peg_introduces_exactly_one_reversal": True,
            "empty_word_is_preserved_at_every_layer": True,
            "compiler_does_not_strictify_a_slower_source_machine": True,
            "palindrome_strict_realtime_recognizer_remains_an_imported_premise": True,
        },
        "control_orientation_family": audit_control_and_orientation(),
        "tape_zipper_family": audit_tape_zipper(),
        "source_markers": markers,
    }
    print(json.dumps(result, indent=2, sort_keys=True))


if __name__ == "__main__":
    main()