verify_stack_clock_dichotomy.py

#!/usr/bin/env python3
"""Exhaustive action-fiber audit for FPRD-T175."""

from __future__ import annotations

import itertools
import json
from pathlib import Path


CALL = 1
LOCAL = 0
RETURN = -1
ACTIONS = (CALL, LOCAL, RETURN)
NONEMPTY_FIBERS = tuple(
    frozenset(action for index, action in enumerate(ACTIONS) if mask & (1 << index))
    for mask in range(1, 1 << len(ACTIONS))
)


def advance(heights, fiber):
    result = set()
    for height in heights:
        for action in fiber:
            if action == CALL:
                result.add(height + 1)
            elif action == RETURN:
                result.add(max(0, height - 1))
            else:
                result.add(height)
    return frozenset(result)


def possible_heights(fibers, word):
    heights = frozenset({0})
    for letter in word:
        heights = advance(heights, fibers[letter])
    return heights


def diameter(fibers, word):
    heights = possible_heights(fibers, word)
    return max(heights) - min(heights)


def classify(fibers):
    has_call = any(CALL in fiber for fiber in fibers)
    action_uniform = all(len(fiber) == 1 for fiber in fibers)
    if not has_call:
        return "no_calls"
    if action_uniform:
        return "synchronized"
    return "unbounded"


def witness(fibers, n):
    ambiguous = next(index for index, fiber in enumerate(fibers) if len(fiber) > 1)
    fiber = fibers[ambiguous]
    if CALL in fiber:
        return (ambiguous,) * n

    call_letter = next(index for index, candidate in enumerate(fibers) if CALL in candidate)
    assert LOCAL in fiber and RETURN in fiber
    return (call_letter,) * n + (ambiguous,) * n


def main():
    patterns = 0
    no_call_patterns = 0
    synchronized_patterns = 0
    unbounded_patterns = 0
    zero_diameter_checks = 0
    linear_witness_checks = 0
    witness_symbols = 0

    for alphabet_size in (1, 2, 3):
        for fibers in itertools.product(NONEMPTY_FIBERS, repeat=alphabet_size):
            patterns += 1
            tier = classify(fibers)
            if tier == "no_calls":
                no_call_patterns += 1
                for length in range(7):
                    for word in itertools.product(range(alphabet_size), repeat=length):
                        assert diameter(fibers, word) == 0
                        zero_diameter_checks += 1
            elif tier == "synchronized":
                synchronized_patterns += 1
                for length in range(7):
                    for word in itertools.product(range(alphabet_size), repeat=length):
                        assert diameter(fibers, word) == 0
                        zero_diameter_checks += 1
            else:
                unbounded_patterns += 1
                for n in range(1, 9):
                    word = witness(fibers, n)
                    assert len(word) <= 2 * n
                    assert diameter(fibers, word) >= n
                    linear_witness_checks += 1
                    witness_symbols += len(word)

    output = {
        "status": "pass",
        "scope": "all nonempty action-fiber patterns on observed alphabets through size three",
        "fiber_patterns": patterns,
        "no_call_patterns": no_call_patterns,
        "synchronized_patterns": synchronized_patterns,
        "unbounded_patterns": unbounded_patterns,
        "zero_diameter_word_checks": zero_diameter_checks,
        "linear_witness_checks": linear_witness_checks,
        "witness_symbols": witness_symbols,
        "maximum_requested_separation": 8,
        "does_not_verify": [
            "source-language restrictions on compatible lifts",
            "stack-symbol disagreement at equal height",
            "context-dependent hidden-coordinate maps",
            "causal-selection decidability in the unbounded tier",
        ],
    }
    Path(__file__).with_name("checker-output.json").write_text(
        json.dumps(output, indent=2) + "\n", encoding="utf-8"
    )
    print(json.dumps(output, indent=2))


if __name__ == "__main__":
    main()