check_routed_contexts_independent.py

#!/usr/bin/env python3
"""Independent routing-semantics audit; imports no primary checker.

Finite Python sets/maps are semantic oracles, not native instructions. This
checks the routing wrapper, not theorem 68's producer or its deadline proof.
"""
from itertools import product
import json


def binary_words(maximum):
    return [''.join(bits) for n in range(maximum + 1)
            for bits in product('01', repeat=n)]


def encode(group):
    return ''.join('0' + bit for bit in group) + '11'


def split(name):
    """Streaming-pair syntax oracle, including a nonempty local suffix."""
    group = []
    offset = 0
    while offset + 1 < len(name):
        pair = name[offset:offset + 2]
        offset += 2
        if pair == '11':
            suffix = name[offset:]
            return (''.join(group), suffix) if suffix else None
        if pair not in ('00', '01'):
            return None
        group.append(pair[1])
    return None


def route_rows(edges):
    rows = {}
    for alias, target in edges:
        left, right = split(alias), split(target)
        if left is None or right is None or left[0] != right[0]:
            return None
        group, local = left
        key = group, local
        rows[key] = rows.get(key, frozenset()) | {right[1]}
    return rows


def select(previous, rows, alias):
    parsed = split(alias)
    assert parsed is not None
    group, local = parsed
    current = dict(previous)
    current[group] = current.get(group, frozenset()) | rows.get(
        (group, local), frozenset())
    return current


def answer(version, target):
    parsed = split(target)
    assert parsed is not None
    group, local = parsed
    return local in version.get(group, frozenset())


def run():
    counts = dict(parser_words=0, prefix_pairs=0, relations=0,
                  selection_versions=0, query_checks=0,
                  duplicate_and_missing_checks=0, failure_controls=0)
    groups = binary_words(4)
    codes = [encode(group) for group in groups]
    for i, first in enumerate(codes):
        for j, second in enumerate(codes):
            if i != j:
                assert not second.startswith(first)
                counts['prefix_pairs'] += 1
    for word in binary_words(11):
        result = split(word)
        # Independent definition: enumerate every possible delimiter position.
        candidates = []
        for stop in range(0, len(word) - 2, 2):
            pairs = [word[i:i + 2] for i in range(0, stop, 2)]
            if word[stop:stop + 2] == '11' and all(
                    pair in ('00', '01') for pair in pairs):
                candidates.append((''.join(pair[1] for pair in pairs),
                                   word[stop + 2:]))
        assert result == (candidates[0] if candidates else None)
        assert len(candidates) <= 1
        if result is not None:
            assert encode(result[0]) + result[1] == word
        counts['parser_words'] += 1
    for depth in (16, 64, 257):
        group = '01' * depth
        assert split(encode(group) + '0') == (group, '0')

    # Each nonempty group's local records also fit K=1,d=2,s=1:
    # aliases have length one and residual targets have length two.
    contexts = {'': '', '0': '000', '01': '10101'}
    aliases = [encode(group) + bit for group in contexts for bit in '01']
    edges = [(alias, encode(split(alias)[0]) + contexts[split(alias)[0]] + y)
             for alias in aliases for y in ('00', '01')]
    queries = [encode(group) + prefix + tail
               for group, prefix in contexts.items()
               for tail in ('00', '01', '10', '11')]
    queries += [encode('10') + '0', encode('') + '0']
    missing = encode('10') + '0'
    for relation_mask in range(1 << len(edges)):
        relation = [edge for i, edge in enumerate(edges)
                    if relation_mask >> i & 1]
        # Reverse order and duplicates exercise row interleaving/idempotence.
        records = relation[::2] + relation[1::2][::-1] + relation[:1]
        rows = route_rows(records)
        assert rows is not None
        versions = [{}]
        selected = [frozenset()]
        for mask in range(1, 1 << len(aliases)):
            bit = mask.bit_length() - 1
            predecessor = mask ^ (1 << bit)
            saved = dict(versions[predecessor])
            versions.append(select(versions[predecessor], rows, aliases[bit]))
            selected.append(selected[predecessor] | {aliases[bit]})
            assert versions[predecessor] == saved
        for version, chosen in zip(versions, selected):
            expected = {target for alias, target in relation if alias in chosen}
            for query in queries:
                assert answer(version, query) == (query in expected)
                counts['query_checks'] += 1
            counts['selection_versions'] += 1
        full = versions[-1]
        repeated = select(select(full, rows, aliases[0]), rows, missing)
        for query in queries:
            assert answer(repeated, query) == answer(full, query)
            counts['duplicate_and_missing_checks'] += 1
        counts['relations'] += 1

    # Removing the common-route gate makes a selected target invisible.
    alias, target = encode('0') + '0', encode('1') + '0'
    assert route_rows([(alias, target)]) is None
    invalid_wrapper_version = {'0': frozenset({'0'})}
    cross_relation, selected_aliases = [(alias, target)], {alias}
    direct = {word for name, word in cross_relation if name in selected_aliases}
    assert target in direct and not answer(invalid_wrapper_version, target)
    counts['failure_controls'] += 1
    # Overlapping context prefixes are not uniquely dispatched by spelling.
    query = '000'
    kernels = {'0': frozenset({'00'}), '00': frozenset()}
    exact = any(query.startswith(prefix) and query[len(prefix):] in values
                for prefix, values in kernels.items())
    longest = max((prefix for prefix in kernels if query.startswith(prefix)),
                  key=len)
    one_reader = query[len(longest):] in kernels[longest]
    assert exact and not one_reader
    counts['failure_controls'] += 1
    return counts


if __name__ == '__main__':
    print(json.dumps({'status': 'passed', 'scope': 'routing semantics only',
                      **run()}, sort_keys=True))