verify_replay_fanout.py

#!/usr/bin/env python3
"""Exact finite audit for the replay fan-out separation.

For r through 12, enumerate every bit vector b, construct p_b=0^r b,
and check that odd zero paddings select each coordinate of b as the middle
bit. The response signatures must be all 2^r bit vectors, while every
completed observation queries exactly one prefix coordinate.
"""

from __future__ import annotations

from itertools import product
import json


MAX_R = 12


def middle_position(word: str) -> int:
    """Return the one-based ceil(|word|/2) position."""
    return (len(word) + 1) // 2


def accepted(word: str) -> int:
    return int(word[middle_position(word) - 1] == "1")


def main() -> None:
    prefix_count = 0
    unit_slice_checks = 0
    mutation_checks = 0
    profile_count = 0
    rows = []

    for r in range(1, MAX_R + 1):
        signatures = set()
        selected_positions = set()

        for bits_tuple in product("01", repeat=r):
            bits = "".join(bits_tuple)
            prefix = "0" * r + bits
            prefix_count += 1
            response = []

            for j in range(1, r + 1):
                continuation = "0" * (2 * j - 1)
                completed = prefix + continuation
                position = middle_position(completed)
                assert position == r + j
                assert position <= len(prefix)
                assert accepted(completed) == int(bits[j - 1])
                selected_positions.add(position)
                unit_slice_checks += 1

                mutated_bits = list(bits)
                mutated_bits[j - 1] = "1" if bits[j - 1] == "0" else "0"
                mutated = "0" * r + "".join(mutated_bits) + continuation
                assert accepted(mutated) == 1 - accepted(completed)
                mutation_checks += 1
                response.append(accepted(completed))

            signatures.add(tuple(response))

        assert len(signatures) == 2**r
        assert selected_positions == set(range(r + 1, 2 * r + 1))
        profile_count += len(signatures)
        rows.append(
            {
                "r": r,
                "prefixes": 2**r,
                "selected_old_cells": r,
                "distinct_response_profiles": len(signatures),
                "minimum_configuration_bits": r,
            }
        )

    report = {
        "ok": True,
        "range": {"r_min": 1, "r_max": MAX_R},
        "counts": {
            "prefixes": prefix_count,
            "unit_slice_checks": unit_slice_checks,
            "single_bit_mutation_checks": mutation_checks,
            "distinct_response_profiles": profile_count,
        },
        "rows": rows,
    }
    print(json.dumps(report, indent=2, sort_keys=True))


if __name__ == "__main__":
    main()