Factor of F₂₀

"""Verifier for "Factor of F20" (statement in fermat_factor.json).

Background: the Fermat numbers are F_N = 2**(2**N) + 1. F_20 has 315,653
digits; it has been known to be composite since 1988, but none of its
factors has ever been found.

Problem: find a divisor d of F_N with 1 < d < F_N (N = 20 by default).

How divisibility is checked without ever writing down F_N: d divides
2**E + 1 (where E = 2**N) exactly when 2**E leaves remainder d - 1 (that is,
-1) when divided by d. Python's three-argument pow(2, E, d) computes that
remainder working modulo d throughout. Since E = 2**N, this takes only N
squarings, a few milliseconds even for a 10,000-digit d.

Expected submission: a JSON object with one decimal string:

    {"d": "4194305"}

What the verifier checks, in order:
  1. The payload is at most MAX_BYTES characters and is a JSON object with
     exactly the key "d".
  2. d is a well-formed non-negative decimal string of at most MAX_DIGITS
     digits (see _parse_int).
  3. d > 1, which excludes the trivial divisor 1.
  4. d has at most 2**N bits. F_N itself has 2**N + 1 bits, so this excludes
     the trivial divisor F_N. (At the default caps a 10,000-digit d is far
     smaller than F_20 anyway; this matters when the tests lower N.)
  5. d leaves remainder 1 when divided by 2**(N + 2). Every divisor of F_N
     (for N >= 2) has this form, a classical result of Euler and Lucas, so
     this is a cheap filter that no genuine answer can fail.
  6. 2**(2**N) mod d == d - 1, i.e. d divides F_N.
"""
import json

# Which Fermat number to factor. The tests use N = 5 (F_5 = 641 * 6700417)
# and N = 6 (F_6 = 274177 * 67280421310721) to check known factors.
N = 20
# Maximum number of digits of d.
MAX_DIGITS = 10_000
# Maximum size of the whole submission, in characters.
MAX_BYTES = 20_000


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

def _parse_int(s, max_digits, allow_neg=False):
    """Convert a strictly formatted decimal string to an int, or raise ValueError.

    Accepted: "0", "42", and "-42" when allow_neg is True.
    Rejected: anything that is not a string (for example a JSON number), "",
    "+42", " 42", "007", "-0", non-ASCII digits such as "٣", and strings with
    more than max_digits digits.
    """
    # Cheap length check before any real work: at most max_digits digits,
    # plus one character for an optional minus sign.
    if not isinstance(s, str) or len(s) > max_digits + 1:
        raise ValueError
    # Split off the sign. A "-" is only allowed where negative values make sense.
    neg = s.startswith("-")
    if neg and not allow_neg:
        raise ValueError
    body = s[1:] if neg else s
    # What remains must be 1 to max_digits ASCII digits with no leading zero
    # ("0" on its own is fine). isascii() is needed because isdigit() also
    # accepts digits from other scripts.
    if not (body.isascii() and body.isdigit()) or len(body) > max_digits or (len(body) > 1 and body[0] == "0"):
        raise ValueError
    # "-0" is not a canonical way to write zero.
    if neg and body == "0":
        raise ValueError
    # Python (3.11 and later) refuses int() on strings longer than 4300 digits
    # by default, so the number is built from chunks of 4000 digits.
    n = 0
    for i in range(0, len(body), 4000):
        chunk = body[i:i + 4000]
        n = n * 10 ** len(chunk) + int(chunk)
    return -n if neg else n


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


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

def _check(solution):
    # Steps 1-2: read the JSON object and parse d.
    sol = _load(solution, ("d",), MAX_BYTES)
    d = _parse_int(sol["d"], MAX_DIGITS)

    # F_N = 2**exponent + 1 with exponent = 2**N (`1 << N` means 2**N).
    exponent = 1 << N

    # Steps 3-5: d is not 1, d is smaller than F_N, and d has the form
    # k * 2**(N + 2) + 1 that every divisor of F_N must have.
    if d <= 1 or d.bit_length() > exponent or d % (1 << (N + 2)) != 1:
        return False

    # Step 6: d divides 2**exponent + 1 exactly when 2**exponent mod d is d - 1.
    return pow(2, exponent, d) == d - 1


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
    number, ...) means the submission is rejected, so this function never raises.
    """
    try:
        return _check(solution) is True
    except Exception:
        return False