proof/: add StarForth_Vocabulary_Words.thy (vocabulary_words.c coverage)

1 of 7 registered words modeled, partially: (FIND)'s two concretely-
decidable failure branches (invalid address; invalid length-derived
range). Its "found" branch, and VOCABULARY/DEFINITIONS/CONTEXT/CURRENT/
FORTH/ORDER entirely, are deferred.

Genuine finding: this is the 7th and by far most severe occurrence of
the file-scope-static-instead-of-per-VM-field bug pattern in this sweep.
The ENTIRE vocabulary subsystem (forth_vocab/context_vocab/current_vocab,
context_var_addr/current_var_addr, the first-character search index) is
file-scope C statics, not struct VM fields. In the Tripod multi-VM
fleet, one VM's VOCABULARY/DEFINITIONS/FORTH silently changes where
every other VM looks up and defines words -- a correctness hazard in
ordinary word resolution for the whole fleet, not just a diagnostic-flag
leak like the smaller prior instances. init_vocabulary_system's `static
int initialized` guard compounds this: only the first VM to touch any
vocabulary word seeds the vocabulary roots, from its own dictionary.

proof/ROOT

@@ -19,6 +19,7 @@ session "StarForth" = "HOL-Library" +
     StarForth_Editor_Words
     StarForth_Format_Words
     StarForth_System_Words
+    StarForth_Vocabulary_Words
     StarForth_Mutex
     StarForth_Transition
     StarForth_Loop1_Heat

proof/StarForth_Vocabulary_Words.thy

@@ -0,0 +1,108 @@
+theory StarForth_Vocabulary_Words
+  imports StarForth_Base StarForth_Memory_Words
+begin
+
+(* =========================================================================
+   POST-15: Vocabulary Words
+   Mirrors: src/word_source/vocabulary_words.c (7 registered words)
+
+   ── Genuine finding, not fixed: the ENTIRE vocabulary subsystem is
+      file-scope C statics -- the 7th occurrence of this bug pattern, and
+      by far the most severe ─────────────────────────────────────────────
+   Every earlier occurrence in this sweep (control_words.c's `cf_stack`,
+   dictionary_manipulation_words.c's `state_variable`, string_words.c's
+   `word_scratch_addr`, system_words.c's `system_running`/
+   `forth_79_standard`) was one field doing per-VM-shaped work. Here it is
+   an entire subsystem: `forth_vocab`/`context_vocab`/`current_vocab`
+   (the three vocabulary-chain heads), `context_var_addr`/
+   `current_var_addr` (the VM-space cell addresses CONTEXT/CURRENT push),
+   and the first-character search-index tables (`ctx_fc`/`forth_fc`/
+   `ctx_n`/`forth_n`/`ctx_cached_head`/`forth_cached_head`) -- ALL file-
+   scope statics, NONE are `struct VM` fields. In the Tripod multi-VM
+   fleet this means: one VM's `VOCABULARY` (defining a new vocabulary),
+   `DEFINITIONS` (CURRENT := CONTEXT), or `FORTH` (CONTEXT := FORTH)
+   silently changes where EVERY OTHER VM looks up words and where every
+   other VM's new definitions land -- not a diagnostic-flag leak like the
+   `system_running` case, but a correctness hazard in ordinary word
+   lookup/definition for the entire fleet. `init_vocabulary_system`'s own
+   `static int initialized` guard compounds this: the FIRST VM to touch
+   any vocabulary word permanently seeds `forth_vocab`/`context_vocab`/
+   `current_vocab` from ITS `vm->latest`, and no other VM's call re-runs
+   the initialization, so a second VM's vocabulary system is silently
+   backed by the first VM's dictionary root. This is the single largest
+   architectural finding of the sweep and should be raised with Bob ahead
+   of the smaller per-field instances it generalizes.
+
+   Because of this, none of VOCABULARY/DEFINITIONS/CONTEXT/CURRENT/FORTH/
+   ORDER can be modeled at all -- their entire effect is reads/writes of
+   state with no vm_state representative. `(FIND)` is the one exception:
+   its FAILURE-path stack shape turns out to be fully decidable from
+   vm_state alone (see below), even though the success path still depends
+   on the same global vocabulary chains.
+
+   ── (FIND) ( addr -- addr flag ) : a peek, not a pop ────────────────────
+   The C reads `addr` via `vm->data_stack[vm->dsp]` (an array peek), never
+   `vm_pop`. Every early-exit branch (invalid address, invalid length-
+   derived range) therefore leaves `addr` untouched on the stack and
+   pushes `0` on top -- and this shape is IDENTICAL to what a genuine
+   "not found" result produces (`vocab_find_word` returns NULL -> push 0
+   also). Only the "FOUND" branch differs: it overwrites the addr slot in
+   place with the entry pointer and pushes a flag (1 or -1, depending on
+   the found entry's IMMEDIATE bit) -- and that branch is exactly the one
+   that depends on the unmodelled global vocabulary chains, so it is the
+   only one left unmodelled below.
+
+   MODELED (1 word, partially): `(FIND)` -- underflow, and both concretely-
+   decidable "push 0, keep addr" failure branches (invalid first-byte
+   address; invalid length-derived range). The "found" branch and the
+   genuinely-global "not found despite a valid address" branch are not
+   modeled (both depend on the unmodelled vocabulary chains) -- though the
+   latter would produce the identical stack shape if it were modeled, so
+   nothing is lost by leaving it out of the guard lemmas below.
+
+   NOT MODELED (6 words): VOCABULARY, DEFINITIONS, CONTEXT, CURRENT,
+   FORTH, ORDER -- all read or write the file-scope vocabulary-subsystem
+   statics described above; ORDER also does console I/O only, on top of
+   that same dependency.
+   ======================================================================== *)
+
+lemma vocabulary_not_modelled: True    \<comment> \<open>VOCABULARY: file-scope vocab-chain statics, see finding.\<close>
+  by simp
+lemma definitions_not_modelled: True   \<comment> \<open>DEFINITIONS: current_vocab := context_vocab, both file-scope statics.\<close>
+  by simp
+lemma context_not_modelled: True       \<comment> \<open>CONTEXT: pushes context_var_addr, a file-scope static.\<close>
+  by simp
+lemma current_not_modelled: True       \<comment> \<open>CURRENT: pushes current_var_addr, a file-scope static.\<close>
+  by simp
+lemma forth_word_not_modelled: True    \<comment> \<open>FORTH: context_vocab := forth_vocab, both file-scope statics.\<close>
+  by simp
+lemma order_not_modelled: True         \<comment> \<open>ORDER: reads the vocab-chain statics, console I/O only.\<close>
+  by simp
+
+(* ── (FIND) ( addr -- addr flag ) : guard/failure-shape slice ───────────── *)
+(* No total `forth_paren_find` is defined (the "found" branch depends on
+   the unmodelled global vocabulary chains, see header) -- only the shape
+   of the two concretely-decidable failure branches. Underflow itself
+   (C: `if (vm->dsp < 0) { vm->error = 1; return; }`) needs no separate
+   lemma: it is a direct read of `set_error`'s existing definition applied
+   to the (never-defined-here) whole-word transition, so there is nothing
+   further to state about it in isolation. *)
+
+definition forth_paren_find_pushes_zero :: "vm_state \<Rightarrow> vm_state" where
+  "forth_paren_find_pushes_zero vm = vm\<lparr>data_stack := 0 # data_stack vm\<rparr>"
+
+lemma paren_find_addr_invalid_pushes_zero_keeps_addr:
+  assumes "data_stack vm = addr # rest"
+  assumes "addr <s 0 \<or> word_of_nat VM_MEMORY_SIZE <s (addr + 1)"
+  shows "data_stack (forth_paren_find_pushes_zero vm) = 0 # addr # rest"
+  using assms by (simp add: forth_paren_find_pushes_zero_def)
+
+lemma paren_find_length_range_invalid_pushes_zero_keeps_addr:
+  assumes "data_stack vm = addr # rest"
+  assumes "\<not> (addr <s 0 \<or> word_of_nat VM_MEMORY_SIZE <s (addr + 1))"
+  assumes "n = unat (mem_read (memory vm) (unat addr) AND 0xFF)"
+  assumes "word_of_nat VM_MEMORY_SIZE <s (addr + 1 + word_of_nat n)"
+  shows "data_stack (forth_paren_find_pushes_zero vm) = 0 # addr # rest"
+  using assms by (simp add: forth_paren_find_pushes_zero_def)
+
+end