check_owner_graph_kernel.py

#!/usr/bin/env python3
"""Finite semantic audit of full-row store composition as graph activation.

Host sets, integers and graph traversal are independent semantic oracles, not a
native implementation or timing bound. All stores/edges have ordinary literal
names; the serialized instance contains every incidence and selection. There
are no supplied graph handles in the audited language representation.
"""
from itertools import combinations, product
import json


def encode_store(word):
    return ''.join('00' if bit == '0' else '01' for bit in word) + '11'


def middle(store, alias):
    return '01' + encode_store(store) + alias


def closure(clauses, source):
    # Direct least-model evaluation, independent of the graph endpoint oracle.
    reached = {source}
    while True:
        additions = {y for x, y in clauses if x in reached} - reached
        if not additions:
            return reached
        reached.update(additions)


def brute_sat(clauses, source, target):
    names = sorted({source, target} | {x for pair in clauses for x in pair})
    free = [x for x in names if x not in (source, target)]
    for bits in product((False, True), repeat=len(free)):
        assignment = dict(zip(free, bits))
        assignment.update({source: True, target: False})
        if all(not assignment[x] or assignment[y] for x, y in clauses):
            return True
    return False


def instance(edges, active):
    vertices = sorted({v for e in edges for v in e})
    # Variable-width ordinary store names and common-width ordinary edge names.
    stores = {v: '1' * (v + 1) + '0' for v in vertices}
    width = max(1, (len(edges) - 1).bit_length())
    targets = {e: format(i, f'0{width}b') for i, e in enumerate(edges)}
    source = '00' + '101'
    right = []
    for v in vertices:  # Once-only groups, no externally supplied decomposition.
        for e in edges:
            if v in e:
                right.append((middle(stores[v], '0'), '1' + targets[e]))
    # Mention every store; missing alias 1 denotes an empty row.
    left = [(source, middle(stores[v], '0' if v in active else '1'))
            for v in vertices]
    text = ''.join(f'(-{x},+{y});' for x, y in right + left)
    # Parse the actual literal implication fields back out, without graph IDs.
    parsed = []
    for record in text.split(';'):
        if record:
            x, y = record[1:-1].split(',')
            assert x.startswith('-') and y.startswith('+')
            parsed.append((x[1:], y[1:]))
    assert parsed == right + left
    return parsed, source, targets, len(text), right


def run():
    counts = dict(graphs=0, source_subsets=0, edge_queries=0,
                  brute_sat_queries=0, encoded_symbols=0, star_examples=0)
    for size in range(2, 6):
        possible = list(combinations(range(size), 2))
        for mask in range(1, 1 << len(possible)):
            edges = [e for i, e in enumerate(possible) if mask >> i & 1]
            vertices = sorted({v for e in edges for v in e})
            counts['graphs'] += 1
            for bits in product((False, True), repeat=len(vertices)):
                active = {v for v, bit in zip(vertices, bits) if bit}
                clauses, source, targets, length, right = instance(edges, active)
                reached = closure(clauses, source)
                counts['source_subsets'] += 1
                counts['encoded_symbols'] += length
                for e, q in targets.items():
                    target = '1' + q
                    endpoint_or = any(v in active for v in e)
                    assert (target in reached) == endpoint_or
                    # Independent relational product via matching literal middle names.
                    selected = {y for x, y in clauses if x == source}
                    composed = any(x in selected and y == target for x, y in right)
                    assert composed == endpoint_or
                    # A Horn closure avoiding the negative pin itself supplies a model.
                    sat_model = all(x not in reached or y in reached for x, y in clauses)
                    assert sat_model
                    assert (target not in reached) == (not endpoint_or)
                    counts['edge_queries'] += 1
                    if size <= 3:
                        assert brute_sat(clauses, source, target) == (not endpoint_or)
                        counts['brute_sat_queries'] += 1
                # Off-support ordinary target, including a different width, stays false.
                assert '1' + '0' * (len(next(iter(targets.values()))) + 1) not in reached
    stars = []
    for leaves in (1, 2, 4, 8, 16, 32, 64):
        edges = [(0, v) for v in range(1, leaves + 1)]
        on, source, targets, _, right = instance(edges, {0})
        off, _, _, _, _ = instance(edges, set())
        owners = {q: {x for x, y in right if y == '1' + q} for q in targets.values()}
        assert all(len(v) == 2 for v in owners.values())
        changed = {('1' + q) for q in targets.values()} & (closure(on, source) - closure(off, source))
        assert len(changed) == leaves
        stars.append(dict(leaves=leaves, max_target_owners=2,
                          center_row_degree=leaves, changed_answers=len(changed)))
        counts['star_examples'] += 1
    return dict(status='pass', scope='finite literal/Horn semantics, not native execution or a timing lower bound',
                counts=counts, stars=stars)


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