#!/usr/bin/env python3
"""Finite corroboration of the buffer invariant, not a theorem prover.

The local implementation receives a capped height, finite buffer and stack
frames. It does not receive the true clock height or decoded source stack.
The independent oracle operates on ordinary source strings and integer heights.
"""
import itertools
import json
from pathlib import Path


def encode(B, H, source):
    C = max(0, H - B - 1)
    core, buffer = source[:C], source[C:]
    frames = []
    for level in range(1, H + 1):
        payload = None if level <= B + 1 else core[level - B - 2]
        frames.append((min(level - 1, B + 2), payload))
    return min(H, B + 2), buffer, tuple(frames)


def decode(state):
    _, buffer, frames = state
    return tuple(payload for _, payload in frames if payload is not None) + buffer


def source_step(source, action):
    if action in (0, 1):
        return source + (action,)
    if action == "pop":
        return source[:-1] if source else source
    assert action == "keep"
    return source


def clock_step(H, letter):
    return H + 1 if letter == "c" else max(0, H - 1) if letter == "r" else H


def local_step(B, state, action, letter):
    t, buffer, frames = state
    old_length = len(buffer)
    tmp = source_step(buffer, action)
    dh = len(tmp) - old_length
    dH = 1 if letter == "c" else -1 if letter == "r" and t else 0
    difference = old_length - min(t, B + 1) + dh - dH
    if abs(difference) > B:
        return None  # first error; the subsequent error sink is not simulated
    if letter == "c":
        if t >= B + 1:
            assert len(tmp) >= 2
            payload, tmp = tmp[0], tmp[1:]
        else:
            payload = None
        frames = frames + ((t, payload),)
        t = min(t + 1, B + 2)
    elif letter == "r" and t:
        t, payload = frames[-1]
        frames = frames[:-1]
        if payload is not None:
            tmp = (payload,) + tmp
    assert len(tmp) <= 2 * B + 1
    return t, tmp, frames


def bounded_configuration_audit():
    cases = valid = exits = 0
    for B in range(3):
        for H in range(B + 5):
            for h in range(max(0, H - B), H + B + 1):
                for s in itertools.product((0, 1), repeat=h):
                    old = encode(B, H, s)
                    assert decode(old) == s
                    assert bool(old[1]) == bool(s)
                    if s:
                        assert old[1][-1] == s[-1]
                    for action, letter in itertools.product(
                        (0, 1, "pop", "keep"), ("c", "r", "i")
                    ):
                        cases += 1
                        oracle_s = source_step(s, action)
                        oracle_H = clock_step(H, letter)
                        violation = abs(len(oracle_s) - oracle_H) > B
                        actual = local_step(B, old, action, letter)
                        assert (actual is None) == violation
                        if violation:
                            exits += 1
                        else:
                            valid += 1
                            assert actual == encode(B, oracle_H, oracle_s)
                            assert decode(actual) == oracle_s
    # No-margin cut at H-B loses the source top for both of these stacks.
    # An internal source transition can distinguish the tops; an internal
    # VPA transition with empty buffer cannot inspect the real stack.
    assert (0,)[:-1] == (1,)[:-1] == ()
    assert (0,)[-1] != (1,)[-1]
    return dict(configured_bounds=[0, 1, 2], clock_range="0 through B+4",
                stack_alphabet=[0, 1], local_cases=cases,
                in_corridor=valid, first_exits=exits,
                no_margin_failure_witness=True)


def choices(q, s, a):
    if q in ("build", "return") and a == "b" and s:
        return (("r-early", "pop"), ("r-late", "keep"))
    if q == "build" and a == "a":
        return (("b-early", 0), ("b-late", "keep"))
    if a == "c" and q in ("b-early", "b-late"):
        return (("build", "keep" if q == "b-early" else 0),)
    if a == "d" and q in ("r-early", "r-late"):
        return (("return", "keep" if q == "r-early" else "pop"),)
    return ()


def example_audit():
    # Traverse all input words through length eight while carrying both
    # independent source configurations and their compiled buffer states.
    frontier = [("", 0, {("build", ()): encode(1, 0, ())})]
    words = transitions = 0
    for depth in range(9):
        following = []
        for w, H, states in frontier:
            words += 1
            accept = any(q in ("build", "return") and not s for q, s in states)
            expected = any(w == "ac" * n + "bd" * n for n in range(3))
            assert accept == expected, (w, states)
            for (q, s), compiled in states.items():
                assert abs(len(s) - H) <= 1
                assert decode(compiled) == s
            if depth == 8:
                continue
            for a in "acbd":
                kind = "c" if a == "a" else "r" if a == "b" else "i"
                H2 = clock_step(H, kind)
                states2 = {}
                for (q, s), compiled in states.items():
                    for q2, op in choices(q, s, a):
                        transitions += 1
                        s2 = source_step(s, op)
                        c2 = local_step(1, compiled, op, kind)
                        assert c2 is not None
                        assert c2 == encode(1, H2, s2)
                        states2[q2, s2] = c2
                following.append((w + a, H2, states2))
        frontier = following
    assert local_step(0, encode(0, 0, ()), "keep", "c") is None
    return dict(max_input_length=8, words=words, legal_transitions=transitions,
                delayed_push_rejects_bound_zero=True)


def main():
    report = {
        "status": "passed",
        "scope": "Finite local buffer simulation and first-exit checks; finite early/late source example.",
        "not_verified": [
            "unrestricted theorem in a proof assistant",
            "full VPA generation or determinization",
            "pushdown emptiness and shortest-witness implementation",
            "record-to-scaffold compiler",
            "imported literature theorems",
        ],
        "local": bounded_configuration_audit(),
        "example": example_audit(),
    }
    output = Path(__file__).with_name("checker-output.json")
    output.write_text(json.dumps(report, indent=2) + "\n")
    print(json.dumps(report, indent=2))


if __name__ == "__main__":
    main()