check_prefix_profile_access.py

"""Independent finite controls for the restricted prefix-profile access note."""
from itertools import product
import json
from check_complete_level_profiles import Counter, ruler, increment, value


def cube(n):
    return {''.join(w) for w in product('01', repeat=n)}


def full(words, prefix, distance):
    return all(prefix + suffix in words for suffix in cube(distance))


def run():
    evidence = dict(rows=0, sibling_bits=0, cutoff_flags=0,
                    shared_dags=0, distinct_required_nodes=0,
                    flip_transcripts=0, fixed_prefix_witnesses=0,
                    counter_escape_checks=0, slice_frontier_checks=0)
    for n in range(2, 9):
        anchors = set().union(*( { '0'*d+'1'+v for v in cube(n) }
                                for d in range(n)))
        for z in product((0, 1), repeat=n):
            words = anchors | set().union(*(
                {'0'*d+'1'+v for v in cube(n-d-1)} if z[d] else set()
                for d in range(n)))
            assert '0'*n not in words
            for d in range(n):
                for t in range(n+1):
                    assert full(words, '0'*d+'1', t) == (t == n or (t == n-d-1 and bool(z[d])))
                    evidence['sibling_bits'] += 1
            after = words | {'0'*n}
            c = Counter(None, ruler(n))
            for word in words:
                if len(word) == n:
                    c = increment(c)
            old = c
            c = increment(c)
            assert c.full == all(z)
            assert value(old, n) == sum(bit * 2**(n-d-1) for d, bit in enumerate(z))
            evidence['counter_escape_checks'] += 1
            if n in (2, 4, 8) and all(z):
                for width in range(n, 2*n+1):
                    slice_words = {v for v in after if len(v) == width}
                    counts = {}
                    for word in slice_words:
                        for depth in range(width):
                            prefix = word[:depth]
                            counts[prefix] = counts.get(prefix, 0) + 1
                    mixed = sum(count < 2**(width-len(prefix))
                                for prefix, count in counts.items())
                    assert mixed <= n
                    evidence['slice_frontier_checks'] += 1
            cutoff = max((d+1 for d in range(n) if not z[d]), default=0)
            for e in range(n+1):
                assert full(after, '0'*e, n-e) == (e >= cutoff)
                evidence['cutoff_flags'] += 1
            evidence['rows'] += 1

    # Fully hash-cons all suffixes; IDs are oracle bookkeeping, not client operations.
    for n in range(2, 65):
        nodes = []
        intern = {}
        roots = []
        for d in range(n):
            ptr = None
            for k in range(n, -1, -1):
                key = (int(k in (n, n-d-1)), ptr)
                if key not in intern:
                    intern[key] = len(nodes)
                    nodes.append(key)
                ptr = intern[key]
            roots.append(ptr)
        required = []
        targets = []
        for d, ptr in enumerate(roots):
            for k in range(n-d):
                required.append(ptr)
                if k == n-d-1:
                    targets.append(ptr)
                else:
                    ptr = nodes[ptr][1]
        assert len(required) == len(set(required)) == n*(n+1)//2
        # For every omitted target, all remaining node observations are identical
        # after its sole label flips. Pointers and all node IDs stay fixed.
        for target in targets:
            changed = list(nodes)
            changed[target] = (0, nodes[target][1])
            assert all(nodes[i] == changed[i] for i in range(len(nodes)) if i != target)
            values = []
            for d, ptr in enumerate(roots):
                for _ in range(n-d-1):
                    ptr = changed[ptr][1]
                values.append(changed[ptr][0])
            assert sum(values) == n-1
            evidence['flip_transcripts'] += 1
        evidence['shared_dags'] += 1
        evidence['distinct_required_nodes'] += len(required)

    for r in range(6):
        n = r+2
        a, b = '0'*n, '0'*(n-1)+'1'
        universe = cube(n)
        A, B = universe-{a}, universe-{b}
        assert len(A) == len(B)
        for d in range(r+1):
            for p in cube(d):
                for t in range(n+1):
                    assert full(A, p, t) == full(B, p, t)
        assert A | {a} == universe
        assert B | {a} != universe
        evidence['fixed_prefix_witnesses'] += 1
    return evidence


if __name__ == '__main__':
    print(json.dumps(run(), sort_keys=True))