Van der Waerden number W(2,7)

"""Verifier for "van der Waerden number W(2,7)" (statement in vdw_2_7.json).

Problem: colour the integers 1..N with two colours so that no arithmetic
progression of AP_LEN terms, a, a + s, ..., a + (AP_LEN - 1) * s with s >= 1,
is monochromatic (all one colour). The best known lower bound is
W(2,7) > 3703, so a valid colouring of 1..3704 would improve it.

Expected submission: a JSON object with the N colours as JSON integers 0 or
1, where coloring[i] is the colour of the integer i + 1, e.g.

    {"coloring": [0, 1, 1, 0]}

What the verifier checks, in order:
  1. The payload is at most MAX_BYTES characters and is a JSON object with
     exactly the key "coloring".
  2. "coloring" is a list of exactly N integers, each 0 or 1.
  3. No progression of AP_LEN terms inside 1..N is monochromatic.

How step 3 is done: for each colour, the positions with that colour are
stored as the bits of one big integer `cells` (bit i set when integer i + 1
has the colour). For a step s, the integer

    cells & (cells >> s) & (cells >> 2s) & ... & (cells >> (AP_LEN - 1) * s)

has bit a set exactly when positions a, a + s, ..., a + (AP_LEN - 1) * s all
have the colour, so it is non-zero iff a monochromatic progression with step s
exists. Positions beyond N are zero bits, so progressions cannot run past N.
This tests the ~N^2 / 12 = 1.1 million progressions at N = 3704 with a few
thousand big-integer operations, a few milliseconds.
"""
import json

# Length of the integer range 1..N to colour.
N = 3704
# Number of terms in a forbidden progression.
AP_LEN = 7
# Maximum size of the whole submission, in characters.
MAX_BYTES = 50_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):
    # Steps 1-2: read the JSON object and the N colours.
    sol = _load(solution, ("coloring",), MAX_BYTES)
    coloring = _int_list(sol["coloring"], N, 0, 1)

    # Step 3: look for a monochromatic progression in each colour.
    for colour in (0, 1):
        # Bit i of `cells` is set when the integer i + 1 has this colour.
        cells = sum(1 << i for i, c in enumerate(coloring) if c == colour)
        # The largest step that still fits AP_LEN terms into 1..N.
        for step in range(1, (N - 1) // (AP_LEN - 1) + 1):
            # Bit a of `run` survives only if a, a + step, ..., a + (AP_LEN - 1) * step
            # all have this colour.
            run = cells
            for k in range(1, AP_LEN):
                run &= cells >> (k * step)
            if run:
                return False
    return True


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