verify_transport_spectrum.py

#!/usr/bin/env python3
"""Finite audit for FPRD-T157 stationary transport spectra."""

from __future__ import annotations

import json
from dataclasses import dataclass
from itertools import product
from pathlib import Path


Point = tuple[int, ...]
Descriptor = None | str | tuple[int, ...]


def leq(left: Point, right: Point) -> bool:
    return all(a <= b for a, b in zip(left, right))


def minimal_basis(points: set[Point]) -> set[Point]:
    return {point for point in points if not any(other != point and leq(other, point) for other in points)}


def upward_closure(points: set[Point], grid: tuple[range, ...]) -> set[Point]:
    universe = set(product(*grid))
    return {target for target in universe if any(leq(source, target) for source in points)}


def audit_finite_bases() -> dict[str, int]:
    grid2 = (range(1, 5), range(1, 5))
    universe2 = list(product(*grid2))
    subsets = 0
    closure_reconstructions = 0
    antichain_checks = 0

    for mask in range(1 << len(universe2)):
        subset = {point for index, point in enumerate(universe2) if (mask >> index) & 1}
        closure = upward_closure(subset, grid2)
        basis = minimal_basis(closure)
        assert upward_closure(basis, grid2) == closure
        assert all(not leq(left, right) for left in basis for right in basis if left != right)
        subsets += 1
        closure_reconstructions += 1
        antichain_checks += 1

    four_dimensional_families = 0
    four_dimensional_basis_checks = 0
    for seed in range(4096):
        points = {
            (
                1 + ((seed + 3 * index) % 4),
                1 + ((seed // 3 + 5 * index) % 4),
                1 + ((seed // 7 + 7 * index) % 4),
                1 + ((seed // 11 + 11 * index) % 4),
            )
            for index in range(1 + seed % 9)
        }
        basis = minimal_basis(points)
        assert all(any(leq(source, point) for source in basis) for point in points)
        assert all(not leq(left, right) for left in basis for right in basis if left != right)
        four_dimensional_families += 1
        four_dimensional_basis_checks += 1

    return {
        "two_dimensional_subsets": subsets,
        "closure_reconstructions": closure_reconstructions,
        "antichain_checks": antichain_checks,
        "four_dimensional_families": four_dimensional_families,
        "four_dimensional_basis_checks": four_dimensional_basis_checks,
    }


@dataclass(frozen=True)
class TinyMachine:
    seed: int
    degree: int

    def step(self, state: int, symbol: int, old_label: int | None) -> tuple[int, int, tuple[Descriptor, ...]]:
        label_value = 0 if old_label is None else old_label
        new_state = (state + symbol + label_value + self.seed) % 2
        new_label = (state ^ symbol ^ label_value ^ self.seed) & 1
        descriptors: list[Descriptor] = []
        for port in range(self.degree):
            code = (self.seed + 2 * state + 3 * symbol + 5 * label_value + port) % 3
            if code == 0:
                descriptors.append(None)
            elif code == 1:
                descriptors.append("SELF")
            else:
                descriptors.append((port,))
        return new_state, new_label, tuple(descriptors)


def resolve(old_rows: list[tuple[int, tuple[int | None, ...]]], descriptor: Descriptor) -> int | None | str:
    if descriptor is None or descriptor == "SELF":
        return descriptor
    if not old_rows:
        return None
    node = len(old_rows) - 1
    for port in descriptor:
        target = old_rows[node][1][port]
        if target is None:
            return None
        node = target
    return node


def run_single(machine: TinyMachine, word: tuple[int, ...]) -> tuple[int, list[tuple[int, tuple[int | None, ...]]]]:
    state = 0
    rows: list[tuple[int, tuple[int | None, ...]]] = []
    for symbol in word:
        old_label = rows[-1][0] if rows else None
        state, label, descriptors = machine.step(state, symbol, old_label)
        new_index = len(rows)
        ports = tuple(
            new_index if descriptor == "SELF" else resolve(rows, descriptor)
            for descriptor in descriptors
        )
        rows.append((label, ports))
    return state, rows


def translate(descriptor: Descriptor, offset: int) -> Descriptor:
    if descriptor is None or descriptor == "SELF":
        return descriptor
    return tuple(offset + port for port in descriptor)


def run_pair(first: TinyMachine, second: TinyMachine, word: tuple[int, ...]) -> tuple[tuple[int, int], list[tuple[tuple[int, int], tuple[int | None, ...]]]]:
    state = (0, 0)
    rows: list[tuple[tuple[int, int], tuple[int | None, ...]]] = []
    for symbol in word:
        old_labels = rows[-1][0] if rows else (None, None)
        next1, label1, desc1 = first.step(state[0], symbol, old_labels[0])
        next2, label2, desc2 = second.step(state[1], symbol, old_labels[1])
        descriptors = tuple(translate(item, 0) for item in desc1) + tuple(
            translate(item, first.degree) for item in desc2
        )
        old_projection = [
            (
                0,
                row[1],
            )
            for row in rows
        ]
        new_index = len(rows)
        ports = tuple(
            new_index if descriptor == "SELF" else resolve(old_projection, descriptor)
            for descriptor in descriptors
        )
        rows.append(((label1, label2), ports))
        state = (next1, next2)
    return state, rows


def audit_pairing() -> dict[str, int]:
    machines = [TinyMachine(seed, 1 + seed % 2) for seed in range(24)]
    machine_pairs = 0
    paired_runs = 0
    projected_row_checks = 0
    boolean_output_checks = 0

    words = [word for length in range(7) for word in product((0, 1), repeat=length)]
    for first, second in product(machines, repeat=2):
        machine_pairs += 1
        for word in words:
            state1, rows1 = run_single(first, word)
            state2, rows2 = run_single(second, word)
            pair_state, paired = run_pair(first, second, word)
            assert pair_state == (state1, state2)
            assert len(rows1) == len(rows2) == len(paired)
            for index, ((label1, ports1), (label2, ports2), (labels, ports)) in enumerate(zip(rows1, rows2, paired)):
                assert labels == (label1, label2)
                assert ports[: first.degree] == ports1
                assert ports[first.degree :] == ports2
                assert all(target is None or 0 <= target <= index for target in ports)
                projected_row_checks += 1
            for truth_table in range(16):
                left = state1 & 1
                right = state2 & 1
                paired_answer = (truth_table >> (2 * left + right)) & 1
                expected = (truth_table >> (2 * (pair_state[0] & 1) + (pair_state[1] & 1))) & 1
                assert paired_answer == expected
                boolean_output_checks += 1
            paired_runs += 1

    return {
        "tiny_machines": len(machines),
        "machine_pairs": machine_pairs,
        "paired_runs": paired_runs,
        "projected_row_checks": projected_row_checks,
        "boolean_output_checks": boolean_output_checks,
    }


def run() -> dict[str, object]:
    result: dict[str, object] = {"status": "pass"}
    result.update(audit_finite_bases())
    result.update(audit_pairing())
    return result


if __name__ == "__main__":
    result = run()
    output = Path(__file__).with_name("checker-output.json")
    output.write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8")
    print(json.dumps(result, indent=2))