33 points, no convex heptagon

"""Verifier for "33 points, no convex heptagon" (statement in erdos_szekeres_7.json).

Problem: place NUM_POINTS distinct points with integer coordinates in
{0, ..., COORD_MAX}^2, no three on a line, such that no HEPTAGON of them are
in convex position (i.e. are the vertices of a convex polygon). Erdos and
Szekeres built 32 points with no convex heptagon and conjectured that any 33
points in general position contain one; a valid submission disproves that.

Expected submission: a JSON object with the points as [x, y] pairs of JSON
integers, e.g.

    {"points": [[0, 0], [10, 0], [0, 10], [3, 3]]}

What the verifier checks, in order:
  1. The payload is at most MAX_BYTES characters and is a JSON object with
     exactly the key "points".
  2. "points" is a list of exactly NUM_POINTS pairs of integers in
     0..COORD_MAX.
  3. The points are pairwise distinct.
  4. No three points are collinear (all C(33, 3) = 5,456 triples). This runs
     before the expensive step, so bad inputs fail fast.
  5. No HEPTAGON points are in convex position (see _has_convex_polygon).

All geometry uses the exact integer orientation test; there is no floating
point anywhere. Step 5 does not test the C(33, 7) = 4,272,048 subsets one by
one: a dynamic program over convex chains finds the answer in about
C(33, 3) * 33 elementary steps, a few hundredths of a second.
"""
import itertools
import json

# Number of points to place.
NUM_POINTS = 33
# Size of the forbidden convex polygon (7: a convex heptagon).
HEPTAGON = 7
# Largest allowed coordinate.
COORD_MAX = 10_000
# Maximum size of the whole submission, in characters.
MAX_BYTES = 5_000


# ---------------------------------------------------------------------------
# Input-parsing and geometry 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


def _int_grid(cells, n, lo, hi):
    """Return exactly n points [i, j] with both coordinates in [lo, hi] as tuples, or raise."""
    if not isinstance(cells, list) or len(cells) != n:
        raise ValueError
    return [tuple(_int_list(c, 2, lo, hi)) for c in cells]


def _orient(a, b, c):
    """Orientation of the triangle a, b, c: > 0 if it turns counterclockwise,
    < 0 if clockwise, 0 if the three points are collinear.

    This is twice the signed area of the triangle, computed exactly because
    the coordinates are integers.
    """
    return (b[0] - a[0]) * (c[1] - a[1]) - (b[1] - a[1]) * (c[0] - a[0])


def _no_three_collinear(points):
    """True iff no three of `points` lie on a common line (checks every triple)."""
    return all(_orient(a, b, c) != 0 for a, b, c in itertools.combinations(points, 3))


def _angular_order(p, points):
    """Sort `points`, all lying above p, counterclockwise around p.

    Insertion sort driven by the exact orientation test: q comes before r
    exactly when p, q, r turn counterclockwise.
    """
    ordered = []
    for q in points:
        i = len(ordered)
        while i > 0 and _orient(p, q, ordered[i - 1]) > 0:
            i -= 1
        ordered.insert(i, q)
    return ordered


def _has_convex_polygon(points, k):
    """True iff some k of `points` (no three collinear) form a convex polygon.

    Every convex polygon has a unique lowest vertex p (smallest y, then
    smallest x). Its other vertices all lie above p, and going
    counterclockwise they appear in increasing angle around p. So, for each
    choice of p, the points above it are sorted by angle, and chains
    p -> c[h] -> c[i] -> c[j] -> ... are grown in that order, each new edge
    turning left from the previous one.

    longest[j][i] is the largest number of vertices (p included) of such a
    chain whose last edge is c[i] -> c[j]. Every chain p -> c[i] -> c[j] is a
    valid start (3 vertices, since the angle increases). A chain can be
    extended by c[j] -> c[l] when c[i], c[j], c[l] turn left. It closes into a
    convex polygon when its last edge c[i] -> c[j] also turns left towards p.
    A convex polygon with at least k vertices contains k points in convex
    position, so the search stops at the first closable chain with >= k.
    """
    for p in points:
        above = [q for q in points if (q[1], q[0]) > (p[1], p[0])]
        c = _angular_order(p, above)
        longest = [[0] * len(c) for _ in c]
        for j in range(len(c)):
            for i in range(j):
                best = 3  # the triangle p, c[i], c[j]
                for h in range(i):
                    if _orient(c[h], c[i], c[j]) > 0:
                        best = max(best, longest[i][h] + 1)
                longest[j][i] = best
                if best >= k and _orient(c[i], c[j], p) > 0:
                    return True
    return False


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

def _check(solution):
    # Steps 1-2: read the JSON object and the points.
    sol = _load(solution, ("points",), MAX_BYTES)
    points = _int_grid(sol["points"], NUM_POINTS, 0, COORD_MAX)

    # Step 3: no point may be used twice.
    if len(set(points)) != len(points):
        return False

    # Step 4: general position (cheap, and needed by step 5).
    if not _no_three_collinear(points):
        return False

    # Step 5: no HEPTAGON points in convex position.
    return not _has_convex_polygon(points, HEPTAGON)


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