check_interval_reuse_frontier.py

#!/usr/bin/env python3
"""Finite semantic controls and a restricted FIFO deadline counterexample.

Tuples and integers are audit machinery, not a native implementation. No
literal full-level input is generated; its preparation is outside this audit.
"""
from itertools import combinations
import json
import random


def insert(state, n):
    """Persistent missing-interval update, including previously unseen maxima."""
    h, blocks = state
    if n > h:
        return n, blocks + (((h + 1, n - 1),) if n > h + 1 else ())
    out = []
    for a, b in blocks:
        if not a <= n <= b:
            out.append((a, b))
        else:
            if a < n:
                out.append((a, n - 1))
            if n < b:
                out.append((n + 1, b))
    return h, tuple(out)


def oracle(widths):
    h = max(widths, default=0)
    missing = [n for n in range(1, h + 1) if n not in widths]
    blocks = []
    for n in missing:
        if blocks and blocks[-1][1] == n - 1:
            blocks[-1] = (blocks[-1][0], n)
        else:
            blocks.append((n, n))
    return h, tuple(blocks)


def fifo_witness(window, service, query_service):
    # The head compares separately prepared equal numerals, without identity
    # shortcuts. Service includes all later selection/name/delimiter work.
    names = [bin(i)[2:] for i in range(1, window + 5)]
    later_symbols = sum(len(s) + 3 for s in names[2:]) + 8
    budget = service * later_symbols + query_service * 3
    exponent = budget + 3
    big = 1 << exponent
    h = big + 1
    histories = [[big, big, special] + [big] * (window + 1)
                 for special in (2, big)]
    answers = []
    signatures = []
    for endpoints in histories:
        # A full LSB-first comparison must consume every bit for equality.
        x, y = big, big
        for _ in range(budget):
            assert x and y
            x >>= 1
            y >>= 1
        assert x and y  # No later job can have started in this contract.
        recent = endpoints[-window:] if window else []
        signatures.append((big, x, y, tuple(recent), len(endpoints)))
        answers.append(any(b <= 2 <= h for b in endpoints))
    assert signatures[0] == signatures[1]
    assert answers == [True, False]
    return exponent


def main():
    transitions = 0
    for mask in range(1 << 10):
        widths = frozenset(i + 1 for i in range(10) if mask >> i & 1)
        state = oracle(widths)
        for n in range(1, 14):
            assert insert(state, n) == oracle(widths | {n})
            transitions += 1
    rng = random.Random(188)
    versions = [((0, ()), frozenset())]
    for _ in range(5000):
        state, widths = rng.choice(versions)
        n = rng.randrange(1, 100)
        updated = insert(state, n)
        assert updated == oracle(widths | {n})
        assert state == oracle(widths)
        versions.append((updated, widths | {n}))
    suffix_checks = 0
    for h in range(1, 12):
        for size in range(1, min(h, 4) + 1):
            for endpoints in combinations(range(1, h + 1), size):
                for n in range(1, h + 2):
                    assert any(b <= n <= h for b in endpoints) == (min(endpoints) <= n <= h)
                    suffix_checks += 1
    cutoff_checks = 0
    for cutoff in range(1, 9):
        mask = [False] * cutoff
        selected = []
        for endpoint in (100000, 19, 8, 1000, 3, 17, 1):
            selected.append(endpoint)
            # Fixed-cutoff prepared-interface escape: c observations per row.
            mask = [old or endpoint <= n for n, old in enumerate(mask, 1)]
            for n, value in enumerate(mask, 1):
                assert value == (min(selected) <= n)
                cutoff_checks += 1
    witnesses = [fifo_witness(w, q, r) for w in range(9)
                 for q in (1, 4, 16) for r in (1, 8, 32)]
    for t in range(1, 50):
        occupied = {2 * j for j in range(1, t + 1)}
        assert len(oracle(occupied)[1]) == t
    print(json.dumps(dict(interval_transitions=transitions, retained_forks=5000,
                         suffix_memberships=suffix_checks, fifo_witnesses=len(witnesses),
                         largest_comparison_exponent=max(witnesses),
                         alternating_component_controls=49, fixed_cutoff_memberships=cutoff_checks), indent=2))


if __name__ == '__main__':
    main()