check_derived_prefix_parity.py

#!/usr/bin/env python3
"""Exact checks for the derived-control prefix-parity WFL construction.

Model
-----
Data bits b_1...b_L are read left-to-right.  A binary Mealy encoder emits one
site value a_t after reading b_t.  Then a reversed one-hot selector y_1...y_L
is appended, where y_{L+1-i}=1 selects prefix i.  A fold at the boundary
pairs cell t with selector cell L+1-t, and final Look is

    OR_t (a_t AND y_{L+1-t}).

Thus Look returns a_i.  The target is prefix parity
    p_i = b_1 XOR ... XOR b_i.

The script verifies the construction, exhaustively enumerates all q=1 and
q=2 binary Mealy encoders, and exhibits the failure of controller-state-only
future-row equivalence.
"""

from itertools import product


def prefix_parities(bits):
    p = 0
    ans = []
    for bit in bits:
        p ^= bit
        ans.append(p)
    return tuple(ans)


def midpoint_look(emitted, selected_i):
    """Simulate reverse one-hot + midpoint fold, indices are one-based."""
    L = len(emitted)
    selector = [0] * L
    selector[L - selected_i] = 1
    return int(any(emitted[t] and selector[L - 1 - t] for t in range(L)))


def parity_encoder(bits):
    state = 0
    emitted = []
    for bit in bits:
        state ^= bit  # transition, then emit
        emitted.append(state)
    return state, tuple(emitted)


def run_machine(bits, q, delta, emit):
    state = 0
    out = []
    for bit in bits:
        old = state
        state = delta[old * 2 + bit]
        out.append(emit[old * 2 + bit])
    return state, tuple(out)


def machines(q):
    entries = q * 2
    for delta in product(range(q), repeat=entries):
        for emit in product((0, 1), repeat=entries):
            yield delta, emit


def realizes_prefix_parity(q, delta, emit, max_length):
    for L in range(1, max_length + 1):
        for bits in product((0, 1), repeat=L):
            _, out = run_machine(bits, q, delta, emit)
            if out != prefix_parities(bits):
                return False
    return True


def census(max_length=5):
    result = {}
    for q in (1, 2):
        good = []
        total = 0
        for delta, emit in machines(q):
            total += 1
            if realizes_prefix_parity(q, delta, emit, max_length):
                good.append((delta, emit))
        result[q] = (total, good)
    return result


def check_construction(max_length=8):
    tested = 0
    for L in range(1, max_length + 1):
        for bits in product((0, 1), repeat=L):
            state, emitted = parity_encoder(bits)
            assert state == (sum(bits) & 1)
            target = prefix_parities(bits)
            assert emitted == target
            for i in range(1, L + 1):
                assert midpoint_look(emitted, i) == target[i - 1]
                tested += 1
    return tested


def state_only_counterexample():
    # Same controller state (terminal parity zero), different stored rows.
    u = (0, 0)
    v = (1, 1)
    su, eu = parity_encoder(u)
    sv, ev = parity_encoder(v)
    assert su == sv == 0
    assert eu == (0, 0) and ev == (1, 0)
    assert midpoint_look(eu, 1) == 0
    assert midpoint_look(ev, 1) == 1
    return u, v, su, eu, ev


def aggregate_height_counterexample():
    # Same final state and same number of true emitted sites, but different
    # indexed substrate profiles.
    u = (1, 1, 0)  # emitted trace 100
    v = (0, 1, 1)  # emitted trace 010
    su, eu = parity_encoder(u)
    sv, ev = parity_encoder(v)
    assert su == sv == 0
    assert sum(eu) == sum(ev) == 1
    assert midpoint_look(eu, 1) != midpoint_look(ev, 1)
    return u, v, su, eu, ev


def strict_moore_delay_counterexample():
    """Pre-transition Moore output cannot emit p_1 for both first bits."""
    # At t=1 the pre-transition state is the same initial state for b=0 and b=1.
    # Therefore an output depending on state alone is identical on both inputs.
    return {"input_0_target": 0, "input_1_target": 1, "same_initial_state": True}


def congruence_census(max_length=8):
    """Count state classes and late-query semantic classes at each grade."""
    rows = []
    for L in range(1, max_length + 1):
        words = list(product((0, 1), repeat=L))
        state_classes = {parity_encoder(w)[0] for w in words}
        semantic_rows = {parity_encoder(w)[1] for w in words}
        # The trace map is injective: b_1=p_1 and b_t=p_{t-1} XOR p_t.
        assert len(semantic_rows) == len(words)
        collision_pairs = 0
        distinguished_pairs = 0
        for n, u in enumerate(words):
            su, eu = parity_encoder(u)
            for v in words[n + 1 :]:
                sv, ev = parity_encoder(v)
                if su == sv:
                    collision_pairs += 1
                    if eu != ev:
                        distinguished_pairs += 1
        rows.append(
            (L, len(state_classes), len(semantic_rows), collision_pairs, distinguished_pairs)
        )
    return rows


if __name__ == "__main__":
    tested = check_construction()
    print(f"construction checks: {tested} selected-prefix cases passed")

    result = census()
    for q, (total, good) in result.items():
        print(f"q={q}: {len(good)} / {total} machines realize all prefixes through L=5")
        if good:
            print(f"  first delta={good[0][0]} emit={good[0][1]}")

    u, v, s, eu, ev = state_only_counterexample()
    print("state-only counterexample:")
    print(f"  u={u}, v={v}, shared state={s}, emitted rows={eu} versus {ev}")
    print("  selector i=1 distinguishes them after the data phase")

    u, v, s, eu, ev = aggregate_height_counterexample()
    print("aggregate-height counterexample:")
    print(f"  u={u}, v={v}, shared state={s}, equal site count={sum(eu)}")
    print(f"  indexed emitted rows={eu} versus {ev}; selector i=1 distinguishes")

    delay = strict_moore_delay_counterexample()
    print("strict pre-transition Moore audit:", delay)
    print("  transition-then-emit is sufficient; strict Moore needs one-cell delay/flush")

    print("right-congruence census:")
    print("  L state_classes semantic_rows same_state_pairs distinguished_by_late_query")
    for row in congruence_census():
        print(" ", *row)