verify_direction_stress_test.py

#!/usr/bin/env python3
"""Finite checks accompanying two written proofs, not theorem verification.

Run from any directory; writes JSON next to this script. No third-party modules.
No general BFG/VPA conversion, separation decider, Presburger elimination,
clock-existence algorithm, or scaffold generator is implemented.
"""
from dataclasses import dataclass
from fractions import Fraction
from itertools import product
from math import factorial
from pathlib import Path
import json


@dataclass(frozen=True)
class Cell:
    last: bool
    tail: object = None


def chain(n):
    root = None
    for _ in range(n):
        root = Cell(root is None, root)
    return root


def length(root):
    n = 0
    while root is not None:
        n += 1
        root = root.tail
    return n


def sign(z):
    return (z > 0) - (z < 0)


def unit_update(sgn, root, carry):
    """Branches use sign and old top label only; at most one allocation."""
    if carry == 0:
        return sgn, root, 0
    if sgn == 0 or sgn == carry:
        return carry, Cell(sgn == 0, root), 1
    return (0 if root.last else sgn), root.tail, 0


def arithmetic_checks():
    cases = 0
    maximum_allocation = 0
    for modulus in range(1, 9):
        for z in range(-80, 81):
            q, r = divmod(z, modulus)
            root = chain(abs(q))
            for delta in range(-modulus, modulus + 1):
                carry, new_r = divmod(r + delta, modulus)
                assert carry in (-1, 0, 1)
                new_sign, new_root, allocated = unit_update(sign(q), root, carry)
                observed = modulus * new_sign * length(new_root) + new_r
                assert observed == z + delta
                assert (new_sign >= 0) == (observed >= 0)
                assert (new_sign == 0 and new_r == 0) == (observed == 0)
                assert length(root) == abs(q)  # old immutable version retained
                maximum_allocation = max(maximum_allocation, allocated)
                cases += 1
    # Explicit two-monitor example, checked at every prefix of every sampled word.
    prefixes = 0
    for size in range(9):
        for letters in product('abc', repeat=size):
            signs, roots = [0, 0], [None, None]
            counts = dict.fromkeys('abc', 0)
            previous = 'a'
            ordered = True
            for letter in letters:
                ordered = ordered and letter >= previous
                previous = letter
                counts[letter] += 1
                increments = {'a': (1, 0), 'b': (-1, 1), 'c': (0, -1)}[letter]
                for i, delta in enumerate(increments):
                    signs[i], roots[i], allocated = unit_update(signs[i], roots[i], delta)
                    assert allocated <= 1
                answer = ordered and signs == [0, 0]
                oracle = ordered and counts['a'] == counts['b'] == counts['c']
                assert answer == oracle
                prefixes += 1
    return {'local_domain': 'M=1..8, Z=-80..80, every delta=-M..M',
            'local_cases': cases, 'maximum_allocations_per_monitor_step': maximum_allocation,
            'example': 'a^n b^n c^n; all abc words of length <=8, every prefix',
            'example_prefix_checks': prefixes}


def clock_cycle(nxt, out, start):
    seen, states = {}, []
    r = start
    while r not in seen:
        seen[r] = len(states)
        states.append(r)
        r = nxt[r]
    cycle = states[seen[r]:]
    return Fraction(sum(out[q] for q in cycle), len(cycle))


def tail_checks():
    cases = 0
    # Check a finite error envelope implied by unary transient/cycle analysis.
    for s in (1, 2, 3):
        for nxt in product(range(s), repeat=s):
            for out in product((-1, 0, 1), repeat=s):
                for start in range(s):
                    mu = clock_cycle(nxt, out, start)
                    for initial in (0, 3, 11):
                        r, height = start, initial
                        for ticks in range(1, 81):
                            height = max(0, height + out[r])
                            r = nxt[r]
                            ideal = max(Fraction(0), initial + mu * ticks)
                            # Signed-sum deviation <=4s, reflection <=8s.
                            assert abs(height - ideal) <= 8 * s
                        cases += 1
    # Positive pair W x / W y. The separator reads the last marker.
    examples = []
    for depth in range(13):
        for marker in ('x', 'y'):
            source_root = None
            clock_h = 0
            word = '(' * depth + ')' * depth + marker + '#'
            for char in word:
                if char == '(':
                    source_root = Cell(source_root is None, source_root)
                    clock_h += 1
                elif char == ')':
                    source_root = source_root.tail
                    clock_h = max(0, clock_h - 1)
                assert clock_h == length(source_root)
            mode = int(marker == 'x')
            for _ in range(25):
                if mode:
                    source_root = Cell(source_root is None, source_root)
                    clock_h += 1
                assert clock_h == length(source_root)
            examples.append({'nesting': depth, 'mode': mode, 'tail_height': clock_h})
    return {'unary_graphs': 'all total t transitions and -1/0/1 outputs on 1..3 states',
            'initial_heights': [0, 3, 11], 'tail_length': 80, 'cases': cases,
            'positive_separator_examples': examples}


def collision_checks():
    unary = 0
    for s in range(1, 6):
        for transition in product(range(s), repeat=s):
            for start in range(s):
                q = start
                for _ in range(s):
                    q = transition[q]
                after_n = q
                for _ in range(factorial(s)):
                    q = transition[q]
                assert q == after_n
                unary += 1
    # Every two-state transition table on the four-letter alphabet.
    s, n, p = 2, 2, 2
    u, v = 'a'*n+'b'*n+'c'*n+'d'*n, 'a'*(n+p)+'b'*n+'c'*n+'d'*(n+p)
    collisions = 0
    for table in product(range(s), repeat=4*s):
        def run(word):
            q = 0
            for char in word:
                q = table['abcd'.index(char)*s + q]
            return q
        assert run(u) == run(v)
        collisions += 1
    return {'unary_identity': 'f^s=f^(s+s!), all functions on s=1..5 states',
            'unary_start_cases': unary,
            'two_state_four_letter_tables': collisions, 'example_K1': u, 'example_K0': v,
            'unrestricted_claim': 'proved algebraically in the note, not by this enumeration'}


def main():
    result = {'status': 'finite executable corroboration only; no formal verification',
              'arithmetic': arithmetic_checks(), 'tail_clocks': tail_checks(),
              'separator_collisions': collision_checks(),
              'not_implemented': ['BFG-to-VPA reduction', 'VPA determinization',
                                  'general separator synthesis', 'Presburger quantifier elimination',
                                  'general scaffold compiler', 'unrestricted clock synthesis']}
    path = Path(__file__).with_name('direction-stress-test-output.json')
    path.write_text(json.dumps(result, indent=2) + '\n')
    print(json.dumps({'passed': True, 'output': path.name,
                      'scope': result['status']}, indent=2))


if __name__ == '__main__':
    main()