check_persistent_selector_contracts.py

#!/usr/bin/env python3
"""Finite semantic audit of Dietz's traversal-run selector decomposition.

Rebuilding Python lists is an oracle, not the paper's dynamic implementation.
Initial default run starts share one sentinel and are excluded from the
noninitial boundary-incidence bound. No native transfer is asserted.
"""
import bisect
from collections import Counter
import json
import random


def traversal(children):
    result = []
    def visit(v):
        result.append(v)
        for child in children[v]:
            visit(child)
        result.append(v)
    visit(0)
    return result


def ancestor_value(parent, writes, v, index):
    while v:
        stored_index, value = writes[v]
        if stored_index == index:
            return value
        v = parent[v]
    return 0


def audit_tree(parent, writes, children, indices):
    order = traversal(children)
    first = {}
    for pos, v in enumerate(order):
        first.setdefault(v, pos)
    boundaries = Counter()
    total_runs = reads = 0
    written = Counter(i for i, _ in writes.values())
    for i in range(indices):
        values = [ancestor_value(parent, writes, v, i) for v in order]
        starts = [0] + [p for p in range(1, len(values)) if values[p] != values[p - 1]]
        payloads = [values[p] for p in starts]
        assert len(starts) <= 2 * written[i] + 1
        total_runs += len(starts)
        for p in starts[1:]:
            boundaries[p] += 1
        for v, p in first.items():
            j = bisect.bisect_right(starts, p) - 1
            assert payloads[j] == ancestor_value(parent, writes, v, i)
            reads += 1
    assert all(count <= 2 for count in boundaries.values())
    return reads, total_runs, len(boundaries), max(boundaries.values(), default=0)


def run_audits():
    rng = random.Random(245)
    trees = reads = runs = boundaries = snapshots = 0
    maximum_boundary = 0
    for indices in (1, 2, 7, 17, 64):
        for shape in ('chain', 'star', 'branched'):
            parent, writes, children = {0: None}, {}, {0: []}
            frozen = {}
            for v in range(1, 121):
                p = v - 1 if shape == 'chain' else 0 if shape == 'star' else rng.randrange(v)
                parent[v] = p
                writes[v] = rng.randrange(indices), rng.randrange(5)
                children[v] = []
                # Both left and right sibling insertions exercise traversal reorder.
                children[p].insert(rng.randrange(len(children[p]) + 1), v)
                if v % 20 == 0:
                    a, b, c, d = audit_tree(parent, writes, children, indices)
                    reads += a
                    runs += b
                    boundaries += c
                    maximum_boundary = max(maximum_boundary, d)
                    trees += 1
                    for (old_v, i), value in frozen.items():
                        assert ancestor_value(parent, writes, old_v, i) == value
                        snapshots += 1
                    frozen.update({(old_v, i): ancestor_value(parent, writes, old_v, i)
                                   for old_v in range(v + 1) for i in range(indices)})
    return trees, reads, runs, boundaries, maximum_boundary, snapshots


def shared_record_control():
    # Brodal §4 deliberately uses one mutable shared component record.
    # A raw pointer alias is not by itself a persistent snapshot.
    component = {'colour': 'white', 'root': 3}
    members = [{'cr': component} for _ in range(12)]
    alleged_snapshot = members[0]['cr']
    before = dict(alleged_snapshot)
    component['colour'] = 'black'
    component['root'] = None
    assert all(x['cr']['colour'] == 'black' for x in members)
    assert alleged_snapshot != before
    # Copying just that record preserves old aliases, but new member routing
    # is then a separate task. This is illustrative, not a game simulation.
    old_component = {'colour': 'white', 'root': 3}
    new_component = dict(old_component, colour='black', root=None)
    assert old_component['colour'] == 'white' and new_component['colour'] == 'black'
    return 1


def sentinel_control():
    indices = 17
    starts = {i: [0] for i in range(indices)}
    assert sum(0 in s for s in starts.values()) == 17
    assert sum(any(p > 0 for p in s) for s in starts.values()) == 0
    return indices


def main():
    trees, reads, runs, boundaries, maximum, snapshots = run_audits()
    print(json.dumps({'seed': 245, 'version_tree_snapshots': trees,
                      'ancestor_vs_run_predecessor_reads': reads,
                      'run_intervals_checked': runs,
                      'noninitial_boundary_checks': boundaries,
                      'maximum_noninitial_incidence': maximum,
                      'retained_branch_value_checks': snapshots,
                      'shared_initial_sentinel_indices': sentinel_control(),
                      'brodal_shared_record_illustrations': shared_record_control(),
                      'status': 'passed'}, indent=2))


if __name__ == '__main__':
    main()