check_mixed_region_coupling.py

#!/usr/bin/env python3
"""Independent finite audit of one-time mixed-coordinate charging.
Canonical aligned Boolean trees; counts are tree-coordinate occurrences,
not distinct DAG records. Integer masks are independent semantic oracles.
"""
from itertools import product
from random import Random
import json


def tree(mask, height):
    width = 1 << height
    if mask == 0:
        return False
    if mask == (1 << width) - 1:
        return True
    half = width // 2
    return (tree(mask & ((1 << half) - 1), height - 1),
            tree(mask >> half, height - 1))


def mixed(t, path=()):
    if isinstance(t, bool):
        return set()
    return {path} | mixed(t[0], path + (0,)) | mixed(t[1], path + (1,))


def merge(a, b, expanded, path=()):
    if b is False:
        return a
    if b is True or a is True:
        return True
    if a is False:
        return b
    expanded.add(path)
    left = merge(a[0], b[0], expanded, path + (0,))
    right = merge(a[1], b[1], expanded, path + (1,))
    if left is True and right is True:
        return True
    if left is False and right is False:
        return False
    return (left, right)


def check(a_mask, c_mask, incoming, height):
    base = tree(a_mask, height)
    c = tree(c_mask, height)
    augmented = merge(base, c, set())
    potential = mixed(c)
    charged = set()
    base_expansions = augmented_expansions = 0
    for mask in incoming:
        b = tree(mask, height)
        old_events, new_events = set(), set()
        base = merge(base, b, old_events)
        augmented = merge(augmented, b, new_events)
        extra = new_events - old_events
        assert extra <= potential
        assert not (extra & charged)
        charged |= extra
        base_expansions += len(old_events)
        augmented_expansions += len(new_events)
        assert augmented_expansions <= base_expansions + len(potential)
        a_mask |= mask
        assert base == tree(a_mask, height)
        assert augmented == tree(a_mask | c_mask, height)
    return len(incoming)


def main():
    histories = operations = 0
    for a, c, b1, b2 in product(range(16), repeat=4):
        operations += check(a, c, (b1, b2), 2)
        histories += 1
    rng = Random(200)
    for _ in range(10000):
        a, c = rng.randrange(256), rng.randrange(256)
        bs = [rng.randrange(256) for _ in range(8)]
        operations += check(a, c, bs, 3)
        histories += 1
    print(json.dumps(dict(histories=histories,
                          old_job_insertions=operations,
                          coordinate_charges_unique=True)))


if __name__ == '__main__':
    main()