Robert Allan James
eb46da65f5
StarForth_Lifecycle_Words_Hosted.thy: BIRTH/KILL/PAUSE/RESUME/USE are all the SAME vm_state transition (pop u, pop caddr, log -- the C's own "kernel build skips this file via Makefile glob" framing means this covers only the hosted stand-ins; the real kernel capsule-birth-protocol words live in src/starkernel/, out of this sweep's scope). First file in the sweep where every registered word's full vm_state footprint is captured with no deferred remainder -- name extraction is a pure memory read, logging is pure I/O. Models the genuine partial-pop-before-error case (C doesn't check vm->error between its two vm_pop calls). StarForth_Defer_Words.thy: another duplicate-registration finding, same class as defining_words.c vs dictionary_manipulation_words.c's [/]/STATE -- word_registry.c registers this file's DEFER/IS/DEFER@ (Module 27) AFTER defining_words.c's (Module 17), unconditionally in BOTH builds (defer_words.c has no __STARKERNEL__ guard despite CLAUDE.md's "kernel- only addition" framing; the hosted Makefile's SRC wildcard includes it regardless). This makes StarForth_Defining_Words.thy's DEFER/IS/DEFER@ sentinels describe dead, shadowed code -- corrected in place with cross-references. The live version hits the same three model gaps anyway (dictionary-entry creation, data-field addressing, mutable per-entry dispatch), so only IS's stack-underflow guard is new. StarForth_Log_Words.thy: the five level-constant pushes, LOG-LEVEL!'s guard+clamp, and all five LOG-*-STR words fully modelled (the STR words share lifecycle_words_hosted.c's "pop2 + bounds-check, no vm_state write" shape). LOG-LEVEL@, the (do-log-N) runtime words (raw threaded-code pointer, same class as LIT), and the LOG-*" immediates (TIB + compile- time dependencies) deferred. Finding: LOG-ERROR..DEBUG and LOG-LEVEL@ push with no overflow guard -- more instances of the pattern first found at DECAY-RATE@. Suite now 51 theories, green.
77 lines
4.2 KiB
Plaintext
77 lines
4.2 KiB
Plaintext
theory StarForth_Defer_Words
|
|
imports StarForth_Base
|
|
begin
|
|
|
|
(* =========================================================================
|
|
Mirrors: src/word_source/defer_words.c
|
|
Registers: DEFER IS DEFER@
|
|
|
|
── Duplicate-registration finding, same class as `[`/`]`/STATE ─────────
|
|
`word_registry.c` registers `defining_words.c`'s DEFER/IS/DEFER@ at
|
|
Module 17 (line 126) and THIS file's DEFER/IS/DEFER@ at Module 27
|
|
(line 137) -- unconditionally, with no `#ifdef __STARKERNEL__` guarding
|
|
either call. Despite CLAUDE.md categorising `defer_words.c` as a
|
|
"kernel-side-only addition," the hosted `Makefile`'s `SRC` is a bare
|
|
`wildcard src/word_source/*.c` (line 443) with no exclusion for this
|
|
file, and `defer_words.c` itself has no `#ifndef __STARKERNEL__` guard
|
|
the way `lifecycle_words_hosted.c` does -- so it compiles and registers
|
|
in BOTH builds. Registered later, this file's DEFER/IS/DEFER@ SHADOW
|
|
`defining_words.c`'s and are the only reachable versions in either
|
|
build. **This corrects StarForth_Defining_Words.thy's
|
|
`defer_not_modelled`/`is_not_modelled`/`defer_fetch_not_modelled`
|
|
sentinels: those describe dead, shadowed code, not the live
|
|
implementation.** (Those sentinels are still accurate as descriptions
|
|
of what that dead code WOULD do, and the underlying model gaps this
|
|
file hits below are the same ones anyway, so nothing there needs to be
|
|
retracted -- just understood as describing unreachable code.)
|
|
|
|
── Why this file isn't more tractable despite being the live version ──
|
|
Every one of DEFER/IS/DEFER@'s real effects still hits the same three
|
|
gaps StarForth_Defining_Words.thy's file header names: (a) dictionary-
|
|
entry creation (`vm_create_word`, used by DEFER), (b) data-field
|
|
addressing (`vm_dictionary_get_data_field` -- DEFER's initial zero-set,
|
|
IS's xt store, DEFER@'s xt fetch, and `defer_runtime`'s own read all
|
|
depend on it), (c) mutable per-entry dispatch (`defer_runtime` reads a
|
|
`DictEntry*` out of the DF cell and calls through it -- `word_table` is
|
|
a fixed global in this suite's model, see StarForth_Base.thy). IS and
|
|
DEFER@ additionally depend on `vm_find_word` (the FIND-family name-
|
|
resolution gap) and a raw `de->func != defer_runtime` function-pointer
|
|
identity comparison, itself unmodellable since `word_table` doesn't
|
|
expose per-entry function identity as a queryable value in this model.
|
|
|
|
── Scope ─────────────────────────────────────────────────────────────
|
|
Only IS's stack-underflow guard is modelled (the one real vm_state
|
|
condition that doesn't depend on any of the above). Everything else in
|
|
all three words is not modelled.
|
|
======================================================================== *)
|
|
|
|
(* ── IS ( xt -- ) : underflow guard only ──────────────────────────────── *)
|
|
(* C: `if (vm->dsp < 0) { ...; vm->error = 1; return; }` before popping xt
|
|
-- i.e. needs at least one element. Everything after the pop (name
|
|
parse, FIND, defer_runtime identity check, DF store) is unmodelled. *)
|
|
|
|
definition forth_is_guard :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_is_guard vm =
|
|
(if data_stack vm = [] then set_error vm else vm)"
|
|
|
|
lemma is_underflow:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_is_guard vm)"
|
|
by (simp add: forth_is_guard_def set_error_def assms)
|
|
|
|
lemma is_guard_rest_not_modelled: True
|
|
\<comment> \<open>Beyond the underflow guard: name parse (unmodelled TIB dependency),
|
|
vm_find_word (FIND-family gap), the `func != defer_runtime` identity
|
|
check (unmodellable -- word_table has no per-entry function-identity
|
|
query in this model), and the DF store (gap b). See file header.\<close>
|
|
by simp
|
|
|
|
lemma defer_not_modelled: True \<comment> \<open>DEFER: vm_create_word (gap a) + DF zero-init (gap b).\<close>
|
|
by simp
|
|
lemma defer_runtime_not_modelled: True \<comment> \<open>defer_runtime: DF read (gap b) + call-through (gap c).\<close>
|
|
by simp
|
|
lemma defer_fetch_not_modelled: True \<comment> \<open>DEFER@: FIND (name-resolution gap) + DF read (gap b).\<close>
|
|
by simp
|
|
|
|
end
|