verify_selector_covers.py

#!/usr/bin/env python3
"""Finite product audit for FPRD-T167 and logic audit for FPRD-T168."""

from __future__ import annotations

import itertools
import json
from pathlib import Path


BITS = (0, 1)


def words(max_len):
    yield ()
    for n in range(1, max_len + 1):
        yield from itertools.product(BITS, repeat=n)


WORDS = tuple(words(4))


def one_state_selectors():
    """All one-state binary synchronous selectors."""
    for outputs in itertools.product(BITS, repeat=2):
        yield outputs


def transduce(selector, word):
    return tuple(selector[a] for a in word)


def run_source(table, accepting, word):
    state = 0
    trace = []
    for letter in word:
        state, action = table[2 * state + letter]
        trace.append(action)
    return state, tuple(trace), state in accepting


def run_packed(table, accepting, selectors, word):
    states = [0] * len(selectors)
    traces = [[] for _ in selectors]
    for letter in word:
        for i, selector in enumerate(selectors):
            emitted = selector[letter]
            states[i], action = table[2 * states[i] + emitted]
            traces[i].append(action)
    return tuple(states), tuple(tuple(t) for t in traces), any(
        state in accepting for state in states
    )


def audit_finite_covers():
    selectors = tuple(one_state_selectors())
    choices = tuple(itertools.product(BITS, BITS))  # next state, local action
    comparisons = 0
    families = 0

    for table in itertools.product(choices, repeat=4):
        for mask in range(4):
            accepting = frozenset(i for i in BITS if mask & (1 << i))
            for width in (1, 2, 3):
                for family in itertools.product(selectors, repeat=width):
                    families += 1
                    for word in WORDS:
                        sources = tuple(
                            run_source(table, accepting, transduce(selector, word))
                            for selector in family
                        )
                        packed = run_packed(table, accepting, family, word)
                        assert packed[0] == tuple(source[0] for source in sources)
                        assert packed[1] == tuple(source[1] for source in sources)
                        assert packed[2] == any(source[2] for source in sources)
                        comparisons += 1
    return len(selectors), families, comparisons


def audit_raw_cover_growth():
    checks = 0
    witnesses = []
    for hidden_choices in range(2, 6):
        for selector_count in range(1, 65):
            n = 0
            while hidden_choices**n <= selector_count:
                n += 1
            assert hidden_choices**n > selector_count
            witnesses.append((hidden_choices, selector_count, n))
            checks += 1
    return checks, witnesses


def audit_hard_lift_logic():
    # Encoded implications only. External premises are not reverified here.
    visible_lift_in_sca = True
    projection_outside_sca = True
    finite_selector_cover = False
    if visible_lift_in_sca and projection_outside_sca:
        finite_selector_cover = False
    assert not finite_selector_cover
    return {
        "visible_lift_transport": "finite",
        "projected_transport": "infinite",
        "causal_selection_number": "infinity",
    }


def main():
    selector_count, families, comparisons = audit_finite_covers()
    growth_checks, witnesses = audit_raw_cover_growth()
    output = {
        "status": "pass",
        "scope": "finite selector product identity and implication orientation",
        "does_not_verify": [
            "FPRD-T91's visible-lift construction",
            "the persistent-stack compiler in full generality",
            "Kim-Park Theorem 4.19 or its Lean artifact",
            "necessity of finite selector covers for arbitrary SCA projections",
        ],
        "one_state_binary_selectors": selector_count,
        "packed_selector_families": families,
        "packed_run_comparisons": comparisons,
        "raw_cover_growth_checks": growth_checks,
        "largest_raw_cover_witness": witnesses[-1],
        "resource_bound": "(m*d,k,g^m,q^m*product(s_i))",
        "hard_lift": audit_hard_lift_logic(),
    }
    Path(__file__).with_name("checker-output.json").write_text(
        json.dumps(output, indent=2) + "\n", encoding="utf-8"
    )
    print(json.dumps(output, indent=2))


if __name__ == "__main__":
    main()