verify_stack_observer.py

#!/usr/bin/env python3
"""Finite corroboration only; no determinizer, emptiness solver or proof assistant.

The paired update uses a finite cap/buffer and the paired top. An independent
oracle stores the two ordinary stack words and re-encodes the expected state.
Tuple copying here is a testing convenience, not a runtime complexity claim.
"""
import itertools
import json
from pathlib import Path

from verify_bounded_stack_skew import encode, decode, source_step


def words(n):
    for k in range(n + 1):
        yield from itertools.product((0, 1), repeat=k)


def observer_action(top, letter):
    if letter in ("0", "1"):
        return int(letter)
    if letter == "x":
        return 0 if top is None else "pop" if top == 0 else "keep"
    if letter == "z":
        return "keep" if top is None else 1 if top == 0 else "pop"
    if letter == "p":
        return "pop" if top is not None else "keep"
    assert letter == "k"
    return "keep"


def paired_encode(B, reference, source):
    cap, buffer, frames = encode(B, len(reference), source)
    return cap, buffer, tuple(zip(reference, frames))


def paired_decode(state):
    cap, buffer, pairs = state
    return decode((cap, buffer, tuple(frame for _, frame in pairs)))


def paired_step(B, state, reference_action, source_action):
    cap, buffer, pairs = state
    actual_ref = ("keep" if reference_action == "pop" and not pairs
                  else reference_action)
    change_ref = 1 if actual_ref in (0, 1) else -1 if actual_ref == "pop" else 0
    temporary = source_step(buffer, source_action)
    change_source = len(temporary) - len(buffer)
    error = len(buffer) - min(cap, B + 1) + change_source - change_ref
    if abs(error) > B:
        return None
    if change_ref == 1:
        payload = None
        if cap >= B + 1:
            assert len(temporary) >= 2
            payload, temporary = temporary[0], temporary[1:]
        pairs = pairs + ((actual_ref, (cap, payload)),)
        cap = min(cap + 1, B + 2)
    elif change_ref == -1:
        _, (cap, payload) = pairs[-1]
        pairs = pairs[:-1]
        if payload is not None:
            temporary = (payload,) + temporary
    assert len(temporary) <= 2 * B + 1
    return cap, temporary, pairs


def local_pair_audit():
    counts = {"transitions": 0, "inside": 0, "first_exits": 0,
              "bottom_noops": 0}
    # Reference stacks all binary words through height 4, source heights
    # within B, B=0,1,2; six symbol-sensitive reference commands, four P ops.
    for B in range(3):
        for reference in words(4):
            H = len(reference)
            for h in range(max(0, H - B), H + B + 1):
                for source in itertools.product((0, 1), repeat=h):
                    old = paired_encode(B, reference, source)
                    for letter, action in itertools.product("01xzpk", (0, 1, "pop", "keep")):
                        ra = observer_action(reference[-1] if reference else None, letter)
                        new_ref = source_step(reference, ra)
                        new_source = source_step(source, action)
                        actual = paired_step(B, old, ra, action)
                        violation = abs(len(new_ref) - len(new_source)) > B
                        assert (actual is None) == violation
                        assert old == paired_encode(B, reference, source)
                        counts["transitions"] += 1
                        counts["bottom_noops"] += int(letter == "p" and not reference)
                        if violation:
                            counts["first_exits"] += 1
                        else:
                            counts["inside"] += 1
                            assert actual == paired_encode(B, new_ref, new_source)
                            assert paired_decode(actual) == new_source
                            assert tuple(symbol for symbol, _ in actual[2]) == new_ref
    return counts


def valley_operation(phase, stack, letter):
    if letter == "a":
        if phase != "build":
            return None
        return "build", 0
    assert letter == "b"
    if phase == "grow" or not stack:
        return "grow", 0
    return "fall", "pop"


def delayed_valley_audit():
    checks = runs = 0
    zero_failure = None
    for n in range(7):
        for m in range(7):
            operations = "a" * n + "b" * m
            for delays in itertools.product((False, True), repeat=len(operations)):
                reference = source = ()
                ref_phase = src_phase = "build"
                paired = paired_encode(1, reference, source)
                for letter, delay in zip(operations, delays):
                    next_ref_phase, ra = valley_operation(ref_phase, reference, letter)
                    next_src_phase, sa = valley_operation(src_phase, source, letter)
                    assert ra == sa and next_ref_phase == next_src_phase
                    for ref_action, src_action in ((ra, "keep" if delay else sa),
                                                   ("keep", sa if delay else "keep")):
                        reference = source_step(reference, ref_action)
                        source = source_step(source, src_action)
                        paired = paired_step(1, paired, ref_action, src_action)
                        assert paired is not None
                        assert paired == paired_encode(1, reference, source)
                        assert paired_decode(paired) == source
                        assert abs(len(reference) - len(source)) <= 1
                        if zero_failure is None and abs(len(reference) - len(source)):
                            zero_failure = {"prefix": "a", "choice": "delay first push",
                                            "reference_height": 1, "source_height": 0}
                            assert paired_step(0, paired_encode(0, (), ()), 0, "keep") is None
                        checks += 1
                    ref_phase, src_phase = next_ref_phase, next_src_phase
                    assert source == reference
                assert len(source) == abs(n - m)
                assert (not source) == (n == m)
                runs += 1
    return {"n_and_m": [0, 6], "runs_with_all_early_late_choices": runs,
            "prefix_updates": checks, "B1_passed": True, "B0_witness": zero_failure}


def spread_audit():
    maximum_diameter = maximum_radius = 0
    for length in range(9):
        heights = set(range(min(length, 2) + 1))
        selected = 0 if length == 0 else 1
        radius = max(abs(h - selected) for h in heights)
        diameter = max(heights) - min(heights)
        assert radius <= diameter <= 2 * radius
        maximum_diameter = max(maximum_diameter, diameter)
        maximum_radius = max(maximum_radius, radius)
    assert (maximum_radius, maximum_diameter) == (1, 2)
    # Complete all-rejecting unary source with push/keep on every letter.
    for length in range(13):
        heights = {0}
        for _ in range(length):
            heights |= {h + 1 for h in heights}
        assert heights == set(range(length + 1))
    return {"sharp_factor_two_lengths": [0, 8], "radius": 1, "diameter": 2,
            "unbounded_family_checked_lengths": [0, 12],
            "unboundedness_status": "induction in the note, not established by this finite check"}


def view(stack, depth):
    top_first = stack[::-1]
    return top_first[:depth] + (None,) * max(0, depth - len(stack))


def metric_audit():
    stacks = list(words(5))
    comparisons = updates = 0
    for x, y in itertools.product(stacks, repeat=2):
        for letter in "01xzpk":
            fx = source_step(x, observer_action(x[-1] if x else None, letter))
            fy = source_step(y, observer_action(y[-1] if y else None, letter))
            for m in range(7):
                if view(x, m + 1) == view(y, m + 1):
                    assert view(fx, m) == view(fy, m)
                    updates += 1
        # Bit complement preserves first differing padded position exactly.
        cx, cy = tuple(1 - b for b in x), tuple(1 - b for b in y)
        for m in range(7):
            assert (view(x, m) == view(y, m)) == (view(cx, m) == view(cy, m))
            comparisons += 1
    return {"control_states": 1, "binary_stack_max_height": 5,
            "view_depths": [0, 6], "local_modulus_implications": updates,
            "complement_view_comparisons": comparisons}


def main():
    result = {"status": "passed", "scope": "Finite corroboration; no formal verification.",
              "local_pairing": local_pair_audit(), "delayed_valley": delayed_valley_audit(),
              "intrinsic_spread": spread_audit(), "observation_metric": metric_audit(),
              "not_implemented": ["VPA determinization", "pushdown emptiness",
                                  "arbitrary-machine compiler", "scaffold generation",
                                  "proof-assistant verification"]}
    output = Path(__file__).with_name("stack-observer-output.json")
    output.write_text(json.dumps(result, indent=2) + "\n")
    print(json.dumps(result, indent=2))


if __name__ == "__main__":
    main()