check_envelope_reuse.py

#!/usr/bin/env python3
"""Independent finite semantic audit for a learned fixed prefix envelope.

Host sets and recursive views are mathematical oracles, not a native machine
simulation. These checks do not certify pointer routing, allocation, or input
symbol deadlines. The written bounded-batch proof supplies those obligations.
"""
from __future__ import annotations
import itertools
import json
import random
from collections import Counter

COUNTS = Counter()


def words(d):
    return tuple(''.join(p) for p in itertools.product('01', repeat=d))


def prefix(a, b):
    return a[:next((i for i, (x, y) in enumerate(zip(a, b)) if x != y), len(a))]


def mixed(row, d):
    # Independent cylinder-population oracle, including absent literal leaves.
    return sum(0 < sum(w.startswith(p) for w in row) < 2 ** (d - i)
               for i in range(d) for p in words(i))


def view(row, d):
    if not row:
        return 0
    if len(row) == 2 ** d:
        return 1
    return tuple(view({w[1:] for w in row if w[0] == bit}, d - 1)
                 for bit in '01')


def child(v, bit):
    return v if isinstance(v, int) else v[int(bit)]


def member(v, word):
    for bit in word:
        v = child(v, bit)
    assert isinstance(v, int)
    return bool(v)


def splice(a, b):
    if b == 0 or a == 1:
        return a, 1
    if b == 1 or a == 0:
        return b, 1
    left, lc = splice(a[0], b[0])
    right, rc = splice(a[1], b[1])
    return (1 if left == right == 1 else (left, right)), 1 + lc + rc


def budget_update(row, w, d, capacity):
    old = view(row, d)
    a = v = capacity - mixed(row, d)
    for bit in w:
        m = int(not isinstance(old, int))
        f = child(old, str(1 - int(bit))) == 1
        a += m - 1
        v = v + m if f else a
        old = child(old, bit)
    return capacity - mixed(row, d) if old == 1 else v


def query(v, p, n, q):
    return len(q) == n and q.startswith(p) and member(v, q[len(p):])


def audit_insertions():
    for d in range(1, 4):
        cube = words(d)
        for mask in range(1 << len(cube)):
            row = frozenset(w for i, w in enumerate(cube) if mask >> i & 1)
            snapshot = view(row, d)
            for w in cube:
                for capacity in (1, d, 2 * d):
                    got = budget_update(row, w, d, capacity)
                    assert got == capacity - mixed(row | {w}, d)
                    COUNTS['signed_budget_updates'] += 1
                for q in cube:
                    assert member(snapshot, q) == (q in row)
                    COUNTS['retained_memberships'] += 1


def audit_bootstrap():
    for n in range(1, 5):
        for w0, w1 in itertools.permutations(words(n), 2):
            p = prefix(w0, w1)
            x, y = w0[len(p):], w1[len(p):]
            d = len(x)
            assert d >= 1 and x[0] != y[0]
            capacity = 5
            # Streaming same-alias budget, no depth arithmetic at endpoint.
            b = capacity
            for i in range(1, d):
                b -= 3 if i == 1 else 2
            assert b == capacity - mixed({x, y}, d)
            tails = (view({x[1:]}, d - 1), view({y[1:]}, d - 1))
            if x[0] == '1':
                tails = tails[::-1]
            pair = 1 if d == 1 else tails
            assert pair == view({x, y}, d)
            for same in (False, True):
                rows = [{x, y}] if same else [{x}, {y}]
                for row in rows:
                    v = view(row, d)
                    for q in words(n) + ('', w0 + '0', w0[:-1]):
                        assert query(v, p, n, q) == (q in {p + z for z in row})
                        COUNTS['bootstrap_literal_queries'] += 1
                COUNTS['bootstrap_cases'] += 1


def audit_growth_and_selections():
    rng = random.Random(218)
    for d in range(1, 6):
        cube = words(d)
        p = '0' * (d * d + 7)
        n = len(p) + d
        rows = {i: frozenset() for i in range(4)}
        histories = []
        bad = 0
        capacity = d
        for _ in range(80):
            i, w = rng.randrange(4), rng.choice(cube)
            before = rows[i]
            after = before | {w}
            bad += int(mixed(after, d) > capacity) - int(mixed(before, d) > capacity)
            rows = dict(rows)
            rows[i] = after
            assert bad == sum(mixed(r, d) > capacity for r in rows.values())
            histories.append((dict(rows), tuple(view(rows[j], d) for j in range(4))))
            COUNTS['growth_records'] += 1
        for snapshot, views in histories:
            for i in range(4):
                for q in cube:
                    assert query(views[i], p, n, p + q) == (q in snapshot[i])
                    COUNTS['growth_snapshot_queries'] += 1
        for bit in range(d):
            x = frozenset(w for w in cube if w[bit] == '1')
            complement = frozenset(cube) - x
            selections = [complement, x, frozenset({cube[0]})]
            committed = pending = 0
            expected = frozenset()
            for step, incoming in enumerate(selections):
                old_pending = pending
                committed, calls = splice(committed, pending)
                # Count mixed nodes independently by decoding the pending view.
                pending_set = {w for w in cube if member(old_pending, w)}
                assert calls <= 1 + 2 * mixed(pending_set, d)
                if step == 2:
                    assert calls == 1 + 2 * mixed(x, d)
                    COUNTS['complement_pair_exact_costs'] += 1
                pending = view(incoming, d)
                expected |= incoming
                for q in cube:
                    got = query(committed, p, n, p + q) or query(pending, p, n, p + q)
                    assert got == (q in expected)
                    COUNTS['immediate_selection_queries'] += 1
                COUNTS['selection_jobs'] += 1


def audit_gap():
    for d in range(2, 25):
        support = {'0' * d, '1' * d}
        row = {'0' * d}
        # Reduced observed-support tree has a single branch and two leaves.
        support_mixed = 1
        # Avoid exponentially enumerating the ambient cube: every strict zero
        # prefix is mixed, and no other prefix contains a present leaf.
        ambient_mixed = len(next(iter(row)))
        assert support_mixed == 1 and ambient_mixed == d
        assert prefix(*sorted(support)) == ''
        COUNTS['ambient_gap_examples'] += 1


def main():
    audit_insertions()
    audit_bootstrap()
    audit_growth_and_selections()
    audit_gap()
    print(json.dumps({'status': 'passed', 'counts': dict(sorted(COUNTS.items())),
                      'scope': 'finite semantic and splice-call audit; not native execution'}, indent=2))


if __name__ == '__main__':
    main()