# DF-5196 — warp_saver star wrap off-by-one: `vid[SCRW*SCRH]` written (1 byte past the 64000-byte mode-13h framebuffer)

File: `sys/dev/misc/syscons/warp/warp_saver.c:70-77`

## What

`warp_update()` advances each star by `i` (1..4) and wraps with

```c
star[k] += i;
if (star[k] > SCRW*SCRH)     /* warp_saver.c:74 — `>`, must be `>=` */
    star[k] -= SCRW*SCRH;
vid[star[k]] = i;            /* warp_saver.c:76 */
```

`star[k]` is initialized to `krandom() % (SCRW*SCRH)` ∈ [0,63999]
(warp_saver.c:121) and the arithmetic keeps it in [0,64000]: every value
**greater than** 64000 is wrapped, but the value **exactly equal** to
64000 is not. A star resting at 63996..63999 (depending on speed class
i=1..4) advances to exactly 64000 and is *drawn* there (`vid[64000] =
i`); on the next update it is *erased* there (`vid[star[k]] = 0`,
warp_saver.c:72) before wrapping normally.

## Proof (deterministic, host-side)

`warp_model.py` in this directory is a 1:1 arithmetic model of the loop
(same constants, same statement order). Over 100,000 updates with the
same init distribution:

```
max index written    = 64000  (framebuffer = 64000 bytes)
writes at vid[64000] = 706    (byte past framebuffer)
writes >= 64000      = 706    <- never beyond 64000
```

Also proves the companion invariant: `k` terminates at exactly
STARS-1 (120+60+30+15 = 225 = STARS) — `star[]` itself is never
indexed out of bounds, and unlike the snake saver (DF-5194) there is
no runaway: 64000 is the *maximum* index ever touched.

## Why Info (not higher)

On the only in-tree adapter that serves M_VGA_CG320 (vga.c),
a successful mode switch points `va_window` at the 64 KB A0000
aperture (`va_window_size = GRAPHICS_BUF_SIZE = 0x10000`,
sys/dev/video/fb/vga.c:581, sys/dev/video/fb/vgareg.h:43-44).
Offset 64000 (0xFA00) therefore lands **inside** the mapped VGA
window, in offscreen video RAM — no kernel memory is touched, nothing
is displayed, no fault occurs. The defect is a latent bounds bug +
hardening opportunity (any future adapter exposing M_VGA_CG320 with a
64000-byte or tightly-sized window would take a real OOB MMIO write;
the value written is attacker-uncontrolled but loop-chosen: 0..4).

## Fix

One character: `>` → `>=` (keeps the invariant star[k] ∈ [0,63999];
63999+4=64003 wraps to 3 exactly as before, 64000 now wraps to 0).

## Reproduce the model (host, no guest needed)

```
python3 warp_model.py        # see model_output.txt for recorded output
```

Phase V (guest PoC) skipped per contract: Info hardening finding, no
demonstrable kernel-memory impact on any in-tree adapter.