theory StarForth_Editor_Words
  imports StarForth_Base
begin

(* =========================================================================
   POST-12: Editor Words
   Mirrors: src/word_source/editor_words.c (4 registered words)

   SCOPE, decided 2026-08-14: none of the 4 registered words are modeled --
   the first file in this sweep with zero tractable words (block_words.c,
   the previous "worst case", still had SCR). Every word here routes
   through the shared helper `line_ptr`, which calls straight into the
   same block-subsystem cache StarForth_Block_Words.thy already documented
   as out of scope: `blk_get_buffer`/`blk_is_valid` (block_subsystem.h),
   backed by real disk I/O, none of it in vm_state. There is no analogue
   of SCR here -- editor_words.c's `current_scr` *dereferences* memory at
   `vm->scr_addr` (`vm_load_cell(vm, vm->scr_addr)`) rather than pushing
   the address itself, so even the SCR-range guard clauses ultimately gate
   entry into `line_ptr`, which is where every word's real effect lives.

   L ( u -- )     : line_ptr + print_line_64 (console I/O).
   S ( c-addr len u -- ) : line_ptr + memcpy into the block buffer (disk-
                    backed memory, not vm_state) + mark_buffer_dirty
                    (block-window cache, same gap as block_words.c).
   SHOW ( -- )    : line_ptr x16 (one per line) + printf (console I/O).
   EDIT ( u -- )  : an interactive stdin/stdout REPL loop (fgets in a
                    `for (;;)`) that dispatches to L/S/SHOW plus
                    save_all_buffers (block-window cache) -- not a
                    single-step vm_state transition in any sense the rest
                    of this suite's words are, same category as
                    block_words.c's LOAD/THRU (recursive/looping, not a
                    leaf effect).

   Nothing new added to vm_state or StarForth_Base.thy for this file --
   there is nothing self-contained enough to need it.
   ======================================================================== *)

lemma l_not_modelled: True       \<comment> \<open>L: line_ptr (block-window cache + blk_is_valid) + console I/O.\<close>
  by simp
lemma s_not_modelled: True       \<comment> \<open>S: line_ptr + memcpy into block buffer + mark_buffer_dirty.\<close>
  by simp
lemma show_not_modelled: True    \<comment> \<open>SHOW: line_ptr x16 + console I/O.\<close>
  by simp
lemma edit_not_modelled: True    \<comment> \<open>EDIT: interactive stdin/stdout REPL loop, not a single-step transition.\<close>
  by simp

end