check_learned_contexts.py

#!/usr/bin/env python3
"""Learned-context producer and inherited pending-index finite audit.

Immutable trie and pending-reader operations reuse the maintained section15
model. Host tuples, dictionaries, lengths and clocks are semantic stand-ins,
not native instructions. Literal full-word sets form the separate oracle.
"""
import json
from itertools import permutations, product
from random import Random
from check_pending_substitution import (
    B, Bucket, Reader, RightRow, STATS, add_left, close, cls, lookup, walk)


def prepare(records, cap, degree, span):
    contexts, rows = [], {}
    captures = 0
    for v, w in records:
        if not v or not w:
            return None
        remaining, window, fresh = len(v) + 1, (), ()
        cursors = [tuple(p) for p in contexts]
        viable = [True] * len(contexts)
        tails = [() for _ in contexts]
        for bit in w:
            if remaining:
                remaining -= 1
            else:
                fresh += window[:1]
                window = window[1:]
            window += (bit,)
            for j in range(len(contexts)):
                if not viable[j]:
                    continue
                if cursors[j]:
                    viable[j] = cursors[j][0] == bit
                    cursors[j] = cursors[j][1:]
                else:
                    tails[j] += (bit,)
        matches = [j for j in range(len(contexts))
                   if viable[j] and not cursors[j]]
        if matches:
            j = matches[0]
            tail = tails[j]
        else:
            if remaining or len(contexts) == cap:
                return None
            j, tail = len(contexts), window
            contexts.append(fresh)
            captures += 1
        if not tail or abs(cls(v) - cls(tail)) > span:
            return None
        old = rows.get(v, ())
        if (j, tail) not in old:
            old += ((j, tail),)
        if len(old) > degree:
            return None
        rows[v] = old
    frozen = [B] * cap
    for v, targets in rows.items():
        for j in range(cap):
            receipt = RightRow(targets=tuple(
                (tail, cls(tail)-cls(v)) for tag, tail in targets if tag == j))
            frozen[j] = close(walk(frozen[j], v), receipt)
    return tuple(contexts), tuple(frozen), captures


class Lane:
    """Each feed is one actual bit, with no terminal replay."""
    def __init__(self, context, index):
        self.context, self.index = context, index
        self.ok, self.n, self.j = True, 0, 0
        self.current = self.ahead = None
        self.prefix = self.queue = ()

    def feed(self, bit):
        if not self.ok:
            return
        if self.context:
            self.ok = self.context[0] == bit
            self.context = self.context[1:]
            return
        self.n += 1
        if self.n == 1:
            self.current = Reader(self.index.get(0, Bucket()))
            self.current.feed(bit)
            self.prefix = self.queue = (bit,)
            self.ahead = Reader(self.index.get(1, Bucket()))
            return
        self.current.feed(bit)
        self.prefix += (bit,)
        self.queue += (bit,)
        for _ in range(2):
            if self.queue:
                self.ahead.feed(self.queue[0])
                self.queue = self.queue[1:]
        if self.n == 2 ** (self.j + 1):
            assert not self.queue and self.ahead.consumed == self.n
            self.current = self.ahead
            self.j += 1
            self.ahead = Reader(self.index.get(self.j + 1, Bucket()))
            self.queue = self.prefix

    def answer(self):
        return bool(self.ok and not self.context and self.n
                    and self.current.contains())


def main():
    rng = Random(207)
    counts = dict(tables=0, versions=0, prefix_queries=0, negative=0,
                  context_captures=0)
    cases = []
    for stem in ('', '0', '101', '0'*32):
        for perm in permutations(('00', '01', '10')):
            records = [(v, stem + q + b) for v, q in zip(('00','01','10'), perm)
                       for b in '01']
            cases.append((records, 1, 2, 1))
    # Later shorter contexts, empty contexts, arbitrary targets and row overlap.
    cases += [([('0','0100'),('1','000'),('00','11')],3,3,1),
              ([('0','000'),('0','100'),('1','011')],2,2,1)]
    for _ in range(100):
        names = [''.join(rng.choice('01') for _ in range(rng.randint(1,5)))
                 for _ in range(7)]
        records = [(v, ''.join(rng.choice('01') for _ in range(rng.randint(2,12))))
                   for v in names]
        cases.append((records,3,3,2))
    for records, cap, degree, span in cases:
        result = prepare(records + records[-1:], cap, degree, span)
        if result is None:
            continue
        contexts, frozen, captures = result
        counts['tables'] += 1
        counts['context_captures'] += captures
        literal = {}
        for v,w in records:
            literal.setdefault(v,set()).add(w)
        roots, selected, snapshots = (B,)*cap, {}, []
        aliases = list(literal) + ['1111111']
        for t in range(18):
            u, v = ('0','101')[t%2], rng.choice(aliases)
            roots = tuple(add_left(root, table, u, v, degree, span)
                          for root,table in zip(roots,frozen))
            selected = {key:set(value) for key,value in selected.items()}
            selected.setdefault(u,set()).update(literal.get(v,set()))
            snapshots.append((roots,selected))
        # Revisit every old root after all later updates have completed.
        for roots, selected in snapshots:
            counts['versions'] += 1
            queries = {w for _,w in records}
            queries |= {w[:-1] for _,w in records} | {w+'1' for _,w in records}
            queries |= {''.join(bits) for n in range(1,5) for bits in product('01',repeat=n)}
            for u in ('0','101','111'):
                truth = selected.get(u,set())
                for w in queries:
                    lanes = [Lane(p, lookup(roots[j],u) or {})
                             for j,p in enumerate(contexts)]
                    for n,bit in enumerate(w,1):
                        for lane in lanes:
                            lane.feed(bit)
                        got = any(lane.answer() for lane in lanes)
                        assert got == (w[:n] in truth), (contexts,u,w,n)
                        counts['prefix_queries'] += 1
                        counts['negative'] += not got
    assert prepare([],1,2,1) == ((),(B,),0)
    assert prepare([('00','0')],1,2,1) is None
    assert prepare([('0','000'),('1','0')],1,2,1) is None
    assert counts['context_captures'] > counts['tables']
    print(json.dumps({**counts,'inherited_pending_model':STATS},sort_keys=True))


if __name__ == '__main__':
    main()