#!/usr/bin/env python3
"""Exact-arithmetic checks for the finite fragment of the accompanying paper.

These checks validate a reference implementation and finite examples. They do
not constitute a proof-assistant formalization of the universal theorems.
Only Python's standard library is required.
"""

from fractions import Fraction as F
from itertools import combinations, permutations, product
import json


def allocate(budget, needs):
    """Return (guarantee, service fractions, resource allocations).

    Inputs are finite nonnegative rational vectors. The budget must have at
    least one coordinate. Every need vector must have the same dimension.
    """
    b = tuple(map(F, budget))
    n = tuple(tuple(map(F, row)) for row in needs)
    if not b or any(len(row) != len(b) for row in n):
        raise ValueError("Expected a nonempty budget and matching need vectors")
    if any(v < 0 for v in b) or any(v < 0 for row in n for v in row):
        raise ValueError("Resource values must be nonnegative")
    totals = tuple(sum((row[k] for row in n), F(0)) for k in range(len(b)))
    candidates = [F(1)] + [bk / nk for bk, nk in zip(b, totals) if nk > 0]
    guarantee = min(candidates)
    service = tuple(guarantee if any(row) else F(1) for row in n)
    allocation = tuple(tuple(u * v for v in row) for u, row in zip(service, n))
    return guarantee, service, allocation


def is_feasible(budget, needs, service):
    return (
        len(service) == len(needs)
        and all(F(0) <= u <= F(1) for u in service)
        and all(any(row) or u == 1 for u, row in zip(service, needs))
        and all(
            sum((u * row[k] for u, row in zip(service, needs)), F(0)) <= budget[k]
            for k in range(len(budget))
        )
    )


def service_guarantee(needs, service):
    return min([u for row, u in zip(needs, service) if any(row)], default=F(1))


def check_example():
    contributions = ((8, 4), (4, 8), (0, 4), (0, 0))
    reserve = (4, 4)
    b = tuple(sum(row[k] for row in contributions) - reserve[k] for k in range(2))
    n = ((1, 2), (3, 2), (4, 4), (4, 8))
    guarantee, service, allocation = allocate(b, n)
    expected = ((F(2, 3), F(4, 3)), (F(2), F(4, 3)),
                (F(8, 3), F(8, 3)), (F(8, 3), F(16, 3)))
    assert b == (8, 12)
    assert guarantee == F(2, 3)
    assert allocation == expected
    assert is_feasible(b, n, service)
    assert tuple(map(sum, zip(*allocation))) == (F(8), F(32, 3))
    assert all(v > 0 for v in allocation[-1]) and contributions[-1] == (0, 0)
    for perm in permutations(range(4)):
        renamed = allocate(b, [n[i] for i in perm])
        assert renamed[0] == guarantee
        assert renamed[2] == tuple(allocation[i] for i in perm)
    return {"budget": list(b), "guarantee": str(guarantee),
            "allocation": [[str(v) for v in row] for row in allocation]}


def check_exhaustive_grid():
    instances = feasible_candidates = 0
    fractions = (F(0), F(1, 2), F(1))
    for entries in product((0, 1), repeat=6):
        needs = tuple(tuple(map(F, entries[2*i:2*i+2])) for i in range(3))
        totals = tuple(map(sum, zip(*needs)))
        for budget in product((F(0), F(1), F(2)), repeat=2):
            guarantee, service, allocation = allocate(budget, needs)
            assert is_feasible(budget, needs, service)
            assert service_guarantee(needs, service) == guarantee
            assert (guarantee == 1) == all(n <= b for n, b in zip(totals, budget))
            for candidate in product(fractions, repeat=3):
                if is_feasible(budget, needs, candidate):
                    feasible_candidates += 1
                    assert service_guarantee(needs, candidate) <= guarantee
            for perm in permutations(range(3)):
                permuted = allocate(budget, [needs[i] for i in perm])
                assert permuted[0] == guarantee
                assert permuted[2] == tuple(allocation[i] for i in perm)
            instances += 1
    assert instances == 576
    return {"input_instances": instances, "feasible_grid_candidates": feasible_candidates}


def check_boundaries_and_equal_needs():
    assert allocate((0, 0), ((0, 0), (0, 0), (0, 0)))[0] == 1
    assert allocate((0, 0), ((1, 0), (0, 0), (0, 1)))[0] == 0
    assert allocate((2, 0), ((1, 0), (1, 0), (0, 0)))[0] == 1
    same_need = allocate((2, 3), ((2, 4), (2, 4), (0, 0)))
    assert same_need[2][0] == same_need[2][1]
    # Individual contributions are deliberately absent from allocate's inputs.
    # If alternative contribution tables yield the same budget, outputs agree.
    c1, c2 = ((4, 0), (0, 4), (0, 0)), ((0, 0), (4, 4), (0, 0))
    b1, b2 = tuple(map(sum, zip(*c1))), tuple(map(sum, zip(*c2)))
    assert b1 == b2
    n = ((1, 2), (3, 2), (4, 4))
    assert allocate(b1, n) == allocate(b2, n)
    for budget, needs in [((-1, 0), ((0, 0),)), ((1,), ((1, 2),)), ((), ())]:
        try:
            allocate(budget, needs)
        except ValueError:
            pass
        else:
            raise AssertionError("Malformed input was accepted")


def check_quorum_and_symmetry():
    agents = set(range(4))
    quorums = [set(v) for k in (3, 4) for v in combinations(agents, k)]
    for v, w in product(quorums, repeat=2):
        assert len(v & w) >= 2
        for bad in agents:
            assert (v & w) - {bad}
    all_perms = list(permutations(range(4)))
    for selected in agents:
        assert any(perm[selected] != selected for perm in all_perms)
    uniform = (F(1, 4),) * 4
    assert sum(uniform) == 1
    assert all(tuple(uniform[i] for i in perm) == uniform for perm in all_perms)
    return {"quorum_sets": len(quorums), "ordered_quorum_pairs": len(quorums)**2,
            "permutations": len(all_perms)}


def main():
    example = check_example()
    grid = check_exhaustive_grid()
    check_boundaries_and_equal_needs()
    governance = check_quorum_and_symmetry()
    print(json.dumps({"status": "passed", "example": example, "grid": grid,
                      "governance": governance,
                      "scope": "Finite exact-arithmetic checks; not proof-assistant verification"},
                     indent=2))


if __name__ == "__main__":
    main()