check_namespace_reindexing.py

#!/usr/bin/env python3
"""Finite semantic audit of independently reindexed target namespaces.

Host sets, tuples and graph traversal are independent semantic oracles, not a
native scaffolding simulation or a deadline/lower-bound certificate. Run directly
with Python 3; output is a compact JSON evidence record.
"""
from itertools import permutations, product
import json


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


def words(width):
    return tuple(format(i, '0%db' % width) for i in range(2 ** width))


def instance(width, rows):
    """Construct ordinary right incidences from independently chosen permutations."""
    suffixes = words(width - 1)
    assert 1 <= len(rows) <= len(suffixes)
    assert all(sorted(row) == list(range(len(suffixes))) for row in rows)
    primary = tuple('0' + x for x in suffixes[:len(rows)])
    foreign = tuple('1' + x for x in suffixes)
    right = set()
    targets = []
    expected_owner = {}
    for i, row in enumerate(rows):
        for j, x in enumerate(suffixes):
            q = encode(primary[i]) + x
            targets.append(q)
            right.add((primary[i], q))
            right.add((foreign[row[j]], q))
            expected_owner[q] = foreign[row[j]]
    return primary, foreign, tuple(targets), frozenset(right), expected_owner


def horn_unsat(right, selected, query):
    """Forward closure of implications with positive source, negative target pins."""
    source = ('source', 'a')
    implications = {(source, ('store', b)) for b in selected}
    implications.update((('store', b), ('target', q)) for b, q in right)
    reached = {source}
    while True:
        enlarged = reached | {v for u, v in implications if u in reached}
        if enlarged == reached:
            return ('target', query) in reached
        reached = enlarged


def mixed_count(support, row):
    """Mixed branching nodes in the literal support trie, unary chains suppressed."""
    prefixes = {q[:j] for q in support for j in range(len(q))}
    total = 0
    for prefix in prefixes:
        descendants = {q for q in support if q.startswith(prefix)}
        branches = {q[len(prefix)] for q in descendants}
        if len(branches) == 2 and descendants & row and descendants - row:
            total += 1
    return total


def audit():
    counts = dict(instances=0, activation_vectors=0, queries=0,
                  horn_queries=0, retained_snapshot_queries=0,
                  identity_queries=0, diagonal_examples=0)
    budget_rows = []
    for width, namespace_count in ((2, 1), (2, 2), (3, 1), (3, 2)):
        suffixes = words(width - 1)
        h = len(suffixes)
        for rows in product(tuple(permutations(range(h))), repeat=namespace_count):
            primary, foreign, targets, right, owner = instance(width, rows)
            counts['instances'] += 1
            assert len(right) == 2 * namespace_count * h
            assert all(len(q) == 3 * width + 1 <= 5 * width for q in targets)
            assert all(sum(b == c for b, q in right) == h for c in primary)
            assert all(sum(b == c for b, q in right) == namespace_count for c in foreign)
            assert all(sum(q == z for b, q in right) == 2 for z in targets)
            for b in foreign:
                row = {q for c, q in right if c == b}
                assert len(set(targets) - row) == namespace_count * (h - 1)
                assert mixed_count(targets, row) >= namespace_count
            snapshots = []
            for bits in product((False, True), repeat=h):
                selected = frozenset(b for b, bit in zip(foreign, bits) if bit)
                counts['activation_vectors'] += 1
                direct = frozenset(q for b, q in right if b in selected)
                snapshots.append((selected, direct))
                for q in targets + ('0', '111', targets[0] + '0'):
                    formula = q in owner and owner[q] in selected
                    assert (q in direct) == formula == horn_unsat(right, selected, q)
                    counts['queries'] += 1
                    counts['horn_queries'] += 1
                # Both no-op alias 1 and repeated alias 0 preserve a snapshot.
                after_empty = selected | frozenset()
                assert after_empty == selected
                if selected:
                    assert selected | {next(iter(selected))} == selected
                # All targets in every retained immutable version stay unchanged.
                for old_selected, old_direct in snapshots:
                    for q in targets:
                        assert (q in old_direct) == (owner[q] in old_selected)
                        counts['retained_snapshot_queries'] += 1
            if all(row == tuple(range(h)) for row in rows):
                for selected, direct in snapshots:
                    for i, c in enumerate(primary):
                        for x in suffixes:
                            q = encode(c) + x
                            # Fixed query-side decoder: skip E(c), prefix suffix by 1.
                            assert (q in direct) == ('1' + x in selected)
                            counts['identity_queries'] += 1
    # Growing equal-width examples: exact foreign row sizes and unavoidable
    # coordinate changes in a separately materialized Boolean answer table.
    for width in range(2, 8):
        h = 2 ** (width - 1)
        rows = tuple(tuple((j + i) % h for j in range(h)) for i in range(h))
        primary, foreign, targets, right, owner = instance(width, rows)
        b = foreign[0]
        row = {q for c, q in right if c == b}
        changed = sum(False != (q in row) for q in targets)
        assert changed == h
        mixed = mixed_count(targets, row)
        assert mixed >= h
        budget_rows.append(dict(width=width, namespaces=h, foreign_degree=h,
                                target_length=3 * width + 1, mixed_nodes=mixed,
                                changed_separate_answer_cells=changed))
    # A finite instance of the fixed-family diagonal: enumerate every predicted
    # owner set of size < h at one fixed query and complete a contrary permutation.
    h = 4
    for predicted_bits in product((False, True), repeat=h):
        predicted = {i for i, bit in enumerate(predicted_bits) if bit}
        if len(predicted) == h:
            continue
        absent = min(set(range(h)) - predicted)
        permutation = (absent,) + tuple(i for i in range(h) if i != absent)
        _, foreign, targets, right, owner = instance(3, (permutation,))
        q = targets[0]
        assert owner[q] == foreign[absent]
        assert all(owner[q] != foreign[j] for j in predicted)
        assert horn_unsat(right, {foreign[absent]}, q)
        counts['diagonal_examples'] += 1
    return dict(status='pass', scope='finite relation/Horn semantics, immutable '
                'snapshots, identity routing control, and representation diagnostics; '
                'not native execution or an unrestricted lower bound',
                counts=counts, growth=budget_rows)


if __name__ == '__main__':
    print(json.dumps(audit(), indent=2))