"""MIRROR_AUDIT: deterministic checks for the declared root and reader protocol.

This file establishes only the finite algebra and toy-reader schemas named
below. Economic, legal, physical, and clinical adapters need their own sources.
"""

from __future__ import annotations

from dataclasses import asdict, dataclass
import json
from typing import Callable, Hashable, Iterable, TypeVar

from condition_constraint_can_translator import (
    G,
    I,
    L_PHI_RAW,
    PHASE_I,
    Q,
    S_RAW,
    Mat2,
    root_exact,
    self_test,
)


T = TypeVar("T", bound=Hashable)
U = TypeVar("U", bound=Hashable)
V = TypeVar("V", bound=Hashable)


@dataclass(frozen=True)
class AuditCheck:
    gate: str
    status: str
    receipt: str


def fiber_refines(states: Iterable[T], reader: Callable[[T], U], decision: Callable[[T], V]) -> bool:
    states = tuple(states)
    return all(reader(x) != reader(y) or decision(x) == decision(y) for x in states for y in states)


def decision_collision(
    states: Iterable[T], reader: Callable[[T], U], decision: Callable[[T], V]
) -> tuple[T, T] | None:
    states = tuple(states)
    for x in states:
        for y in states:
            if reader(x) == reader(y) and decision(x) != decision(y):
                return x, y
    return None


def factor_through_read(
    states: Iterable[T], reader: Callable[[T], U], decision: Callable[[T], V]
) -> dict[U, V] | None:
    """Return the decoder or None when the reader has a decision collision."""
    decoder: dict[U, V] = {}
    for state in states:
        coordinate, value = reader(state), decision(state)
        if coordinate in decoder and decoder[coordinate] != value:
            return None
        decoder[coordinate] = value
    return decoder


def mirror_root_checks() -> AuditCheck:
    l_phi_inverse_raw = Mat2(2, -1, -1, 3)
    d2 = I.scale(2)
    assert root_exact()
    assert G @ S_RAW @ G == S_RAW.scale(-5)       # H S H = -S, cleared
    assert G @ L_PHI_RAW @ G == l_phi_inverse_raw.scale(5)
    assert L_PHI_RAW @ l_phi_inverse_raw == I.scale(5)
    assert G @ PHASE_I @ G == PHASE_I.scale(-5)    # H i H = -i, cleared
    assert G @ d2 @ G == d2.scale(5)               # H D_2 H = D_2, cleared
    return AuditCheck(
        "Condition",
        "PASS",
        "Q, Omega, G, scalar, lift, and phase identities hold after clearing irrational denominators.",
    )


def translator_checks() -> AuditCheck:
    observed = {(x["name"], x["gate"], x["reason"]) for x in self_test()}
    required = {
        ("scalar<2>", "can", ""),
        ("scalar<0>", "fold", "constraint"),
        ("golden_lift", "can", ""),
        ("phase_i_sqrt7", "can", ""),
        ("phase_as_scalar", "fold", "constraint"),
        ("untyped", "fold", "untyped"),
    }
    assert observed == required
    return AuditCheck(
        "Type",
        "PASS",
        "Typed -> Condition -> Constraint -> Can|Fold is exercised on six deterministic paths.",
    )


@dataclass(frozen=True)
class SettlementState:
    gross_in: int
    gross_out: int


def net(state: SettlementState) -> int:
    return state.gross_in - state.gross_out


def gross_total(state: SettlementState) -> int:
    return state.gross_in + state.gross_out


def reader_fiber_checks() -> list[AuditCheck]:
    states = (SettlementState(1, 1), SettlementState(2, 2))
    assert decision_collision(states, net, gross_total) is not None
    assert factor_through_read(states, net, gross_total) is None
    assert fiber_refines(states, net, net)
    return [
        AuditCheck(
            "Constraint",
            "PASS",
            "A same-read / different-decision pair blocks a coordinate-only factorization on its declared reader fiber.",
        ),
        AuditCheck(
            "Falsifier",
            "PASS",
            "The finite witness makes the failure condition explicit rather than silently choosing one preimage.",
        ),
    ]


def transport_return_checks() -> list[AuditCheck]:
    def reader(x: int) -> int:
        return x % 2

    def policy(coordinate: int) -> int:
        return coordinate + 1

    def plant(state: int, action: int) -> int:
        return state + action

    def closed_loop(state: int) -> int:
        return plant(state, policy(reader(state)))

    assert closed_loop(3) == plant(3, policy(reader(3)))
    assert factor_through_read((0, 1, 2, 3), reader, reader) == {0: 0, 1: 1}
    phase = lambda n: n % 4
    assert phase(11 + 4) == phase(11)
    assert 11 + 4 != 11
    return [
        AuditCheck("Transport", "PASS", "The closed loop is T(x, kappa(R(x))); the read alone is not an action."),
        AuditCheck("Return", "PASS", "The phase reader returns after four ticks while the occurrence index advances."),
    ]


def run_audit() -> dict[str, object]:
    checks = [mirror_root_checks(), translator_checks(), *reader_fiber_checks(), *transport_return_checks()]
    checks.append(
        AuditCheck(
            "Receipt",
            "PASS",
            "All declared finite checks passed with exact integer arithmetic and finite witnesses.",
        )
    )
    return {
        "audit": "MIRROR_AUDIT root carrier + retained reader fibers",
        "status": "PASS",
        "checks": [asdict(check) for check in checks],
        "boundary": (
            "This receipt establishes only the declared finite algebra and toy-reader schemas; "
            "external adapters require their own evidence."
        ),
    }


if __name__ == "__main__":
    print(json.dumps(run_audit(), indent=2))