verify_distance_one_collapse.py

#!/usr/bin/env python3
"""Finite audit for FPRD-T159 distance-one collapse."""

from __future__ import annotations

import importlib.util
import itertools
import json
from dataclasses import dataclass
from pathlib import Path


MISSING = -1
SELF = -2


@dataclass(frozen=True)
class Scaffold:
    labels: tuple[int, ...]
    edges: tuple[tuple[int, ...], ...]

    @property
    def top(self) -> int:
        return len(self.labels) - 1


def view(scaffold: Scaffold, node: int, radius: int):
    if node == MISSING:
        return ("missing",)
    if radius == 0:
        return ("label", scaffold.labels[node])
    return (
        "node",
        scaffold.labels[node],
        tuple(view(scaffold, target, radius - 1) for target in scaffold.edges[node]),
    )


def root_view(scaffold: Scaffold):
    return ("missing",) if not scaffold.labels else view(scaffold, scaffold.top, 1)


def score(item) -> int:
    if isinstance(item, int):
        return item + 13
    if isinstance(item, str):
        return sum(ord(char) for char in item)
    return 17 + sum((index + 5) * score(value) for index, value in enumerate(item))


@dataclass(frozen=True)
class DistanceOneMachine:
    seed: int
    degree: int
    labels: int = 2
    controls: int = 3

    def transition_from_view(self, state: int, symbol: int, old_view):
        code = score((self.seed, state, symbol, old_view))
        options: list[object] = [MISSING, SELF, (), *[(port,) for port in range(self.degree)]]
        next_state = (state + symbol + code + self.seed) % self.controls
        label = (code // 3 + state + symbol) % self.labels
        descriptors = tuple(options[(code + 7 * port) % len(options)] for port in range(self.degree))
        return next_state, label, descriptors

    def accepting(self, state: int) -> bool:
        return state == self.seed % self.controls


def follow(scaffold: Scaffold, descriptor: tuple[int, ...]) -> int:
    if not scaffold.labels:
        return MISSING
    node = scaffold.top
    for port in descriptor:
        if node == MISSING:
            return MISSING
        node = scaffold.edges[node][port]
    return node


def step(machine: DistanceOneMachine, state: int, scaffold: Scaffold, symbol: int):
    next_state, label, descriptors = machine.transition_from_view(state, symbol, root_view(scaffold))
    new_index = len(scaffold.labels)
    targets = []
    for descriptor in descriptors:
        if descriptor == MISSING:
            targets.append(MISSING)
        elif descriptor == SELF:
            targets.append(new_index)
        else:
            targets.append(follow(scaffold, descriptor))
    return next_state, Scaffold(scaffold.labels + (label,), scaffold.edges + (tuple(targets),))


def target_zero_view(old_view, descriptor, new_label: int):
    if descriptor == MISSING:
        return ("missing",)
    if descriptor == SELF:
        return ("label", new_label)
    if old_view == ("missing",):
        return ("missing",)
    if descriptor == ():
        return ("label", old_view[1])
    child = old_view[2][descriptor[0]]
    if child == ("missing",):
        return child
    return ("label", child[1])


def dfa_step(machine: DistanceOneMachine, summary, symbol: int):
    state, old_view = summary
    next_state, label, descriptors = machine.transition_from_view(state, symbol, old_view)
    new_view = (
        "node",
        label,
        tuple(target_zero_view(old_view, descriptor, label) for descriptor in descriptors),
    )
    return next_state, new_view


def run_scaffold(machine: DistanceOneMachine, word: tuple[int, ...]):
    state = 0
    scaffold = Scaffold((), ())
    for symbol in word:
        state, scaffold = step(machine, state, scaffold, symbol)
    return state, scaffold


def run_dfa(machine: DistanceOneMachine, word: tuple[int, ...]):
    summary = (0, ("missing",))
    for symbol in word:
        summary = dfa_step(machine, summary, symbol)
    return summary


def view_capacity(degree: int, labels: int, radius: int) -> int:
    total = labels + 1
    for _ in range(radius):
        total = 1 + (labels + 1) * (total**degree)
    return total


def audit_direct_compilation() -> dict[str, int]:
    machines = [DistanceOneMachine(seed, 1 + seed % 2) for seed in range(24)]
    words = [word for length in range(9) for word in itertools.product((0, 1), repeat=length)]
    compiled_runs = 0
    summary_matches = 0
    acceptance_matches = 0
    state_bound_checks = 0

    for machine in machines:
        reachable = set()
        for word in words:
            state, scaffold = run_scaffold(machine, word)
            summary = run_dfa(machine, word)
            assert summary == (state, root_view(scaffold))
            assert machine.accepting(summary[0]) == machine.accepting(state)
            reachable.add(summary)
            compiled_runs += 1
            summary_matches += 1
            acceptance_matches += 1
        bound = machine.controls * view_capacity(machine.degree, machine.labels, 1)
        assert len(reachable) <= bound
        state_bound_checks += 1

    return {
        "tiny_machines": len(machines),
        "compiled_runs": compiled_runs,
        "summary_matches": summary_matches,
        "acceptance_matches": acceptance_matches,
        "state_bound_checks": state_bound_checks,
    }


def scaffold_family(node_count: int, degree: int):
    labels = itertools.product(range(2), repeat=node_count)
    edge_options = [
        list(itertools.product([MISSING, *range(node)], repeat=degree))
        for node in range(node_count)
    ]
    for label_row in labels:
        for edges in itertools.product(*edge_options):
            yield Scaffold(tuple(label_row), tuple(edges))


def audit_summary_determinism() -> dict[str, int]:
    families = [
        (DistanceOneMachine(2, 1), 5),
        (DistanceOneMachine(5, 2), 4),
    ]
    old_scaffolds = 0
    transitions_checked = 0
    same_summary_comparisons = 0
    summary_classes = 0

    for machine, node_count in families:
        material = list(scaffold_family(node_count, machine.degree))
        old_scaffolds += len(material)
        for state in range(machine.controls):
            for symbol in (0, 1):
                representatives = {}
                for scaffold in material:
                    summary = (state, root_view(scaffold))
                    next_state, next_scaffold = step(machine, state, scaffold, symbol)
                    next_summary = (next_state, root_view(next_scaffold))
                    assert next_summary == dfa_step(machine, summary, symbol)
                    transitions_checked += 1
                    if summary in representatives:
                        assert representatives[summary] == next_summary
                        same_summary_comparisons += 1
                    else:
                        representatives[summary] = next_summary
                summary_classes += len(representatives)

    return {
        "old_scaffold_machine_instances": old_scaffolds,
        "finite_scaffold_transitions": transitions_checked,
        "same_summary_comparisons": same_summary_comparisons,
        "summary_classes": summary_classes,
    }


def audit_selector_strictness() -> dict[str, int | str]:
    selector_path = Path(__file__).parents[1] / "replay-fanout" / "verify_persistent_selector.py"
    spec = importlib.util.spec_from_file_location("persistent_selector", selector_path)
    assert spec is not None and spec.loader is not None
    module = importlib.util.module_from_spec(spec)
    spec.loader.exec_module(module)
    result = module.main()
    assert result["ok"] is True
    assert result["degree"] == 2
    assert result["distance"] == 2
    assert result["nodes_per_symbol"] == 1
    assert result["counts"]["residual_profiles"] == sum(2**n for n in range(1, 11))
    return {
        "selector_words": result["counts"]["all_words"],
        "selector_queries": result["counts"]["selector_queries"],
        "selector_residual_profiles": result["counts"]["residual_profiles"],
        "selector_max_data_length": result["max_data_length"],
        "selector_distance": result["distance"],
        "selector_degree": result["degree"],
    }


def audit_capacity_formula() -> dict[str, int]:
    checks = 0
    for degree in range(1, 6):
        for labels in range(1, 6):
            expected = 1 + (labels + 1) ** (degree + 1)
            assert view_capacity(degree, labels, 1) == expected
            checks += 1
    return {"distance_one_capacity_checks": checks}


def main() -> None:
    result: dict[str, object] = {
        "scope": {
            "direct_compilation": "24 deterministic distance-one machines and every binary word through length 8",
            "summary_determinism": "all binary-labelled backward scaffolds: degree 1 on 5 nodes and degree 2 on 4 nodes",
            "strictness": "persistent selector through total word length 10 and data length 10",
        },
        **audit_direct_compilation(),
        **audit_summary_determinism(),
        **audit_selector_strictness(),
        **audit_capacity_formula(),
        "status": "pass",
    }
    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))


if __name__ == "__main__":
    main()