From fe3169dac92fc54b8e404a3013210d8215e3b609 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Thu, 13 Aug 2026 22:58:18 -0400 Subject: [PATCH] proof/: add StarForth_String_Words.thy (BL/COUNT/CMOVE/CMOVE>/BLANK/-TRAILING/SCAN/SKIP/COMPARE) Covers the 9 self-contained words in string_words.c that operate purely on data_stack/memory with no dependency outside the existing model. Introduces vm_addr_ok_m, a literal transcription of the real C vm_addr_ok bounds check (src/vm.c:815-820) using VM_MEMORY_SIZE -- more precise than the sign-only check earlier memory words used -- and resolve_span, a shared helper for the auto-detect-counted-string pattern that recurs across six of this file's words. 16 words deliberately not modeled, in three groups (full reasoning in the theory header): (a) WORD/SPAN/TIB/>IN/SOURCE/QUERY/EXPECT depend on the lazily-allocated TIB input subsystem (vm->tib_buf via vm_input_ensure), which has no vm_state counterpart; QUERY/EXPECT also call fgets(stdin) directly, real I/O with no HOL formalization; (b) CONVERT/NUMBER/ENCLOSE depend on raw C-string scanning (strlen past a single vm_addr_ok-checked byte -- a genuine unbounded-read hazard, noted not chased) or strtol(); (c) S"/(s")/LITERAL/[LITERAL]/['] depend on the same compile-time/threaded-code machinery already out of scope from control_words.c. SEARCH is deferred despite being self-contained -- its nested substring search needs a bigger proof-engineering lift than the single-pass helpers used here. Third occurrence of the file-scope-static-instead-of-per-VM-field bug pattern noted (WORD's word_scratch_addr), matching control_words.c's cf_stack and dictionary_manipulation_words.c's state_variable -- not fixed, flagged for aggregation when raised to Bob. 29 theory files verify with zero errors. Co-Authored-By: Claude Sonnet 5 --- proof/ROOT | 1 + proof/StarForth_String_Words.thy | 407 +++++++++++++++++++++++++++++++ 2 files changed, 408 insertions(+) create mode 100644 proof/StarForth_String_Words.thy diff --git a/proof/ROOT b/proof/ROOT index 7ae6dd5..71ff2ce 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -13,6 +13,7 @@ session "StarForth" = "HOL-Library" + StarForth_Dictionary_Words StarForth_Dictionary_Manipulation_Words StarForth_Control_Words + StarForth_String_Words StarForth_Mutex StarForth_Transition StarForth_Loop1_Heat diff --git a/proof/StarForth_String_Words.thy b/proof/StarForth_String_Words.thy new file mode 100644 index 0000000..4f62189 --- /dev/null +++ b/proof/StarForth_String_Words.thy @@ -0,0 +1,407 @@ +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 \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 \ nat \ bool" where + "vm_addr_ok_m a n \ n \ VM_MEMORY_SIZE \ a \ 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 \ cell) \ nat \ nat \ (nat \ bool)" where + "resolve_span mem a n = + (if n \ 255 \ vm_addr_ok_m a 1 \ (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 \ vm_state" where + "forth_bl vm = vm\data_stack := 32 # data_stack vm\" + +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 ` vm_state" where + "forth_count vm = + (case data_stack vm of + [] \ set_error vm + | addr1 # rest \ + let a = unat addr1 + in if \ vm_addr_ok_m a 1 + then set_error (vm\data_stack := rest\) + else let count = mem_read (memory vm) a AND 0xFF + in if \ vm_addr_ok_m (a + 1) (unat count) + then set_error (vm\data_stack := rest\) + else vm\data_stack := count # word_of_nat (a + 1) # rest\)" + +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 \ cell) \ nat \ nat \ nat \ (nat \ 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 \ vm_state" where + "forth_cmove vm = + (case data_stack vm of + u # addr2 # addr1 # rest \ + (if u data_stack := rest\) + else if u = 0 then vm\data_stack := rest\ + else let src = unat addr1; dst = unat addr2; n = unat u + in if \ vm_addr_ok_m src n \ \ vm_addr_ok_m dst n + then set_error (vm\data_stack := rest\) + else vm\data_stack := rest, memory := mem_copy_asc (memory vm) src dst n\) + | _ \ 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 u 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 \ cell) \ nat \ nat \ nat \ (nat \ 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 \ vm_state" where + "forth_cmove_greater vm = + (case data_stack vm of + u # addr2 # addr1 # rest \ + (if u data_stack := rest\) + else if u = 0 then vm\data_stack := rest\ + else let src = unat addr1; dst = unat addr2; n = unat u + in if \ vm_addr_ok_m src n \ \ vm_addr_ok_m dst n + then set_error (vm\data_stack := rest\) + else vm\data_stack := rest, memory := mem_copy_desc (memory vm) src dst n\) + | _ \ set_error vm)" + +lemma cmove_greater_normal: + assumes "data_stack vm = u # addr2 # addr1 # rest" + assumes "\ u 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 \ cell) \ nat \ nat \ cell \ (nat \ 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 \ vm_state" where + "forth_blank vm = + (case data_stack vm of + u # addr # rest \ + (if u data_stack := rest\) + else if u = 0 then vm\data_stack := rest\ + else let (s, ok) = resolve_span (memory vm) (unat addr) (unat u) + in if \ ok then set_error (vm\data_stack := rest\) + else vm\data_stack := rest, memory := mem_fill (memory vm) s (unat u) 32\) + | _ \ set_error vm)" + +lemma blank_negative_errors: + assumes "data_stack vm = u # addr # rest" + assumes "u u 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 \ cell) \ nat \ nat \ 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 \ vm_state" where + "forth_minus_trailing vm = + (case data_stack vm of + u # addr # rest \ + let n = (if u ok then set_error (vm\data_stack := rest\) + else vm\data_stack := word_of_nat (trim_trailing (memory vm) s n) # word_of_nat s # rest\ + | _ \ 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 (mem_read mem (s + (n - 1)) AND 0xFF) \ 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 \ cell) \ nat \ cell \ nat \ 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 \ vm_state" where + "forth_scan vm = + (case data_stack vm of + ch # u # addr # rest \ + let n = (if u ok then set_error (vm\data_stack := rest\) + else let i = scan_for (memory vm) s (ch AND 0xFF) n + in vm\data_stack := word_of_nat (n - i) # word_of_nat (s + i) # rest\ + | _ \ set_error vm)" + +lemma scan_underflow: + assumes "data_stack vm = [] \ (\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 cell) \ nat \ cell \ nat \ 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 \ vm_state" where + "forth_skip vm = + (case data_stack vm of + ch # u # addr # rest \ + let n = (if u ok then set_error (vm\data_stack := rest\) + else let i = skip_while_eq (memory vm) s (ch AND 0xFF) n + in vm\data_stack := word_of_nat (n - i) # word_of_nat (s + i) # rest\ + | _ \ set_error vm)" + +lemma skip_underflow: + assumes "data_stack vm = [] \ (\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 "\ u (mem_read (memory vm) s AND 0xFF) \ 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 \ cell) \ nat \ nat \ nat \ 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 \ c2 then (if c1 < c2 then -1 else 1) + else bytes_compare mem (s1 + 1) (s2 + 1) k)" + +definition forth_compare :: "vm_state \ vm_state" where + "forth_compare 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 let m = min n1 n2; + cmp0 = bytes_compare (memory vm) s1 s2 m; + cmp = (if cmp0 \ 0 then cmp0 + else if n1 < n2 then -1 else if n1 > n2 then 1 else 0) + in vm\data_stack := word_of_int cmp # rest\ + | _ \ 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