verify_gap_reductions.py

#!/usr/bin/env python3
"""Finite corroboration of Section 2/3 identities, not a decision algorithm.

Run from any directory. JSON goes to stdout. Only Python's standard library
is used. Source nominal pops at zero are interpreted as permitted no-ops;
disabled bottom-pop histories form a subset of the histories checked here.
"""
import json


def optional_step(values, clock_action):
    if clock_action >= 0:
        return {v + clock_action for v in values}
    return values | {v - 1 for v in values if v > 0}


def drain_lengths(height, counter, require_final_zero=True):
    """Enumerate all legal matching-phase lengths, then emit remaining stack."""
    outputs = set()
    h, y = height, counter
    while True:
        if not require_final_zero or y == 0:
            outputs.add(h)
        if h == 0 or y == 0:
            break
        h -= 1
        y -= 1
    return outputs


def audit_histories(max_depth):
    counts = [0] * (max_depth + 1)
    bottom_noops = 0

    def visit(depth, h, H, optional_values, clock_actions, source_increments):
        nonlocal bottom_noops
        counts[depth] += 1
        suffixes = [sum(clock_actions[k:]) for k in range(depth + 1)]
        assert H == max(suffixes)
        assert sum(source_increments) == h
        assert H - h == max(s - h for s in suffixes)
        assert h - H == min(h - s for s in suffixes)
        assert min(optional_values) == H
        outputs = set().union(*(drain_lengths(h, y) for y in optional_values))
        if h >= H:
            assert max(outputs) == h - H
        else:
            assert not outputs
        if depth == max_depth:
            return
        for nominal in (-1, 0, 1):
            h_next = max(0, h + nominal)
            actual = h_next - h
            for c in (-1, 0, 1):
                if nominal == -1 and h == 0:
                    bottom_noops += 1
                    assert actual == 0
                visit(depth + 1, h_next, max(0, H + c),
                      optional_step(optional_values, c),
                      clock_actions + (c,), source_increments + (actual,))

    visit(0, 0, 0, {0}, (), ())
    return {"maximum_history_length": max_depth,
            "histories_by_length": counts,
            "histories_total": sum(counts),
            "empty_pop_edges": bottom_noops}


def main():
    histories = audit_histories(6)
    drain_cases = 0
    for h in range(13):
        for y in range(13):
            expected = {h - y} if y <= h else set()
            assert drain_lengths(h, y) == expected
            drain_cases += 1

    # Deliberately wrong variants must fail on explicit boundary examples.
    n = 4  # matching push/+1: the true source lead is zero.
    wrong_max_cut = max(n - (n - k) for k in range(n + 1))
    assert wrong_max_cut == n
    wrong_drain = drain_lengths(2, 2, require_final_zero=False)
    assert wrong_drain == {0, 1, 2}
    # Clock -1,+1 reflects to 1 although its signed sum is zero.
    H = 0
    for c in (-1, 1):
        H = max(0, H + c)
    assert H == 1 and abs(sum((-1, 1))) == 0
    # Optional skips may enlarge the counter: not valid for clock-ahead maxima.
    values = {0}
    for c in (1, -1):
        values = optional_step(values, c)
    assert values == {0, 1}

    print(json.dumps({
        "status": "passed",
        "scope": "Finite elementary-reduction audit only; not theorem verification.",
        "history_audit": histories,
        "drain_audit": {"h_and_y_range": [0, 12], "cases": drain_cases},
        "negative_controls": {
            "max_instead_of_min_cut": {"true_gap": 0, "wrong_gap": wrong_max_cut},
            "drain_without_final_counter_zero": {
                "h": 2, "y": 2, "correct_outputs": [0],
                "wrong_outputs": sorted(wrong_drain)},
            "absolute_signed_sum": {"clock_actions": [-1, 1],
                                    "reflected_height": 1, "wrong_height": 0},
            "using_optional_counter_for_clock_ahead": {
                "clock_actions": [1, -1], "reflected_height": 0,
                "optional_values": sorted(values)}},
        "not_implemented": ["PDA-to-CFG or Parikh conversion",
                            "PVASS amalgamation or embedding witnesses",
                            "PVASS reachability or downward closure",
                            "unknown-bound decision or clock synthesis",
                            "persistent compiler"],
        "formal_verification": "none"
    }, indent=2))


if __name__ == "__main__":
    main()