verify_native_structural_normal_form.py

#!/usr/bin/env python3
"""T160/T161 audit at the native LMR view boundary; no external dependencies.

Transitions receive only a finite unfolded view, never a graph or node ID.
None is both the missing view and the unlabelled base's radius-zero view.
Graph IDs are available only to the interpreter and the invariant checker.
"""
from __future__ import annotations

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

MISSING, SELF = -1, -2


@dataclass(frozen=True)
class Graph:
    labels: tuple
    edges: tuple

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


def base(degree):
    return Graph((None,), ((MISSING,) * degree,))


def follow(graph, node, word):
    for port in word:
        if node == MISSING:
            break
        node = graph.edges[node][port]
    return node


def view(graph, node, radius):
    if node == MISSING:
        return None
    if radius == 0:
        return graph.labels[node]
    return (graph.labels[node], tuple(view(graph, target, radius - 1)
                                     for target in graph.edges[node]))


def extend(graph, label, descriptors):
    assert label is not None  # Only the initial node is unlabelled.
    targets = tuple(MISSING if p == MISSING else len(graph.labels) if p == SELF
                    else follow(graph, graph.top, p) for p in descriptors)
    assert all(MISSING <= target <= len(graph.labels) for target in targets)
    return Graph(graph.labels + (label,), graph.edges + (targets,))


@dataclass(frozen=True)
class Layout:
    degree: int
    distance: int
    labels: int
    controls: int

    @property
    def words(self):
        return tuple(w for n in range(1, self.distance + 1)
                     for w in product(range(self.degree), repeat=n))

    @property
    def marker_width(self):
        return (self.labels * self.controls).bit_length()


def shortcut_descriptor(word, direct, ports):
    for index, port in enumerate(word):
        path = direct[port]
        if path == MISSING:
            return MISSING
        if path == SELF:
            continue
        suffix = word[index + 1:]
        return tuple(ports[w] for w in (path, suffix) if w)
    return SELF


def marker_code(node_view, layout):
    # Each marker's radius-zero or radius-one endpoint is present iff bit=1.
    assert node_view is not None and isinstance(node_view, tuple)
    return sum(1 << bit for bit, child in
               enumerate(node_view[1][len(layout.words):]) if child is not None)


def decode_pair(node_view, layout, initial):
    code = marker_code(node_view, layout)
    if code == 0:
        assert node_view[0] is None
        return None, initial
    assert node_view[0] == 0 and 1 <= code <= layout.labels * layout.controls
    return divmod(code - 1, layout.controls)


def reconstruct(native_two_view, layout, structural, initial=0):
    """Pure function of N_2. It has no graph, node IDs, or pointer-equality test."""
    ports = {w: index for index, w in enumerate(layout.words)}

    def build(prefix, remaining):
        endpoint = native_two_view if not prefix else native_two_view[1][ports[prefix]]
        if endpoint is None:
            return None
        label = decode_pair(endpoint, layout, initial)[0] if structural else endpoint[0]
        if remaining == 0:
            return label  # Deliberately collapse base and missing at depth zero.
        return (label, tuple(build(prefix + (p,), remaining - 1)
                             for p in range(layout.degree)))

    return build((), layout.distance)


def score(value):
    if value is None:
        return 17
    if isinstance(value, int):
        return value + 31
    return 19 + sum((i + 3) * score(v) for i, v in enumerate(value))


@dataclass(frozen=True)
class Machine:
    layout: Layout
    seed: int

    @property
    def initial(self):
        return self.seed % self.layout.controls

    def accepting(self, state):
        return state == (self.seed // 2) % self.layout.controls

    def transition(self, state, symbol, old_view):
        layout = self.layout
        code = score((state, symbol, old_view, self.seed))
        options = (MISSING, SELF, (), *layout.words)
        return ((code + symbol) % layout.controls,
                (code // 7) % layout.labels,
                tuple(options[(code // (p + 1) + 13 * p) % len(options)]
                      for p in range(layout.degree)))


def compiled_transition(machine, symbol, native_two_view, structural, control):
    layout = machine.layout
    source_state = decode_pair(native_two_view, layout, machine.initial)[1] if structural else control
    source_view = reconstruct(native_two_view, layout, structural, machine.initial)
    state, label, direct = machine.transition(source_state, symbol, source_view)
    ports = {w: i for i, w in enumerate(layout.words)}
    descriptors = tuple(shortcut_descriptor(w, direct, ports) for w in layout.words)
    if structural:
        code = 1 + label * layout.controls + state
        descriptors += tuple(SELF if code & (1 << bit) else MISSING
                             for bit in range(layout.marker_width))
    assert all(p in (MISSING, SELF) or len(p) <= 2 for p in descriptors)
    return (int(machine.accepting(state)) if structural else state,
            0 if structural else label, descriptors)


def closure(source, history, layout, structural):
    edges = []
    labels = []
    for node, label in enumerate(source.labels):
        row = tuple(follow(source, node, w) for w in layout.words)
        if structural:
            code = 0 if node == 0 else 1 + label * layout.controls + history[node - 1]
            row += tuple(node if code & (1 << bit) else MISSING
                         for bit in range(layout.marker_width))
        edges.append(row)
        labels.append(None if node == 0 else 0 if structural else label)
    return Graph(tuple(labels), tuple(edges))


def audit_runs(counts):
    words = tuple(w for n in range(8) for w in product((0, 1), repeat=n))
    for degree, distance, (labels, controls), seed in product(
            (1, 2), (1, 2, 3), ((1, 1), (2, 3)), (0, 1)):
        layout = Layout(degree, distance, labels, controls)
        machine = Machine(layout, seed)
        counts['source_machines'] += 1
        for word in words:
            source = base(degree)
            shortcut = base(len(layout.words))
            structural = base(len(layout.words) + layout.marker_width)
            state = shortcut_state = machine.initial
            physical = int(machine.accepting(state))
            history = ()
            counts['native_base_initializations'] += 1
            for symbol in (*word, None):
                source_view = view(source, source.top, distance)
                for graph, coded in ((shortcut, False), (structural, True)):
                    assert reconstruct(view(graph, graph.top, 2), layout, coded,
                                       machine.initial) == source_view
                    counts['native_view_reconstructions'] += 1
                assert decode_pair(view(structural, structural.top, 2), layout,
                                   machine.initial)[1] == state
                assert shortcut_state == state
                assert bool(physical) == machine.accepting(state)
                counts['prefix_acceptance_checks'] += 1
                if symbol is None:
                    break
                next_state, label, direct = machine.transition(state, symbol, source_view)
                shortcut_state, slabel, srow = compiled_transition(
                    machine, symbol, view(shortcut, shortcut.top, 2), False, shortcut_state)
                physical, plabel, prow = compiled_transition(
                    machine, symbol, view(structural, structural.top, 2), True, physical)
                source = extend(source, label, direct)
                shortcut = extend(shortcut, slabel, srow)
                structural = extend(structural, plabel, prow)
                state = next_state
                history += (state,)
                assert shortcut == closure(source, history, layout, False)
                assert structural == closure(source, history, layout, True)
                counts['paired_transition_checks'] += 1
                counts['native_base_endpoint_visits'] += sum(
                    follow(source, source.top, w) == 0 for w in layout.words)
            counts['compiled_runs'] += 1


def graphs(degree, size):
    if size == 1:
        yield base(degree)
        return
    for graph in graphs(degree, size - 1):
        for label in (0, 1):
            for row in product(range(MISSING, size), repeat=degree):
                yield Graph(graph.labels + (label,), graph.edges + (row,))


def audit_arbitrary_views(counts):
    # All legal backward graphs of these sizes, including old SELF loops and
    # distinct graphs with the same unfolded view. Node zero stays native.
    for degree, max_size in ((1, 4), (2, 3)):
        for size in range(1, max_size + 1):
            for source in graphs(degree, size):
                counts['native_graphs'] += 1
                for history in product((0, 1), repeat=size - 1):
                    for distance in (1, 2, 3):
                        layout = Layout(degree, distance, 2, 2)
                        for coded in (False, True):
                            compiled = closure(source, history, layout, coded)
                            assert reconstruct(view(compiled, compiled.top, 2), layout,
                                               coded, 1) == view(source, source.top, distance)
                            counts['exhaustive_native_view_checks'] += 1
                        assert decode_pair(view(compiled, compiled.top, 2), layout, 1)[1] == (
                            history[-1] if history else 1)
                        counts['exhaustive_state_checks'] += 1


def audit_boundary_witnesses():
    layout = Layout(1, 2, 1, 1)
    reaches_base = Graph((None, 0), ((MISSING,), (0,)))
    reaches_missing = Graph((None, 0), ((MISSING,), (MISSING,)))
    left = closure(reaches_base, (0,), layout, False)
    right = closure(reaches_missing, (0,), layout, False)
    assert view(left, 1, 1) == view(right, 1, 1)
    assert view(reaches_base, 1, 2) != view(reaches_missing, 1, 2)
    assert view(left, 1, 2) != view(right, 1, 2)
    for source, compiled in ((reaches_base, left), (reaches_missing, right)):
        assert reconstruct(view(compiled, 1, 2), layout, False) == view(source, 1, 2)
    native_base = base(1)
    assert view(native_base, 0, 0) == view(native_base, MISSING, 0)
    assert view(native_base, 0, 1) != view(native_base, MISSING, 1)
    # A source observer that accepts exactly a nonmissing radius-one root
    # distinguishes the first native step from the old empty-graph convention.
    assert (view(native_base, 0, 1) is not None) != (None is not None)
    coded_base = base(len(layout.words) + layout.marker_width)
    assert decode_pair(view(coded_base, 0, 2), layout, 0) == (None, 0)
    # Full ordinary pair code coverage is separate from actual base executions.
    pair_checks = 0
    for labels, controls in product(range(1, 9), repeat=2):
        code_layout = Layout(1, 1, labels, controls)
        width = code_layout.marker_width
        assert 2 ** (width - 1) < 1 + labels * controls <= 2 ** width
        for label, state in product(range(labels), range(controls)):
            code = 1 + label * controls + state
            graph = extend(base(1 + width), 0,
                           (MISSING,) + tuple(SELF if code & (1 << bit) else MISSING
                                              for bit in range(width)))
            assert decode_pair(view(graph, graph.top, 1), code_layout, 0) == (label, state)
            pair_checks += 1
    return {'radius_one_collision_witness': True,
            'radius_two_repairs_collision': True,
            'empty_graph_mutation_detected': True,
            'base_zero_decoded_in_native_view': True,
            'ordinary_pair_roundtrips': pair_checks}


def main():
    counts = Counter()
    audit_runs(counts)
    audit_arbitrary_views(counts)
    output = {'status': 'pass', 'model': 'LMR Definitions 10-15, native unlabelled base',
              'compiler_observation': 'only the unfolded radius-two view; no node IDs',
              **dict(counts), **audit_boundary_witnesses(),
              'scope': 'Finite executable checks, not a formal proof or exhaustive machine search.'}
    target = Path(__file__).with_name('native-checker-output.json')
    target.write_text(json.dumps(output, indent=2) + '\n')
    print(json.dumps(output, indent=2))


if __name__ == '__main__':
    main()