verify_selection_chain_rule.py

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

from __future__ import annotations

import itertools
import json
from pathlib import Path


BITS = (0, 1)


def subsets(items, max_size=2):
    return tuple(
        combo
        for size in range(1, max_size + 1)
        for combo in itertools.combinations(items, size)
    )


# One-state outer selectors choose b from the observed x.
OUTER_SELECTORS = tuple(itertools.product(BITS, repeat=2))
# One-state inner selectors choose c from the intermediate letter (x,b).
INNER_SELECTORS = tuple(itertools.product(BITS, repeat=4))
OUTER_FAMILIES = subsets(OUTER_SELECTORS)
INNER_FAMILIES = subsets(INNER_SELECTORS)


def top_index(x, b, c):
    return 1 + 4 * x + 2 * b + c


def accepts_top(mask, word):
    if not word:
        return bool(mask & 1)
    assert len(word) == 1
    x, b, c = word[0]
    return bool(mask & (1 << top_index(x, b, c)))


def accepts_middle(mask, word):
    if not word:
        return accepts_top(mask, ())
    x, b = word[0]
    return any(accepts_top(mask, ((x, b, c),)) for c in BITS)


def accepts_bottom(mask, word):
    if not word:
        return accepts_middle(mask, ())
    x = word[0]
    return any(accepts_middle(mask, ((x, b),)) for b in BITS)


BOTTOM_WORDS = ((), (0,), (1,))
MIDDLE_WORDS = ((),) + tuple(((x, b),) for x in BITS for b in BITS)


def inner_select(selector, word):
    return tuple((x, b, selector[2 * x + b]) for x, b in word)


def outer_select(selector, word):
    return tuple((x, selector[x]) for x in word)


def inner_family_covers(mask, family):
    return all(
        accepts_middle(mask, word)
        == any(accepts_top(mask, inner_select(selector, word)) for selector in family)
        for word in MIDDLE_WORDS
    )


def outer_family_covers(mask, family):
    return all(
        accepts_bottom(mask, word)
        == any(accepts_middle(mask, outer_select(selector, word)) for selector in family)
        for word in BOTTOM_WORDS
    )


def composed_family_covers(mask, inner_family, outer_family):
    return all(
        accepts_bottom(mask, word)
        == any(
            accepts_top(
                mask,
                inner_select(inner, outer_select(outer, word)),
            )
            for inner in inner_family
            for outer in outer_family
        )
        for word in BOTTOM_WORDS
    )


def audit_cover_chain_rule():
    language_count = 1 << 9  # empty word plus eight top letters
    valid_stage_pairs = 0
    composed_cover_checks = 0
    horizon_checks = 0

    for mask in range(language_count):
        valid_inner = [
            family for family in INNER_FAMILIES if inner_family_covers(mask, family)
        ]
        valid_outer = [
            family for family in OUTER_FAMILIES if outer_family_covers(mask, family)
        ]
        for inner_family in valid_inner:
            for outer_family in valid_outer:
                valid_stage_pairs += 1
                assert composed_family_covers(mask, inner_family, outer_family)
                assert len(inner_family) * len(outer_family) <= 4
                composed_cover_checks += len(BOTTOM_WORDS)
                horizon_checks += 2  # empty-word and one-letter restrictions

    return {
        "top_languages": language_count,
        "inner_selectors": len(INNER_SELECTORS),
        "outer_selectors": len(OUTER_SELECTORS),
        "inner_families": len(INNER_FAMILIES),
        "outer_families": len(OUTER_FAMILIES),
        "valid_stage_family_pairs": valid_stage_pairs,
        "composed_cover_word_checks": composed_cover_checks,
        "horizon_composition_checks": horizon_checks,
    }


def two_state_machines(input_size, ignore_low_bit=False):
    """Two-state Mealy machines emitting one bit per letter."""
    effective_inputs = input_size // 2 if ignore_low_bit else input_size
    for entries in itertools.product(range(4), repeat=2 * effective_inputs):
        table = []
        for state in range(2):
            row = []
            for symbol in range(input_size):
                key = symbol // 2 if ignore_low_bit else symbol
                code = entries[state * effective_inputs + key]
                row.append((code // 2, code % 2))
            table.append(tuple(row))
        yield tuple(table)


def run(machine, word):
    state = 0
    output = []
    for symbol in word:
        state, emitted = machine[state][symbol]
        output.append(emitted)
    return state, tuple(output)


def audit_product_states():
    # Outer input x emits b. Inner input is encoded as 2*x+b and emits c.
    outers = tuple(two_state_machines(2))
    # This 256-machine inner subfamily ignores b in its state/output table.
    inners = tuple(two_state_machines(4, ignore_low_bit=True))
    words = tuple(
        word
        for length in range(4)
        for word in itertools.product(BITS, repeat=length)
    )
    comparisons = 0

    for outer in outers:
        for inner in inners:
            for word in words:
                outer_state, bs = run(outer, word)
                middle = tuple(2 * x + b for x, b in zip(word, bs))
                inner_state, cs = run(inner, middle)

                pair = (0, 0)
                direct_cs = []
                for x in word:
                    next_outer, b = outer[pair[1]][x]
                    next_inner, c = inner[pair[0]][2 * x + b]
                    pair = (next_inner, next_outer)
                    direct_cs.append(c)

                assert pair == (inner_state, outer_state)
                assert tuple(direct_cs) == cs
                comparisons += 1

    return {
        "two_state_outer_machines": len(outers),
        "two_state_inner_subfamily": len(inners),
        "product_state_bound": 4,
        "product_run_comparisons": comparisons,
    }


def main():
    output = {
        "status": "pass",
        "scope": "finite selector-cover composition and product-state simulation",
        **audit_cover_chain_rule(),
        **audit_product_states(),
        "resource_law": "(m,s) odot (n,t) = (m*n,s*t)",
        "uniform_transport_bound": "(m*n*d,k,g^(m*n),q^(m*n)*s^(m*n)*t^n)",
        "does_not_verify": [
            "Pareto optimality of the product selector profile",
            "necessity of finite selector covers for bounded transport",
            "asynchronous or unbounded-memory selectors",
            "any external SCA or PEG separation",
        ],
    }
    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()