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

proof/: add StarForth_Dictionary_Manipulation_Words.thy ([/]/STATE/SMUDGE/HIDDEN/INTERPRET)

Browse Source 
Covers the mode/flag half of dictionary_manipulation_words.c that's provable
against the existing vm_mode/dictionary/latest_id model. The raw-pointer
DictEntry navigation half (>BODY/>NAME/NAME>/>LINK/LINK>/CFA/LFA/NFA/PFA/
TRAVERSE/FIND/') is left unmodelled -- same class of gap as control_words.c's
deferred vm_ip/return-stack-as-raw-pointers issue, since the abstract
dict_entry record is word_id-indexed, not addressed, and has no counterpart
for struct-relative pointer arithmetic (name_len, link, body offset).

Genuine findings recorded in comments, not fixed:
- [, ], STATE, and INTERPRET all read/write a file-scope `static cell_t
  state_variable` -- NOT vm->state_var, the real per-VM STATE field used
  everywhere else in the interpreter. In the Tripod multi-VM fleet this
  static is shared across every VM instance, not per-VM.
- dictionary_m_word_hidden's dead #else branch (unreachable since
  WORD_HIDDEN is always defined) calls a function that doesn't exist
  (dictionary_word_smudge vs. the real static dictionary_m_word_smudge).

27 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 19:33:42 -04:00
co-authored by Claude Sonnet 5
parent 92474c5219
commit 77d8f0606a
2 changed files with 235 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
proof/ROOT
+1
View File
@@ -11,6 +11,7 @@ session "StarForth" = "HOL-Library" +
StarForth_Return_Stack_Words
StarForth_Memory_Words
StarForth_Dictionary_Words
StarForth_Dictionary_Manipulation_Words
StarForth_Mutex
StarForth_Transition
StarForth_Loop1_Heat
proof/StarForth_Dictionary_Manipulation_Words.thy
+234
View File
@@ -0,0 +1,234 @@
theory StarForth_Dictionary_Manipulation_Words
imports StarForth_Base
begin
(* =========================================================================
POST-07: Dictionary Manipulation Words
Mirrors: src/word_source/dictionary_manipulation_words.c
This file splits sharply into two classes:
1. Mode/flag words ([, ], SMUDGE, HIDDEN, INTERPRET) -- provable against
the existing vm_mode / dictionary / latest_id fields.
2. Raw-pointer dictionary-navigation words (>BODY, >NAME, NAME>, >LINK,
LINK>, CFA, LFA, NFA, PFA, TRAVERSE, FIND, ') -- NOT modelled. Every
one of these casts a cell_t directly to/from a C `DictEntry*` and
walks struct fields (name_len, link, the byte after the header) that
have no counterpart in the abstract `dict_entry` record (StarForth_
Base.thy:293), which is indexed abstractly by word_id, not by a raw
memory address at all. This is the same class of gap already flagged
for control_words.c's vm_ip/return-stack-as-raw-pointers (see that
file's resume-point note) -- formalizing it would mean re-deriving
the C struct layout (header size, name_len byte, link pointer
arithmetic, body alignment) as a second, address-based dictionary
model living alongside the existing word_id-based one. Out of scope
for this pass; flagged per-word below as documented gaps, not lemmas.
Per CLAUDE.md: `dictionary_m_word_find` (registered as "FIND") is the
real, tested, non-standard FIND word ("parses from input stream").
This file only *reads* it for modelling purposes here -- consistent
with "never modify FIND", since nothing in proof/ touches the C
source.
── Genuine findings, not fixed ──────────────────────────────────────────
1. `[`, `]`, `STATE`, and `INTERPRET` all read/write a `static cell_t
state_variable` at FILE SCOPE (line 49) -- NOT `vm->state_var`
(include/vm.h:431, the real per-VM STATE field actively used by
vm.c/vm_core.c/vm_bootstrap.c/capsule_loader.c on both hosted and
kernel builds). This static is a single process-wide variable, not
even per-VM: in the Tripod multi-VM fleet, EVERY VM's `[`/`]`/
`INTERPRET` mutates the SAME shared cell, and `STATE` pushes ITS
address (a bare host pointer, not a VM address) -- identical across
every VM instance. `vm->state_var` itself is correctly toggled
elsewhere in the real interpreter loop, so the dictionary-space
compile/interpret bookkeeping isn't broken, but these four FORTH
words are effectively wired to a dead, cross-VM-shared shadow
variable instead of the VM's own state. Modelled below using only
`vm_mode` (which `[`/`]` DO correctly set) -- the dead static write
has no vm_state counterpart and is simply omitted, not "fixed".
2. `dictionary_m_word_hidden`'s `#else` fallback branch (taken only if
`WORD_HIDDEN` is undefined -- it is always defined per include/vm.h:
181, so this branch is dead in every build configuration seen) calls
`dictionary_word_smudge`, which does not exist: the real function in
this file is `static void dictionary_m_word_smudge` (note the `_m_`
and `static` -- not externally callable even if the name were right).
Latent compile-time bug, unreachable under current WORD_HIDDEN
always-defined builds. Not modelled (dead branch), not fixed.
======================================================================== *)
(* ── [ ( -- ) : enter interpretation mode ─────────────────────────────── *)
(* C: vm->mode = MODE_INTERPRET; state_variable = 0 (dead static, see above). *)
definition forth_left_bracket :: "vm_state \<Rightarrow> vm_state" where
"forth_left_bracket vm = vm\<lparr>vm_mode := ModeInterpret\<rparr>"
lemma left_bracket_sets_interpret:
"vm_mode (forth_left_bracket vm) = ModeInterpret"
by (simp add: forth_left_bracket_def)
lemma left_bracket_data_stack_unchanged:
"data_stack (forth_left_bracket vm) = data_stack vm"
by (simp add: forth_left_bracket_def)
lemma left_bracket_never_errors:
"vm_error (forth_left_bracket vm) = vm_error vm"
by (simp add: forth_left_bracket_def)
(* ── ] ( -- ) : enter compilation mode ─────────────────────────────────── *)
(* C: vm->mode = MODE_COMPILE; state_variable = -1 (dead static, see above). *)
definition forth_right_bracket :: "vm_state \<Rightarrow> vm_state" where
"forth_right_bracket vm = vm\<lparr>vm_mode := ModeCompile\<rparr>"
lemma right_bracket_sets_compile:
"vm_mode (forth_right_bracket vm) = ModeCompile"
by (simp add: forth_right_bracket_def)
lemma right_bracket_data_stack_unchanged:
"data_stack (forth_right_bracket vm) = data_stack vm"
by (simp add: forth_right_bracket_def)
lemma right_bracket_never_errors:
"vm_error (forth_right_bracket vm) = vm_error vm"
by (simp add: forth_right_bracket_def)
(* ── [ then ] / ] then [ : mode is exactly what was set last ─────────────── *)
lemma bracket_right_then_left:
"vm_mode (forth_left_bracket (forth_right_bracket vm)) = ModeInterpret"
by (simp add: forth_left_bracket_def)
lemma bracket_left_then_right:
"vm_mode (forth_right_bracket (forth_left_bracket vm)) = ModeCompile"
by (simp add: forth_right_bracket_def)
(* ── STATE ( -- addr ) -- NOT MODELLED ────────────────────────────────── *)
lemma state_not_modelled: True
\<comment> \<open>STATE pushes `(cell_t)(uintptr_t)&state_variable` -- the address of a
bare host C static, not a VM address and not `vm->state_addr`/
`vm->state_var` (which DO exist in the abstract model and ARE the real
per-VM state, see the file-level finding above). There is nothing in
vm_state for this word to legitimately push; modelling it would mean
inventing a fake address for a variable outside the VM's own address
space entirely. Left undocumented as a lemma, gap only.\<close>
by simp
(* ── SMUDGE ( -- ) : compile-only guard, empty body ──────────────────────── *)
(* C: error unless vm->mode == MODE_COMPILE; the "existing body that toggles
the smudge bit" is literally absent (comment placeholder only, no code).
So the word's entire effect, when it doesn't error, is: nothing. *)
definition forth_smudge :: "vm_state \<Rightarrow> vm_state" where
"forth_smudge vm = (if vm_mode vm \<noteq> ModeCompile then set_error vm else vm)"
lemma smudge_requires_compile_mode:
assumes "vm_mode vm \<noteq> ModeCompile"
shows "vm_error (forth_smudge vm)"
by (simp add: forth_smudge_def set_error_def assms)
lemma smudge_in_compile_mode_is_noop:
assumes "vm_mode vm = ModeCompile"
shows "forth_smudge vm = vm"
by (simp add: forth_smudge_def assms)
(* ── HIDDEN ( -- ) : set WORD_HIDDEN (0x40) on the latest word ──────────── *)
(* C: error unless vm->mode == MODE_COMPILE; error if vm->latest is NULL;
else e->flags |= WORD_HIDDEN (the #else dead-branch, see file note #2,
is unreachable and not modelled). *)
definition WORD_HIDDEN :: nat where "WORD_HIDDEN = 0x40"
definition forth_hidden :: "vm_state \<Rightarrow> vm_state" where
"forth_hidden vm =
(if vm_mode vm \<noteq> ModeCompile
then set_error vm
else case latest_id vm of
None \<Rightarrow> set_error vm
| Some wid \<Rightarrow>
(case dictionary vm wid of
None \<Rightarrow> set_error vm
| Some e \<Rightarrow>
vm\<lparr>dictionary := (dictionary vm)
(wid := Some (e\<lparr>de_flags := de_flags e OR WORD_HIDDEN\<rparr>))\<rparr>))"
lemma hidden_requires_compile_mode:
assumes "vm_mode vm \<noteq> ModeCompile"
shows "vm_error (forth_hidden vm)"
by (simp add: forth_hidden_def set_error_def assms)
lemma hidden_requires_latest:
assumes "vm_mode vm = ModeCompile"
assumes "latest_id vm = None"
shows "vm_error (forth_hidden vm)"
by (simp add: forth_hidden_def set_error_def assms)
lemma hidden_requires_latest_present_in_dict:
assumes "vm_mode vm = ModeCompile"
assumes "latest_id vm = Some wid"
assumes "dictionary vm wid = None"
shows "vm_error (forth_hidden vm)"
by (simp add: forth_hidden_def set_error_def assms)
lemma hidden_sets_flag:
assumes "vm_mode vm = ModeCompile"
assumes "latest_id vm = Some wid"
assumes "dictionary vm wid = Some e"
shows "\<exists>e'. dictionary (forth_hidden vm) wid = Some e' \<and>
de_flags e' = de_flags e OR WORD_HIDDEN"
using assms by (simp add: forth_hidden_def)
lemma hidden_data_stack_unchanged:
"data_stack (forth_hidden vm) = data_stack vm"
by (auto simp: forth_hidden_def set_error_def split: option.split)
(* ── INTERPRET ( -- ) ──────────────────────────────────────────────────── *)
(* C: vm->mode = MODE_INTERPRET; state_variable = 0 (dead static, see file
note). Comment in the C source admits the word does not itself invoke
the interpreter loop ("This word exists mainly for completeness and mode
setting") -- so its real effect is identical to `[`. *)
definition forth_interpret :: "vm_state \<Rightarrow> vm_state" where
"forth_interpret = forth_left_bracket"
lemma interpret_is_left_bracket:
"forth_interpret vm = forth_left_bracket vm"
by (simp add: forth_interpret_def)
lemma interpret_sets_interpret_mode:
"vm_mode (forth_interpret vm) = ModeInterpret"
by (simp add: forth_interpret_def forth_left_bracket_def)
(* ── Raw-pointer dictionary navigation -- NOT MODELLED ────────────────────
See the file-level note at the top: >BODY, >NAME, NAME>, >LINK, LINK>,
CFA, LFA, NFA, PFA, TRAVERSE, FIND, ' all cast cell_t <-> DictEntry* and
walk struct-layout details (name_len, link, header-relative body offset)
absent from the word_id-indexed abstract dict_entry model. Each gets a
named sentinel lemma so the gap is greppable per word, matching the
SP@/SP! convention in StarForth_Dictionary_Words.thy. *)
lemma to_body_not_modelled: True \<comment> \<open>>BODY: xt -> DictEntry* -> data field addr (struct-relative pointer arithmetic).\<close>
by simp
lemma to_name_not_modelled: True \<comment> \<open>>NAME: xt -> DictEntry* -> &entry->name (struct field address).\<close>
by simp
lemma name_to_not_modelled: True \<comment> \<open>NAME>: linear scan of vm->latest chain by raw name-field pointer identity.\<close>
by simp
lemma to_link_not_modelled: True \<comment> \<open>>LINK (= LFA): addr -> DictEntry* -> &entry->link (struct field address).\<close>
by simp
lemma link_from_not_modelled: True \<comment> \<open>LINK>: dereferences a DictEntry** raw pointer.\<close>
by simp
lemma cfa_not_modelled: True \<comment> \<open>CFA: identity cast addr -> DictEntry* -> xt; no abstract counterpart needed but the cast itself is untyped.\<close>
by simp
lemma nfa_not_modelled: True \<comment> \<open>NFA: same struct-field address as >NAME.\<close>
by simp
lemma pfa_not_modelled: True \<comment> \<open>PFA: get_body_address -- header size + name_len + alignment arithmetic.\<close>
by simp
lemma traverse_not_modelled: True \<comment> \<open>TRAVERSE: raw byte-pointer arithmetic over a length-prefixed name field.\<close>
by simp
lemma find_not_modelled: True \<comment> \<open>FIND: parses input stream (vm_parse_word) + vm_find_word lookup, neither modelled anywhere in this suite yet. Per CLAUDE.md this is the real, tested, non-standard FIND -- read-only reference here, the C is untouched.\<close>
by simp
lemma tick_not_modelled: True \<comment> \<open>' (tick): identical parse+lookup dependency as FIND, plus a not-found error path FIND itself doesn't have.\<close>
by simp
end