check_banded_interval_independent.py

#!/usr/bin/env python3
"""Independent adversarial semantic checks for the banded interval worker.

Exhaust every eight-leaf coverage pattern and interval, then interrupt each
phase of one boundary insertion with two additional releases. Integer and
whole-state inspections belong only to the oracle. Imported worker operations
retain the primary checker's persistent-primitive modeling scope; this script
does not establish native running time.
"""
import json

import check_banded_interval_reuse as model


def coverage_tree(bits):
    if len(bits) == 1:
        return bool(bits[0])
    middle = len(bits) // 2
    return model.join(coverage_tree(bits[:middle]), coverage_tree(bits[middle:]))


def main():
    insertions = forks = work_checks = 0
    for mask in range(256):
        old_bits = [bool((mask >> i) & 1) for i in range(8)]
        old_tree = coverage_tree(old_bits)
        for lower in range(8, 16):
            for upper in range(lower, 16):
                insertion = model.start_insert(
                    old_tree, model.units(3), model.digits(lower),
                    model.digits(upper))
                steps = 0
                while insertion.phase != 'done':
                    insertion = model.insert_step(insertion)
                    steps += 1
                assert steps <= 16 * 4 + 16
                expected = [covered or lower <= i + 8 <= upper
                            for i, covered in enumerate(old_bits)]
                assert model.tree_bits(insertion.result, 3) == expected
                assert model.tree_bits(old_tree, 3) == old_bits
                insertions += 1

    worker = model.release(model.Worker(), model.digits(11), model.digits(14))
    while worker.suffix:
        if worker.suffix[0].insertion is not None:
            for lower, upper in [(8, 8), (15, 15), (9, 12), (1, 2), (32, 45)]:
                fork = model.release(worker, model.digits(lower), model.digits(upper))
                fork = model.release(fork, model.digits(10), model.digits(10))
                intervals = [(11, 14), (lower, upper), (10, 10)]
                expected = [any(a <= n <= b for a, b in intervals)
                            for n in range(1, 65)]
                assert model.query(fork, 64) == expected
                for cutoff in range(1, 8):
                    _, before = model.drain_to(worker, cutoff)
                    _, after = model.drain_to(fork, cutoff)
                    assert after <= before + 512 * cutoff
                    work_checks += 1
                forks += 1
        worker = model.service(worker)

    print(json.dumps({
        'arbitrary_coverage_insertions': insertions,
        'same_band_and_nested_forks': forks,
        'residual_work_checks': work_checks,
    }))


if __name__ == '__main__':
    main()