verify_causal_preimages.py

#!/usr/bin/env python3
"""Finite audit for FPRD-T166.

The local machine abstracts a scaffold transition into a finite control,
finite view, and emitted local action. The product identity is independent of
the internal meaning of the action or view update.
"""

from __future__ import annotations

import itertools
import json
from pathlib import Path


BITS = (0, 1)


def words(max_len: int):
    yield ()
    for n in range(1, max_len + 1):
        yield from itertools.product(BITS, repeat=n)


WORDS3 = tuple(words(3))
WORDS6 = tuple(words(6))


def all_transducers():
    """All two-state binary synchronous Mealy machines."""
    choices = tuple(itertools.product(BITS, BITS))  # next state, output
    for table in itertools.product(choices, repeat=4):
        yield table


def transduce(table, word, initial=0):
    state = initial
    output = []
    for letter in word:
        state, emitted = table[2 * state + letter]
        output.append(emitted)
    return state, tuple(output)


def run_source(table, accepting, env, word, q_count, view_count):
    control = 0
    view = 0
    actions = []
    for letter in word:
        index = (control * 2 + letter) * view_count + view
        control, action = table[index]
        actions.append(action)
        view = env[view * 2 + action]
    return control, view, tuple(actions), control in accepting


def run_product(transducer, table, accepting, env, word, q_count, view_count):
    t_state = 0
    control = 0
    view = 0
    actions = []
    for letter in word:
        t_state, emitted = transducer[2 * t_state + letter]
        index = (control * 2 + emitted) * view_count + view
        control, action = table[index]
        actions.append(action)
        view = env[view * 2 + action]
    return t_state, control, view, tuple(actions), control in accepting


def audit_product_identity():
    transducers = tuple(all_transducers())
    comparisons = 0
    table_pairs = 0

    # One control, two abstract views, two actions. Exhaust every local table,
    # every view-update environment, and both accepting sets.
    q_count = 1
    view_count = 2
    local_choices = ((0, 0), (0, 1))
    for table in itertools.product(local_choices, repeat=4):
        for env in itertools.product(BITS, repeat=4):
            for accepting in (frozenset(), frozenset({0})):
                table_pairs += 1
                for transducer in transducers:
                    for word in WORDS3:
                        _, out = transduce(transducer, word)
                        source = run_source(table, accepting, env, out, q_count, view_count)
                        product = run_product(
                            transducer, table, accepting, env, word, q_count, view_count
                        )
                        assert source == product[1:]
                        comparisons += 1

    # Two controls, one abstract view, two actions. This exhausts nontrivial
    # source-control and accepting-state behavior.
    q_count = 2
    view_count = 1
    local_choices = tuple(itertools.product(range(q_count), BITS))
    env = (0, 0)
    for table in itertools.product(local_choices, repeat=4):
        for mask in range(4):
            accepting = frozenset(q for q in range(2) if mask & (1 << q))
            table_pairs += 1
            for transducer in transducers:
                for word in WORDS3:
                    _, out = transduce(transducer, word)
                    source = run_source(table, accepting, env, out, q_count, view_count)
                    product = run_product(
                        transducer, table, accepting, env, word, q_count, view_count
                    )
                    assert source == product[1:]
                    comparisons += 1

    return len(transducers), table_pairs, comparisons


def inverse_transducer(table):
    """Inverse of a statewise-permuting binary Mealy machine."""
    inverse = [None] * 4
    for state in BITS:
        seen = set()
        for letter in BITS:
            next_state, output = table[2 * state + letter]
            assert output not in seen
            seen.add(output)
            inverse[2 * state + output] = (next_state, letter)
    return tuple(inverse)


def audit_reversible_coordinates():
    count = 0
    roundtrips = 0
    for next_states in itertools.product(BITS, repeat=4):
        for output_swaps in itertools.product(BITS, repeat=2):
            table = []
            for state in BITS:
                swap = output_swaps[state]
                for letter in BITS:
                    table.append((next_states[2 * state + letter], letter ^ swap))
            table = tuple(table)
            inverse = inverse_transducer(table)
            count += 1
            for word in WORDS6:
                _, encoded = transduce(table, word)
                _, decoded = transduce(inverse, encoded)
                assert decoded == word
                _, decoded_first = transduce(inverse, word)
                _, encoded_second = transduce(table, decoded_first)
                assert encoded_second == word
                roundtrips += 2
    return count, roundtrips


def main():
    transducers, local_families, comparisons = audit_product_identity()
    invertible, roundtrips = audit_reversible_coordinates()
    output = {
        "status": "pass",
        "scope": "finite-state product identity and reversible-coordinate orientation",
        "does_not_verify": [
            "every scaffolding automaton",
            "closure under nondeterministic or existential transductions",
            "any converse for forgotten-action projection",
        ],
        "binary_two_state_transducers": transducers,
        "local_machine_environment_families": local_families,
        "product_run_comparisons": comparisons,
        "invertible_binary_mealy_machines": invertible,
        "inverse_roundtrip_checks": roundtrips,
        "resource_bound": "(d,k,g,q) -> (d,k,g,s*q)",
        "persistent_graph": "unchanged",
    }
    path = Path(__file__).with_name("checker-output.json")
    path.write_text(json.dumps(output, indent=2) + "\n", encoding="utf-8")
    print(json.dumps(output, indent=2))


if __name__ == "__main__":
    main()