theory StarForth_Log_Words
  imports StarForth_Base
begin

(* =========================================================================
   Mirrors: src/word_source/log_words.c
   Registers: LOG-ERROR LOG-WARN LOG-INFO LOG-TEST LOG-DEBUG LOG-LEVEL!
              LOG-LEVEL@ (do-log-error/warn/info/test/debug)
              LOG-ERROR"/WARN"/INFO"/TEST"/DEBUG" (IMMEDIATE)
              LOG-ERROR-STR/WARN-STR/INFO-STR/TEST-STR/DEBUG-STR

   ── Scope ─────────────────────────────────────────────────────────────
   Fully modelled: the five level-constant pushes (LOG-ERROR..LOG-DEBUG),
   LOG-LEVEL!'s guard+clamp (the clamped VALUE is a pure function of the
   popped cell, even though where it's stored -- the log subsystem's
   active level -- is outside vm_state), and all five LOG-*-STR words
   (same "pop2 + bounds-check guard, no further vm_state effect" shape as
   StarForth_Lifecycle_Words_Hosted.thy -- log_message is I/O-only, reads
   memory but never writes it).

   NOT modelled: LOG-LEVEL@ (pushes the log subsystem's active level, a
   value with no vm_state counterpart -- same class of gap as SEED/RANDOM's
   g_prng_state, just for a different global); the five (do-log-N) name-family
   runtime words (read/advance the return-stack top as a raw C pointer
   into inline threaded-code data, the same "raw host pointer, not a VM
   address" gap already flagged for LIT in StarForth_Defining_Words.thy);
   `log_emit_string` and the five `LOG-*"` immediates built on it (TIB/
   input-buffer dependency in interpret mode, PLUS compile-mode dependency
   on vm_find_word + vm_compile_word + vm_allot -- several already-flagged
   gaps compounded in one helper).

   ── CORRECTED finding: LOG-* words are NOT missing a guard ─────────────
   LOG-ERROR/WARN/INFO/TEST/DEBUG and LOG-LEVEL@ all push via C's
   `vm_push()` (src/stack_management.c:75), which bounds-checks internally
   -- this file's earlier claim of a missing `ds_full` check was a gap in
   this theory's abstract push model, not a real defect in the C.
   Re-verified 2026-08-14; see proof/FINDINGS.md §2 for the full
   correction across every file this pattern was raised against.
   ======================================================================== *)

definition LOG_ERROR_LEVEL :: cell where "LOG_ERROR_LEVEL = 0"
definition LOG_WARN_LEVEL  :: cell where "LOG_WARN_LEVEL  = 1"
definition LOG_INFO_LEVEL  :: cell where "LOG_INFO_LEVEL  = 2"
definition LOG_TEST_LEVEL  :: cell where "LOG_TEST_LEVEL  = 3"
definition LOG_DEBUG_LEVEL :: cell where "LOG_DEBUG_LEVEL = 4"
definition LOG_LINE_MAX    :: nat  where "LOG_LINE_MAX    = 256"

(* ── LOG-ERROR / LOG-WARN / LOG-INFO / LOG-TEST / LOG-DEBUG ( -- n ) ────── *)

definition forth_log_error :: "vm_state \<Rightarrow> vm_state" where
  "forth_log_error vm = vm\<lparr>data_stack := LOG_ERROR_LEVEL # data_stack vm\<rparr>"
definition forth_log_warn :: "vm_state \<Rightarrow> vm_state" where
  "forth_log_warn vm = vm\<lparr>data_stack := LOG_WARN_LEVEL # data_stack vm\<rparr>"
definition forth_log_info :: "vm_state \<Rightarrow> vm_state" where
  "forth_log_info vm = vm\<lparr>data_stack := LOG_INFO_LEVEL # data_stack vm\<rparr>"
definition forth_log_test :: "vm_state \<Rightarrow> vm_state" where
  "forth_log_test vm = vm\<lparr>data_stack := LOG_TEST_LEVEL # data_stack vm\<rparr>"
definition forth_log_debug :: "vm_state \<Rightarrow> vm_state" where
  "forth_log_debug vm = vm\<lparr>data_stack := LOG_DEBUG_LEVEL # data_stack vm\<rparr>"

lemma log_error_pushes: "data_stack (forth_log_error vm) = 0 # data_stack vm"
  by (simp add: forth_log_error_def LOG_ERROR_LEVEL_def)
lemma log_warn_pushes: "data_stack (forth_log_warn vm) = 1 # data_stack vm"
  by (simp add: forth_log_warn_def LOG_WARN_LEVEL_def)
lemma log_info_pushes: "data_stack (forth_log_info vm) = 2 # data_stack vm"
  by (simp add: forth_log_info_def LOG_INFO_LEVEL_def)
lemma log_test_pushes: "data_stack (forth_log_test vm) = 3 # data_stack vm"
  by (simp add: forth_log_test_def LOG_TEST_LEVEL_def)
lemma log_debug_pushes: "data_stack (forth_log_debug vm) = 4 # data_stack vm"
  by (simp add: forth_log_debug_def LOG_DEBUG_LEVEL_def)

lemma log_levels_no_overflow_guard: True
  \<comment> \<open>See file header finding -- all five push unconditionally.\<close>
  by simp

(* ── LOG-LEVEL! ( n -- ) : guard + pure clamp ─────────────────────────── *)
(* C: error if stack empty; else pop n, clamp to [LOG_ERROR, LOG_DEBUG],
   call log_set_level(n) -- the STORE target is outside vm_state, but the
   clamped value is a pure function of the input, modelled as such. *)

definition log_level_clamp :: "cell \<Rightarrow> cell" where
  "log_level_clamp n =
     (if n <s LOG_ERROR_LEVEL then LOG_ERROR_LEVEL
      else if LOG_DEBUG_LEVEL <s n then LOG_DEBUG_LEVEL
      else n)"

definition forth_log_level_store_guard :: "vm_state \<Rightarrow> vm_state" where
  "forth_log_level_store_guard vm =
    (case data_stack vm of
       []     \<Rightarrow> set_error vm
     | n # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>)"

lemma log_level_store_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_log_level_store_guard vm)"
  by (simp add: forth_log_level_store_guard_def set_error_def assms)

lemma log_level_store_pops_one:
  assumes "data_stack vm = n # xs"
  shows "data_stack (forth_log_level_store_guard vm) = xs"
  by (simp add: forth_log_level_store_guard_def assms)

lemma log_level_clamp_bounds:
  "\<not> (log_level_clamp n <s LOG_ERROR_LEVEL)"
  "\<not> (LOG_DEBUG_LEVEL <s log_level_clamp n)"
  by (auto simp: log_level_clamp_def LOG_ERROR_LEVEL_def LOG_DEBUG_LEVEL_def
                 word_sle_eq word_sless_alt)

lemma log_level_clamp_identity_in_range:
  assumes "\<not> n <s LOG_ERROR_LEVEL" "\<not> LOG_DEBUG_LEVEL <s n"
  shows "log_level_clamp n = n"
  using assms by (simp add: log_level_clamp_def)

lemma log_level_store_target_not_modelled: True
  \<comment> \<open>log_set_level(n) writes the log subsystem's active level, which has
     no vm_state counterpart.\<close>
  by simp

(* ── LOG-LEVEL@ ( -- n ) -- NOT MODELLED ──────────────────────────────── *)

lemma log_level_fetch_not_modelled: True
  \<comment> \<open>Pushes log_get_level(), reading the same unmodelled global
     LOG-LEVEL! writes to. Push is via vm_push(), which bounds-checks --
     see corrected file header.\<close>
  by simp

(* ── (do-log-N) runtime words -- NOT MODELLED ─────────────────────────── *)

lemma do_log_runtime_words_not_modelled: True
  \<comment> \<open>All five read/advance vm->return_stack[vm->rsp] as a raw C uint8_t*
     into inline threaded-code data -- the same raw-host-pointer gap
     already flagged for LIT (StarForth_Defining_Words.thy), not the
     IP-as-vaddr usage control_words.c's return-stack addresses already
     resolved.\<close>
  by simp

(* ── LOG-*" (IMMEDIATE) and log_emit_string -- NOT MODELLED ──────────── *)

lemma log_quote_words_not_modelled: True
  \<comment> \<open>log_emit_string: TIB/input-buffer dependency (interpret mode) plus,
     in compile mode, vm_find_word + vm_compile_word + vm_allot -- several
     already-flagged gaps compounded in one helper shared by all five
     LOG-*" immediates.\<close>
  by simp

(* ── LOG-ERROR-STR / -WARN-STR / -INFO-STR / -TEST-STR / -DEBUG-STR
   ( c-addr u -- ) : fully modelled, same shape as lifecycle words ───────
   C: error if dsp<1; pop u, pop addr; if u<=0, no-op (beyond the pops);
   if addr out of [0, VM_MEMORY_SIZE - u] range, error; else clamp u to
   LOG_LINE_MAX-1 and log_message a READ of vm->memory[addr..addr+u) --
   no vm_state write at all beyond the two pops. All five share this
   shape (log_str_emit), differing only in the log level passed through,
   which has no vm_state footprint. *)

definition forth_log_str_emit :: "vm_state \<Rightarrow> vm_state" where
  "forth_log_str_emit vm =
    (case data_stack vm of
       u # addr # xs \<Rightarrow>
         (if u \<le>s 0 then vm\<lparr>data_stack := xs\<rparr>
          else if addr <s 0 \<or> unat addr + unat u > VM_MEMORY_SIZE
          then set_error (vm\<lparr>data_stack := xs\<rparr>)
          else vm\<lparr>data_stack := xs\<rparr>)
     | _ \<Rightarrow> set_error vm)"

lemma log_str_emit_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_log_str_emit vm)"
  by (simp add: forth_log_str_emit_def set_error_def assms)

lemma log_str_emit_underflow_one:
  assumes "data_stack vm = [x]"
  shows "vm_error (forth_log_str_emit vm)"
  by (simp add: forth_log_str_emit_def set_error_def assms)

lemma log_str_emit_nonpositive_len_pops_only:
  assumes "data_stack vm = u # addr # xs"
  assumes "u \<le>s 0"
  shows "forth_log_str_emit vm = vm\<lparr>data_stack := xs\<rparr>"
  using assms by (simp add: forth_log_str_emit_def)

lemma log_str_emit_out_of_range_errors:
  assumes "data_stack vm = u # addr # xs"
  assumes "\<not> u \<le>s 0"
  assumes "addr <s 0 \<or> unat addr + unat u > VM_MEMORY_SIZE"
  shows "vm_error (forth_log_str_emit vm)"
  using assms by (simp add: forth_log_str_emit_def set_error_def)

lemma log_str_emit_normal:
  assumes "data_stack vm = u # addr # xs"
  assumes "\<not> u \<le>s 0"
  assumes "\<not> (addr <s 0 \<or> unat addr + unat u > VM_MEMORY_SIZE)"
  shows "forth_log_str_emit vm = vm\<lparr>data_stack := xs\<rparr>"
  using assms by (simp add: forth_log_str_emit_def)

lemma log_str_emit_never_writes_memory:
  "memory (forth_log_str_emit vm) = memory vm"
  by (auto simp: forth_log_str_emit_def set_error_def split: list.split)

definition forth_log_error_str :: "vm_state \<Rightarrow> vm_state" where "forth_log_error_str = forth_log_str_emit"
definition forth_log_warn_str  :: "vm_state \<Rightarrow> vm_state" where "forth_log_warn_str  = forth_log_str_emit"
definition forth_log_info_str  :: "vm_state \<Rightarrow> vm_state" where "forth_log_info_str  = forth_log_str_emit"
definition forth_log_test_str  :: "vm_state \<Rightarrow> vm_state" where "forth_log_test_str  = forth_log_str_emit"
definition forth_log_debug_str :: "vm_state \<Rightarrow> vm_state" where "forth_log_debug_str = forth_log_str_emit"

lemma log_error_str_is_emit: "forth_log_error_str vm = forth_log_str_emit vm" by (simp add: forth_log_error_str_def)
lemma log_warn_str_is_emit:  "forth_log_warn_str  vm = forth_log_str_emit vm" by (simp add: forth_log_warn_str_def)
lemma log_info_str_is_emit:  "forth_log_info_str  vm = forth_log_str_emit vm" by (simp add: forth_log_info_str_def)
lemma log_test_str_is_emit:  "forth_log_test_str  vm = forth_log_str_emit vm" by (simp add: forth_log_test_str_def)
lemma log_debug_str_is_emit: "forth_log_debug_str vm = forth_log_str_emit vm" by (simp add: forth_log_debug_str_def)

end