verify_structural_normal_form.py

#!/usr/bin/env python3
"""Finite audit for FPRD-T161 structural scaffold normal form."""

from __future__ import annotations

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


T160_PATH = (
    Path(__file__).parents[1]
    / "distance-two-normal-form"
    / "verify_distance_two_normal_form.py"
)
SPEC = importlib.util.spec_from_file_location("distance_two_normal_form", T160_PATH)
assert SPEC is not None and SPEC.loader is not None
t160 = importlib.util.module_from_spec(SPEC)
sys.modules[SPEC.name] = t160
SPEC.loader.exec_module(t160)

MISSING = t160.MISSING
SELF = t160.SELF
Scaffold = t160.Scaffold
OriginalMachine = t160.OriginalMachine
ShortcutLayout = t160.ShortcutLayout


def marker_width(labels: int, controls: int) -> int:
    """One zero code is reserved for the distinguished base node."""
    return math.ceil(math.log2(1 + labels * controls))


def pair_code(label: int, state: int, labels: int, controls: int) -> int:
    assert 0 <= label < labels and 0 <= state < controls
    return 1 + label * controls + state


def marker_descriptors(code: int, width: int):
    assert 0 <= code < 2**width
    return tuple(SELF if code & (1 << bit) else MISSING for bit in range(width))


def decode_marker_code(scaffold: Scaffold, node: int, marker_start: int, width: int) -> int:
    if node == MISSING:
        raise ValueError("missing is not a labelled node")
    code = 0
    for bit in range(width):
        target = scaffold.edges[node][marker_start + bit]
        assert target in (MISSING, node)
        if target != MISSING:
            code |= 1 << bit
    return code


def decode_pair(code: int, labels: int, controls: int) -> tuple[int, int]:
    assert 1 <= code <= labels * controls
    value = code - 1
    return value // controls, value % controls


@dataclass(frozen=True)
class StructuralLayout:
    shortcuts: ShortcutLayout
    labels: int
    controls: int
    markers: int

    @classmethod
    def make(cls, degree: int, distance: int, labels: int, controls: int):
        shortcuts = ShortcutLayout.make(degree, distance)
        return cls(shortcuts, labels, controls, marker_width(labels, controls))

    @property
    def marker_start(self) -> int:
        return self.shortcuts.degree

    @property
    def degree(self) -> int:
        return self.shortcuts.degree + self.markers


def source_endpoint(compiled: Scaffold, layout: StructuralLayout, prefix: tuple[int, ...]) -> int:
    if not compiled.labels:
        return MISSING
    if not prefix:
        return compiled.top
    return compiled.edges[compiled.top][layout.shortcuts.port_of[prefix]]


def decode_source_label(compiled: Scaffold, layout: StructuralLayout, node: int) -> int:
    code = decode_marker_code(compiled, node, layout.marker_start, layout.markers)
    label, _ = decode_pair(code, layout.labels, layout.controls)
    return label


def reconstruct_source_view(compiled: Scaffold, layout: StructuralLayout):
    if not compiled.labels:
        return ("missing",)

    def build(prefix: tuple[int, ...], remaining: int):
        node = source_endpoint(compiled, layout, prefix)
        if node == MISSING:
            return ("missing",)
        label = decode_source_label(compiled, layout, node)
        if remaining == 0:
            return ("label", label)
        return (
            "node",
            label,
            tuple(
                build(prefix + (port,), remaining - 1)
                for port in range(layout.shortcuts.original_degree)
            ),
        )

    return build((), layout.shortcuts.original_distance)


def reconstruct_source_state(compiled: Scaffold, layout: StructuralLayout, initial: int) -> int:
    if not compiled.labels:
        return initial
    code = decode_marker_code(compiled, compiled.top, layout.marker_start, layout.markers)
    _, state = decode_pair(code, layout.labels, layout.controls)
    return state


def compiled_step(machine: OriginalMachine, layout: StructuralLayout, scaffold: Scaffold, symbol: int):
    state = reconstruct_source_state(scaffold, layout, 0)
    old_view = reconstruct_source_view(scaffold, layout)
    next_state, source_label, direct = machine.transition(state, symbol, old_view)
    shortcuts = tuple(
        t160.compile_shortcut_descriptor(word, direct, layout.shortcuts)
        for word in layout.shortcuts.port_words
    )
    code = pair_code(source_label, next_state, layout.labels, layout.controls)
    descriptors = shortcuts + marker_descriptors(code, layout.markers)
    assert all(
        descriptor in (MISSING, SELF) or len(descriptor) <= 2
        for descriptor in descriptors
    )
    return (
        1 if machine.accepting(next_state) else 0,
        t160.extend(scaffold, 0, descriptors),
        next_state,
        source_label,
    )


def audit_machine_compilation() -> dict[str, int]:
    machines = [
        OriginalMachine(seed + 17 * distance + 31 * degree, degree, distance)
        for degree in (1, 2)
        for distance in (1, 2, 3)
        for seed in range(2)
    ]
    prefixes = [
        word
        for length in range(8)
        for word in itertools.product((0, 1), repeat=length)
    ]
    compiled_runs = 0
    transition_checks = 0
    view_checks = 0
    state_checks = 0
    shortcut_checks = 0
    marker_checks = 0
    acceptance_checks = 0
    unary_label_checks = 0
    two_control_checks = 0

    for machine in machines:
        layout = StructuralLayout.make(
            machine.degree, machine.distance, machine.labels, machine.controls
        )
        expected_degree = sum(
            machine.degree**length for length in range(1, machine.distance + 1)
        ) + marker_width(machine.labels, machine.controls)
        assert layout.degree == expected_degree
        for prefix in prefixes:
            source = Scaffold((), ())
            compiled = Scaffold((), ())
            source_state = 0
            physical_control = 1 if machine.accepting(0) else 0
            created_pairs: list[tuple[int, int]] = []
            for symbol in prefix:
                assert reconstruct_source_view(compiled, layout) == t160.root_view(
                    source, machine.distance
                )
                view_checks += 1
                assert reconstruct_source_state(compiled, layout, 0) == source_state
                state_checks += 1

                source_state, source, _ = t160.original_step(
                    machine, source_state, source, symbol
                )
                physical_control, compiled, decoded_state, decoded_label = compiled_step(
                    machine, layout, compiled, symbol
                )
                created_pairs.append((decoded_label, decoded_state))
                transition_checks += 1

                assert decoded_state == source_state
                assert decoded_label == source.labels[-1]
                assert all(label == 0 for label in compiled.labels)
                unary_label_checks += len(compiled.labels)
                assert physical_control in (0, 1)
                two_control_checks += 1
                assert bool(physical_control) == machine.accepting(source_state)
                acceptance_checks += 1

                closure = t160.shortcut_closure(source, layout.shortcuts)
                for node in range(len(source.labels)):
                    assert compiled.edges[node][: layout.marker_start] == closure.edges[node]
                    shortcut_checks += layout.marker_start
                    code = decode_marker_code(
                        compiled, node, layout.marker_start, layout.markers
                    )
                    assert decode_pair(code, machine.labels, machine.controls) == created_pairs[node]
                    marker_checks += layout.markers
            assert bool(physical_control) == machine.accepting(source_state)
            compiled_runs += 1

    return {
        "tiny_source_machines": len(machines),
        "compiled_runs": compiled_runs,
        "transition_checks": transition_checks,
        "view_reconstruction_checks": view_checks,
        "state_reconstruction_checks": state_checks,
        "shortcut_edge_checks": shortcut_checks,
        "marker_bit_checks": marker_checks,
        "acceptance_checks": acceptance_checks,
        "unary_label_checks": unary_label_checks,
        "two_control_checks": two_control_checks,
    }


def audit_codes() -> dict[str, int]:
    parameter_pairs = 0
    ordinary_codes = 0
    marker_roundtrips = 0
    base_zero_checks = 0
    unused_codes = 0
    for labels in range(1, 9):
        for controls in range(1, 9):
            parameter_pairs += 1
            width = marker_width(labels, controls)
            assert 2**width >= 1 + labels * controls
            assert width == 0 or 2 ** (width - 1) < 1 + labels * controls
            base_zero_checks += 1
            for label in range(labels):
                for state in range(controls):
                    code = pair_code(label, state, labels, controls)
                    descriptors = marker_descriptors(code, width)
                    recovered = sum(
                        (1 << bit) for bit, descriptor in enumerate(descriptors) if descriptor == SELF
                    )
                    assert recovered == code
                    assert decode_pair(recovered, labels, controls) == (label, state)
                    ordinary_codes += 1
                    marker_roundtrips += width
            unused_codes += 2**width - (1 + labels * controls)
    return {
        "code_parameter_pairs": parameter_pairs,
        "ordinary_pair_codes": ordinary_codes,
        "marker_roundtrip_bits": marker_roundtrips,
        "base_zero_checks": base_zero_checks,
        "unused_structural_codes": unused_codes,
    }


def main() -> None:
    result: dict[str, object] = {
        "scope": {
            "machine_compilation": "12 machines, degree 1..2, source distance 1..3, all binary prefixes through length 7",
            "structural_codes": "all working-alphabet and control sizes 1..8",
            "base_node": "zero code reserved; every ordinary label-state pair uses a nonzero marker code",
        },
        **audit_machine_compilation(),
        **audit_codes(),
        "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()