theory StarForth_Format_Words
  imports StarForth_Base StarForth_Memory_Words
begin

(* =========================================================================
   POST-13: Format / Numeric-Conversion Words
   Mirrors: src/word_source/format_words.c (18 registered words)

   ── Genuine finding, not fixed: BASE output and BASE input silently desync ─
   `current_base()` (used by every number-OUTPUT word below: `.`/`.R`/`U.`/
   `U.R`/`#`/`#S`) reads `vm->base` directly -- the C struct's host-mirror
   cell_t field. `DECIMAL`/`HEX`/`OCTAL` (and `BASE` itself) never touch
   that field: they call `vm_store_cell(vm, vm->base_addr, ...)`, writing
   only the FORTH-visible memory cell at `vm->base_addr`. The ONLY place
   that keeps the two in sync is `vm_set_base()` (src/vm.c:109), which
   `format_words.c` never calls -- and `vm_set_base()` itself is only ever
   invoked once, at boot (`vm_bootstrap.c:222`, hard-coded to 10). Number
   *parsing* (`vm_get_base()`, src/vm.c:84, used by the numeric-literal
   reader) DOES prefer the memory cell, so it correctly honors HEX/OCTAL/
   DECIMAL -- but number *output* never sees the change. Net effect: `HEX
   FF .` continues to print in whatever base `vm->base` last held (10,
   forever, since nothing else ever sets it), even though `HEX` genuinely
   changed the FORTH BASE variable that parsing and BASE-fetching code see.
   Proved below as `decimal_does_not_change_vm_base` et al. -- a formal,
   machine-checked witness of the desync, not a hypothesis.

   ── Genuine finding, not fixed: `?` and `DUMP` dereference a raw host
      pointer, bypassing the VM's own memory abstraction entirely ─────────
   Every other memory-reading word in this codebase goes through
   `vm_load_cell`/`vm->memory[...]` with `vm_addr_ok` bounds checking (see
   StarForth_Memory_Words.thy's `@`/`C@`). `format_word_question` (`?`) and
   `format_word_dump` (`DUMP`) instead cast the popped cell straight to a
   host pointer via a C-style cast to `cell_t`-pointer / `uint8_t`-pointer
   (see format_words.c's format_word_question/format_word_dump) --
   casting the popped FORTH cell DIRECTLY to a host pointer and
   dereferencing it, with only a null check (`addr == 0`), never a
   VM-memory-bounds check. Any FORTH program (or ACL-unprivileged user,
   if these words are ever exposed past `zuse_session`) can hand `?`/`DUMP`
   an arbitrary non-zero integer and get an arbitrary host-memory read --
   a real, exploitable out-of-VM-bounds read, categorically worse than
   `TYPE`'s in-VM overflow bypass (StarForth_IO_Words.thy). Not modeled as
   a memory read below (it isn't a `vm->memory` access at all, so nothing
   in this suite's memory model applies) -- only the pop/guard shape is
   modeled; the dereference itself is exactly the finding.

   MODELED (17 words): BASE, DECIMAL, HEX, OCTAL, `<#`, HOLD, SIGN, `#>`,
   `.`, `.R`, `U.`, `U.R`, `D.`, `D.R`, `.S`, `?`, `DUMP`.

   NOT MODELED (2 words): `#` and `#S`. `#` performs `div_ud_by_base`, a
   16-bit-chunked long division of a double-cell (128-bit-equivalent)
   magnitude by an arbitrary base 2..36 -- multi-precision division
   algorithm correctness is its own proof project, on the scale of the
   block-window cache or TIB input-subsystem deferrals elsewhere in this
   sweep, not a one-word extension. `#S` loops `#` in an unbounded `for
   (;;)` until the quotient reaches zero -- termination itself would need
   to be established (it does, since the magnitude strictly decreases each
   iteration under division by base \<ge> 2, but that argument depends on
   `#`'s own arithmetic being modeled first). Both deferred together.
   ======================================================================== *)

definition PN_CAP :: nat where "PN_CAP = 64"
  \<comment> \<open>○ CODE-MUST-MATCH: #define PN_CAP 64 in format_words.c\<close>

(* ── BASE ( -- addr ) : pushes the ADDRESS of the BASE cell, like SCR ───── *)

definition forth_base :: "vm_state \<Rightarrow> vm_state" where
  "forth_base vm = vm\<lparr>data_stack := word_of_nat (base_addr vm) # data_stack vm\<rparr>"

lemma base_pushes_base_addr:
  "data_stack (forth_base vm) = word_of_nat (base_addr vm) # data_stack vm"
  by (simp add: forth_base_def)

(* ── DECIMAL / HEX / OCTAL ( -- ) : write the memory cell, NOT vm_base ──── *)

definition forth_decimal :: "vm_state \<Rightarrow> vm_state" where
  "forth_decimal vm = vm\<lparr>memory := mem_write (memory vm) (base_addr vm) 10\<rparr>"

definition forth_hex :: "vm_state \<Rightarrow> vm_state" where
  "forth_hex vm = vm\<lparr>memory := mem_write (memory vm) (base_addr vm) 16\<rparr>"

definition forth_octal :: "vm_state \<Rightarrow> vm_state" where
  "forth_octal vm = vm\<lparr>memory := mem_write (memory vm) (base_addr vm) 8\<rparr>"

lemma decimal_sets_base_cell:
  "mem_read (memory (forth_decimal vm)) (base_addr vm) = 10"
  by (simp add: forth_decimal_def mem_read_def mem_write_def)

lemma decimal_does_not_change_vm_base:
  "vm_base (forth_decimal vm) = vm_base vm"
  by (simp add: forth_decimal_def)

lemma hex_sets_base_cell:
  "mem_read (memory (forth_hex vm)) (base_addr vm) = 16"
  by (simp add: forth_hex_def mem_read_def mem_write_def)

lemma hex_does_not_change_vm_base:
  "vm_base (forth_hex vm) = vm_base vm"
  by (simp add: forth_hex_def)

lemma octal_sets_base_cell:
  "mem_read (memory (forth_octal vm)) (base_addr vm) = 8"
  by (simp add: forth_octal_def mem_read_def mem_write_def)

lemma octal_does_not_change_vm_base:
  "vm_base (forth_octal vm) = vm_base vm"
  by (simp add: forth_octal_def)

(* ── <# ( -- ) : hold_pos := 0, clear PN_CAP bytes at hold_addr ─────────── *)

definition forth_begin_conversion :: "vm_state \<Rightarrow> vm_state" where
  "forth_begin_conversion vm =
    vm\<lparr>hold_pos := 0,
       memory := (\<lambda>a. if hold_addr vm \<le> a \<and> a < hold_addr vm + PN_CAP
                       then 0 else memory vm a)\<rparr>"

lemma begin_conversion_resets_hold_pos:
  "hold_pos (forth_begin_conversion vm) = 0"
  by (simp add: forth_begin_conversion_def)

lemma begin_conversion_clears_buffer:
  assumes "hold_addr vm \<le> a" "a < hold_addr vm + PN_CAP"
  shows "memory (forth_begin_conversion vm) a = 0"
  using assms by (simp add: forth_begin_conversion_def)

lemma begin_conversion_data_stack_unchanged:
  "data_stack (forth_begin_conversion vm) = data_stack vm"
  by (simp add: forth_begin_conversion_def)

(* ── HOLD ( c -- ) : prepend byte to the pictured-number buffer ─────────── *)

definition forth_hold :: "vm_state \<Rightarrow> vm_state" where
  "forth_hold vm =
    (case data_stack vm of
       []     \<Rightarrow> set_error vm
     | c # rest \<Rightarrow>
         if c <s 0 \<or> (255 :: cell) <s c
         then set_error (vm\<lparr>data_stack := rest\<rparr>)
         else if hold_pos vm \<ge> PN_CAP - 1
              then set_error (vm\<lparr>data_stack := rest\<rparr>)
              else vm\<lparr>data_stack := rest,
                      memory := (\<lambda>a. if a = hold_addr vm then c
                                     else if hold_addr vm < a \<and> a \<le> hold_addr vm + hold_pos vm
                                          then memory vm (a - 1)
                                          else memory vm a),
                      hold_pos := hold_pos vm + 1\<rparr>)"

lemma hold_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_hold vm)"
  by (simp add: forth_hold_def set_error_def assms)

lemma hold_out_of_range:
  assumes "data_stack vm = c # rest" "c <s 0 \<or> (255 :: cell) <s c"
  shows "vm_error (forth_hold vm) \<and> data_stack (forth_hold vm) = rest"
  using assms by (simp add: forth_hold_def set_error_def)

lemma hold_buffer_full:
  assumes "data_stack vm = c # rest" "\<not> (c <s 0 \<or> (255 :: cell) <s c)" "hold_pos vm \<ge> PN_CAP - 1"
  shows "vm_error (forth_hold vm) \<and> data_stack (forth_hold vm) = rest"
  using assms by (simp add: forth_hold_def set_error_def)

lemma hold_normal_prepends_and_advances:
  assumes "data_stack vm = c # rest" "\<not> (c <s 0 \<or> (255 :: cell) <s c)" "hold_pos vm < PN_CAP - 1"
  shows "data_stack (forth_hold vm) = rest"
    and "memory (forth_hold vm) (hold_addr vm) = c"
    and "hold_pos (forth_hold vm) = hold_pos vm + 1"
  using assms by (simp_all add: forth_hold_def)

(* ── SIGN ( n -- ) : prepend '-' via HOLD iff n < 0 ──────────────────────── *)

definition forth_sign :: "vm_state \<Rightarrow> vm_state" where
  "forth_sign vm =
    (case data_stack vm of
       []     \<Rightarrow> set_error vm
     | n # rest \<Rightarrow>
         if n <s 0
         then forth_hold (vm\<lparr>data_stack := (45 :: cell) # rest\<rparr>)  \<comment> \<open>'-' = ASCII 45\<close>
         else vm\<lparr>data_stack := rest\<rparr>)"

lemma sign_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_sign vm)"
  by (simp add: forth_sign_def set_error_def assms)

lemma sign_nonnegative_just_pops:
  assumes "data_stack vm = n # rest" "\<not> n <s 0"
  shows "data_stack (forth_sign vm) = rest"
  using assms by (simp add: forth_sign_def)

lemma sign_negative_calls_hold:
  assumes "data_stack vm = n # rest" "n <s 0"
  shows "forth_sign vm = forth_hold (vm\<lparr>data_stack := (45 :: cell) # rest\<rparr>)"
  using assms by (simp add: forth_sign_def)

(* ── # / #S -- NOT MODELLED, see SCOPE above ─────────────────────────────── *)

lemma hash_not_modelled: True    \<comment> \<open>#: chunked multi-precision division, own proof project.\<close>
  by simp
lemma hash_s_not_modelled: True  \<comment> \<open>#S: loops #, inherits its gap plus loop termination.\<close>
  by simp

(* ── #> ( [ud] -- addr u ) : drop optional double, push hold buffer view ── *)

definition forth_end_conversion :: "vm_state \<Rightarrow> vm_state" where
  "forth_end_conversion vm =
    (let ds' = (if length (data_stack vm) \<ge> 2 then drop 2 (data_stack vm) else data_stack vm)
     in vm\<lparr>data_stack := word_of_nat (hold_pos vm) # word_of_nat (hold_addr vm) # ds'\<rparr>)"

lemma end_conversion_never_errors:
  "vm_error (forth_end_conversion vm) = vm_error vm"
  by (simp add: forth_end_conversion_def Let_def)

lemma end_conversion_pushes_buffer_view:
  "data_stack (forth_end_conversion vm) =
     word_of_nat (hold_pos vm) # word_of_nat (hold_addr vm) #
       (if length (data_stack vm) \<ge> 2 then drop 2 (data_stack vm) else data_stack vm)"
  by (simp add: forth_end_conversion_def Let_def)

(* ── . / U. ( n -- ) : pop one, print (unmodelled I/O) ───────────────────── *)

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

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

lemma dot_underflow: "data_stack vm = [] \<Longrightarrow> vm_error (forth_dot vm)"
  by (simp add: forth_dot_def set_error_def)
lemma dot_pops_one: "data_stack vm = n # rest \<Longrightarrow> data_stack (forth_dot vm) = rest"
  by (simp add: forth_dot_def)
lemma u_dot_underflow: "data_stack vm = [] \<Longrightarrow> vm_error (forth_u_dot vm)"
  by (simp add: forth_u_dot_def set_error_def)
lemma u_dot_pops_one: "data_stack vm = n # rest \<Longrightarrow> data_stack (forth_u_dot vm) = rest"
  by (simp add: forth_u_dot_def)

(* ── .R / U.R ( n width -- ) : pop two, print (unmodelled I/O) ──────────── *)

definition forth_dot_r :: "vm_state \<Rightarrow> vm_state" where
  "forth_dot_r vm =
    (if length (data_stack vm) < 2 then set_error vm
     else vm\<lparr>data_stack := drop 2 (data_stack vm)\<rparr>)"

definition forth_u_dot_r :: "vm_state \<Rightarrow> vm_state" where
  "forth_u_dot_r vm =
    (if length (data_stack vm) < 2 then set_error vm
     else vm\<lparr>data_stack := drop 2 (data_stack vm)\<rparr>)"

lemma dot_r_underflow: "length (data_stack vm) < 2 \<Longrightarrow> vm_error (forth_dot_r vm)"
  by (simp add: forth_dot_r_def set_error_def)
lemma dot_r_pops_two:
  "length (data_stack vm) \<ge> 2 \<Longrightarrow> data_stack (forth_dot_r vm) = drop 2 (data_stack vm)"
  by (simp add: forth_dot_r_def)
lemma u_dot_r_underflow: "length (data_stack vm) < 2 \<Longrightarrow> vm_error (forth_u_dot_r vm)"
  by (simp add: forth_u_dot_r_def set_error_def)
lemma u_dot_r_pops_two:
  "length (data_stack vm) \<ge> 2 \<Longrightarrow> data_stack (forth_u_dot_r vm) = drop 2 (data_stack vm)"
  by (simp add: forth_u_dot_r_def)

(* ── D. ( d -- ) : pop two, print (unmodelled I/O, both branches) ───────── *)

definition forth_d_dot :: "vm_state \<Rightarrow> vm_state" where
  "forth_d_dot vm =
    (if length (data_stack vm) < 2 then set_error vm
     else vm\<lparr>data_stack := drop 2 (data_stack vm)\<rparr>)"

lemma d_dot_underflow: "length (data_stack vm) < 2 \<Longrightarrow> vm_error (forth_d_dot vm)"
  by (simp add: forth_d_dot_def set_error_def)
lemma d_dot_pops_two:
  "length (data_stack vm) \<ge> 2 \<Longrightarrow> data_stack (forth_d_dot vm) = drop 2 (data_stack vm)"
  by (simp add: forth_d_dot_def)

(* ── D.R ( d width -- ) : pop three, print (unmodelled I/O, both branches) *)

definition forth_d_dot_r :: "vm_state \<Rightarrow> vm_state" where
  "forth_d_dot_r vm =
    (if length (data_stack vm) < 3 then set_error vm
     else vm\<lparr>data_stack := drop 3 (data_stack vm)\<rparr>)"

lemma d_dot_r_underflow: "length (data_stack vm) < 3 \<Longrightarrow> vm_error (forth_d_dot_r vm)"
  by (simp add: forth_d_dot_r_def set_error_def)
lemma d_dot_r_pops_three:
  "length (data_stack vm) \<ge> 3 \<Longrightarrow> data_stack (forth_d_dot_r vm) = drop 3 (data_stack vm)"
  by (simp add: forth_d_dot_r_def)

(* ── .S ( -- ) : pure I/O, no vm_state effect at all ─────────────────────── *)

definition forth_dot_s :: "vm_state \<Rightarrow> vm_state" where
  "forth_dot_s vm = vm"

lemma dot_s_is_identity: "forth_dot_s vm = vm"
  by (simp add: forth_dot_s_def)

(* ── ? ( addr -- ) : pop one; error iff addr = 0; see header finding ────── *)

definition forth_question :: "vm_state \<Rightarrow> vm_state" where
  "forth_question vm =
    (case data_stack vm of
       []        \<Rightarrow> set_error vm
     | addr # rest \<Rightarrow>
         if addr = 0 then set_error (vm\<lparr>data_stack := rest\<rparr>)
         else vm\<lparr>data_stack := rest\<rparr>)  \<comment> \<open>raw host-pointer deref, unmodelled\<close>"

lemma question_underflow: "data_stack vm = [] \<Longrightarrow> vm_error (forth_question vm)"
  by (simp add: forth_question_def set_error_def)
lemma question_null_errors:
  "data_stack vm = 0 # rest \<Longrightarrow> vm_error (forth_question vm) \<and> data_stack (forth_question vm) = rest"
  by (simp add: forth_question_def set_error_def)
lemma question_pops_one:
  "data_stack vm = addr # rest \<Longrightarrow> data_stack (forth_question vm) = rest"
  by (simp add: forth_question_def)

(* ── DUMP ( addr u -- ) : pop two; error iff u<0 or addr=0; see finding ─── *)

definition forth_dump :: "vm_state \<Rightarrow> vm_state" where
  "forth_dump vm =
    (case data_stack vm of
       u # addr # rest \<Rightarrow>
         if u <s 0 then set_error (vm\<lparr>data_stack := rest\<rparr>)
         else if addr = 0 then set_error (vm\<lparr>data_stack := rest\<rparr>)
         else vm\<lparr>data_stack := rest\<rparr>  \<comment> \<open>raw host-pointer deref, unmodelled\<close>
     | _ \<Rightarrow> set_error vm)"

lemma dump_underflow:
  assumes "length (data_stack vm) < 2"
  shows "vm_error (forth_dump vm)"
proof (cases "data_stack vm")
  case Nil then show ?thesis using assms by (simp add: forth_dump_def set_error_def)
next
  case (Cons x xs) then show ?thesis using assms
    by (cases xs) (auto simp: forth_dump_def set_error_def)
qed

lemma dump_negative_count_errors:
  assumes "data_stack vm = u # addr # rest" "u <s 0"
  shows "vm_error (forth_dump vm) \<and> data_stack (forth_dump vm) = rest"
  using assms by (simp add: forth_dump_def set_error_def)

lemma dump_null_addr_errors:
  assumes "data_stack vm = u # 0 # rest" "\<not> u <s 0"
  shows "vm_error (forth_dump vm) \<and> data_stack (forth_dump vm) = rest"
  using assms by (simp add: forth_dump_def set_error_def)

lemma dump_pops_two:
  assumes "data_stack vm = u # addr # rest"
  shows "data_stack (forth_dump vm) = rest"
  using assms by (simp add: forth_dump_def)

end