#!/usr/bin/env python3
"""Arithmetic model of warp_saver.c warp_update() (sys/dev/misc/syscons/warp/warp_saver.c:65-78).
Proves: (1) k <= STARS-1 always (120+60+30+15 = 225 = STARS);
(2) star[k] parks at EXACTLY SCRW*SCRH (wrap test is `>`, should be `>=`),
    so vid[64000] is written -- 1 byte past the 64000-byte mode-13h framebuffer;
(3) 64000 is the max index touched (no runaway)."""
import random

SCRW, SCRH, SPP = 320, 200, 15
STARS = SPP * (1 + 2 + 4 + 8)          # 225
FB = SCRW * SCRH                        # 64000

star = [random.randrange(FB) for _ in range(STARS)]   # warp_init():121
min_idx, max_idx, hits, oob = 1 << 30, -1, 0, 0

def track(idx):
    global min_idx, max_idx, hits, oob
    min_idx = min(min_idx, idx); max_idx = max(max_idx, idx)
    if idx == FB: hits += 1
    if idx >= FB: oob += 1

def warp_update():
    k = 0
    n = SPP * 8
    for i in range(1, 5):
        for _ in range(n):
            assert k < STARS, "k ran past STARS"
            track(star[k])             # vid[star[k]] = 0   (erase)
            star[k] += i
            if star[k] > FB:           # warp_saver.c:74  <-- `>` not `>=`
                star[k] -= FB
            track(star[k])             # vid[star[k]] = i   (draw)
            k += 1
        n //= 2

for _ in range(100_000):
    warp_update()

print(f"warp_update() model, 100000 updates, STARS={STARS}")
print(f"min index written    = {min_idx}")
print(f"max index written    = {max_idx}  (framebuffer = {FB} bytes)")
print(f"writes at vid[64000] = {hits}  (byte past framebuffer)")
print(f"writes >= 64000      = {oob}")
assert max_idx == FB, "unexpected runaway"
print("VERDICT: OFF-BY-ONE CONFIRMED -- star rests at exactly SCRW*SCRH and is "
      "drawn+erased at vid[64000]; no index beyond 64000 ever occurs (`>` at "
      "warp_saver.c:74 should be `>=`)")