LithosAnanake/proof/StarForth_IO_Words.thy

theory StarForth_IO_Words
  imports StarForth_Base StarForth_Dictionary_Words
begin

(* =========================================================================
   POST-11: I/O & Terminal Words
   Mirrors: src/word_source/io_words.c (9 registered words)

   SCOPE, decided 2026-08-14: unlike block_words.c (the previous file),
   this one turned out NOT to need a near-total deferral -- worth recording
   since the previous resume-point note predicted "expect this to look
   like block_words.c" and that prediction was itself worth re-checking,
   not trusting (same discipline as the stale-blocker lesson from earlier
   in this sweep). Every word here has a real console I/O side effect
   (putchar/getchar/fflush), which is never modeled anywhere in this
   suite -- but MOST of them also have a fully deterministic, precisely
   specifiable effect on data_stack/return_stack/memory independent of
   that I/O, and that part is what gets modeled below, with the I/O
   itself simply noted as an unmodelled side channel each time.

   MODELED (7 words): EMIT, CR, ?TERMINAL, TYPE, SPACE, SPACES,
   (do-string).

   NOT MODELED (2 words), for two different reasons:
   - KEY: pushes `(cell_t) getchar()` -- unlike every other word here,
     this one's result VALUE depends on real external input, not just an
     unmodelled side effect of an otherwise-determined transition. Same
     category as string_words.c's EXPECT/QUERY (deferred there for
     exactly this reason), even though KEY's own overflow guard alone is
     trivial.
   - ." (dot_quote): the compile-time immediate word depends on
     vm->input_buffer/input_pos/input_length, the same unmodelled
     TIB-adjacent input state string_words.c's S" was deferred for.
     (do-string) -- ."'s RUNTIME companion -- is NOT in this category and
     IS modeled below, using the same return-stack-held-address-into-
     memory technique already established for control_words.c's branch
     words and string_words.c's deferred (s") sibling.

   ── Genuine finding, not fixed: ?TERMINAL is a permanent stub ──────────
   `io_word_question_terminal`'s own comment admits it: "Simple
   implementation - always return false for now." It is registered,
   callable, and returns a well-formed flag -- but that flag NEVER
   reflects real terminal state, unconditionally. Modeled faithfully as
   the constant `forth_false`, not "fixed" to poll anything.

   ── Genuine finding, not fixed: TYPE's bounds check has an integer-
   overflow bypass, a real out-of-bounds read ──────────────────────────
   `io_word_type`'s guard is `addr < 0 || count < 0 || (addr+count) >
   VM_MEMORY_SIZE`, evaluated in signed cell_t arithmetic. If addr and
   count are both large-but-individually-positive (e.g. both 2^62), their
   sum overflows the signed 64-bit range and wraps to a NEGATIVE value
   (two's complement, matching this codebase's established wraparound
   semantics elsewhere, e.g. the ALLOT finding earlier in this sweep) --
   which then compares as LESS than VM_MEMORY_SIZE, so the check reports
   "in bounds" for a request that is wildly out of bounds. Unlike the
   ALLOT case (re-analyzed earlier in this sweep and found to be actually
   safe), this one is a genuine, exploitable bypass: the subsequent loop
   reads `vm->memory[addr+i]` for i up to a huge count, a real
   out-of-bounds heap read. `type_overflow_witness_passes_check` and
   `type_overflow_witness_is_actually_oob` below give a concrete,
   machine-checked witness (addr = count = 2^62). Transcribed faithfully,
   not fixed -- report, don't silently patch, per standing instruction.
   ======================================================================== *)

(* ── EMIT ( c -- ) ─────────────────────────────────────────────────────── *)

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

lemma emit_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_emit vm)"
  by (simp add: forth_emit_def set_error_def assms)

lemma emit_pops_one:
  assumes "data_stack vm = c # rest"
  shows "data_stack (forth_emit vm) = rest"
  by (simp add: forth_emit_def assms)

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

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

lemma cr_is_identity:
  "forth_cr vm = vm"
  by (simp add: forth_cr_def)

(* ── ?TERMINAL ( -- flag ) : permanent stub, see header finding ─────────── *)

definition forth_question_terminal :: "vm_state \<Rightarrow> vm_state" where
  "forth_question_terminal vm =
    (if ds_full vm then set_error vm else vm\<lparr>data_stack := forth_false # data_stack vm\<rparr>)"

lemma question_terminal_overflow:
  assumes "ds_full vm"
  shows "vm_error (forth_question_terminal vm)"
  by (simp add: forth_question_terminal_def set_error_def assms)

lemma question_terminal_always_false:
  assumes "\<not> ds_full vm"
  shows "data_stack (forth_question_terminal vm) = forth_false # data_stack vm"
  by (simp add: forth_question_terminal_def assms)

(* ── TYPE ( addr u -- ) : see header finding on the overflow bypass ─────── *)

definition forth_type :: "vm_state \<Rightarrow> vm_state" where
  "forth_type vm =
    (case data_stack vm of
       count # addr # rest \<Rightarrow>
         if addr <s 0 \<or> count <s 0 \<or> word_of_nat VM_MEMORY_SIZE <s (addr + count)
         then set_error (vm\<lparr>data_stack := rest\<rparr>)
         else vm\<lparr>data_stack := rest\<rparr>  \<comment> \<open>printing is the only further effect, unmodelled\<close>
     | _ \<Rightarrow> set_error vm)"

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

lemma type_normal:
  assumes "data_stack vm = count # addr # rest"
  assumes "\<not> (addr <s 0 \<or> count <s 0 \<or> word_of_nat VM_MEMORY_SIZE <s (addr + count))"
  shows "data_stack (forth_type vm) = rest"
  using assms by (simp add: forth_type_def)

lemma type_overflow_witness_passes_check:
  "\<not> ((2 ^ 62 :: cell) <s 0 \<or> (2 ^ 62 :: cell) <s 0 \<or>
      word_of_nat VM_MEMORY_SIZE <s ((2 ^ 62 :: cell) + (2 ^ 62 :: cell)))"
  by eval

lemma type_overflow_witness_is_actually_oob:
  "unat (2 ^ 62 :: cell) + unat (2 ^ 62 :: cell) > VM_MEMORY_SIZE"
  \<comment> \<open>NOT `by eval`: `eval` on `unat` forces the code generator to represent
     the resulting nat in unary Peano form (no `Code_Target_Nat` import in
     this session's HOL-Library setup), so evaluating `unat` of a word as
     large as 2^62 tries to build ~4.6e18 `Suc` constructors -- this is what
     hung the build for 15+ minutes and drove free memory toward zero
     (2026-08-14). `unat_numeral` sidesteps code generation entirely: it's a
     symbolic simp lemma (`unat (numeral b) = numeral b mod 2^LENGTH('a)`),
     so the numeral arithmetic stays in `simp`'s fast binary-numeral engine,
     never touching `eval`.\<close>
  by (simp add: unat_numeral VM_MEMORY_SIZE_def)

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

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

lemma space_is_identity:
  "forth_space vm = vm"
  by (simp add: forth_space_def)

(* ── SPACES ( n -- ) : always pops, regardless of n's sign ──────────────── *)
(* C: negative n silently skips the print loop via an early `return` --
   NOT an error path, and the pop of n already happened unconditionally
   before that check. So the vm_state effect is identical for every n. *)

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

lemma spaces_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_spaces vm)"
  by (simp add: forth_spaces_def set_error_def assms)

lemma spaces_pops_one_regardless_of_sign:
  assumes "data_stack vm = n # rest"
  shows "data_stack (forth_spaces vm) = rest"
  by (simp add: forth_spaces_def assms)

(* ── (do-string) ( -- ) : runtime companion of ." ────────────────────────
   Same return-stack-held-address-into-memory technique as
   StarForth_Control_Words.thy's (BRANCH)/(0BRANCH) and
   StarForth_String_Words.thy's deferred (s") sibling. Printing the string
   itself is the unmodelled side effect; the IP-advance is fully
   deterministic and modeled precisely, including the C's exact
   cell-alignment padding formula (reusing CELL_BYTES from
   StarForth_Dictionary_Words.thy). *)

definition forth_do_string :: "vm_state \<Rightarrow> vm_state" where
  "forth_do_string vm =
    (case return_stack vm of
       []       \<Rightarrow> set_error vm
     | ip # rst \<Rightarrow>
         let n = unat (mem_read (memory vm) (unat ip) AND 0xFF);
             skip = 1 + n;
             m = skip mod CELL_BYTES;
             padded = (if m = 0 then skip else skip + (CELL_BYTES - m))
         in vm\<lparr>return_stack := (ip + word_of_nat padded) # rst\<rparr>)"

lemma do_string_underflow:
  assumes "return_stack vm = []"
  shows "vm_error (forth_do_string vm)"
  by (simp add: forth_do_string_def set_error_def assms)

lemma do_string_data_stack_unchanged:
  "data_stack (forth_do_string vm) = data_stack vm"
  by (auto simp: forth_do_string_def set_error_def Let_def split: list.split)

lemma do_string_advances_ip_past_aligned_block:
  assumes "return_stack vm = ip # rst"
  assumes "n = unat (mem_read (memory vm) (unat ip) AND 0xFF)"
  assumes "(1 + n) mod CELL_BYTES = 0"
  shows "return_stack (forth_do_string vm) = (ip + word_of_nat (1 + n)) # rst"
  using assms by (simp add: forth_do_string_def Let_def)

(* ── ." -- NOT MODELLED, see SCOPE above ─────────────────────────────────── *)

lemma dot_quote_not_modelled: True
  \<comment> \<open>Compile-time half of S"'s io_words.c sibling: depends on
     vm->input_buffer/input_pos/input_length, the TIB-adjacent input
     state deferred throughout string_words.c (WORD/SPAN/TIB/etc). See
     StarForth_String_Words.thy's header for the full argument.\<close>
  by simp

(* ── KEY -- NOT MODELLED, see SCOPE above ────────────────────────────────── *)

lemma key_not_modelled: True
  \<comment> \<open>KEY's pushed VALUE is `(cell_t) getchar()` -- real external input,
     not determined by vm_state alone (unlike every other word in this
     file, where I/O is a side effect of an otherwise fully-determined
     transition). Same category as string_words.c's EXPECT/QUERY.\<close>
  by simp

end