1 Commits
Author SHA1 Message Date
Robert Allan James 1e76ebea97 proof/: add console-fabric word coverage (framebuffer/keyboard/scroll/ttf)
Stadium console fabric words (FABRIC.md items 4.3.3/4.3.5/4.3.7e/4.4q/
4.4v/4.4y). All four files gate their real hardware-touching bodies
behind __STARKERNEL__ (and, for keyboard, architecture too):

- StarForth_Framebuffer_Words.thy: PLOT/FB-WIDTH/FB-HEIGHT fully modelled
  for the hosted-build fallback (deterministic, no hardware dependency);
  kernel bodies (fb_put_pixel/fb_width/fb_height) deferred. Finding:
  FB-WIDTH/FB-HEIGHT have no overflow guard before pushing -- second
  instance of this class of bug after DECAY-RATE@.
- StarForth_Keyboard_Words.thy: all 6 words' non-kernel-or-wrong-arch
  fallback modelled (fixed constant pushes / no-op); third and fourth
  missing-overflow-guard instances. Real hardware polling
  (i8042/virtio-input) deferred.
- StarForth_Scroll_Words.thy / StarForth_TTF_Words.thy: both files gate
  registration itself behind __STARKERNEL__, so their words don't exist
  at all in a hosted build -- no fallback to model, sentinel-only.

Suite now 48 theories, confirmed green via a full clean rebuild (HOL-
Library cold-built in 15m18s after an accidental heap clear, StarForth
itself 33s).
2026-08-14 16:15:27 -04:00