#!/usr/bin/env python3
"""
Independent verifier for covering designs C(v,k,t).

Usage:
    python verify_cvt.py <design_file>

where <design_file> is a text file whose FIRST LINE is
        v k t
and each subsequent non-empty line is one block: k distinct integers
in 0..v-1, in ascending order, separated by whitespace.

The verifier recomputes the Schoenheim lower bound L(v,k,t), checks that
every t-subset of {0,...,v-1} is contained in at least one block, and
prints PASS/FAIL together with the block count b, L, and the coverage
multiplicity profile. Exit code 0 = pass, 1 = fail, 2 = malformed input.

This file contains no imports beyond the standard library and performs an
explicit exhaustive check: it enumerates all C(v,t) t-subsets.
"""
import sys
from math import comb
from itertools import combinations


def schoenheim(v: int, k: int, t: int) -> int:
    """Iterated ceiling bound: value := ceil((v-i)/(k-i) * value), i = t-1 .. 0."""
    val = 1
    for i in range(t - 1, -1, -1):
        val = -((-(v - i) * val) // (k - i))  # integer ceil
    return val


def main(path: str) -> int:
    with open(path, "r", encoding="utf-8") as f:
        lines = [ln.strip() for ln in f if ln.strip() and not ln.strip().startswith("#")]

    if not lines:
        print("FAIL: empty file")
        return 2
    head = lines[0].split()
    try:
        v, k, t = int(head[0]), int(head[1]), int(head[2])
    except (ValueError, IndexError):
        print("FAIL: first line must be 'v k t'")
        return 2

    blocks = []
    for ln in lines[1:]:
        parts = ln.split()
        if len(parts) != k:
            print(f"FAIL: block '{ln}' has {len(parts)} points, expected {k}")
            return 2
        try:
            b = [int(x) for x in parts]
        except ValueError:
            print(f"FAIL: non-integer point in block '{ln}'")
            return 2
        if any(x < 0 or x >= v for x in b):
            print(f"FAIL: point out of range in block '{ln}'")
            return 2
        if any(b[i] >= b[i + 1] for i in range(k - 1)):
            print(f"FAIL: block '{ln}' not strictly ascending / has repeats")
            return 2
        blocks.append(b)

    num_t = comb(v, t)
    covered = [0] * num_t

    # Rank each t-subset in colex order: sum_i C(x_i, i+1)
    def colex_rank(sub):
        return sum(comb(sub[i], i + 1) for i in range(len(sub)))

    seen_blocks = set()
    for b in blocks:
        key = tuple(b)
        if key in seen_blocks:
            print(f"NOTE: duplicate block {b} ignored")
            continue
        seen_blocks.add(key)
        for sub in combinations(b, t):
            covered[colex_rank(sub)] += 1

    uncovered = sum(1 for c in covered if c == 0)
    L = schoenheim(v, k, t)
    bcount = len(seen_blocks)

    profile = {}
    for c in covered:
        profile[c] = profile.get(c, 0) + 1

    print(f"cell          : C({v},{k},{t})")
    print(f"blocks read   : {len(blocks)}, distinct: {bcount}")
    print(f"Schoenheim L  : {L}")
    print(f"t-subsets     : {num_t}, uncovered: {uncovered}")
    print(f"multiplicity  : {dict(sorted(profile.items()))}")

    if uncovered == 0:
        verdict = "PASS"
        extra = ""
        if bcount == L:
            extra = " -- b = L: cell CLOSED (optimal by the Schoenheim bound)"
        elif bcount < L:
            extra = " -- IMPOSSIBLE: b < Schoenheim bound, design cannot exist; check input"
            verdict = "FAIL"
        print(f"{verdict}: valid ({v},{k},{t}) covering{extra}")
        return 0 if verdict == "PASS" else 1
    else:
        print("FAIL: not a covering")
        return 1


if __name__ == "__main__":
    if len(sys.argv) != 2:
        print(__doc__)
        sys.exit(2)
    sys.exit(main(sys.argv[1]))