Projective plane of order 12

"""Verifier for "Projective plane of order 12" (statement in projective_plane_12.json).

Problem: a finite projective plane of order n has n^2 + n + 1 points and as
many lines, each line containing n + 1 points, such that any two lines meet
in exactly one point, every point lies on exactly n + 1 lines, and any two
points lie on exactly one common line. Planes exist for every prime-power
order; 12 is the smallest order that is neither a prime power nor ruled out.

Expected submission: a JSON object with the lines as lists of point ids
(JSON integers 0 .. n^2 + n), e.g. (the start of the order-2 Fano plane)

    {"lines": [[0, 1, 3], [1, 2, 4], [2, 3, 5]]}

What the verifier checks, in order (for n = ORDER):
  1. The payload is at most MAX_BYTES characters and is a JSON object with
     exactly the key "lines".
  2. "lines" is a list of exactly n^2 + n + 1 lines, each n + 1 distinct
     point ids in 0 .. n^2 + n.
  3. Any two lines meet in exactly one point.
  4. Every point lies on exactly n + 1 lines.
  5. Any two points lie on exactly one common line.

At order 12 step 3 compares C(157, 2) = 12,246 pairs of lines, each stored as
a bitmask of its points, and step 5 goes through the 157 * C(13, 2) = 12,246
point pairs the lines contain. Both take milliseconds.
"""
import collections
import itertools
import json

# Order n of the plane. It fixes everything else: n^2 + n + 1 points and
# lines, n + 1 points on every line and n + 1 lines through every point.
ORDER = 12
# Maximum size of the whole submission, in characters.
MAX_BYTES = 100_000


# ---------------------------------------------------------------------------
# Input-parsing helpers. The same code is copied into every verifier that
# needs it, so that each file works on its own.
# ---------------------------------------------------------------------------

def _load(solution, keys, max_bytes):
    """Parse the submission as a JSON object with exactly the given keys, or raise."""
    # Refuse oversized payloads before handing them to the JSON parser.
    if not isinstance(solution, str) or len(solution) > max_bytes:
        raise ValueError
    d = json.loads(solution)
    # It must be an object (not a list, string or number) whose keys are
    # exactly the expected ones: nothing missing, nothing extra.
    if not isinstance(d, dict) or set(d) != set(keys):
        raise ValueError
    return d


def _int_list(values, n, lo, hi):
    """Return `values` if it is a list of exactly n integers in [lo, hi], or raise.

    The length is checked before any element is looked at. `type(v) is int`
    (rather than isinstance) also rejects true and false, which Python treats
    as the integers 1 and 0; floats such as 1.0 and strings such as "1" are
    rejected as well.
    """
    if not isinstance(values, list) or len(values) != n:
        raise ValueError
    for v in values:
        if type(v) is not int or not lo <= v <= hi:
            raise ValueError
    return values


# ---------------------------------------------------------------------------
# The actual check.
# ---------------------------------------------------------------------------

def _check(solution):
    num_points = ORDER * ORDER + ORDER + 1  # also the number of lines
    per_line = ORDER + 1  # points on each line, and lines through each point

    # Step 1: read the JSON object with its single key "lines".
    sol = _load(solution, ("lines",), MAX_BYTES)

    # Step 2: the right number of lines, each made of distinct valid points.
    # The number of lines is checked before any line is parsed.
    lines = sol["lines"]
    if not isinstance(lines, list) or len(lines) != num_points:
        return False
    lines = [_int_list(line, per_line, 0, num_points - 1) for line in lines]
    if any(len(set(line)) != per_line for line in lines):
        return False

    # Step 3: any two lines share exactly one point. With each line stored as
    # a bitmask of its points, the shared points are the bits of a & b.
    masks = [sum(1 << x for x in line) for line in lines]
    if any((a & b).bit_count() != 1 for a, b in itertools.combinations(masks, 2)):
        return False

    # Step 4: every point is on exactly per_line lines.
    lines_through = collections.Counter(x for line in lines for x in line)
    if any(lines_through[x] != per_line for x in range(num_points)):
        return False

    # Step 5: any two points are on exactly one common line. Each line covers
    # the pairs of its own points; over all lines every pair of points must be
    # covered, and none twice.
    pairs = [pair for line in lines for pair in itertools.combinations(sorted(line), 2)]
    return len(pairs) == len(set(pairs)) == num_points * (num_points - 1) // 2


def verify(solution: str, rng) -> bool:
    """Platform entry point: return True only for a valid, correct solution.

    `rng` (a numpy.random.Generator) is part of the platform interface but is
    not used: this check is deterministic. Any exception (malformed JSON, a bad
    value, ...) means the submission is rejected, so this function never raises.
    """
    try:
        return _check(solution) is True
    except Exception:
        return False