{
  "finding_id": "DF-5196",
  "status": "untested",
  "reproduced": false,
  "impact": "none",
  "confidence": "certain",
  "verdict": "Off-by-one wrap in warp_update(): `if (star[k] > SCRW*SCRH)` (warp_saver.c:74) fails to wrap the coordinate that lands on exactly SCRW*SCRH, so a star is drawn and later erased at vid[64000] \u2014 one byte past the 64000-byte M_VGA_CG320 framebuffer. Proven by a 100,000-update arithmetic model (warp_model.py: 706 hits at vid[64000], max index 64000, never beyond; k terminates at exactly STARS-1 so star[] is never indexed OOB and there is no DF-5194-style runaway). Impact is none on in-tree code: the only M_VGA_CG320 provider (vga.c) exposes a 64KB A0000 window (va_window_size=0x10000, vga.c:581 + vgareg.h:43-44), so the byte lands in offscreen VRAM. Info hardening finding \u2014 guest PoC skipped per contract; the byte is invisible by construction.",
  "exploit_chain": "",
  "evidence": "warp_model.py + model_output.txt (max index 64000, 706 writes at vid[64000], 0 beyond); source: warp_saver.c:70-77 (loop), :74 (the `>`), :121 (init bound); window size proof: sys/dev/video/fb/vga.c:581, sys/dev/video/fb/vgareg.h:43-44; guest reachability (read-only): dmesg sc0+vga0 iomem 0xa0000-0xbffff, saver_waver.ko absent from /boot/kernel (built from sys/dev/misc/syscons/warp/Makefile, kldload is root-only)",
  "kernel_refs": [
    "sys/dev/misc/syscons/warp/warp_saver.c:70",
    "sys/dev/misc/syscons/warp/warp_saver.c:74",
    "sys/dev/misc/syscons/warp/warp_saver.c:76",
    "sys/dev/misc/syscons/warp/warp_saver.c:121",
    "sys/dev/video/fb/vga.c:581",
    "sys/dev/video/fb/vgareg.h:43"
  ],
  "poc_changes": "n/a \u2014 no kernel PoC built (Info hardening; Phase V skipped per contract). Host-side deterministic arithmetic model included instead.",
  "attempts": 0,
  "guest_uname": "DragonFly dfbsd 6.5-DEVELOPMENT DragonFly 6.5-DEVELOPMENT #0: Thu Jul  2 06:02:54 UTC 2026 root@dfbsd:/usr/obj/usr/src/sys/X86_64_GENERIC x86_64",
  "runtime_sec": 4,
  "guest_dirty": 0,
  "build_cmd": "python3 warp_model.py (host-side arithmetic model, not a guest kernel PoC)",
  "run_cmd": "python3 warp_model.py",
  "code_hash": "eed8d2576484eb6b41c8a0813d849b825bdea3703162e06575e6689054a93be3",
  "notes": "Companion invariants proven by the same model: k <= STARS-1 (120+60+30+15=225=STARS) so the star[] array itself is never OOB; DF-5194-style runaway impossible (64000 is the max index). Guest inspected read-only (up, not dirtied); no console blanking attempted to avoid the known DF-5195 syscons deadlock.",
  "recommended_fix": "warp_saver.c:74: change `star[k] > SCRW*SCRH` to `star[k] >= SCRW*SCRH` (one char; preserves star[k] in [0,63999]).",
  "fix_status": "not_applicable",
  "fix_baseline_reproduced": 0,
  "fix_patched_reproduced": 0,
  "fix_verdict": "Fix validation not applicable: no misbehavior reproduces on in-tree adapters (the stray byte is invisible offscreen VRAM); the one-character change is provably semantics-preserving except at exactly 64000, which becomes 0.",
  "fix_evidence": "See VERDICT.md Fix section for the diff and invariant argument."
}