infer_stack_clocks.py

#!/usr/bin/env python3
"""Finite-cycle clock certificates and explicitly bounded corroboration.

Source edges are (from_state, input_letter, nominal_action, to_state).
Guards and symbols are deliberately absent from this conservative abstraction.
The mathematical note explains why any source with this abstraction is covered.
No general pushdown solver or proof-assistant verification is implemented.
"""
from itertools import product
import json
from pathlib import Path


def graph_for(edges, initials, transition, output, start=0):
    """Reachable guard-erased source x input-observer product."""
    seeds = {(q, start) for q in initials}
    seen, pending, weighted = set(seeds), list(seeds), []
    while pending:
        q, r = pending.pop()
        for p, a, d, target in edges:
            if p != q:
                continue
            assert d in (-1, 0, 1)
            v = (target, transition[r, a])
            weighted.append(((q, r), v, d - output[r, a]))
            if v not in seen:
                seen.add(v)
                pending.append(v)
    return seen, seeds, weighted


def path_bounds(vertices, initials, edges):
    """Return a certificate or None for an unbounded signed-path abstraction.

The Nth relaxation detects a reachable positive or negative cycle. None is
not a conclusion about legal source runs, reflected heights, or languages.
"""
    n = len(vertices)
    assert n > 0 and set(initials) <= set(vertices)
    lo = {v: 0 for v in initials}
    hi = dict(lo)
    for _ in range(n - 1):
        lo2, hi2 = dict(lo), dict(hi)
        for u, v, w in edges:
            if u in lo:
                lo2[v] = min(lo2.get(v, lo[u] + w), lo[u] + w)
                hi2[v] = max(hi2.get(v, hi[u] + w), hi[u] + w)
        lo, hi = lo2, hi2
    for u, v, w in edges:
        if u in lo and (v not in lo or lo[u] + w < lo[v]
                        or hi[u] + w > hi[v]):
            return None
    lower, upper = min(lo.values()), max(hi.values())
    return dict(lower=lower, upper=upper, bound=upper-lower,
                minimum=lo, maximum=hi, reachable_vertices=len(lo))


def check_certificate(initials, edges, cert):
    """Independent local inequalities verify any proposed path bound."""
    lo, hi = cert['minimum'], cert['maximum']
    assert all(lo[v] <= 0 <= hi[v] for v in initials)
    for u, v, w in edges:
        if u in lo:
            assert v in lo and v in hi
            assert lo[v] <= lo[u] + w and hi[v] >= hi[u] + w
    assert cert['lower'] == min(lo.values())
    assert cert['upper'] == max(hi.values())
    assert cert['bound'] == cert['upper'] - cert['lower']


def infer(edges, initials, alphabet, budget):
    """Exhaust all observer tables through the supplied positive state budget.

Returns the first certificate found, or None if this finite certificate
search is exhausted. It does not decide unrestricted clock existence.
"""
    assert budget >= 1
    tried = 0
    for k in range(1, budget + 1):
        keys = list(product(range(k), alphabet))
        for dests in product(range(k), repeat=len(keys)):
            transition = dict(zip(keys, dests))
            for actions in product((0, 1, -1), repeat=len(keys)):
                output = dict(zip(keys, actions))
                tried += 1
                vertices, seeds, weighted = graph_for(
                    edges, initials, transition, output)
                cert = path_bounds(vertices, seeds, weighted)
                if cert is not None:
                    check_certificate(seeds, weighted, cert)
                    return dict(states=k, transition=transition, output=output,
                                certificate=cert, candidates_tested=tried)
    return None


def compact(result):
    if result is None:
        return None
    return dict(states=result['states'],
                table=[dict(state=r, letter=a,
                            next_state=result['transition'][r, a],
                            action=result['output'][r, a])
                       for r, a in result['transition']],
                interval=[result['certificate']['lower'],
                          result['certificate']['upper']],
                bound=result['certificate']['bound'],
                candidates_tested=result['candidates_tested'])


def graph_audit():
    # Independent oracle: a two-vertex graph has only self loops and the
    # two-edge cycle as directed simple cycles. Unreachable cycles are ignored.
    cases = 0
    locations = list(product(range(2), repeat=2))
    for values in product((None, -2, -1, 0, 1, 2), repeat=4):
        w = dict(zip(locations, values))
        reached = {0, 1} if w[0, 1] is not None else {0}
        bad = any(w[v, v] not in (None, 0) for v in reached)
        if 1 in reached and w[1, 0] is not None:
            bad |= w[0, 1] + w[1, 0] != 0
        edges = [(u, v, z) for (u, v), z in w.items() if z is not None]
        cert = path_bounds({0, 1}, {0}, edges)
        assert (cert is None) == bad
        if cert:
            check_certificate({0}, edges, cert)
        cases += 1
    # An acyclic join with two path weights is valid; global exact-potential
    # checking would incorrectly reject it.
    diamond = [(0, 1, 0), (0, 2, 1), (1, 3, 0), (2, 3, 0)]
    c = path_bounds(set(range(4)), {0}, diamond)
    assert (c['lower'], c['upper']) == (0, 1)
    return dict(two_vertex_graphs=cases, edge_weights=[-2,-1,0,1,2],
                oracle='explicit simple-cycle enumeration', acyclic_join=True)


def reflection_audit():
    pairs = list(product((-1, 0, 1), repeat=2))
    count = 0
    for n in range(6):
        for actions in product(pairs, repeat=n):
            x = y = h = H = mx = my = lower = upper = 0
            for d, c in actions:
                x += d
                y += c
                mx, my = min(mx, x), min(my, y)
                h, H = max(0, h+d), max(0, H+c)
                lower, upper = min(lower, x-y), max(upper, x-y)
                assert h == x-mx and H == y-my
                assert abs(h-H) <= upper-lower
            count += 1
    return dict(max_length=5, paired_action_words=count,
                oracle='direct nonnegative unit-height updates')


def examples():
    early_late = [
        ('build','a',1,'be'), ('build','a',0,'bl'),
        ('be','c',0,'build'), ('bl','c',1,'build'),
        ('build','b',-1,'re'), ('build','b',0,'rl'),
        ('drain','b',-1,'re'), ('drain','b',0,'rl'),
        ('re','d',0,'drain'), ('rl','d',-1,'drain')]
    tau = {(0,a):0 for a in 'acbd'}
    out = {(0,a):d for a,d in zip('acbd',(1,0,-1,0))}
    v,i,e = graph_for(early_late, {'build'}, tau, out)
    cert = path_bounds(v,i,e)
    check_certificate(i,e,cert)
    assert (cert['lower'],cert['upper'],cert['bound']) == (-1,1,2)
    inferred = infer(early_late, {'build'}, 'acbd', 1)
    assert inferred is not None

    phase = [('build','a',1,'build'), ('build','#',0,'drain'),
             ('drain','a',-1,'drain')]
    assert infer(phase, {'build'}, 'a#', 1) is None
    phase_result = infer(phase, {'build'}, 'a#', 2)
    assert phase_result and phase_result['states'] == 2
    assert phase_result['certificate']['bound'] == 0

    push_keep = [(0,'x',1,0), (0,'x',0,0)]
    pop_keep = [(0,'x',-1,0), (0,'x',0,0)]
    assert infer(push_keep, {0}, 'x', 3) is None
    assert infer(pop_keep, {0}, 'x', 3) is None
    # Legal bottom-only runs, and guarded push-once runs, have bounded height
    # despite failing the graph certificate. These are finite corroborations;
    # the note supplies the every-length arguments.
    for n in range(9):
        for actions in product((-1, 0), repeat=n):
            h = 0
            for d in actions:
                h = max(0, h+d)
                assert h == 0
        assert abs(n-0) == n  # push-all versus keep-all legal heights
    return dict(early_late_supplied_clock=dict(interval=[-1,1],bound=2),
                early_late_inferred=compact(inferred),
                phase_inferred=compact(phase_result),
                negative_search_max_observer_states=3,
                push_keep_rejected=True, pop_keep_rejected=True,
                bottom_only_max_length=8,
                guarded_push_once='same abstract graph as push/keep; height <= 1')


def main():
    report = dict(
        status='passed',
        scope='Finite-cycle certificate implementation and bounded corroboration.',
        graph=graph_audit(), reflection=reflection_audit(), examples=examples(),
        not_verified=[
            'unrestricted theorems in a proof assistant',
            'VPA generator, determinization or general pushdown reachability',
            'record-to-scaffold compiler',
            'completeness for bounded actual-height skew',
            'optimal clock size or smallest actual skew bound',
            'literature novelty'])
    Path(__file__).with_name('clock-inference-output.json').write_text(
        json.dumps(report, indent=2) + '\n')
    print(json.dumps(report, indent=2))


if __name__ == '__main__':
    main()