diff --git a/proof/ROOT b/proof/ROOT index 57969f8..d2859b1 100644 --- a/proof/ROOT +++ b/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 diff --git a/proof/StarForth_Vocabulary_Words.thy b/proof/StarForth_Vocabulary_Words.thy new file mode 100644 index 0000000..f1ce961 --- /dev/null +++ b/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 \ \VOCABULARY: file-scope vocab-chain statics, see finding.\ + by simp +lemma definitions_not_modelled: True \ \DEFINITIONS: current_vocab := context_vocab, both file-scope statics.\ + by simp +lemma context_not_modelled: True \ \CONTEXT: pushes context_var_addr, a file-scope static.\ + by simp +lemma current_not_modelled: True \ \CURRENT: pushes current_var_addr, a file-scope static.\ + by simp +lemma forth_word_not_modelled: True \ \FORTH: context_vocab := forth_vocab, both file-scope statics.\ + by simp +lemma order_not_modelled: True \ \ORDER: reads the vocab-chain statics, console I/O only.\ + 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 \ vm_state" where + "forth_paren_find_pushes_zero vm = vm\data_stack := 0 # data_stack vm\" + +lemma paren_find_addr_invalid_pushes_zero_keeps_addr: + assumes "data_stack vm = addr # rest" + assumes "addr word_of_nat VM_MEMORY_SIZE (addr word_of_nat VM_MEMORY_SIZE