check_virtual_initialization.py

#!/usr/bin/env python3
"""Finite commutation audit, not a proof of the general batch compiler.

One root, one field, one fresh slot, old radius one; every fixed initial
graph of <=2 binary-labelled records, every root, and every two-plan sequence.
Virtual references occupy finite tags and have no physical edge.
"""
from itertools import product
import json

M = None


def virtual_graphs():
    for h in range(3):
        pointers = [M] + [('V', i) for i in range(h)]
        for labels in product(range(2), repeat=h):
            for fields in product(pointers, repeat=h):
                table = tuple(zip(labels, fields))
                for root in pointers:
                    yield table, root


def plans():
    # M, old root, and one field below old root. F is the current fresh slot.
    for root in ('M', 'O0', 'O1'):
        yield None, None, root
    for label, field, root in product(range(2), ('M', 'O0', 'O1', 'F'), ('M', 'O0', 'O1', 'F')):
        yield label, field, root


def source_read(pointer, table, records):
    return table[pointer[1]] if pointer[0] == 'V' else records[pointer[1]]


def source_target(expr, root, table, records, tick):
    if expr == 'M':
        return M
    if expr == 'F':
        return ('D', tick)
    if expr == 'O0' or root is M:
        return root
    return source_read(root, table, records)[1]


def port(pointer):
    # Tag is stored at the source port, not inferred from target-node identity.
    if pointer is M:
        return ('M', None), None
    if pointer[0] == 'V':
        return pointer, None
    return ('D', 0), pointer[1]


def unport(tag_and_edge):
    tag, edge = tag_and_edge
    return M if tag[0] == 'M' else tag if tag[0] == 'V' else ('D', edge)


def compiled_target(expr, initial_root, table, nodes, tick):
    if expr == 'M':
        return M, 0
    if expr == 'F':
        return ('D', tick), 0  # SELF descriptor
    if tick == 1:
        p = initial_root
        length = 0
    else:
        p = unport(nodes[tick - 1]['root'])
        length = 1 if p is not M and p[0] == 'D' else 0
    if expr == 'O1' and p is not M:
        if p[0] == 'V':
            p = table[p[1]][1]  # fixed table: no physical traversal
        else:
            p = unport(nodes[p[1]]['field'])
            length += 1
    if p is not M and p[0] == 'D':
        assert p[1] < tick
    assert length <= 2  # r+1, including the root port
    return p, length


def step(plan, root, table, records, nodes, initial_root):
    tick = len(nodes)
    label, field_expr, root_expr = plan
    fields = None
    dynamic = dict(records)
    if label is not None:
        fields = source_target(field_expr, root, table, records, tick)
        dynamic[tick] = (label, fields)
    new_root = source_target(root_expr, root, table, records, tick)
    physical_root, root_length = compiled_target(root_expr, initial_root, table, nodes, tick)
    assert physical_root == new_root
    field_length = 0
    if label is not None:
        physical_field, field_length = compiled_target(field_expr, initial_root, table, nodes, tick)
        assert physical_field == fields
    else:
        physical_field = M
    encoded = nodes + [{'label': label, 'field': port(physical_field), 'root': port(physical_root)}]
    assert len(encoded) == len(nodes) + 1
    assert len(dynamic) - len(records) <= 1
    assert unport(encoded[-1]['root']) == new_root
    for birth, (tag, target) in dynamic.items():
        assert encoded[birth]['label'] == tag
        assert unport(encoded[birth]['field']) == target
    return new_root, dynamic, encoded, max(root_length, field_length)


def main():
    initial_count = first_steps = second_steps = 0
    max_path = 0
    all_plans = tuple(plans())
    for table, initial_root in virtual_graphs():
        initial_count += 1
        # At time zero the finite table and initialization state decode the
        # entire initial graph, even when H>A. No scaffold node is allocated.
        assert all(p is M or p[0] == 'V' for _, p in table)
        for first in all_plans:
            root, records, nodes, length = step(first, initial_root, table, {}, [None], initial_root)
            first_steps += 1
            max_path = max(max_path, length)
            for second in all_plans:
                _, _, _, length = step(second, root, table, records, nodes, initial_root)
                second_steps += 1
                max_path = max(max_path, length)
    assert initial_count == 117 and len(all_plans) == 35
    assert second_steps == 143325 and max_path == 2
    print(json.dumps({'status': 'pass', 'initial_graph_root_configurations': initial_count,
                     'plans': len(all_plans), 'one_step_checks': first_steps,
                     'two_step_checks': second_steps, 'maximum_physical_path': max_path,
                     'parameters': {'roots': 1, 'fresh_slots': 1, 'fields': 1, 'old_radius': 1},
                     'scope': 'Finite virtual-table and dynamic-slot commutation; not a full compiler or sequence-implementation verification.'}, indent=2))


if __name__ == '__main__':
    main()