Beal conjecture counterexample

"""Verifier for "Beal conjecture counterexample" (statement in beal_counterexample.json).

Problem: find positive integers A, B, C, x, y, z with x, y, z >= 3 and
gcd(A, B, C) == 1 such that

    A**x + B**y == C**z

The Beal conjecture says this is impossible; a submission that passes this
verifier disproves it.

Expected submission: a JSON object whose values are decimal strings, e.g.

    {"A": "12", "B": "35", "C": "7", "x": "3", "y": "4", "z": "5"}

What the verifier checks, in order:
  1. The payload is at most MAX_BYTES characters and is a JSON object with
     exactly the keys A, B, C, x, y, z.
  2. Each value is a well-formed non-negative decimal string of at most
     MAX_DIGITS digits (see _parse_int).
  3. Every exponent is at least MIN_EXP and every base is at least 1.
  4. A, B and C have no common factor. Without this rule there are trivial
     solutions such as 2**3 + 2**3 == 2**4.
  5. Each power is small enough to compute: exponent * bit length of the base
     must be at most MAX_POWER_BITS. This is checked before any power is
     computed, so an input like A = 2, x = 10**9999 is rejected immediately
     instead of exhausting memory.
  6. A**x + B**y == C**z, with exact integer arithmetic.
"""
import json
import math

# Smallest allowed exponent. The conjecture uses 3; the tests lower it to 2,
# where solutions such as 2**5 + 7**2 == 3**4 exist.
MIN_EXP = 3
# Maximum number of digits allowed in each of the six values.
MAX_DIGITS = 10_000
# Maximum size, in bits, of each of A**x, B**y and C**z, measured as
# exponent * bit length of the base (an upper bound on the power's size).
MAX_POWER_BITS = 2_000_000
# Maximum size of the whole submission, in characters.
MAX_BYTES = 80_000

# The keys the submission must contain, in the order they are unpacked below.
KEYS = ("A", "B", "C", "x", "y", "z")


# ---------------------------------------------------------------------------
# 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 all six values.
    sol = _load(solution, KEYS, MAX_BYTES)
    A, B, C, x, y, z = (_parse_int(sol[k], MAX_DIGITS) for k in KEYS)

    # Step 3: exponents must be at least MIN_EXP, bases must be positive.
    if min(x, y, z) < MIN_EXP or min(A, B, C) < 1:
        return False

    # Step 4: the three bases must share no common prime factor.
    if math.gcd(A, B, C) != 1:
        return False

    # Step 5: refuse any power too large to compute. A number with b bits
    # raised to the power e has at most e * b bits, so this bounds the work
    # before it is done.
    for base, exp in ((A, x), (B, y), (C, z)):
        if exp * base.bit_length() > MAX_POWER_BITS:
            return False

    # Step 6: the equation itself, exactly. At the default caps this is at most
    # three 2,000,000-bit powers, about 0.2 s.
    return A ** x + B ** y == C ** z


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