#!/usr/bin/env python3
"""Finite sanity check for the paper's simulation proposition; not a formal proof."""
from itertools import product


def reachable(initial, edges):
    seen = set(initial)
    while True:
        expanded = seen | {b for a, b in edges if a in seen}
        if expanded == seen:
            return seen
        seen = expanded


def subsets(items):
    for mask in range(1 << len(items)):
        yield {item for i, item in enumerate(items) if mask & (1 << i)}


def main():
    states = (0, 1)
    pairs = tuple(product(states, repeat=2))
    checked = 0
    for concrete_edges in subsets(pairs):
        for abstract_edges in subsets(pairs):
            closure = {a: reachable({a}, abstract_edges) for a in states}
            for mapping in product(states, repeat=2):
                if not all(mapping[b] in closure[mapping[a]] for a, b in concrete_edges):
                    continue
                for abstract_initial in subsets(states):
                    for invariant in subsets(states):
                        if not abstract_initial <= invariant:
                            continue
                        if any(a in invariant and b not in invariant for a, b in abstract_edges):
                            continue
                        for concrete_initial in subsets(states):
                            if not {mapping[c] for c in concrete_initial} <= abstract_initial:
                                continue
                            assert all(mapping[c] in invariant for c in reachable(concrete_initial, concrete_edges))
                            checked += 1

    # Both local updates preserve each bit's type, but either intermediate
    # configuration violates the intended cross-agent equality invariant.
    initial = (0, 0)
    update_x = (1, initial[1])
    update_y = (initial[0], 1)
    assert initial[0] == initial[1]
    assert update_x[0] != update_x[1] and update_y[0] != update_y[1]
    assert (1, 1)[0] == (1, 1)[1]
    print(f"Checked {checked} finite simulation cases and the interference example.")
    print("This bounded enumeration does not verify the general theorem or any deployment.")


if __name__ == "__main__":
    main()