#!/usr/bin/env python3
"""General integer floor transition.

Q and S are positive integers and d is an integer.
d_next = floor(Q*d/S), rho = Q*d - S*d_next.

This is not the 24 September 2026 canonical 399 checker, not an SRSD
conformance award, and not a Lean proof. Mandatory checks do not use
Python assert statements, so python -O does not remove them.
"""
from __future__ import annotations

import ast
import sys
from pathlib import Path

CHECKS = 0
Q399 = 339949771344778
S399 = 10**15


def require(ok: bool, message: str) -> None:
    global CHECKS
    CHECKS += 1
    if not bool(ok):
        raise ValueError(message)


def step(q: int, s: int, d: int) -> tuple[int, int]:
    require(isinstance(q, int) and isinstance(s, int) and isinstance(d, int), "integers required")
    require(q > 0 and s > 0, "Q and S must be positive")
    d_next = (q * d) // s
    rho = q * d - s * d_next
    return d_next, rho


def check_forward(q: int, s: int, d: int) -> None:
    d_next, rho = step(q, s, d)
    require(0 <= rho < s, "residual bounds")
    require(q * d == s * d_next + rho, "division identity")
    require((s * d_next + rho) // q == d, "produced record recovers d")
    require((s * d_next + rho) % q == 0, "produced record is exact")


def reconstruct(q: int, s: int, d_next: int, rho: int, *, nonnegative: bool) -> int:
    require(isinstance(d_next, int) and isinstance(rho, int), "record entries must be integers")
    require(q > 0 and s > 0, "Q and S must be positive")
    require(0 <= rho < s, "residual outside [0,S)")
    numerator = s * d_next + rho
    require(numerator % q == 0, "S*d_next+rho is not divisible by Q")
    d = numerator // q
    if nonnegative:
        require(d >= 0, "predecessor outside the nonnegative domain")
    return d


def rejects(fn) -> None:
    try:
        fn()
    except ValueError:
        require(True, "rejection observed")
        return
    require(False, "invalid record was accepted")


def main() -> None:
    print("general integer floor transition")
    print("Python", sys.version.split()[0])
    print("Optimization mode:", sys.flags.optimize)
    print("Lean: NOT RUN. ASD-STE100: SOURCE_UNAVAILABLE.")
    for q, s in ((1, 1), (2, 5), (5, 2), (5, 5), (Q399, S399)):
        for d in (0, 1, -1, s - 1, s, -s, 399, -(10**12)):
            check_forward(q, s, d)
    check_forward(10**6 + 3, 10**9 + 7, -(10**18))
    d_next, rho = step(Q399, S399, 399)
    require(Q399 * 399 == 135 * S399 + 639958766566422, "canonical 399 product")
    require(d_next == 135 and rho == 639958766566422, "canonical 399 residual")
    # Q < S is not a hypothesis. Q = 5 and S = 2 is already included.
    require(step(5, 2, 1) == (2, 1), "expansion case")
    d = reconstruct(5, 2, -3, 1, nonnegative=False)
    require(d == -1, "negative predecessor on Z")
    require(step(5, 2, d) == (-3, 1), "negative record is produced by its predecessor")
    rejects(lambda: reconstruct(5, 2, -3, 1, nonnegative=True))
    rejects(lambda: reconstruct(5, 2, 1, 2, nonnegative=False))
    rejects(lambda: reconstruct(5, 2, 1, -1, nonnegative=False))
    rejects(lambda: reconstruct(4, 6, 1, 1, nonnegative=False))
    rejects(lambda: step(0, 1, 0))
    rejects(lambda: step(1, 0, 0))
    rejects(lambda: step(-3, 2, 1))
    tree = ast.parse(Path(__file__).read_text(encoding="utf-8"))
    require(not any(isinstance(node, ast.Assert) for node in ast.walk(tree)), "assert present")
    print("CHECKS", CHECKS)
    print("DECLARED_CHECKS_PASS")
    print("This pass covers the listed integers only. It is not a proof review,")
    print("not SRSD conformance, and not a verification of the archive.")


if __name__ == "__main__":
    main()