check_regular_stack_certificates.py

#!/usr/bin/env python3
"""Exact DFA checker for regular-stack-certificates.md.

Default: emit example instances, exact decisions and bounded implementation audits.
--check FILE: check one JSON instance (use an example's `instance` object).
States are integers; stack and input symbols are strings. Stack top is first.
No saturation, synthesis, VPA determinization or scaffold generator is included.
"""
import argparse
from collections import deque
from itertools import product
import json


class DFA:
    def __init__(self, alphabet, spec):
        self.alphabet = tuple(alphabet)
        self.index = {a: i for i, a in enumerate(alphabet)}
        self.start = spec['start']
        self.final = set(spec['final'])
        self.table = spec['transitions']
        n = len(self.table)
        if not n or type(self.start) is not int or not 0 <= self.start < n:
            raise ValueError('invalid DFA start')
        if any(type(x) is not int or not 0 <= x < n for x in self.final):
            raise ValueError('invalid DFA final state')
        if any(len(row) != len(alphabet) or any(type(x) is not int or not 0 <= x < n for x in row) for row in self.table):
            raise ValueError('DFA must be complete over the stack alphabet')

    def step(self, state, a):
        return self.table[state][self.index[a]]

    def accepts(self, word):
        state = self.start
        for a in word:
            state = self.step(state, a)
        return state in self.final

    def nonempty(self):
        seen, todo = {self.start}, [self.start]
        while todo:
            s = todo.pop()
            if s in self.final:
                return True
            for t in self.table[s]:
                if t not in seen:
                    seen.add(t)
                    todo.append(t)
        return False


def spec(transitions, final, start=0):
    return {'start': start, 'final': list(final), 'transitions': transitions}


def empty_spec(alphabet):
    return spec([[0] * len(alphabet)], [])


def singleton(word, alphabet):
    n = len(word)
    return spec([[i + 1 if i < n and a == word[i] else n + 1 for a in alphabet]
                 for i in range(n + 2)], [n])


def image(op, arg, word):
    if op == 'push':
        return (arg,) + tuple(word)
    if op == 'pop' and word:
        return tuple(word[1:])
    return tuple(word)


def branch_failure(old, target, e, top, clock_zero, op, arg):
    """Exact emptiness of D intersect preimage(complement(target)).

    Returns an old-stack tuple, or None after exhausting the finite product.
    top=None is the empty-stack case. Length cap retains the first-symbol flag.
    """
    cap = max(e, 0) + 1
    target_start = target.step(target.start, arg) if op == 'push' else target.start
    start = old.start, target_start, 0
    todo, seen = deque([(start, ())]), {start}
    while todo:
        (s, t, length), word = todo.popleft()
        top_ok = (length == 0) if top is None else (length > 0)
        clock_ok = (length == e) if clock_zero else (length > e)
        if top_ok and clock_ok and s in old.final and t not in target.final:
            return word
        if top is None:
            continue
        for a in old.alphabet:
            if length == 0 and a != top:
                continue
            nt = t if op == 'pop' and length == 0 else target.step(t, a)
            nxt = old.step(s, a), nt, min(cap, length + 1)
            if nxt not in seen:
                seen.add(nxt)
                todo.append((nxt, word + (a,)))
    return None


def coordinate_failure(A, e):
    if e <= 0:
        return None
    todo, seen = deque([((A.start, 0), ())]), {(A.start, 0)}
    while todo:
        (s, n), word = todo.popleft()
        if n < e and s in A.final:
            return word
        if n >= e:
            continue
        for a in A.alphabet:
            nxt = A.step(s, a), n + 1
            if nxt not in seen:
                seen.add(nxt)
                todo.append((nxt, word + (a,)))
    return None


def new_e(e, top, clock_zero, op, c):
    d = 1 if op == 'push' else (-1 if op == 'pop' and top is not None else 0)
    k = 0 if c == -1 and clock_zero else c
    return e + d - k


def check(instance):
    P, C = instance['source'], instance['clock']
    alphabet = P['stack_alphabet']
    if not alphabet or len(set(alphabet)) != len(alphabet) or not all(isinstance(a, str) for a in alphabet):
        raise ValueError('invalid stack alphabet')
    Q, R, letters = set(P['states']), set(C['states']), set(P['alphabet'])
    if not all(type(s) is int for s in Q | R) or not all(isinstance(a, str) for a in letters):
        raise ValueError('states must be integers and input letters strings')
    if not P['initial'] or not set(P['initial']) <= Q or C['initial'] not in R:
        raise ValueError('invalid initialization')
    table = {}
    for r, a, nr, c in C['table']:
        if r not in R or nr not in R or a not in letters or type(c) is not int or c not in (-1, 0, 1) or (r, a) in table:
            raise ValueError('invalid or duplicate clock rule')
        table[r, a] = nr, c
    if set(table) != set(product(R, letters)):
        raise ValueError('clock must be complete')
    for rule in P['rules']:
        if rule['q'] not in Q or rule['next'] not in Q or rule['letter'] not in letters:
            raise ValueError('invalid source rule')
        if not set(rule['guard']) <= set(alphabet) | {None}:
            raise ValueError('invalid top guard; null denotes empty')
        if rule['op'] not in ('push', 'pop', 'keep') or (rule['op'] == 'push' and rule['symbol'] not in alphabet):
            raise ValueError('invalid stack operation')
    rows = {}
    for row in instance['rows']:
        key = row['q'], row['r'], row['e']
        if key in rows or key[0] not in Q or key[1] not in R or type(key[2]) is not int:
            raise ValueError('invalid or duplicate row')
        rows[key] = DFA(alphabet, row['dfa'])
    empty = DFA(alphabet, empty_spec(alphabet))
    for key, A in sorted(rows.items()):
        w = coordinate_failure(A, key[2])
        if w is not None:
            return {'valid': False, 'reason': 'negative implicit clock', 'mode': list(key), 'stack': list(w)}
    for q in sorted(set(P['initial'])):
        if not rows.get((q, C['initial'], 0), empty).accepts(()):
            return {'valid': False, 'reason': 'initialization', 'q': q}
    for (q, r, e), A in sorted(rows.items()):
        for i, rule in enumerate(P['rules']):
            if rule['q'] != q:
                continue
            nr, c = table[r, rule['letter']]
            for top, clock_zero in product(rule['guard'], (True, False)):
                ne = new_e(e, top, clock_zero, rule['op'], c)
                key = rule['next'], nr, ne
                target = rows.get(key, empty)
                w = branch_failure(A, target, e, top, clock_zero, rule['op'], rule.get('symbol'))
                if w is not None:
                    return {'valid': False, 'reason': 'closure', 'mode': [q, r, e],
                            'stack': list(w), 'rule_index': i, 'clock_zero': clock_zero,
                            'target_mode': list(key), 'target_stack': list(image(rule['op'], rule.get('symbol'), w))}
    return {'valid': True, 'bound': max(abs(e) for (_, _, e), A in rows.items() if A.nonempty())}


def rule(q, a, guard, op, nxt, symbol=None):
    return {'q': q, 'letter': a, 'guard': guard, 'op': op, 'next': nxt, 'symbol': symbol}


def row(q, e, dfa, r=0):
    return {'q': q, 'r': r, 'e': e, 'dfa': dfa}


def make_instance(rules, outputs, rows, states=(0,)):
    return {'source': {'states': list(states), 'initial': [0], 'alphabet': list(outputs),
                       'stack_alphabet': ['A', 'B'], 'rules': rules},
            'clock': {'states': [0], 'initial': 0,
                      'table': [[0, a, 0, c] for a, c in outputs.items()]}, 'rows': rows}


def examples():
    G = ['A', 'B']
    any_top = [None] + G
    epsilon = singleton((), G)
    abstar = spec([[1, 2], [2, 0], [2, 2]], [0])
    babstar = spec([[3, 1], [2, 3], [3, 1], [3, 3]], [1])
    paired = make_instance([
        rule(0, 'a', any_top, 'push', 1, 'B'), rule(1, 'c', ['B'], 'push', 0, 'A'),
        rule(0, 'b', ['A'], 'pop', 2), rule(2, 'd', ['B'], 'pop', 0),
        rule(0, 'x', any_top, 'keep', 0), rule(0, 'x', ['B'], 'push', 0, 'B')],
        {'a': 1, 'c': 1, 'b': -1, 'd': -1, 'x': 0},
        [row(0, 0, abstar), row(1, 0, babstar), row(2, 0, babstar)], (0, 1, 2))
    bottom = make_instance([rule(0, 'x', any_top, 'pop', 0), rule(0, 'x', any_top, 'keep', 0)],
                           {'x': 0}, [row(0, 0, epsilon)])
    once = make_instance([rule(0, 'x', [None], 'push', 0, 'A'), rule(0, 'x', G, 'keep', 0)],
                         {'x': 0}, [row(0, 0, epsilon), row(0, 1, singleton(('A',), G))])
    ahead = json.loads(json.dumps(bottom))
    ahead['clock'] = {'states': [0, 1], 'initial': 0, 'table': [[0, 'x', 1, 1], [1, 'x', 1, 0]]}
    ahead['rows'] = [row(0, 0, epsilon), row(0, -1, epsilon, r=1)]
    allwords = json.loads(json.dumps(paired))
    allwords['rows'] = [row(q, 0, spec([[0, 0]], [0])) for q in range(3)]
    coarse = json.loads(json.dumps(paired))
    coarse['rows'] = [row(0, 0, spec([[1, 2], [1, 1], [2, 2]], [0, 1])),
                      row(1, 0, spec([[2, 1], [1, 1], [2, 2]], [1])),
                      row(2, 0, spec([[2, 1], [1, 1], [2, 2]], [1]))]
    unbounded = make_instance([rule(0, 'x', any_top, 'push', 0, 'A'), rule(0, 'x', any_top, 'keep', 0)],
                              {'x': 0}, [row(0, 0, epsilon), row(0, 1, singleton(('A',), G))])
    malformed = json.loads(json.dumps(bottom))
    malformed['rows'].append(row(0, 1, epsilon))
    long_failure = make_instance([rule(0, 'a', any_top, 'push', 0, 'A')], {'a': 1},
                                 [row(0, 0, spec([[i + 1 if i < 12 else 13, 13] for i in range(14)], range(13)))])
    return [('alternating_symbol_pairs', paired, True), ('bottom_pop_keep', bottom, True),
            ('guarded_push_once', once, True), ('clock_ahead', ahead, True),
            ('forgot_all_symbols', allwords, False), ('kept_only_top', coarse, False),
            ('unbounded_push_keep_candidate', unbounded, False),
            ('invalid_clock_coordinate', malformed, False), ('failure_at_length_twelve', long_failure, False)]


def audit():
    # Exhaust the small unary DFA family; direct membership is the separate oracle.
    family = [DFA(['A'], spec([[a], [b]], [i for i in range(2) if mask >> i & 1]))
              for a, b, mask in product(range(2), range(2), range(4))]
    total = 0
    for old, target, e, top, zero, op in product(family, family, (-1, 0, 1), (None, 'A'), (True, False), ('push', 'pop', 'keep')):
        w = branch_failure(old, target, e, top, zero, op, 'A')
        oracle = None
        for n in range(17):
            v = ('A',) * n
            if (v[0] if v else None) != top or not ((n == e) if zero else (n > e)):
                continue
            if old.accepts(v) and not target.accepts(image(op, 'A', v)):
                oracle = v
                break
        assert w == oracle
        total += 1
    coordinate_cases = 0
    for n in range(6):
        for w in product(('A', 'B'), repeat=n):
            for e, c, op in product(range(-3, 4), (-1, 0, 1), ('push', 'pop', 'keep')):
                H = n - e
                if H < 0:
                    continue
                ne = new_e(e, w[0] if w else None, H == 0, op, c)
                assert ne == len(image(op, 'A', w)) - max(0, H + c)
                coordinate_cases += 1
    return {'unary_dfa_descriptions': len(family), 'exact_product_vs_direct_cases': total,
            'unary_ranges': {'DFA_states': 2, 'start': 0, 'transitions_and_finals': 'all',
                             'e': [-1, 1], 'top_cases': ['empty', 'A'], 'clock_cases': ['zero', 'positive'],
                             'operations': ['push A', 'pop', 'keep'], 'direct_lengths': [0, 16]},
            'coordinate_cases': coordinate_cases,
            'coordinate_ranges': {'alphabet': ['A', 'B'], 'stack_length': [0, 5], 'e': [-3, 3],
                                  'clock_output': [-1, 0, 1], 'operations': ['push A', 'pop', 'keep'],
                                  'restriction': 'nonnegative implicit clock'},
            'status': 'bounded implementation corroboration passed'}


def main():
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument('--check', metavar='JSON')
    args = parser.parse_args()
    if args.check:
        with open(args.check, encoding='utf-8') as f:
            result = check(json.load(f))
        print(json.dumps(result, indent=2, sort_keys=True))
        raise SystemExit(0 if result['valid'] else 1)
    results = []
    for name, instance, expected in examples():
        result = check(instance)
        assert result['valid'] == expected, (name, result)
        results.append({'name': name, 'instance': instance, 'exact_check': result})
    assert len(results[-1]['exact_check']['stack']) == 12
    print(json.dumps({'note': 'regular-stack-certificates.md', 'examples': results,
                     'exact_scope': 'finite-product decisions of all regular certificate obligations',
                     'finite_audit': audit(), 'not_implemented': ['saturation', 'synthesis',
                     'VPA determinization', 'scaffold generation', 'proof assistant']}, indent=2, sort_keys=True))


if __name__ == '__main__':
    main()