verify_cut_response.py

#!/usr/bin/env python3
"""Exact finite audit for cut-response factorization and linear observers."""

from __future__ import annotations

import itertools
import json
from pathlib import Path


def bit(value: int) -> int:
    return value.bit_count() & 1


def gf2_rank(rows: list[int]) -> int:
    basis: dict[int, int] = {}
    for row in rows:
        value = row
        while value:
            pivot = value.bit_length() - 1
            if pivot in basis:
                value ^= basis[pivot]
            else:
                basis[pivot] = value
                break
    return len(basis)


def matrix_rows(mask: int, prefixes: int, continuations: int) -> tuple[tuple[int, ...], ...]:
    return tuple(
        tuple((mask >> (p * continuations + c)) & 1 for c in range(continuations))
        for p in range(prefixes)
    )


def factors_through(rows: tuple[tuple[int, ...], ...], encoding: tuple[int, ...]) -> bool:
    seen: dict[int, tuple[int, ...]] = {}
    for row, code in zip(rows, encoding):
        if code in seen and seen[code] != row:
            return False
        seen[code] = row
    return True


def audit_boolean_matrices() -> dict[str, int]:
    matrices = 0
    cells = 0
    canonical_decodes = 0
    undersized_encodings_rejected = 0

    for prefixes in range(1, 5):
        for continuations in range(1, 5):
            for mask in range(1 << (prefixes * continuations)):
                rows = matrix_rows(mask, prefixes, continuations)
                distinct = tuple(dict.fromkeys(rows))
                code = {row: index for index, row in enumerate(distinct)}
                encoding = tuple(code[row] for row in rows)
                assert factors_through(rows, encoding)

                if len(distinct) > 1:
                    smaller = len(distinct) - 1
                    for candidate in itertools.product(range(smaller), repeat=prefixes):
                        undersized_encodings_rejected += 1
                        assert not factors_through(rows, candidate)

                matrices += 1
                cells += prefixes * continuations
                canonical_decodes += prefixes * continuations

    return {
        "boolean_matrices": matrices,
        "boolean_cells": cells,
        "canonical_decodes": canonical_decodes,
        "undersized_encodings_rejected": undersized_encodings_rejected,
    }


def audit_linear_observers() -> dict[str, int | dict[str, int]]:
    families = 0
    response_entries = 0
    profiles = 0
    support_mutant_failures = 0
    observer_count_mutant_failures = 0
    capacity_checks = 0
    by_dimension: dict[str, int] = {}

    for n in range(1, 5):
        observers = list(range(1 << n))
        family_count = 0
        for mask in range(1 << len(observers)):
            selected = [a for a in observers if (mask >> a) & 1]
            rank = gf2_rank(selected)
            rows = {
                tuple(bit(x & a) for a in selected)
                for x in range(1 << n)
            }
            assert len(rows) == 1 << rank

            max_support = max((a.bit_count() for a in selected), default=0)
            if max_support != rank:
                support_mutant_failures += 1
            if len(selected) != rank:
                observer_count_mutant_failures += 1

            for budget in range(n + 1):
                assert ((1 << rank) <= (1 << budget)) == (rank <= budget)
                capacity_checks += 1

            families += 1
            family_count += 1
            profiles += len(rows)
            response_entries += (1 << n) * len(selected)
        by_dimension[str(n)] = family_count

    # Named opposite-direction witnesses for the support-size mutant.
    for n in range(2, 5):
        coordinate_basis = [1 << index for index in range(n)]
        full_parity = [(1 << n) - 1]
        assert gf2_rank(coordinate_basis) == n
        assert max(a.bit_count() for a in coordinate_basis) == 1
        assert gf2_rank(full_parity) == 1
        assert max(a.bit_count() for a in full_parity) == n

    return {
        "observer_families": families,
        "families_by_ambient_dimension": by_dimension,
        "linear_response_entries": response_entries,
        "distinct_linear_profiles": profiles,
        "capacity_checks": capacity_checks,
        "support_size_mutant_failures": support_mutant_failures,
        "observer_count_mutant_failures": observer_count_mutant_failures,
        "named_opposite_direction_witnesses": 6,
    }


def main() -> None:
    result = {
        "scope": {
            "all_boolean_matrices": "1..4 prefixes by 1..4 continuations",
            "all_binary_linear_observer_families": "ambient dimensions 1..4",
        },
        **audit_boolean_matrices(),
        **audit_linear_observers(),
        "status": "pass",
    }
    output = Path(__file__).with_name("checker-output.json")
    output.write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8")
    print(json.dumps(result, indent=2))


if __name__ == "__main__":
    main()