From a1d24fdb6f1ae5bcab3f5e85568b9e6c991f5e5d Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Thu, 13 Aug 2026 23:05:48 -0400 Subject: [PATCH] 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 --- proof/StarForth_String_Words.thy | 119 +++++++++++++++++++++++++++++++ 1 file changed, 119 insertions(+) diff --git a/proof/StarForth_String_Words.thy b/proof/StarForth_String_Words.thy index 4f62189..45b7f2c 100644 --- a/proof/StarForth_String_Words.thy +++ b/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 \ cell) \ nat \ nat \ nat \ 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) \ 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 \ cell) \ nat \ nat \ nat \ nat \ 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 \ vm_state" where + "forth_search vm = + (case data_stack vm of + u2 # addr2 # u1 # addr1 # rest \ + let n1 = (if u1 ok1 \ \ ok2 then set_error (vm\data_stack := rest\) + else if n2 = 0 + then vm\data_stack := forth_true # word_of_nat n1 # word_of_nat s1 # rest\ + else if n2 > n1 + then vm\data_stack := forth_false # word_of_nat n1 # word_of_nat s1 # rest\ + else (case search_from (memory vm) s1 s2 n2 (n1 - n2) of + Some i \ vm\data_stack := forth_true # word_of_nat (n1 - i) # word_of_nat (s1 + i) # rest\ + | None \ vm\data_stack := forth_false # word_of_nat n1 # word_of_nat s1 # rest\) + | _ \ 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 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 0" "\ 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 0" "\ 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