"""Regression checks for the causal-event / online-chain transfer.

The mathematical theorem imported in the accompanying packet is the exact
online chain-partition value for represented, two-dimensional, up-growing
posets.  This checker verifies the FPRD-specific compilation seam:

    (x, y)  ->  event (t, p) = (K + x + y, C - y).

Under hold-or-recede-one motion, event e can precede event f exactly when the
two source coordinates are componentwise ordered.

It also keeps two hostile controls:

* the existing width-two event adversary really needs three online tracks;
* if revelation is forced to occur at service time, not every *supplied
  realizer* can be made diagonal merely by monotonically respacing its two
  coordinate orders.  The exact transfer therefore uses a pre-execution
  announcement/commitment layer and does not silently prove a real-time
  theorem.  This control is not a representation-independent obstruction:
  the same poset may have another realizer that does admit diagonal timing.
"""

from __future__ import annotations

from itertools import combinations, permutations, product


def event_of(point: tuple[int, int], k_shift: int = 20, c_shift: int = 20):
    x, y = point
    return k_shift + x + y, c_shift - y


def causal_precedes(e: tuple[int, int], f: tuple[int, int]) -> bool:
    t, p = e
    u, q = f
    return t <= u and q <= p and p - q <= u - t


def product_precedes(a: tuple[int, int], b: tuple[int, int]) -> bool:
    return a[0] <= b[0] and a[1] <= b[1]


def width(events: list[tuple[int, int]]) -> int:
    for size in range(len(events), -1, -1):
        for subset in combinations(events, size):
            if all(
                not causal_precedes(a, b) and not causal_precedes(b, a)
                for a, b in combinations(subset, 2)
            ):
                return size
    return 0


def min_chain_cover(events: list[tuple[int, int]]) -> int:
    """DAG path-cover computation, independent of the antichain search."""

    n = len(events)
    adj = [
        [
            j
            for j in range(n)
            if i != j
            and causal_precedes(events[i], events[j])
            and events[i] != events[j]
        ]
        for i in range(n)
    ]
    match_right = [-1] * n

    def augment(i: int, seen: set[int]) -> bool:
        for j in adj[i]:
            if j in seen:
                continue
            seen.add(j)
            if match_right[j] == -1 or augment(match_right[j], seen):
                match_right[j] = i
                return True
        return False

    matching = sum(augment(i, set()) for i in range(n))
    return n - matching


def path_between(e: tuple[int, int], f: tuple[int, int]):
    """Construct one legal hold/recede schedule between comparable events."""

    assert causal_precedes(e, f)
    t, p = e
    u, q = f
    moves = p - q
    holds = (u - t) - moves
    return [p] * holds + [p - j for j in range(1, moves + 1)]


def check_mapping() -> int:
    points = list(product(range(5), repeat=2))
    checked = 0
    for a in points:
        for b in points:
            assert product_precedes(a, b) == causal_precedes(event_of(a), event_of(b))
            checked += 1
    return checked


def check_dilworth_samples() -> int:
    base = [event_of(p) for p in product(range(3), repeat=2)]
    checked = 0
    for mask in range(1 << len(base)):
        events = [base[i] for i in range(len(base)) if mask >> i & 1]
        assert width(events) == min_chain_cover(events)
        checked += 1
    return checked


def check_motion() -> int:
    points = list(product(range(5), repeat=2))
    checked = 0
    for a in points:
        for b in points:
            if not product_precedes(a, b):
                continue
            e, f = event_of(a), event_of(b)
            schedule = path_between(e, f)
            assert len(schedule) == f[0] - e[0]
            previous = e[1]
            for position in schedule:
                assert position in (previous, previous - 1)
                previous = position
            assert previous == f[1]
            checked += 1
    return checked


def check_width_two_adversary() -> None:
    # The already-audited T68 witness, retained as the w=2 boundary control.
    a, b = (28, 8), (28, 12)
    c, d, d_prime = (36, 6), (38, 0), (38, 10)
    assert width([a, b, c, d]) == 2
    assert width([a, b, c, d_prime]) == 2

    # If the track serving c came from a, the other live track remains at b
    # and neither can serve d.  The symmetric branch strands d_prime.
    assert causal_precedes(a, c) and causal_precedes(b, c)
    assert not causal_precedes(c, d) and not causal_precedes(b, d)
    assert not causal_precedes(c, d_prime) and not causal_precedes(a, d_prime)


def check_fixed_realizer_timing_control() -> bool:
    """Check an exact certificate against respacing one supplied realizer.

    A service-time revelation theorem would need every presented linear
    extension to have *some* suitable dominance representation.  The
    six-point system below establishes only the narrower fact that one
    supplied realizer cannot be repaired by monotone rescaling of its
    coordinate orders.

    Write A_i=a_{i+1}-a_i>0 and B_i=b_{i+1}-b_i>0.  Three required arrival
    inequalities imply

      A0+A1+A2-B1 < 0,
      B0+B1+B2+B3+B4-A1-A2-A3 < 0,
      A2+A3+A4-B3 < 0.

    Their sum is A0+A2+A4+B0+B2+B4 < 0, impossible.  The coefficient
    calculation below is an exact Farkas-style certificate.  This is a
    control on one tempting proof route, not a dependency of the positive
    transfer and not an obstruction to choosing a different realizer.
    """

    second_rank = (2, 5, 4, 1, 0, 3)
    arrival = (3, 0, 1, 4, 5, 2)
    position = {element: i for i, element in enumerate(arrival)}
    assert all(
        not (i < j and second_rank[i] < second_rank[j])
        or position[i] < position[j]
        for i in range(6)
        for j in range(6)
    )

    # Coordinates are A0..A4,B0..B4.
    inequality_30 = (1, 1, 1, 0, 0, 0, -1, 0, 0, 0)
    inequality_14 = (0, -1, -1, -1, 0, 1, 1, 1, 1, 1)
    inequality_52 = (0, 0, 1, 1, 1, 0, 0, 0, -1, 0)
    summed = tuple(
        inequality_30[i] + inequality_14[i] + inequality_52[i]
        for i in range(10)
    )
    return summed == (1, 0, 1, 0, 1, 1, 0, 1, 0, 1)


def check_alternate_realizer_repairs_timing() -> None:
    """Hostile control: the same order has a diagonally timed realizer.

    This witness was supplied by the independent audit.  It prevents the
    fixed-realizer certificate above from being misreported as an intrinsic
    poset/presentation obstruction.
    """

    original_second_rank = (2, 5, 4, 1, 0, 3)
    arrival = (3, 0, 1, 4, 5, 2)

    def original_precedes(i: int, j: int) -> bool:
        return i <= j and original_second_rank[i] <= original_second_rank[j]

    l1 = (0, 1, 2, 4, 3, 5)
    l2 = (3, 4, 0, 5, 2, 1)
    rank1 = {element: rank for rank, element in enumerate(l1)}
    rank2 = {element: rank for rank, element in enumerate(l2)}

    # The alternate pair realizes exactly the original product order.
    for i in range(6):
        for j in range(6):
            alternate = rank1[i] <= rank1[j] and rank2[i] <= rank2[j]
            assert original_precedes(i, j) == alternate

    x = (-9, -8, -1, 1, 0, 2)
    y = (-1, 5, 4, -12, -2, 0)
    assert all(x[l1[i]] < x[l1[i + 1]] for i in range(5))
    assert all(y[l2[i]] < y[l2[i + 1]] for i in range(5))
    arrival_sums = [x[element] + y[element] for element in arrival]
    assert arrival_sums == [-11, -10, -3, -2, 2, 3]
    assert all(
        arrival_sums[i] < arrival_sums[i + 1]
        for i in range(len(arrival_sums) - 1)
    )


if __name__ == "__main__":
    mapping_checks = check_mapping()
    motion_checks = check_motion()
    dilworth_checks = check_dilworth_samples()
    check_width_two_adversary()
    assert check_fixed_realizer_timing_control()
    check_alternate_realizer_repairs_timing()
    print("causal-poset transfer checks passed")
    print(f"order equivalences checked: {mapping_checks}")
    print(f"explicit track segments checked: {motion_checks}")
    print(f"Dilworth subsets checked: {dilworth_checks}")
    print("timing control: one supplied realizer resists diagonal respacing")
    print("hostile repair: an alternate realizer of the same order is diagonal")