check_activation_contraction.py

#!/usr/bin/env python3
"""Finite semantic/schedule audit; Python operations are not native timing evidence."""
from dataclasses import dataclass
from itertools import product
import json
import random


@dataclass(frozen=True)
class Node:
    mark: bool = False
    zero: object = None
    one: object = None


def insert(root, key):
    root = root or Node()
    if not key:
        return Node(True, root.zero, root.one)
    if key[0] == '0':
        return Node(root.mark, insert(root.zero, key[1:]), root.one)
    return Node(root.mark, root.zero, insert(root.one, key[1:]))


def lookup(root, key):
    for bit in key:
        if root is None:
            return False
        root = root.zero if bit == '0' else root.one
    return bool(root and root.mark)


def words(n):
    return [''.join(x) for x in product('01', repeat=n)]


def classify(word, n, ell):
    if len(word) != n:
        return None, ''
    if all(x == '0' for x in word[:n-ell]):
        return 'A', word[n-ell:]
    if word[ell] == '1' and all(x == '0' for x in word[ell+1:]):
        return 'B', word[:ell]
    return None, ''


def oracle_permutation(n, ell):
    # Independent explicit disjoint transpositions, not the readout classifier.
    result = {z: z for z in words(n)}
    for t in words(ell):
        a, b = '0' * (n-ell) + t, t + '1' + '0' * (n-ell-1)
        assert a != b
        result[a], result[b] = b, a
    assert len(set(result.values())) == 2**n
    assert all(result[result[z]] == z for z in result)
    return result


def activate(roots, owner, n, ell, alias=0):
    if alias:
        return roots
    full, short_a, short_b = roots
    full = insert(full, owner)
    if owner.startswith('1'):
        alpha, beta = owner[1:1+n], owner[1+n:]
        kind, t = classify(beta, n, ell)
        if kind == 'A':
            short_a = insert(short_a, alpha+t)
        if kind == 'B':
            short_b = insert(short_b, alpha+t)
    return full, short_a, short_b


def foreign(roots, alpha, z, n, ell):
    kind, t = classify(z, n, ell)
    if kind == 'A':
        return lookup(roots[2], alpha+t)
    if kind == 'B':
        return lookup(roots[1], alpha+t)
    return lookup(roots[0], '1'+alpha+z)


def bootstrap(beta, z):
    # Semantic reconstruction of unary snapshots: no logarithm or supplied ell.
    before_last_one = None
    trailing = 0
    for position, bit in enumerate(beta):
        if bit == '1':
            before_last_one, trailing = position, 0
        else:
            trailing += 1
    ell = before_last_one
    if ell is None or ell < 1 or trailing < ell or len(z) != len(beta):
        return None
    if z[:trailing+1] != '0'*(trailing+1) or z[trailing+1:] != beta[:ell]:
        return None
    return ell


def finish(n, ell, lane):
    releases = ([j for j in range(1, n+1)] if lane == 'I'
                else [n-ell+j for j in range(1, ell+1)] if lane == 'A'
                else [j for j in range(1, ell+1)])
    jobs = [1]*(n+2) + releases
    head = 0
    for tick in range(1, n+1):
        for _ in range(4):
            if head < len(jobs) and jobs[head] <= tick:
                head += 1
    return head == len(jobs)


def local_bit(table, prefix):
    values = {v[len(prefix)-1] for k,v in table.items() if k.startswith(prefix)}
    assert len(values) == 1
    return values.pop()


def main():
    counts = dict(bootstrap_pairs=0, exhaustive_activation_queries=0,
                  retained_queries=0, relation_queries=0, schedules=0,
                  envelope_witnesses=0, short_map_queries=0, prefix_conflict_checks=0)
    # Exhaust every possible first beta/z through width6, against explicit pairs.
    for n in range(1, 7):
        valid = {}
        for ell in range(1, (n-1)//2+1):
            for t in words(ell):
                valid[(t+'1'+'0'*(n-ell-1), '0'*(n-ell)+t)] = ell
        for beta in words(n):
            for z in words(n):
                assert bootstrap(beta, z) == valid.get((beta, z))
                counts['bootstrap_pairs'] += 1
    n, ell, alpha = 3, 1, '010'
    permutation = oracle_permutation(n, ell)
    universe = words(n)
    for mask in range(2**len(universe)):
        roots, active = (None, None, None), set()
        for j, beta in enumerate(universe):
            if mask >> j & 1:
                owner = '1'+alpha+beta
                roots = activate(roots, owner, n, ell)
                active.add(owner)
        for z in universe:
            assert foreign(roots, alpha, z, n, ell) == ('1'+alpha+permutation[z] in active)
            counts['exhaustive_activation_queries'] += 1
    rng = random.Random(237)
    for n in range(3, 10):
        for ell in range(1, (n-1)//2+1):
            permutation = oracle_permutation(n, ell)
            alphas = words(n)[::max(1, 2**n//4)]
            names = ['0'+z for z in words(2*n)[:4]]
            sources = {u: (None, None, None) for u in ['0', '101']}
            active = {u: set() for u in sources}
            versions = []
            # Four independent namespace maps plus partial original support.
            sigma = [{a: rng.choice(alphas) for a in alphas} for _ in range(4)]
            relation = set()
            for namespace, mapping in enumerate(sigma):
                for a, mapped in mapping.items():
                    for z in words(n)[::max(1, 2**n//16)]:
                        q = (namespace, a, z)
                        if rng.randrange(2):
                            relation.add(('1'+mapped+permutation[z], q))
                        if rng.randrange(2):
                            relation.add((names[namespace % len(names)], q))
            for _ in range(60):
                u = rng.choice(list(sources))
                owner = ('1'+rng.choice(alphas)+rng.choice(words(n))
                         if rng.randrange(4) else rng.choice(names))
                alias = rng.randrange(3) == 0
                sources[u] = activate(sources[u], owner, n, ell, alias)
                if not alias:
                    active[u].add(owner)
                versions.append((sources.copy(), {k: frozenset(v) for k,v in active.items()}))
            for roots_by_source, actual in versions[::5]:
                for u, roots in roots_by_source.items():
                    for alpha in alphas:
                        for z in words(n):
                            assert foreign(roots, alpha, z, n, ell) == ('1'+alpha+permutation[z] in actual[u])
                            counts['retained_queries'] += 1
                    for namespace, mapping in enumerate(sigma):
                        for a, mapped in mapping.items():
                            for z in words(n)[::max(1, 2**n//16)]:
                                q = (namespace, a, z)
                                primary = names[namespace % len(names)]
                                owner = '1'+mapped+permutation[z]
                                got = ((primary,q) in relation and lookup(roots[0],primary)
                                       or (owner,q) in relation and foreign(roots,mapped,z,n,ell))
                                expected = any((b,q) in relation for b in actual[u])
                                assert bool(got) == expected
                                counts['relation_queries'] += 1
    for n in range(3, 257):
        for ell in range(1, (n-1)//2+1):
            for lane in ['I','A','B']:
                assert finish(n, ell, lane)
                counts['schedules'] += 1
    # Separate local-bit producer and extensional prefix-consistency oracle.
    for ell in range(1, 5):
        n = 2*ell+1
        domain = words(ell)
        flips = {p: rng.choice('01') for j in range(ell) for p in words(j)}
        table = {t: ''.join(str(int(bit)^int(flips[t[:j]]))
                           for j,bit in enumerate(t)) for t in domain}
        rows = list(table.items())
        for trial in range(15):
            rng.shuffle(rows)
            proposed = rows.copy()
            if trial % 2:
                key, val = rng.choice(rows)
                proposed.append((key, val[:-1]+str(1-int(val[-1]))))
            local, accepted = {}, True
            for key,val in proposed:
                for j in range(1,ell+1):
                    if key[:j] in local and local[key[:j]] != val[j-1]:
                        accepted = False
                    local[key[:j]] = val[j-1]
            expected = all(x[:j] != y[:j] or bx[:j] == by[:j]
                           for x,bx in proposed for y,by in proposed
                           for j in range(ell+1))
            assert accepted == expected
            counts['prefix_conflict_checks'] += 1
        alpha = '0'*n
        roots, active = (None,None,None), set()
        for t in domain:
            for beta in ['0'*(n-ell)+t, t+'1'+'0'*(n-ell-1)]:
                if rng.randrange(2):
                    owner = '1'+alpha+beta
                    roots = activate(roots,owner,n,ell)
                    active.add(owner)
        for kind in ['A','B']:
            for t,mapped in table.items():
                output = ''.join(local_bit(table, t[:j]) for j in range(1,ell+1))
                assert output == mapped
                beta = (mapped+'1'+'0'*(n-ell-1) if kind == 'A'
                        else '0'*(n-ell)+mapped)
                got = lookup(roots[2 if kind=='A' else 1],alpha+output)
                assert got == ('1'+alpha+beta in active)
                counts['short_map_queries'] += 1
    for c in [1,2,4,8,16]:
        for width in [1,2,8,64]:
            ell = 3
            while 2**ell-c*ell < ell or 2**ell <= width:
                ell += 1
            assert 2**ell-c*ell >= ell and 2**ell > width
            counts['envelope_witnesses'] += 1
    print(json.dumps(dict(status='passed', **counts), sort_keys=True))


if __name__ == '__main__':
    main()