Research source · python

verify_distance_two_normal_form.py

site/public/research-artifacts/distance-two-normal-form/verify_distance_two_normal_form.py

360 lines. Source is displayed for inspection; it is not executed by this page.

File fingerprint

SHA-256: cfdec1b8631c20afda846c8dc0788ebd38ae7d1efcf2e69c43ac6ba3dc6b532c

#!/usr/bin/env python3
"""Finite audit for FPRD-T160 distance-two shortcut normalization."""

from __future__ import annotations

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


MISSING = -1
SELF = -2
Descriptor = int | tuple[int, ...]


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

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


def words(degree: int, distance: int, include_empty: bool = True) -> tuple[tuple[int, ...], ...]:
    start = 0 if include_empty else 1
    return tuple(
        word
        for length in range(start, distance + 1)
        for word in itertools.product(range(degree), repeat=length)
    )


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


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, radius: int):
    return ("missing",) if not scaffold.labels else view(scaffold, scaffold.top, radius)


def resolve_descriptor(scaffold: Scaffold, descriptor: Descriptor, new_index: int) -> int:
    if descriptor == MISSING:
        return MISSING
    if descriptor == SELF:
        return new_index
    old_root = MISSING if not scaffold.labels else scaffold.top
    return follow(scaffold, old_root, descriptor)


def extend(scaffold: Scaffold, label: int, descriptors: tuple[Descriptor, ...]) -> Scaffold:
    new_index = len(scaffold.labels)
    targets = tuple(resolve_descriptor(scaffold, descriptor, new_index) for descriptor in descriptors)
    return Scaffold(scaffold.labels + (label,), scaffold.edges + (targets,))


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


@dataclass(frozen=True)
class OriginalMachine:
    seed: int
    degree: int
    distance: int
    labels: int = 3
    controls: int = 4

    def transition(self, state: int, symbol: int, old_view):
        code = score((self.seed, state, symbol, old_view))
        options: tuple[Descriptor, ...] = (MISSING, SELF, *words(self.degree, self.distance))
        next_state = (state + symbol + code + self.seed) % self.controls
        label = (code // 5 + state + symbol) % self.labels
        descriptors = tuple(
            options[(code + 11 * port + self.seed) % 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


@dataclass(frozen=True)
class ShortcutLayout:
    original_degree: int
    original_distance: int
    port_words: tuple[tuple[int, ...], ...]
    port_of: dict[tuple[int, ...], int]

    @classmethod
    def make(cls, degree: int, distance: int):
        port_words = words(degree, distance, include_empty=False)
        return cls(degree, distance, port_words, {word: index for index, word in enumerate(port_words)})

    @property
    def degree(self) -> int:
        return len(self.port_words)


def shortcut_closure(original: Scaffold, layout: ShortcutLayout) -> Scaffold:
    edges = []
    for node in range(len(original.labels)):
        edges.append(tuple(follow(original, node, word) for word in layout.port_words))
    return Scaffold(original.labels, tuple(edges))


def reconstruct_original_view(shortcut: Scaffold, layout: ShortcutLayout):
    if not shortcut.labels:
        return ("missing",)
    root = shortcut.top

    def build(prefix: tuple[int, ...], remaining: int):
        node = root if not prefix else shortcut.edges[root][layout.port_of[prefix]]
        if node == MISSING:
            return ("missing",)
        if remaining == 0:
            return ("label", shortcut.labels[node])
        return (
            "node",
            shortcut.labels[node],
            tuple(build(prefix + (port,), remaining - 1) for port in range(layout.original_degree)),
        )

    return build((), layout.original_distance)


def compile_shortcut_descriptor(
    word: tuple[int, ...],
    direct_descriptors: tuple[Descriptor, ...],
    layout: ShortcutLayout,
) -> Descriptor:
    remaining = word
    while remaining:
        direct = direct_descriptors[remaining[0]]
        remaining = remaining[1:]
        if direct == MISSING:
            return MISSING
        if direct == SELF:
            continue

        old_path = direct
        suffix = remaining
        if not old_path and not suffix:
            return ()
        if not old_path:
            return (layout.port_of[suffix],)
        if not suffix:
            return (layout.port_of[old_path],)
        return (layout.port_of[old_path], layout.port_of[suffix])
    return SELF


def original_step(machine: OriginalMachine, state: int, scaffold: Scaffold, symbol: int):
    next_state, label, descriptors = machine.transition(
        state, symbol, root_view(scaffold, machine.distance)
    )
    return next_state, extend(scaffold, label, descriptors), descriptors


def compiled_step(
    machine: OriginalMachine,
    layout: ShortcutLayout,
    state: int,
    scaffold: Scaffold,
    symbol: int,
):
    old_view = reconstruct_original_view(scaffold, layout)
    next_state, label, direct_descriptors = machine.transition(state, symbol, old_view)
    shortcut_descriptors = tuple(
        compile_shortcut_descriptor(word, direct_descriptors, layout)
        for word in layout.port_words
    )
    assert all(
        descriptor in (MISSING, SELF) or len(descriptor) <= 2
        for descriptor in shortcut_descriptors
    )
    return next_state, extend(scaffold, label, shortcut_descriptors), shortcut_descriptors


def audit_machine_compilation() -> dict[str, int]:
    machines = [
        OriginalMachine(seed + 17 * distance + 31 * degree, degree, distance)
        for degree in (1, 2)
        for distance in (2, 3, 4)
        for seed in range(2)
    ]
    prefixes = [
        word
        for length in range(9)
        for word in itertools.product((0, 1), repeat=length)
    ]
    compiled_runs = 0
    reconstructed_view_checks = 0
    shortcut_edge_checks = 0
    acceptance_checks = 0
    distance_two_descriptor_checks = 0

    for machine in machines:
        layout = ShortcutLayout.make(machine.degree, machine.distance)
        expected_degree = sum(machine.degree**length for length in range(1, machine.distance + 1))
        assert layout.degree == expected_degree
        for prefix in prefixes:
            original = Scaffold((), ())
            compiled = Scaffold((), ())
            original_state = compiled_state = 0
            for symbol in prefix:
                assert reconstruct_original_view(compiled, layout) == root_view(
                    original, machine.distance
                )
                reconstructed_view_checks += 1
                original_state, original, _ = original_step(
                    machine, original_state, original, symbol
                )
                compiled_state, compiled, descriptors = compiled_step(
                    machine, layout, compiled_state, compiled, symbol
                )
                assert compiled_state == original_state
                expected = shortcut_closure(original, layout)
                assert compiled == expected
                shortcut_edge_checks += len(layout.port_words)
                distance_two_descriptor_checks += len(descriptors)
            assert machine.accepting(compiled_state) == machine.accepting(original_state)
            acceptance_checks += 1
            compiled_runs += 1

    return {
        "tiny_original_machines": len(machines),
        "compiled_runs": compiled_runs,
        "reconstructed_view_checks": reconstructed_view_checks,
        "shortcut_edge_checks": shortcut_edge_checks,
        "acceptance_checks": acceptance_checks,
        "distance_two_descriptor_checks": distance_two_descriptor_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 + 1)], 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_symbolic_installation() -> dict[str, int]:
    cases = ((1, 4, 4), (2, 3, 3))
    direct_descriptor_families = 0
    symbolic_shortcuts = 0
    old_scaffolds = 0
    endpoint_matches = 0
    self_shortcuts = 0
    missing_shortcuts = 0
    two_hop_shortcuts = 0

    for degree, distance, nodes in cases:
        layout = ShortcutLayout.make(degree, distance)
        descriptor_options: tuple[Descriptor, ...] = (
            MISSING,
            SELF,
            *words(degree, distance),
        )
        material = list(scaffold_family(nodes, degree))
        old_scaffolds += len(material)
        for direct in itertools.product(descriptor_options, repeat=degree):
            direct_descriptor_families += 1
            compiled_descriptors = tuple(
                compile_shortcut_descriptor(word, direct, layout)
                for word in layout.port_words
            )
            symbolic_shortcuts += len(compiled_descriptors)
            self_shortcuts += sum(descriptor == SELF for descriptor in compiled_descriptors)
            missing_shortcuts += sum(descriptor == MISSING for descriptor in compiled_descriptors)
            two_hop_shortcuts += sum(
                isinstance(descriptor, tuple) and len(descriptor) == 2
                for descriptor in compiled_descriptors
            )
            for old in material:
                original_new = extend(old, 1, direct)
                compiled_old = shortcut_closure(old, layout)
                compiled_new = extend(compiled_old, 1, compiled_descriptors)
                expected = shortcut_closure(original_new, layout)
                assert compiled_new.edges[-1] == expected.edges[-1]
                endpoint_matches += len(layout.port_words)

    return {
        "symbolic_direct_descriptor_families": direct_descriptor_families,
        "symbolic_shortcuts": symbolic_shortcuts,
        "symbolic_old_scaffolds": old_scaffolds,
        "symbolic_endpoint_matches": endpoint_matches,
        "self_shortcuts": self_shortcuts,
        "missing_shortcuts": missing_shortcuts,
        "two_hop_shortcuts": two_hop_shortcuts,
    }


def audit_strict_base_tier() -> dict[str, int]:
    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["distance"] == 2
    assert result["counts"]["residual_profiles"] == 2046
    return {
        "strictness_selector_words": result["counts"]["all_words"],
        "strictness_residual_profiles": result["counts"]["residual_profiles"],
        "strictness_selector_distance": result["distance"],
    }


def main() -> None:
    result: dict[str, object] = {
        "scope": {
            "machine_compilation": "12 machines, degree 1..2, original distance 2..4, all binary prefixes through length 8",
            "symbolic_installation": "all direct descriptor rows for (degree,distance,nodes)=(1,4,4) and (2,3,3)",
            "strictness": "persistent selector through total word length 10",
        },
        **audit_machine_compilation(),
        **audit_symbolic_installation(),
        **audit_strict_base_tier(),
        "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()