check_residual_extensions.py

#!/usr/bin/env python3
"""New finite falsification/checks only; imports the authoritative original checker."""
from functools import lru_cache
from itertools import product
import json
from check_tree_witness import GRAMMAR, semantic_accept, selected_leaf, balanced_tree


def bits(n):
    return [''.join(x) for x in product('01', repeat=n)]


def rank(rows):
    pivots = {}
    for row in rows:
        x = int(row or '0', 2)
        while x:
            p = x.bit_length()
            if p in pivots:
                x ^= pivots[p]
            else:
                pivots[p] = x
                break
    return len(pivots)


def literal_peg(word, right_first=False, guarded_start=False):
    @lru_cache(None)
    def parse(nt, at):
        rules = GRAMMAR['A'] if nt == 'Start' else GRAMMAR[nt]
        if nt in ('A', 'Start') and right_first:
            rules = [rules[1], rules[0], rules[2]]
        for rule in rules:
            end = at
            for sym in rule:
                if sym in GRAMMAR:
                    end = parse(sym, end)
                elif end < len(word) and word[end] == sym:
                    end += 1
                else:
                    end = None
                if end is None:
                    break
            if end is not None and (nt != 'Start' or end == len(word)):
                return end
        return None
    return parse('Start' if guarded_start else 'A', 0) == len(word)


@lru_cache(None)
def shapes(n):
    if n == 1:
        return ('[1]',)
    return tuple('t' + a + b for j in range(1, n)
                 for a in shapes(j) for b in shapes(n-j))


def leaves(data):
    # Traversal can use at most one path bit per t in data.
    return [(p, s[::-1]) for k in range(data.count('t') + 1)
            for p in bits(k) if (s := selected_leaf(data, p)) is not None]


def all_residuals_at_cut(data, j):
    eligible = [(p, s) for p, s in leaves(data) if len(s) >= j]
    # This is the COMPLETE finite continuation universe at this cut.
    suffixes = sorted({y + '#' + p[::-1] for p, s in eligible
                       for y in bits(len(s)-j)})
    observed = {tuple(semantic_accept(data + 'FPRD_READING_BODY#39; + v + z) for z in suffixes)
                for v in bits(j)}
    expected = 2 ** rank([s[:j] for _, s in eligible])
    assert len(observed) == expected, (data, j, len(observed), expected)
    return len(observed)


def main():
    failures = {}
    for right_first in (False, True):
        found = None
        for n in range(1, 8):
            for data in shapes(n):
                for p, _ in leaves(data):
                    word = data + '$1#' + p[::-1]
                    assert semantic_accept(word)
                    if not literal_peg(word, right_first):
                        found = {'word': word, 'leaves': n, 'path': p}
                        break
                if found:
                    break
            if found:
                break
        assert found is not None
        failures['right_first' if right_first else 'left_first'] = found

    guarded_failures = {}
    for right_first in (False, True):
        data, q = ('tt[1][1][1]', '10') if right_first else ('t[1]t[1][1]', '01')
        data, q = ('t[0]' + data, q + '1') if right_first else ('t' + data, q + '0')
        word = data + '$1#' + q
        assert semantic_accept(word) and not literal_peg(word, right_first, True)
        guarded_failures['right_first' if right_first else 'left_first'] = word

    data_cases = ['[1]', 't[1]', 't[01][1]', 'tt[100][010]t[001][111]',
                  'tt[1][00]t[011][1]', 't[]t[1][1]', 'tt[10][1]',
                  't[1]t[010][11]', 'tt[0][10]t[111][00]']
    rank_checks = 0
    for base in data_cases:
        for tail in ('', 't', '][', '[1]', 'tt[]'):
            for j in range(5):
                all_residuals_at_cut(base + tail, j)
                rank_checks += 1

    # Match all update-cut ranks and initial query-cut ranks using interleaved
    # identity rows. The hard rows here are arbitrary test data, not a lower bound.
    profiles = []
    for n in (2, 3, 4):
        g = 1 << (n-1).bit_length()
        m = 1 << (n*n + n*g - 1).bit_length()
        hard = ['0'*n for _ in range(m)]
        easy = hard.copy()
        reserved = set()
        for r in range(g):
            for j in range(n):
                slot = r + g*j
                hard[slot] = easy[slot] = '0'*j + '1' + '0'*(n-j-1)
                reserved.add(slot)
        slots = [i for i in range(m) if i not in reserved][:n*n]
        for k, slot in enumerate(slots):
            hard[slot] = format((k*7 + 3) % (1 << n), f'0{n}b')
        for j in range(n+1):
            assert rank([s[:j] for s in hard]) == rank([s[:j] for s in easy]) == j
        for k in range(g.bit_length()):
            for r in range(1 << k):
                ii = list(range(r, m, 1 << k))
                assert rank([hard[i] for i in ii]) == rank([easy[i] for i in ii]) == n
                # Check exact post-query residual cardinalities independently.
                for rows in (hard, easy):
                    data = balanced_tree(rows)
                    qpre = format(r, f'0{k}b')[::-1] if k else ''
                    h = m.bit_length()-1
                    sigs = {tuple(semantic_accept(data+'FPRD_READING_BODY#39;+x+'#'+qpre+z)
                                  for z in bits(h-k)) for x in bits(n)}
                    assert len(sigs) == 1 << n
        profiles.append({'n': n, 'rows': m, 'matched_query_depth': g.bit_length()-1})

    print(json.dumps({'status':'passed', 'literal_peg_counterexamples':failures,
                      'end_guarded_start_counterexamples':guarded_failures,
                      'arbitrary_data_rank_checks':rank_checks,
                      'matched_profiles':profiles,
                      'scope':'Finite tests of new formulas and two specific PEG conversions; no asymptotic lower bound or PEG non-membership proof.'}, indent=2))


if __name__ == '__main__':
    main()