proof/: add SEARCH to StarForth_String_Words.thy

Closes the one word deferred from the previous pass for being a bigger
proof-engineering lift rather than a hard blocker. Adds bytes_eq (exact
n-byte match at two offsets) and search_from (bounded first-occurrence
search, tries offset 0..budget) as the missing helper, built the same way
bytes_compare was for COMPARE. Covers both C early-return special cases
(empty needle matches at start; needle longer than haystack never matches)
plus the general naive search's found/not-found outcomes.

10 of 25 words in string_words.c now modeled; the remaining 15 are the
TIB/input-subsystem, stdio, and raw-C-string/strtol clusters documented in
the file's header.

29 theory files verify with zero errors.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

proof/StarForth_String_Words.thy

@@ -404,4 +404,123 @@ proof -
   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