check_bounded_fringe_reuse.py

#!/usr/bin/env python3
"""Semantic audit for section 10 of name-funded-ball-reuse.md.

Integers, sets and tuples are oracles, not native operations. The written proof
charges unary gap stacks, width descents, fixed masks and persistent capsules.
The pending worker is imported from the maintained ball audit, not duplicated.
"""
from dataclasses import dataclass
from itertools import product
from random import Random
import json
from check_name_funded_ball_reuse import Receipt, record, step, B


@dataclass(frozen=True)
class Row:
    widths: frozenset = frozenset()
    maximum: int = 0
    gap: int = 0
    mask: tuple = ()  # offsets 1,...,b below the maximum


def insert_width(old, n, b):
    gap = old.gap
    window = [True] * b
    predecessors = window[:]
    for position in range(1, n + 1):
        predecessors = window[:]
        if b:
            window = (window + [position in old.widths])[-b:]
        if position > old.maximum:
            gap += 1
    fresh = n not in old.widths
    if fresh:
        assert gap > 0
        gap -= 1
    if n > old.maximum:
        mask = tuple(reversed(predecessors))
    else:
        mask = list(old.mask)
        distance = old.maximum - n
        if fresh and 1 <= distance <= b:
            mask[distance - 1] = True
        mask = tuple(mask)
    new = Row(old.widths | {n}, max(n, old.maximum), gap, mask)
    assert new.gap == new.maximum - len(new.widths)
    assert new.mask == tuple(new.maximum-j <= 0 or
                            new.maximum-j in new.widths
                            for j in range(1, b+1))
    valid = new.gap == sum(not bit for bit in new.mask)
    oracle = all(j in new.widths for j in range(1, new.maximum-b))
    assert valid == oracle
    return new


def profile(h, mask):
    return frozenset(j for j in range(1, h+1)
                     if h-j == 0 or h-j > len(mask) or mask[h-j-1])


def member(h, mask, width):
    if not 1 <= width <= h:
        return False
    distance = h-width
    return distance == 0 or distance > len(mask) or mask[distance-1]


def query(saved, maximum, mask, length, k):
    s = saved
    lanes = [[s.candidate, s.candidate, 0, 0]]
    answers = promotions = repairs = 0
    b = len(mask)
    for t in range(1, length+1):
        for lane in lanes:
            if lane[2]:
                lane[2] += 1
            else:
                lane[1] -= 1
        for _ in range(8*B):
            if not s.queue and s.active is None:
                break
            before = s.candidate
            s, raised = step(s)
            if raised is not None:
                assert t <= (before+7)//8
                lanes.append([raised, raised, t, before-b-1])
                promotions += 1
        for lane in lanes:
            if lane[2]:
                work = min(4, lane[2])
                lane[1] -= work
                lane[2] -= work
                repairs += work
                if not lane[2]:
                    assert t <= lane[3]
            if not lane[2]:
                assert lane[1] == lane[0]-t
            else:
                assert t <= lane[3]
        assert len(lanes) <= k
        answer = any(not debt and member(h, mask, t)
                     for h, _, debt, _ in lanes)
        assert answer == member(maximum, mask, t)
        answers += 1
    return answers, promotions, repairs


def main():
    rng = Random(183)
    updates = gates = nested = unions = answers = promotions = repairs = 0
    # Every short width history, including gaps, duplicates and maximum jumps.
    for b in range(4):
        for length in range(6):
            for seq in product(range(1, 6), repeat=length):
                row = Row(mask=(True,)*b)
                for n in seq:
                    row = insert_width(row, n, b)
                    updates += 1
    # Literal complete-level gate, arbitrary record order and duplicates.
    for trial in range(100):
        b = trial % 4
        maxima = rng.sample(range(1, 6), rng.randrange(1, 4))
        table = {}
        records = []
        for name in range(4):
            h = rng.choice(maxima)
            mask = tuple(bool(rng.randrange(2)) for _ in range(b))
            widths = profile(h, mask)
            words = {format(i, '0%db' % n) for n in widths for i in range(2**n)}
            table[name] = words
            records.extend((name, w) for w in words)
        rng.shuffle(records)
        records += records[:10]
        rows = [Row(mask=(True,)*b) for _ in range(4)]
        seen = [set() for _ in range(4)]
        counts = [{} for _ in range(4)]
        incomplete = bad = 0
        for name, word in records:
            old = rows[name]
            old_bad = bool(old.maximum) and old.gap != sum(not x for x in old.mask)
            rows[name] = insert_width(old, len(word), b)
            new = rows[name]
            new_bad = new.gap != sum(not x for x in new.mask)
            bad += int(new_bad)-int(old_bad)
            if word not in seen[name]:
                n = len(word)
                old_count = counts[name].get(n, 0)
                if old_count == 0:
                    incomplete += 1
                counts[name][n] = old_count+1
                if old_count+1 == 2**n:
                    incomplete -= 1
                seen[name].add(word)
            assert bad == sum(bool(x.maximum) and x.gap != sum(not z for z in x.mask)
                              for x in rows)
            assert incomplete == sum(0 < c < 2**n for cs in counts
                                     for n, c in cs.items())
        assert bad == incomplete == 0
        assert len({row.maximum for row in rows}) <= len(maxima)
        assert seen == [table[i] for i in range(4)]
        gates += 1
    # Direct set oracle for all same-label pairs; then finite union partitions.
    for b in range(4):
        candidates = [(h, mask) for h in range(1, 25)
                      for mask in product((False, True), repeat=b)]
        for h, mask in candidates:
            for bigger in range(h+b+1, 25, b+1):
                assert profile(h, mask) <= profile(bigger, mask)
                nested += 1
        for _ in range(300):
            chosen = rng.sample(candidates, min(20, len(candidates)))
            slots = {}
            for h, mask in chosen:
                key = (mask, h % (b+1))
                slots[key] = max(h, slots.get(key, 0))
            expected = set().union(*(profile(h, m) for h, m in chosen))
            actual = set().union(*(profile(h, m) for (m, _), h in slots.items()))
            assert actual == expected
            unions += 1
        for _ in range(100):
            mask = tuple(bool(rng.randrange(2)) for _ in range(b))
            low = 4*b+9+rng.randrange(8)
            radii = [low+i*(b+1) for i in range(4)]
            s = Receipt()
            selected = []
            for i in range(1, 45):
                value = rng.choice(radii)
                s = record(s, bin(i)[2:], value)
                selected.append(value)
            a, p, z = query(s, max(selected), mask, max(selected)+2, 4)
            answers += a; promotions += p; repairs += z
        # Symbolic huge maxima force pending comparisons and overlapping repairs.
        for exponent in (64, 256, 1024):
            low = (b+1)*(1 << exponent)
            radii = [low+i*(b+1) for i in range(4)]
            mask = tuple(j % 2 == 0 for j in range(b))
            s = Receipt()
            for i in range(1, 100):
                value = low if i < 96 else radii[i-96]
                s = record(s, bin(i)[2:], value)
            a, p, z = query(s, max(radii), mask, 500, 4)
            answers += a; promotions += p; repairs += z
    assert promotions > 0 and repairs > 0
    print(json.dumps(dict(status='passed', width_updates=updates,
                         literal_gate_histories=gates, nested_pairs=nested,
                         union_partitions=unions, query_prefix_answers=answers,
                         query_promotions=promotions, repair_units=repairs), indent=2))


if __name__ == '__main__':
    main()