check_action_prefix_images.py

#!/usr/bin/env python3
"""Finite semantic checks for assessment144. No native timing model."""
from itertools import product
import json


def actions(k):
    return list(product(range(k + 1), repeat=k))


def compose(a, b):
    """a after b, with coordinate 0 denoting constant zero."""
    return tuple(0 if i == 0 else b[i - 1] for i in a)


def apply(a, b):
    return tuple(0 if i == 0 else b[i - 1] for i in a)


def omega(a):
    p = a
    while compose(p, p) != p:
        p = compose(a, p)
    return p


def audit():
    counts = dict(prefix_mask_cases=0, continuation_evaluations=0,
                  reconstruction_checks=0, sg_pairs=0, split_encodings=0)
    classifications = []
    for k in range(1, 4):
        aa, bb = actions(k), list(product((0, 1), repeat=k))
        for p in aa:
            image = {apply(p, c): c for c in bb}
            for b in bb:
                answers = {}
                for u in aa:
                    answers.setdefault(compose(u, p), set()).add(apply(u, b))
                    counts['continuation_evaluations'] += 1
                    if b in image:
                        assert apply(compose(u, p), image[b]) == apply(u, b)
                        counts['reconstruction_checks'] += 1
                assert all(len(v) == 1 for v in answers.values()) == (b in image)
                counts['prefix_mask_cases'] += 1
        sg = True
        for x in aa:
            e = omega(x)
            xp = compose(x, e)
            for y in aa:
                sg &= compose(compose(xp, y), e) == compose(compose(e, y), xp)
                counts['sg_pairs'] += 1
        assert sg == (k == 1)
        classifications.append({'K': k, 'size': len(aa), 'SG': sg})

    # Actual width-two split: a touches both aliases, then v touches the second.
    columns = [set(), set()]
    for row, target in [('a', 0), ('a', 1), ('v', 1)]:
        columns[target].add(row)
    assert columns == [{'a'}, {'a', 'v'}]
    # All copy/reset choices agreeing on untouched row a force equal outputs.
    for f in actions(2):
        if apply(f, (1, 0)) == (1, 1):
            assert (0, 1) not in {apply(f, b) for b in product((0, 1), repeat=2)}
            counts['split_encodings'] += 1
    assert counts['split_encodings'] == 1
    return {'checks': counts, 'full_monoid_classification': classifications,
            'native_suffix_service_implemented': False}


if __name__ == '__main__':
    print(json.dumps(audit(), indent=2))