verify_pumping_certificates.py

#!/usr/bin/env python3
"""Finite tests for the scoped pumping-certificate note, not a PEG pumping theorem."""

import itertools
import json
from pathlib import Path

# Each immutable node is (label, ordered ports). Node 0 is the native base.
# -1 denotes a missing endpoint; the last allocated node is the current root.
BASE = (("B", (-1,)),)
ROWS = tuple(itertools.product(("0", "1"), ("missing", "self", 0, 1, 2)))


def follow(graph, node, length):
    for _ in range(length):
        node = -1 if node == -1 else graph[node][1][0]
    return node


def append(graph, row):
    label, address = row
    if address == "missing":
        target = -1
    elif address == "self":
        target = len(graph)
    else:
        target = follow(graph, len(graph) - 1, address)
    return graph + ((label, (target,)),)


def bisimilar(left, right):
    pending = [(len(left) - 1, len(right) - 1)]
    seen = set()
    while pending:
        u, v = pending.pop()
        if (u, v) in seen:
            continue
        seen.add((u, v))
        if u == -1 or v == -1:
            if u != v:
                return False
            continue
        lu, pu = left[u]
        lv, pv = right[v]
        if lu != lv or len(pu) != len(pv):
            return False
        pending.extend(zip(pu, pv))
    return True


def trace(graph, node, depth):
    if node == -1:
        return ("missing",)
    if depth == 0:
        return (graph[node][0],)
    return (graph[node][0], trace(graph, graph[node][1][0], depth - 1))


def native_view(graph, node, depth):
    if depth == 0:
        return "bottom" if node == -1 or node == 0 else graph[node][0]
    if node == -1:
        return "bottom"
    return (graph[node][0], native_view(graph, graph[node][1][0], depth - 1))


def main():
    layer = {BASE}
    graphs = set(layer)
    for _ in range(3):
        layer = {append(graph, row) for graph in layer for row in ROWS}
        graphs.update(layer)
    graphs = sorted(graphs, key=repr)
    pairs = equal_pairs = extension_checks = view_checks = 0
    for left in graphs:
        for right in graphs:
            pairs += 1
            equal = bisimilar(left, right)
            # Independent finite unfolding oracle; this depth exceeds the
            # number of states in the disjoint union, including missing sinks.
            depth = len(left) + len(right) + 2
            assert equal == (trace(left, len(left) - 1, depth)
                             == trace(right, len(right) - 1, depth))
            if equal:
                equal_pairs += 1
                for radius in range(5):
                    assert native_view(left, len(left) - 1, radius) == native_view(
                        right, len(right) - 1, radius)
                    view_checks += 1
                for row in ROWS:
                    assert bisimilar(append(left, row), append(right, row))
                    extension_checks += 1

    # Accept-all archival machine: q is constant and each input stores one
    # new 0-node pointing to the previous root. Distinct cuts never bisimulate.
    archive = [BASE]
    for _ in range(32):
        archive.append(append(archive[-1], ("0", 0)))
    archive_pairs = 0
    for i, left in enumerate(archive):
        for right in archive[i + 1:]:
            assert not bisimilar(left, right)
            archive_pairs += 1

    # Arbitrarily deep equal views need not support the same next answer.
    local_counterexamples = 0
    for radius in range(17):
        left = append(BASE, ("0", "missing"))
        right = append(BASE, ("1", "missing"))
        for _ in range(radius + 1):
            left = append(left, ("0", 0))
            right = append(right, ("0", 0))
        assert native_view(left, len(left) - 1, radius) == native_view(
            right, len(right) - 1, radius)
        assert not bisimilar(left, right)
        # A radius-two cursor copies the label and port of the old successor.
        for _ in range(radius + 1):
            def pop(graph):
                child = graph[-1][1][0]
                return graph + ((graph[child][0], graph[child][1]),)
            left, right = pop(left), pop(right)
        assert left[-1][0] != right[-1][0]
        local_counterexamples += 1

    # A concrete radius-two push/pop controller, initialized by '#': E is
    # represented by an E-labelled self-loop. Balanced 'ab' restores its
    # unfolding although allocation history grows. All states are identical;
    # accepting all words suffices to test all-future graph preservation.
    initial = BASE + (("E", (1,)),)
    def step(graph, letter):
        if letter == "a":
            return graph + (("X", (len(graph) - 1,)),)
        child = graph[-1][1][0]
        return graph + ((graph[child][0], graph[child][1]),)
    def run(graph, word):
        for letter in word:
            graph = step(graph, letter)
        return graph
    pumped = 0
    for repeats in range(9):
        repeated = run(initial, "ab" * repeats)
        assert bisimilar(initial, repeated)
        for length in range(7):
            for word in itertools.product("ab", repeat=length):
                assert bisimilar(run(initial, word), run(repeated, word))
                pumped += 1

    result = {
        "status": "pass",
        "scope": "degree-one legal histories through three appends, two labels, path length at most two",
        "graphs": len(graphs), "ordered_pairs": pairs,
        "bisimilar_pairs": equal_pairs, "common_row_extensions": extension_checks,
        "native_view_comparisons": view_checks,
        "archive_distinct_cut_pairs": archive_pairs,
        "local_view_counterexamples": local_counterexamples,
        "pumped_suffix_comparisons": pumped,
        "does_not_verify": [
            "universal existence of pumping certificates",
            "a pumping lemma for all PEGs",
            "a machine-checked unbounded theorem",
            "finite controller state equality is a separate certificate requirement"
        ]
    }
    output = json.dumps(result, indent=2) + "\n"
    Path(__file__).with_name("checker-output.json").write_text(output)
    print(output, end="")


if __name__ == "__main__":
    main()