verify_persistent_selector.py

#!/usr/bin/env python3
"""Literal immutable-row interpreter versus independent language oracle."""
from itertools import product
import json


def follow(heap, root, path):
    for port in path:
        if root is None:
            return None
        root = heap[root][1][port]
    return root


def step(heap, mode, char, mutant=False):
    old = len(heap) - 1
    if mode == 'DATA' and char in '01':
        row = ('B' + char, (len(heap), follow(heap, old, (0,))))
        new_mode, accept = 'DATA', False
    elif (mode, char) == ('DATA', '#') or (mode, char) == ('QUERY', '0'):
        path = (0,) if mode == 'DATA' or mutant else (0, 1)
        head = follow(heap, old, path)
        row = ('W', (head, None))
        new_mode = 'QUERY'
        accept = head is not None and heap[head][0] == 'B1'
    else:
        row = ('W', (None, None))
        new_mode, accept = 'DEAD', False
    return heap + (row,), new_mode, accept


def oracle(word):
    if word.count('#') != 1:
        return False
    data, query = word.split('#')
    return (bool(data) and all(c in '01' for c in data)
            and all(c == '0' for c in query) and len(query) < len(data)
            and data[len(data) - len(query) - 1] == '1')


def run(word, mutant=False):
    heap, mode, accept = (('W', (None, None)),), 'DATA', False
    for char in word:
        heap, mode, accept = step(heap, mode, char, mutant)
    return heap, mode, accept


def chain(heap):
    head = follow(heap, len(heap)-1, (0,))
    result = []
    while head is not None:
        assert heap[head][0] in ('B0', 'B1')
        result.append(heap[head][0][1])
        head = heap[head][1][1]
    return ''.join(result)


def main():
    counts = dict(all_words=0, immutable_steps=0, chain_invariants=0,
                  selector_queries=0, residual_profiles=0, mutant_failures=0)
    witness = None
    def visit(word, heap, mode, accept):
        nonlocal witness
        counts['all_words'] += 1
        assert accept == oracle(word), word
        assert len(heap) == len(word) + 1
        if mode == 'DATA':
            assert chain(heap) == word[::-1]
            counts['chain_invariants'] += 1
        elif mode == 'QUERY':
            data, query = word.split('#')
            assert chain(heap) == data[::-1][len(query):]
            counts['chain_invariants'] += 1
        if run(word, mutant=True)[2] != oracle(word):
            counts['mutant_failures'] += 1
            if witness is None or (len(word), word) < (len(witness), witness):
                witness = word
        if len(word) == 10:
            return
        for char in '01#':
            new_heap, new_mode, new_accept = step(heap, mode, char)
            assert new_heap[:-1] == heap
            counts['immutable_steps'] += 1
            visit(word+char, new_heap, new_mode, new_accept)
    visit('', (('W', (None, None)),), 'DATA', False)
    for n in range(1, 11):
        profiles = set()
        for bits in product('01', repeat=n):
            data = ''.join(bits)
            answers = tuple(run(data + '#' + '0'*j)[2] for j in range(n))
            assert answers == tuple(bit == '1' for bit in data[::-1])
            profiles.add(answers)
            counts['selector_queries'] += n
        assert len(profiles) == 2**n
        counts['residual_profiles'] += len(profiles)
    assert witness is not None
    return dict(ok=True, counts=counts, alphabet='01#', max_word_length=10,
                max_data_length=10, degree=2, distance=2,
                nodes_per_symbol=1, mutation='replace pop path 01 by stay path 0',
                shortest_mutation_witness=witness)


if __name__ == '__main__':
    print(json.dumps(main(), indent=2, sort_keys=True))