LithosAnanake/proof/StarForth_String_Words.thy

theory StarForth_String_Words
  imports StarForth_Base StarForth_Dictionary_Words
begin

unbundle bit_operations_syntax

(* =========================================================================
   POST-09: String & Text Processing Words
   Mirrors: src/word_source/string_words.c (25 registered words; see SCOPE)

   SCOPE, decided 2026-08-14: this is the largest word_source file in the
   sweep by word count. Split into two groups:

   1. MODELED (9 words) -- self-contained: operate purely on data_stack and
      vm->memory via vaddr_t offsets, no dependency on anything outside the
      existing abstract model. BL, COUNT, CMOVE, CMOVE>, BLANK, -TRAILING,
      SCAN, SKIP, COMPARE.

   2. NOT MODELED (16 words), for three distinct reasons:
      a. TIB / input-subsystem dependency (WORD, SPAN, TIB, >IN, SOURCE,
         QUERY, EXPECT): all route through vm_input_ensure/vm_input_tib/
         vm_input_in/vm_input_span (src/vm_api.c), which lazily allocate
         vm->tib_buf via vm_allot on first use. None of vm->tib_buf,
         vm->tib_cap, or a >IN/SPAN cell have any vm_state counterpart.
         Modeling this properly means adding a lazy-init input subsystem
         to vm_state -- out of scope for this pass, flagged for a
         dedicated one, same class of decision as ecw_nesting was for
         StarForth_Double_Words.thy (a real gap, worth scoping properly
         rather than rushing).
      b. Real stdio I/O (EXPECT, QUERY, already listed in (a) since both
         also depend on TIB): calls fgets(stdin) directly. Not formalizable
         as a pure vm_state -> vm_state transition regardless of the TIB
         question -- genuine external interaction, same category as this
         suite has never attempted anywhere else.
      c. Raw C-string / host-library dependency (CONVERT, NUMBER, ENCLOSE):
         CONVERT and ENCLOSE call strlen()/index a host C pointer directly
         with only the FIRST byte's vm_addr_ok verified -- an unbounded
         scan past a single checked byte, relying on NUL-termination that
         nothing in the VM model guarantees (a real hazard, noted but not
         chased further here). NUMBER calls strtol() via
         convert_string_to_number(), a host libc call with no HOL
         counterpart in this suite.
      Also NOT modeled, same subsystem-dependency reasons: S" / (s") (the
      compile-time half depends on vm->input_buffer/input_pos/input_length,
      none in vm_state; the runtime half (s") is technically tractable via
      the same return-stack-as-address technique StarForth_Control_Words.thy
      established, but not worth doing in isolation from S" itself), and
      LITERAL / [LITERAL] (both are empty no-op stubs in the current C --
      trivial, but paired with the S" cluster for this pass) and ['] (tick
      variant, depends on vm_find_word / vm_compile_literal, same class of
      dictionary-compile machinery as control_words.c's compile-time words).
      SEARCH is ALSO not modeled despite being self-contained like its
      neighbors -- its naive nested substring search needs a genuinely
      bigger proof-engineering lift (a bounded search-from-i helper) than
      the single-pass helpers below; deferred for a focused follow-up
      rather than rushed alongside nine other words in one pass.

   ── Genuine finding, not fixed ───────────────────────────────────────────
   `string_word_word` (WORD) uses `static vaddr_t word_scratch_addr = 0` --
   a file-scope C static, lazily allocated on first call and reused for
   EVERY subsequent WORD call by EVERY VM in the process. This is the same
   architectural pattern already flagged twice in this sweep (control_words.c's
   cf_stack, dictionary_manipulation_words.c's state_variable): not per-VM,
   shared mutable global. Noted here even though WORD itself isn't modeled
   in this pass (blocked on the TIB subsystem regardless) -- it's the third
   occurrence of the same bug class, worth aggregating when this gets raised
   to Bob rather than treating each occurrence as an isolated one-off.

   ── vm_addr_ok, modeled precisely this time ──────────────────────────────
   Earlier files (StarForth_Memory_Words.thy) modeled vm_addr_ok loosely via
   a sign check on the cell (`0 \<le>s addr`) plus a placeholder `valid_addr`
   that is unconditionally True. This file has VM_MEMORY_SIZE available
   (added in StarForth_Dictionary_Words.thy) and several words that check
   vm_addr_ok's actual bounds behavior, not just its sign -- so
   vm_addr_ok_m below is a literal transcription of the real C
   (src/vm.c:815-820: reject len > VM_MEMORY_SIZE, else addr <=
   VM_MEMORY_SIZE - len), not a placeholder. Does not retrofit older files.
   ======================================================================== *)

definition vm_addr_ok_m :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
  "vm_addr_ok_m a n \<longleftrightarrow> n \<le> VM_MEMORY_SIZE \<and> a \<le> VM_MEMORY_SIZE - n"

(* ── Shared helper: auto-detect counted-string form ───────────────────────
   Several words (-TRAILING, BLANK, SCAN, SKIP, COMPARE, and the deferred
   SEARCH) share one exact pattern: if the byte at `a` equals `n` and looks
   like a valid count byte, treat [a+1, a+1+n) as the char span; otherwise
   treat [a, a+n) directly. Returns (resolved start address, bounds-ok). *)

definition resolve_span :: "(nat \<Rightarrow> cell) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (nat \<times> bool)" where
  "resolve_span mem a n =
    (if n \<le> 255 \<and> vm_addr_ok_m a 1 \<and> (mem_read mem a AND 0xFF) = word_of_nat n
     then (a + 1, vm_addr_ok_m (a + 1) n)
     else (a, vm_addr_ok_m a n))"

(* ── BL ( -- c ) : push ASCII space ────────────────────────────────────── *)

definition forth_bl :: "vm_state \<Rightarrow> vm_state" where
  "forth_bl vm = vm\<lparr>data_stack := 32 # data_stack vm\<rparr>"

lemma bl_pushes_32:
  "data_stack (forth_bl vm) = 32 # data_stack vm"
  by (simp add: forth_bl_def)

(* ── COUNT ( addr1 -- addr2 u ) ────────────────────────────────────────── *)
(* C: no sign check on addr1 -- VM_ADDR reinterprets it as unsigned
   directly (unlike @/! which check `<s 0` first); a negative addr1 simply
   becomes a huge unat value that vm_addr_ok_m then rejects. Transcribed
   as such, not "fixed" to add a sign check that isn't there. *)

definition forth_count :: "vm_state \<Rightarrow> vm_state" where
  "forth_count vm =
    (case data_stack vm of
       []          \<Rightarrow> set_error vm
     | addr1 # rest \<Rightarrow>
         let a = unat addr1
         in if \<not> vm_addr_ok_m a 1
            then set_error (vm\<lparr>data_stack := rest\<rparr>)
            else let count = mem_read (memory vm) a AND 0xFF
                 in if \<not> vm_addr_ok_m (a + 1) (unat count)
                    then set_error (vm\<lparr>data_stack := rest\<rparr>)
                    else vm\<lparr>data_stack := count # word_of_nat (a + 1) # rest\<rparr>)"

lemma count_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_count vm)"
  by (simp add: forth_count_def set_error_def assms)

lemma count_normal:
  assumes "data_stack vm = addr1 # rest"
  assumes "vm_addr_ok_m (unat addr1) 1"
  assumes "vm_addr_ok_m (unat addr1 + 1) (unat (mem_read (memory vm) (unat addr1) AND 0xFF))"
  shows "data_stack (forth_count vm) =
         (mem_read (memory vm) (unat addr1) AND 0xFF) # word_of_nat (unat addr1 + 1) # rest"
  using assms by (simp add: forth_count_def Let_def)

(* ── CMOVE ( addr1 addr2 u -- ) : ascending byte copy ─────────────────────
   C: dsp<2 -> error; pops u,addr2,addr1 (all three popped BEFORE the u<0
   check, so an error here still leaves data_stack popped, matching
   ALLOT's pop-then-check pattern). u=0 is a silent successful no-op (not
   an error) that still consumes all three stack args. Ascending order
   (index i: 0..n-1, each step reads-then-writes using the CURRENT,
   possibly-already-modified memory) matches the real forward-copy overlap
   semantics -- correct when addr2 >= addr1, wrong otherwise, exactly as
   the C comment states and doesn't defend against. *)

fun mem_copy_asc :: "(nat \<Rightarrow> cell) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (nat \<Rightarrow> cell)" where
  "mem_copy_asc mem src dst 0 = mem"
| "mem_copy_asc mem src dst (Suc k) =
     mem_copy_asc (mem_write mem dst (mem_read mem src)) (src + 1) (dst + 1) k"

definition forth_cmove :: "vm_state \<Rightarrow> vm_state" where
  "forth_cmove vm =
    (case data_stack vm of
       u # addr2 # addr1 # rest \<Rightarrow>
         (if u <s 0 then set_error (vm\<lparr>data_stack := rest\<rparr>)
          else if u = 0 then vm\<lparr>data_stack := rest\<rparr>
          else let src = unat addr1; dst = unat addr2; n = unat u
               in if \<not> vm_addr_ok_m src n \<or> \<not> vm_addr_ok_m dst n
                  then set_error (vm\<lparr>data_stack := rest\<rparr>)
                  else vm\<lparr>data_stack := rest, memory := mem_copy_asc (memory vm) src dst n\<rparr>)
     | _ \<Rightarrow> set_error vm)"

lemma cmove_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_cmove vm)"
  by (simp add: forth_cmove_def set_error_def assms)

lemma cmove_negative_errors:
  assumes "data_stack vm = u # addr2 # addr1 # rest"
  assumes "u <s 0"
  shows "vm_error (forth_cmove vm)"
    and "data_stack (forth_cmove vm) = rest"
  using assms by (simp_all add: forth_cmove_def)

lemma cmove_zero_is_noop:
  assumes "data_stack vm = 0 # addr2 # addr1 # rest"
  shows "data_stack (forth_cmove vm) = rest"
    and "memory (forth_cmove vm) = memory vm"
  using assms by (simp_all add: forth_cmove_def)

lemma cmove_normal:
  assumes "data_stack vm = u # addr2 # addr1 # rest"
  assumes "\<not> u <s 0" "u \<noteq> 0"
  assumes "vm_addr_ok_m (unat addr1) (unat u)"
  assumes "vm_addr_ok_m (unat addr2) (unat u)"
  shows "data_stack (forth_cmove vm) = rest"
    and "memory (forth_cmove vm) = mem_copy_asc (memory vm) (unat addr1) (unat addr2) (unat u)"
  using assms by (simp_all add: forth_cmove_def Let_def)

(* ── CMOVE> ( addr1 addr2 u -- ) : descending byte copy ───────────────── *)

fun mem_copy_desc :: "(nat \<Rightarrow> cell) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (nat \<Rightarrow> cell)" where
  "mem_copy_desc mem src dst 0 = mem"
| "mem_copy_desc mem src dst (Suc k) =
     (let mem' = mem_write mem (dst + k) (mem_read mem (src + k))
      in mem_copy_desc mem' src dst k)"

definition forth_cmove_greater :: "vm_state \<Rightarrow> vm_state" where
  "forth_cmove_greater vm =
    (case data_stack vm of
       u # addr2 # addr1 # rest \<Rightarrow>
         (if u <s 0 then set_error (vm\<lparr>data_stack := rest\<rparr>)
          else if u = 0 then vm\<lparr>data_stack := rest\<rparr>
          else let src = unat addr1; dst = unat addr2; n = unat u
               in if \<not> vm_addr_ok_m src n \<or> \<not> vm_addr_ok_m dst n
                  then set_error (vm\<lparr>data_stack := rest\<rparr>)
                  else vm\<lparr>data_stack := rest, memory := mem_copy_desc (memory vm) src dst n\<rparr>)
     | _ \<Rightarrow> set_error vm)"

lemma cmove_greater_normal:
  assumes "data_stack vm = u # addr2 # addr1 # rest"
  assumes "\<not> u <s 0" "u \<noteq> 0"
  assumes "vm_addr_ok_m (unat addr1) (unat u)"
  assumes "vm_addr_ok_m (unat addr2) (unat u)"
  shows "data_stack (forth_cmove_greater vm) = rest"
    and "memory (forth_cmove_greater vm) = mem_copy_desc (memory vm) (unat addr1) (unat addr2) (unat u)"
  using assms by (simp_all add: forth_cmove_greater_def Let_def)

(* ── BLANK ( addr u -- ) : fill with ASCII space ──────────────────────── *)
(* C: u<0 -> error (does NOT clamp, unlike -TRAILING/SCAN/SKIP/COMPARE
   below); u=0 is a silent no-op. *)

fun mem_fill :: "(nat \<Rightarrow> cell) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> cell \<Rightarrow> (nat \<Rightarrow> cell)" where
  "mem_fill mem addr 0 v = mem"
| "mem_fill mem addr (Suc k) v = mem_fill (mem_write mem addr v) (addr + 1) k v"

definition forth_blank :: "vm_state \<Rightarrow> vm_state" where
  "forth_blank 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 u = 0 then vm\<lparr>data_stack := rest\<rparr>
          else let (s, ok) = resolve_span (memory vm) (unat addr) (unat u)
               in if \<not> ok then set_error (vm\<lparr>data_stack := rest\<rparr>)
                  else vm\<lparr>data_stack := rest, memory := mem_fill (memory vm) s (unat u) 32\<rparr>)
     | _ \<Rightarrow> set_error vm)"

lemma blank_negative_errors:
  assumes "data_stack vm = u # addr # rest"
  assumes "u <s 0"
  shows "vm_error (forth_blank vm)"
  using assms by (simp add: forth_blank_def)

lemma blank_zero_is_noop:
  assumes "data_stack vm = 0 # addr # rest"
  shows "data_stack (forth_blank vm) = rest"
    and "memory (forth_blank vm) = memory vm"
  using assms by (simp_all add: forth_blank_def)

lemma blank_normal:
  assumes "data_stack vm = u # addr # rest"
  assumes "\<not> u <s 0" "u \<noteq> 0"
  assumes "resolve_span (memory vm) (unat addr) (unat u) = (s, True)"
  shows "data_stack (forth_blank vm) = rest"
    and "memory (forth_blank vm) = mem_fill (memory vm) s (unat u) 32"
  using assms by (simp_all add: forth_blank_def)

(* ── -TRAILING ( addr u -- addr' u' ) : trim trailing ASCII spaces ────── *)
(* C: u<0 -> CLAMPED to 0 (not an error, unlike BLANK). *)

fun trim_trailing :: "(nat \<Rightarrow> cell) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
  "trim_trailing mem s 0 = 0"
| "trim_trailing mem s (Suc k) =
     (if (mem_read mem (s + k) AND 0xFF) = 32 then trim_trailing mem s k else Suc k)"

definition forth_minus_trailing :: "vm_state \<Rightarrow> vm_state" where
  "forth_minus_trailing vm =
    (case data_stack vm of
       u # addr # rest \<Rightarrow>
         let n = (if u <s 0 then 0 else unat u);
             (s, ok) = resolve_span (memory vm) (unat addr) n
         in if \<not> ok then set_error (vm\<lparr>data_stack := rest\<rparr>)
            else vm\<lparr>data_stack := word_of_nat (trim_trailing (memory vm) s n) # word_of_nat s # rest\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma minus_trailing_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_minus_trailing vm)"
  by (simp add: forth_minus_trailing_def set_error_def assms)

lemma minus_trailing_normal:
  assumes "data_stack vm = u # addr # rest"
  assumes "n = (if u <s 0 then 0 else unat u)"
  assumes "resolve_span (memory vm) (unat addr) n = (s, True)"
  shows "data_stack (forth_minus_trailing vm) =
         word_of_nat (trim_trailing (memory vm) s n) # word_of_nat s # rest"
  using assms by (simp add: forth_minus_trailing_def Let_def)

lemma trim_trailing_no_trailing_space:
  assumes "n = 0 \<or> (mem_read mem (s + (n - 1)) AND 0xFF) \<noteq> 32"
  shows "trim_trailing mem s n = n"
  using assms by (cases n) auto

(* ── SCAN ( addr u char -- addr' u' ) : find first occurrence ─────────── *)
(* C: u<0 -> CLAMPED to 0. Returns (end, 0) if not found. *)

fun scan_for :: "(nat \<Rightarrow> cell) \<Rightarrow> nat \<Rightarrow> cell \<Rightarrow> nat \<Rightarrow> nat" where
  "scan_for mem s needle 0 = 0"
| "scan_for mem s needle (Suc k) =
     (if (mem_read mem s AND 0xFF) = needle then 0 else 1 + scan_for mem (s + 1) needle k)"

definition forth_scan :: "vm_state \<Rightarrow> vm_state" where
  "forth_scan vm =
    (case data_stack vm of
       ch # u # addr # rest \<Rightarrow>
         let n = (if u <s 0 then 0 else unat u);
             (s, ok) = resolve_span (memory vm) (unat addr) n
         in if \<not> ok then set_error (vm\<lparr>data_stack := rest\<rparr>)
            else let i = scan_for (memory vm) s (ch AND 0xFF) n
                 in vm\<lparr>data_stack := word_of_nat (n - i) # word_of_nat (s + i) # rest\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma scan_underflow:
  assumes "data_stack vm = [] \<or> (\<exists>x. data_stack vm = [x])"
  shows "vm_error (forth_scan vm)"
  using assms by (auto simp: forth_scan_def set_error_def)

lemma scan_not_found_returns_end:
  assumes "data_stack vm = ch # u # addr # rest"
  assumes "n = (if u <s 0 then 0 else unat u)"
  assumes "resolve_span (memory vm) (unat addr) n = (s, True)"
  assumes "scan_for (memory vm) s (ch AND 0xFF) n = n"
  shows "data_stack (forth_scan vm) = 0 # word_of_nat (s + n) # rest"
  using assms by (simp add: forth_scan_def Let_def)

(* ── SKIP ( addr u char -- addr' u' ) : skip leading occurrences ──────── *)

fun skip_while_eq :: "(nat \<Rightarrow> cell) \<Rightarrow> nat \<Rightarrow> cell \<Rightarrow> nat \<Rightarrow> nat" where
  "skip_while_eq mem s needle 0 = 0"
| "skip_while_eq mem s needle (Suc k) =
     (if (mem_read mem s AND 0xFF) = needle then 1 + skip_while_eq mem (s + 1) needle k else 0)"

definition forth_skip :: "vm_state \<Rightarrow> vm_state" where
  "forth_skip vm =
    (case data_stack vm of
       ch # u # addr # rest \<Rightarrow>
         let n = (if u <s 0 then 0 else unat u);
             (s, ok) = resolve_span (memory vm) (unat addr) n
         in if \<not> ok then set_error (vm\<lparr>data_stack := rest\<rparr>)
            else let i = skip_while_eq (memory vm) s (ch AND 0xFF) n
                 in vm\<lparr>data_stack := word_of_nat (n - i) # word_of_nat (s + i) # rest\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma skip_underflow:
  assumes "data_stack vm = [] \<or> (\<exists>x. data_stack vm = [x])"
  shows "vm_error (forth_skip vm)"
  using assms by (auto simp: forth_skip_def set_error_def)

lemma skip_none_matching_is_noop_shape:
  assumes "data_stack vm = ch # u # addr # rest"
  assumes "\<not> u <s 0"
  assumes "resolve_span (memory vm) (unat addr) (unat u) = (s, True)"
  assumes "unat u = 0 \<or> (mem_read (memory vm) s AND 0xFF) \<noteq> ch AND 0xFF"
  shows "data_stack (forth_skip vm) = word_of_nat (unat u) # word_of_nat s # rest"
  using assms by (cases "unat u") (auto simp: forth_skip_def Let_def)

(* ── COMPARE ( addr1 u1 addr2 u2 -- n ) : lexicographic compare ──────── *)
(* C: u1<0/u2<0 -> CLAMPED to 0, not errors. *)

fun bytes_compare :: "(nat \<Rightarrow> cell) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> int" where
  "bytes_compare mem s1 s2 0 = 0"
| "bytes_compare mem s1 s2 (Suc k) =
     (let c1 = mem_read mem s1 AND 0xFF; c2 = mem_read mem s2 AND 0xFF
      in if c1 \<noteq> c2 then (if c1 < c2 then -1 else 1)
         else bytes_compare mem (s1 + 1) (s2 + 1) k)"

definition forth_compare :: "vm_state \<Rightarrow> vm_state" where
  "forth_compare vm =
    (case data_stack vm of
       u2 # addr2 # u1 # addr1 # rest \<Rightarrow>
         let n1 = (if u1 <s 0 then 0 else unat u1);
             n2 = (if u2 <s 0 then 0 else unat u2);
             (s1, ok1) = resolve_span (memory vm) (unat addr1) n1;
             (s2, ok2) = resolve_span (memory vm) (unat addr2) n2
         in if \<not> ok1 \<or> \<not> ok2 then set_error (vm\<lparr>data_stack := rest\<rparr>)
            else let m = min n1 n2;
                     cmp0 = bytes_compare (memory vm) s1 s2 m;
                     cmp = (if cmp0 \<noteq> 0 then cmp0
                            else if n1 < n2 then -1 else if n1 > n2 then 1 else 0)
                 in vm\<lparr>data_stack := word_of_int cmp # rest\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma compare_underflow:
  assumes "length (data_stack vm) < 4"
  shows "vm_error (forth_compare vm)"
proof (cases "data_stack vm")
  case Nil then show ?thesis using assms by (simp add: forth_compare_def set_error_def)
next
  case (Cons x xs) then show ?thesis using assms
    by (cases xs rule: list.exhaust; cases "tl xs" rule: list.exhaust)
       (auto simp: forth_compare_def set_error_def)
qed

lemma compare_equal_strings:
  assumes "data_stack vm = u2 # addr2 # u1 # addr1 # rest"
  assumes "n = (if u1 <s 0 then 0 else unat u1)"
  assumes "n = (if u2 <s 0 then 0 else unat u2)"
  assumes "resolve_span (memory vm) (unat addr1) n = (s, True)"
  assumes "resolve_span (memory vm) (unat addr2) n = (s, True)"
  shows "data_stack (forth_compare vm) = 0 # rest"
proof -
  have "bytes_compare (memory vm) s s n = 0"
    by (induction n arbitrary: s) simp_all
  then show ?thesis using assms by (simp add: forth_compare_def Let_def)
qed

(* ── SEARCH ( addr1 u1 addr2 u2 -- addr3 u3 flag ) ────────────────────────
   Find the first occurrence of s2 (the "needle") inside s1 (the
   "haystack"). Same pop order, clamping, and resolve_span auto-detect as
   COMPARE. Two special cases precede the general search, exactly mirroring
   the C's early returns: empty needle (n2=0) matches at the start; a
   needle longer than the haystack (n2>n1) can never match. Otherwise a
   naive first-occurrence search tries every start offset i in [0, n1-n2].

   This was deferred from the previous pass specifically because it needed
   a bounded search helper beyond the single-pass scan/skip/compare
   helpers already available -- `bytes_eq` (exact n-byte match at two
   offsets) and `search_from` (try offset 0, then 1, ... up to a budget,
   returning the first match or None) below are that helper, built the
   same way `bytes_compare` was for COMPARE. *)

fun bytes_eq :: "(nat \<Rightarrow> cell) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
  "bytes_eq mem s1 s2 0 = True"
| "bytes_eq mem s1 s2 (Suc k) =
     ((mem_read mem s1 AND 0xFF) = (mem_read mem s2 AND 0xFF) \<and> bytes_eq mem (s1 + 1) (s2 + 1) k)"

lemma bytes_eq_reflexive:
  "bytes_eq mem s s n"
  by (induction n arbitrary: s) simp_all

(* search_from mem s1 s2 n2 budget: try matching the n2-byte needle at s2
   against the haystack starting at offsets s1, s1+1, ..., s1+budget (in
   that order -- "first occurrence"). Some i = matched at offset i from
   s1; None = no match in [0,budget]. Mirrors the C loop
   "for (i=0; i<=limit; i++)" with budget=limit=n1-n2. *)
fun search_from :: "(nat \<Rightarrow> cell) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat option" where
  "search_from mem s1 s2 n2 0 = (if bytes_eq mem s1 s2 n2 then Some 0 else None)"
| "search_from mem s1 s2 n2 (Suc budget) =
     (if bytes_eq mem s1 s2 n2 then Some 0
      else map_option Suc (search_from mem (s1 + 1) s2 n2 budget))"

definition forth_search :: "vm_state \<Rightarrow> vm_state" where
  "forth_search vm =
    (case data_stack vm of
       u2 # addr2 # u1 # addr1 # rest \<Rightarrow>
         let n1 = (if u1 <s 0 then 0 else unat u1);
             n2 = (if u2 <s 0 then 0 else unat u2);
             (s1, ok1) = resolve_span (memory vm) (unat addr1) n1;
             (s2, ok2) = resolve_span (memory vm) (unat addr2) n2
         in if \<not> ok1 \<or> \<not> ok2 then set_error (vm\<lparr>data_stack := rest\<rparr>)
            else if n2 = 0
            then vm\<lparr>data_stack := forth_true # word_of_nat n1 # word_of_nat s1 # rest\<rparr>
            else if n2 > n1
            then vm\<lparr>data_stack := forth_false # word_of_nat n1 # word_of_nat s1 # rest\<rparr>
            else (case search_from (memory vm) s1 s2 n2 (n1 - n2) of
                    Some i \<Rightarrow> vm\<lparr>data_stack := forth_true # word_of_nat (n1 - i) # word_of_nat (s1 + i) # rest\<rparr>
                  | None   \<Rightarrow> vm\<lparr>data_stack := forth_false # word_of_nat n1 # word_of_nat s1 # rest\<rparr>)
     | _ \<Rightarrow> set_error vm)"

lemma search_underflow:
  assumes "length (data_stack vm) < 4"
  shows "vm_error (forth_search vm)"
proof (cases "data_stack vm")
  case Nil then show ?thesis using assms by (simp add: forth_search_def set_error_def)
next
  case (Cons x xs) then show ?thesis using assms
    by (cases xs rule: list.exhaust; cases "tl xs" rule: list.exhaust)
       (auto simp: forth_search_def set_error_def)
qed

lemma search_empty_needle_found_at_start:
  assumes "data_stack vm = u2 # addr2 # u1 # addr1 # rest"
  assumes "n1 = (if u1 <s 0 then 0 else unat u1)"
  assumes "u2 = 0"
  assumes "resolve_span (memory vm) (unat addr1) n1 = (s1, True)"
  assumes "resolve_span (memory vm) (unat addr2) 0 = (s2, True)"
  shows "data_stack (forth_search vm) = forth_true # word_of_nat n1 # word_of_nat s1 # rest"
  using assms by (simp add: forth_search_def Let_def)

lemma search_needle_longer_than_haystack_not_found:
  assumes "data_stack vm = u2 # addr2 # u1 # addr1 # rest"
  assumes "n1 = (if u1 <s 0 then 0 else unat u1)"
  assumes "n2 = (if u2 <s 0 then 0 else unat u2)"
  assumes "n2 > n1"
  assumes "resolve_span (memory vm) (unat addr1) n1 = (s1, True)"
  assumes "resolve_span (memory vm) (unat addr2) n2 = (s2, True)"
  shows "data_stack (forth_search vm) = forth_false # word_of_nat n1 # word_of_nat s1 # rest"
  using assms by (simp add: forth_search_def Let_def)

lemma search_found:
  assumes "data_stack vm = u2 # addr2 # u1 # addr1 # rest"
  assumes "n1 = (if u1 <s 0 then 0 else unat u1)"
  assumes "n2 = (if u2 <s 0 then 0 else unat u2)"
  assumes "n2 \<noteq> 0" "\<not> n2 > n1"
  assumes "resolve_span (memory vm) (unat addr1) n1 = (s1, True)"
  assumes "resolve_span (memory vm) (unat addr2) n2 = (s2, True)"
  assumes "search_from (memory vm) s1 s2 n2 (n1 - n2) = Some i"
  shows "data_stack (forth_search vm) =
         forth_true # word_of_nat (n1 - i) # word_of_nat (s1 + i) # rest"
  using assms by (simp add: forth_search_def Let_def)

lemma search_not_found:
  assumes "data_stack vm = u2 # addr2 # u1 # addr1 # rest"
  assumes "n1 = (if u1 <s 0 then 0 else unat u1)"
  assumes "n2 = (if u2 <s 0 then 0 else unat u2)"
  assumes "n2 \<noteq> 0" "\<not> n2 > n1"
  assumes "resolve_span (memory vm) (unat addr1) n1 = (s1, True)"
  assumes "resolve_span (memory vm) (unat addr2) n2 = (s2, True)"
  assumes "search_from (memory vm) s1 s2 n2 (n1 - n2) = None"
  shows "data_stack (forth_search vm) = forth_false # word_of_nat n1 # word_of_nat s1 # rest"
  using assms by (simp add: forth_search_def Let_def)

(* Needle found at the very start of the search window (i=0) whenever the
   first n2 bytes already match -- sanity-checks search_from against the
   simpler bytes_eq building block. *)
lemma search_found_at_offset_zero:
  assumes "bytes_eq mem s1 s2 n2"
  shows "search_from mem s1 s2 n2 budget = Some 0"
  using assms by (cases budget) simp_all

(* Searching a haystack for itself (n1=n2, s1=s2) always succeeds at i=0. *)
lemma search_self_match:
  "search_from mem s s n 0 = Some 0"
  by (simp add: bytes_eq_reflexive)

end