#!/usr/bin/env python3
"""Independent audit for FPRD-SH-T11--T14 and C06--C07.

The transfer audit enumerates two-state unary transition structures, every
binary Boolean support policy, discrete/universal component partitions, all
saturated component initial sets, and all component final sets.  The rigidity
audit separately enumerates every two-letter support policy through arity three
and compares the proposed policy condition with direct homogeneous-target
signature counts.  No original research checker is imported.
"""

from __future__ import annotations

from itertools import combinations, product
import json
from pathlib import Path


STATES = (0, 1)
SUPPORTS = (1, 2, 3)  # nonempty bit masks on two components


def edges(mask: int) -> frozenset[tuple[int, int]]:
    return frozenset(
        (source, target)
        for source in STATES
        for target in STATES
        if mask & (1 << (2 * source + target))
    )


def block(kind: int, state: int) -> int:
    return state if kind == 0 else 0


def classes(kind: int) -> tuple[tuple[int, ...], ...]:
    return ((0,), (1,)) if kind == 0 else ((0, 1),)


def predecessor_compatible(graph: frozenset[tuple[int, int]], kind: int) -> bool:
    for equivalent in classes(kind):
        for left, right in product(equivalent, repeat=2):
            for source_class in classes(kind):
                left_hit = any((source, left) in graph for source in source_class)
                right_hit = any((source, right) in graph for source in source_class)
                if left_hit != right_hit:
                    return False
    return True


def saturated(mask: int, kind: int) -> bool:
    return all(
        all(bool(mask & (1 << state)) == bool(mask & (1 << equivalent[0])) for state in equivalent)
        for equivalent in classes(kind)
    )


def product_edges(
    left: frozenset[tuple[int, int]],
    right: frozenset[tuple[int, int]],
    policy: tuple[int, ...],
) -> frozenset[tuple[tuple[int, int], tuple[int, int]]]:
    result: set[tuple[tuple[int, int], tuple[int, int]]] = set()
    for source in product(STATES, repeat=2):
        for support in policy:
            choices = []
            for coordinate, graph in enumerate((left, right)):
                if support & (1 << coordinate):
                    choices.append(tuple(target for start, target in graph if start == source[coordinate]))
                else:
                    choices.append((source[coordinate],))
            for target in product(*choices):
                result.add((source, target))
    return frozenset(result)


def product_predecessor_compatible(
    graph: frozenset[tuple[tuple[int, int], tuple[int, int]]],
    kinds: tuple[int, int],
) -> bool:
    grouped: dict[tuple[int, int], list[tuple[int, int]]] = {}
    for state in product(STATES, repeat=2):
        grouped.setdefault(tuple(block(kinds[i], state[i]) for i in range(2)), []).append(state)
    for equivalent in grouped.values():
        for left, right in product(equivalent, repeat=2):
            for source_class in grouped.values():
                left_hit = any((source, left) in graph for source in source_class)
                right_hit = any((source, right) in graph for source in source_class)
                if left_hit != right_hit:
                    return False
    return True


def quotient_edges(
    graph: frozenset[tuple[tuple[int, int], tuple[int, int]]],
    kinds: tuple[int, int],
) -> frozenset[tuple[tuple[int, int], tuple[int, int]]]:
    return frozenset(
        (
            tuple(block(kinds[i], source[i]) for i in range(2)),
            tuple(block(kinds[i], target[i]) for i in range(2)),
        )
        for source, target in graph
    )


def quotient_component_edges(
    graph: frozenset[tuple[int, int]], kind: int
) -> frozenset[tuple[int, int]]:
    return frozenset((block(kind, source), block(kind, target)) for source, target in graph)


def rebuilt_product_edges(
    components: tuple[frozenset[tuple[int, int]], frozenset[tuple[int, int]]],
    policy: tuple[int, ...],
    kinds: tuple[int, int],
) -> frozenset[tuple[tuple[int, int], tuple[int, int]]]:
    state_sets = tuple(range(len(classes(kind))) for kind in kinds)
    result: set[tuple[tuple[int, int], tuple[int, int]]] = set()
    for source in product(*state_sets):
        for support in policy:
            choices = []
            for coordinate, graph in enumerate(components):
                if support & (1 << coordinate):
                    choices.append(tuple(target for start, target in graph if start == source[coordinate]))
                else:
                    choices.append((source[coordinate],))
            for target in product(*choices):
                result.add((source, target))
    return frozenset(result)


def product_state_set(left_mask: int, right_mask: int) -> frozenset[tuple[int, int]]:
    return frozenset(
        (left, right)
        for left, right in product(STATES, repeat=2)
        if left_mask & (1 << left) and right_mask & (1 << right)
    )


def quotient_state_set(
    state_set: frozenset[tuple[int, int]], kinds: tuple[int, int]
) -> frozenset[tuple[int, int]]:
    return frozenset(tuple(block(kinds[i], state[i]) for i in range(2)) for state in state_set)


def component_quotient_set(mask: int, kind: int) -> frozenset[int]:
    return frozenset(block(kind, state) for state in STATES if mask & (1 << state))


def audit_transfer() -> dict:
    structural_cases = 0
    admissible_structures = 0
    saturated_initial_pairs = 0
    final_pairs = 0
    failures: list[dict] = []
    for left_mask, right_mask in product(range(16), repeat=2):
        component_graphs = (edges(left_mask), edges(right_mask))
        for policy_mask in range(8):
            policy = tuple(SUPPORTS[i] for i in range(3) if policy_mask & (1 << i))
            whole = product_edges(*component_graphs, policy)
            for kinds in product(range(2), repeat=2):
                structural_cases += 1
                if not all(predecessor_compatible(component_graphs[i], kinds[i]) for i in range(2)):
                    continue
                admissible_structures += 1
                if not product_predecessor_compatible(whole, kinds):
                    failures.append({"kind": "product-predecessors", "case": [left_mask, right_mask, policy_mask, *kinds]})
                    continue
                direct = quotient_edges(whole, kinds)
                rebuilt = rebuilt_product_edges(
                    tuple(quotient_component_edges(component_graphs[i], kinds[i]) for i in range(2)),
                    policy,
                    kinds,
                )
                if direct != rebuilt:
                    failures.append({"kind": "quotient-transitions", "case": [left_mask, right_mask, policy_mask, *kinds]})

                for initial_masks in product(range(4), repeat=2):
                    if not all(saturated(initial_masks[i], kinds[i]) for i in range(2)):
                        continue
                    saturated_initial_pairs += 1
                    direct_initial = quotient_state_set(product_state_set(*initial_masks), kinds)
                    rebuilt_initial = frozenset(product(*(
                        component_quotient_set(initial_masks[i], kinds[i]) for i in range(2)
                    )))
                    if direct_initial != rebuilt_initial:
                        failures.append({"kind": "initial-blocks", "case": [left_mask, right_mask, policy_mask, *kinds, *initial_masks]})

                for final_masks in product(range(4), repeat=2):
                    final_pairs += 1
                    direct_final = quotient_state_set(product_state_set(*final_masks), kinds)
                    rebuilt_final = frozenset(product(*(
                        component_quotient_set(final_masks[i], kinds[i]) for i in range(2)
                    )))
                    if direct_final != rebuilt_final:
                        failures.append({"kind": "final-blocks", "case": [left_mask, right_mask, policy_mask, *kinds, *final_masks]})

    return {
        "transition_partition_cases": structural_cases,
        "predecessor_compatible_cases": admissible_structures,
        "saturated_initial_set_pairs": saturated_initial_pairs,
        "final_set_pairs": final_pairs,
        "failures": failures[:20],
    }


def support_families(arity: int) -> tuple[tuple[int, ...], ...]:
    supports = tuple(range(1, 1 << arity))
    return tuple(
        tuple(support for i, support in enumerate(supports) if mask & (1 << i))
        for mask in range(1 << len(supports))
    )


def rigid(policy: tuple[tuple[int, ...], ...]) -> bool:
    active = [(letter, family[0]) for letter, family in enumerate(policy) if family]
    if any(len(family) != 1 for family in policy if family):
        return False
    return all(
        left_support & right_support
        for (left_letter, left_support), (right_letter, right_support) in combinations(active, 2)
        if left_letter != right_letter
    )


def incoming_signatures(
    target: tuple[int, ...], policy: tuple[tuple[int, ...], tuple[int, ...]]
) -> tuple[tuple[int, int], ...]:
    result = []
    for letter, family in enumerate(policy, start=1):
        for support in family:
            if all(target[i] == letter for i in range(len(target)) if support & (1 << i)):
                result.append((letter, support))
    return tuple(result)


def ambiguous_homogeneous_target(
    arity: int, policy: tuple[tuple[int, ...], tuple[int, ...]]
) -> tuple[int, ...] | None:
    for target in product((0, 1, 2), repeat=arity):
        signatures = incoming_signatures(target, policy)
        covered = 0
        for _, support in signatures:
            covered |= support
        used = sum(1 << i for i, label in enumerate(target) if label)
        if covered == used and len(signatures) > 1:
            return target
    return None


def unmarked_same_letter_forms(arity: int, left: int, right: int) -> tuple[tuple[str, ...], tuple[str, ...]]:
    """Residual shapes for two last-support choices over one-letter stars.

    B is the star body exposed by an advancing coordinate, Q is the retained
    noninitial prefix at a stuttering coordinate, and E is an unused coordinate.
    Distinct supports must therefore remain distinct after position marks are
    erased, including nested and overlapping supports.
    """
    union = left | right
    def form(last: int) -> tuple[str, ...]:
        return tuple(
            "B" if last & (1 << i) else "Q" if union & (1 << i) else "E"
            for i in range(arity)
        )
    return form(left), form(right)


def audit_rigidity() -> dict:
    policies = 0
    rigid_policies = 0
    nonrigid_witnesses = 0
    same_letter_unmarked_pairs = 0
    failures: list[dict] = []
    for arity in (1, 2, 3):
        families = support_families(arity)
        for policy in product(families, repeat=2):
            policies += 1
            is_rigid = rigid(policy)
            witness = ambiguous_homogeneous_target(arity, policy)
            rigid_policies += int(is_rigid)
            nonrigid_witnesses += int(witness is not None)
            if is_rigid == (witness is not None):
                failures.append({"kind": "criterion", "arity": arity, "policy": policy, "witness": witness})
            for family in policy:
                for left, right in combinations(family, 2):
                    same_letter_unmarked_pairs += 1
                    left_form, right_form = unmarked_same_letter_forms(arity, left, right)
                    if left_form == right_form:
                        failures.append({"kind": "unmarked-same-letter", "arity": arity, "supports": [left, right]})

    triangle = ((0b011,), (0b110,), (0b101,))
    controls = {
        "empty_policy_is_rigid": rigid(((), ())),
        "single_active_support_is_rigid": rigid(((0b001,), ())),
        "nested_same_letter_supports_are_not_rigid": not rigid(((0b001, 0b011), ())),
        "disjoint_distinct_letter_supports_are_not_rigid": not rigid(((0b001,), (0b100,))),
        "pairwise_triangle_has_no_common_participant": bool(
            rigid(triangle)
            and (triangle[0][0] & triangle[1][0])
            and (triangle[0][0] & triangle[2][0])
            and (triangle[1][0] & triangle[2][0])
            and not (triangle[0][0] & triangle[1][0] & triangle[2][0])
        ),
    }
    if not all(controls.values()):
        failures.append({"kind": "control", "controls": controls})
    return {
        "two_letter_policies": policies,
        "rigid_policies": rigid_policies,
        "nonrigid_target_witnesses": nonrigid_witnesses,
        "same_letter_unmarked_support_pairs": same_letter_unmarked_pairs,
        "controls": controls,
        "failures": failures[:20],
    }


def main() -> None:
    transfer = audit_transfer()
    rigidity = audit_rigidity()
    result = {
        "status": "pass" if not transfer["failures"] and not rigidity["failures"] else "fail",
        "transfer": transfer,
        "rigidity": rigidity,
    }
    output = Path(__file__).with_name("independent-output.json")
    output.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n")
    print(json.dumps(result, indent=2, sort_keys=True))
    raise SystemExit(0 if result["status"] == "pass" else 1)


if __name__ == "__main__":
    main()