theory StarForth_Scroll_Words
  imports StarForth_Base
begin

(* =========================================================================
   Mirrors: src/word_source/scroll_words.c
   Registers (kernel-only -- see below): SCROLL-BACK SCROLL-FWD

   Part of the Stadium console fabric work (FABRIC.md item 4.4q). Unlike
   framebuffer_words.c/keyboard_words.c, this file's word BODIES and its
   `register_word` calls are BOTH inside `#ifdef __STARKERNEL__` --
   `register_scroll_words` registers nothing at all on a hosted build
   (the `#else` branch is just `(void) vm;`). SCROLL-BACK/SCROLL-FWD
   therefore do not exist as words in the hosted build this suite's other
   console-fabric theories could otherwise fall back to modelling.

   Kernel build: both words pop one cell (via `vm_pop`'s own underflow
   guard, per the file's own comment explaining why no separate `dsp`
   precheck is used -- deferring to whichever convention `vm_pop` itself
   follows rather than risking a mismatch against this codebase's more
   than one historical `dsp` convention), clamp negative values to 0, then
   call `console_fb_scroll_back`/`console_fb_scroll_fwd` -- raw console
   scrollback-view state with no vm_state counterpart. Not modelled: there
   is no hosted-build fallback to fall back to, and the kernel body is a
   hardware/console-state mutation like the rest of this group. *)

lemma scroll_words_not_registered_on_hosted_build: True
  \<comment> \<open>register_scroll_words's hosted-build `#else` branch does nothing --
     SCROLL-BACK/SCROLL-FWD are absent from the dictionary entirely
     outside a kernel build, unlike every other console-fabric file in
     this sweep (which all register unconditionally with a fallback
     body).\<close>
  by simp

lemma scroll_back_not_modelled: True
  \<comment> \<open>Kernel build: pop (vm_pop's own guard) + clamp negative-to-0 + call
     console_fb_scroll_back(n) -- console scrollback state, no vm_state
     counterpart.\<close>
  by simp

lemma scroll_fwd_not_modelled: True
  \<comment> \<open>Same shape as SCROLL-BACK, console_fb_scroll_fwd(n).\<close>
  by simp

end