check_tree_witness.py

#!/usr/bin/env python3
"""Independent CFG-derivation counting, tree semantics, and reduction checks.

Finite corroboration only. The universal results require the proofs in the packet.
No third-party dependencies.
"""
from functools import lru_cache
from itertools import product
import json
import random

DATA = 't[]01'
GRAMMAR = {
    'A': [('t', 'A', '0'), ('t', 'T', 'A', '1'), ('[', 'P1', '#')],
    'T': [('t', 'T', 'T'), ('[', 'B', ']')],
    'B': [('0', 'B'), ('1', 'B'), ('0',), ('1',)],
    'R': [(a, 'R') for a in DATA] + [()],
    'P0': [(']', 'R', 'FPRD_READING_BODY#39;), ('0', 'P0', '0'), ('0', 'P0', '1'),
           ('1', 'P0', '0'), ('1', 'P1', '1')],
    'P1': [('0', 'P1', '0'), ('0', 'P1', '1'), ('1', 'P1', '0'),
           ('1', 'P0', '1')],
}


def derivations(word, start='A'):
    """Count parse trees for the literal CFG, capped at 2, for a whole word."""
    @lru_cache(None)
    def nt(name, pos):
        result = {}
        for rhs in GRAMMAR[name]:
            frontier = {pos: 1}
            for symbol in rhs:
                next_frontier = {}
                for at, ways in frontier.items():
                    if symbol in GRAMMAR:
                        endings = nt(symbol, at)
                    elif at < len(word) and word[at] == symbol:
                        endings = {at + 1: 1}
                    else:
                        endings = {}
                    for end, subways in endings.items():
                        next_frontier[end] = min(2, next_frontier.get(end, 0) + ways * subways)
                frontier = next_frontier
                if not frontier:
                    break
            for end, ways in frontier.items():
                result[end] = min(2, result.get(end, 0) + ways)
        return result
    return nt(start, 0).get(len(word), 0)


def read_leaf(data, pos):
    if pos >= len(data) or data[pos] != '[':
        return None
    end = pos + 1
    while end < len(data) and data[end] in '01':
        end += 1
    if end == pos + 1 or end >= len(data) or data[end] != ']':
        return None
    return data[pos + 1:end], end + 1


def skip_tree(data, pos):
    """Iterative prefix-code parser; unrelated to the CFG count routine."""
    pending = 1
    while pending:
        if pos >= len(data):
            return None
        if data[pos] == 't':
            pending += 1
            pos += 1
        else:
            leaf = read_leaf(data, pos)
            if leaf is None:
                return None
            _, pos = leaf
            pending -= 1
    return pos


def selected_leaf(data, path):
    """Follow the externally supplied root-to-leaf path in a tree prefix."""
    pos = 0
    for bit in path:
        if pos >= len(data) or data[pos] != 't':
            return None
        pos += 1
        if bit == '1':
            pos = skip_tree(data, pos)
            if pos is None:
                return None
    leaf = read_leaf(data, pos)
    return None if leaf is None else leaf[0]


def semantic_accept(word):
    if word.count('FPRD_READING_BODY#39;) != 1 or word.count('#') != 1:
        return False
    data, rest = word.split('FPRD_READING_BODY#39;)
    if '#' not in rest or any(a not in DATA for a in data):
        return False
    x, q = rest.split('#')
    if not x or any(a not in '01' for a in x + q):
        return False
    s = selected_leaf(data, q[::-1])
    return s is not None and len(s) == len(x) and sum(int(a) * int(b) for a, b in zip(s[::-1], x)) % 2 == 1


def balanced_tree(rows):
    if len(rows) == 1:
        return '[' + rows[0][::-1] + ']'
    assert len(rows) % 2 == 0
    h = len(rows) // 2
    return 't' + balanced_tree(rows[:h]) + balanced_tree(rows[h:])


def encoded_word(rows, x, index):
    n = len(x)
    assert all(len(row) == n for row in rows)
    m = 1 << (len(rows) - 1).bit_length()
    padded = rows + ['0' * n] * (m - len(rows))
    h = m.bit_length() - 1
    path = '' if h == 0 else format(index, '0%db' % h)
    return balanced_tree(padded) + 'FPRD_READING_BODY#39; + x + '#' + path[::-1]


def main():
    stats = {'lexical_words': 0, 'structured_words': 0, 'hard_encodings': 0,
             'random_mutations': 0, 'accepted': 0, 'max_derivations': 0}
    samples = []

    def check(word, group, expected=None):
        semantic = semantic_accept(word)
        count = derivations(word)
        assert count == int(semantic), (word, count, semantic)
        if expected is not None:
            assert semantic == expected, (word, semantic, expected)
        stats[group] += 1
        stats['accepted'] += semantic
        stats['max_derivations'] = max(stats['max_derivations'], count)

    # Exhaust malformed and partial data prefixes; q may be empty or invalid-depth.
    for size in range(5):
        for letters in product(DATA, repeat=size):
            data = ''.join(letters)
            for x in ('0', '1'):
                for qsize in range(3):
                    for q in product('01', repeat=qsize):
                        check(data + 'FPRD_READING_BODY#39; + x + '#' + ''.join(q), 'lexical_words')

    # Longer trees, arbitrary ignored tails, and different-depth query paths.
    data_cases = ['[1]', 't[1][0]', 't[0][1]', 'tt[1][0][1]',
                  't[1]t[0][1]', 'tt[10][01]t[11][00]',
                  't[1]', 't[0][1][1]', 't[]t[1][1]', 'tt[1][0]']
    for data in data_cases:
        for tail in ('', 't', '][', '[101]', 'tt[]'):
            for x in ('0', '1', '00', '01', '10', '11', '101'):
                for qsize in range(4):
                    for q in product('01', repeat=qsize):
                        check(data + tail + 'FPRD_READING_BODY#39; + x + '#' + ''.join(q), 'structured_words')

    # Exact finite reductions, including non-power-of-two padding.
    for n, row_count in ((1, 1), (1, 2), (1, 4), (2, 3), (2, 4), (3, 2)):
        vectors = [''.join(bits) for bits in product('01', repeat=n)]
        for rows_tuple in product(vectors, repeat=row_count):
            rows = list(rows_tuple)
            for x in vectors:
                for i in range(row_count):
                    expected = bool(sum(int(a) * int(b) for a, b in zip(rows[i], x)) % 2)
                    word = encoded_word(rows, x, i)
                    check(word, 'hard_encodings', expected)
                    if len(samples) < 20 and expected:
                        samples.append(word)

    rng = random.Random(20260904)
    seeds = [encoded_word(['01', '11', '10', '00'], x, i)
             for x in ('00', '01', '10', '11') for i in range(4)]
    alphabet = DATA + '$#z'
    for _ in range(1500):
        word = rng.choice(seeds)
        at = rng.randrange(len(word) + 1)
        kind = rng.randrange(3)
        if kind == 0:
            word = word[:at] + rng.choice(alphabet) + word[at:]
        elif kind == 1 and at < len(word):
            word = word[:at] + word[at + 1:]
        elif at < len(word):
            word = word[:at] + rng.choice(alphabet) + word[at + 1:]
        check(word, 'random_mutations')

    print(json.dumps({'status': 'passed', 'counts': stats, 'accepted_examples': samples,
                      'scope': 'Finite corroboration of grammar unambiguity, semantic equivalence, and hard-word encoding; not a proof of non-PEG.'}, indent=2))


if __name__ == '__main__':
    main()