admin/LithosAnanake
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

proof/: add StarForth_String_Words.thy (BL/COUNT/CMOVE/CMOVE>/BLANK/-TRAILING/SCAN/SKIP/COMPARE)

Browse Source 
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 <noreply@anthropic.com>
This commit is contained in:
Robert Allan James
2026-08-13 22:58:18 -04:00
co-authored by Claude Sonnet 5
parent b196c95e44
commit fe3169dac9
2 changed files with 408 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
proof/ROOT
+1
View File
@@ -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
proof/StarForth_String_Words.thy
+407
View File
@@ -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 \<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
end