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.
102 lines
5.6 KiB
Plaintext
102 lines
5.6 KiB
Plaintext
theory StarForth_Lifecycle_Words_Hosted
|
|
imports StarForth_Base
|
|
begin
|
|
|
|
(* =========================================================================
|
|
Mirrors: src/word_source/lifecycle_words_hosted.c
|
|
Registers (hosted build only -- see below): BIRTH KILL PAUSE RESUME USE
|
|
|
|
── Build-variant split, opposite of the console-fabric files ──────────
|
|
The ENTIRE file is `#ifndef __STARKERNEL__` -- opposite of framebuffer_
|
|
words.c/keyboard_words.c/scroll_words.c/ttf_words.c, which were kernel-
|
|
only. Per the file's own header comment and CLAUDE.md's Hard Rules
|
|
("BIRTH, RUN, USE are primitives registered in C exactly like DUP...
|
|
Never reach for FIND"), the KERNEL build's BIRTH/KILL/PAUSE/RESUME/USE
|
|
live in `src/starkernel/capsule/lifecycle_words.c` -- a different file
|
|
entirely, in `src/starkernel/` rather than `src/word_source/`, and per
|
|
CLAUDE.md's scope note that tree is real/load-bearing kernel code, not
|
|
this sweep's target (this sweep covers `src/word_source/*.c`, the
|
|
vendored/shared word set). So this theory covers ONLY the hosted
|
|
stand-ins; the real kernel capsule-birth-protocol words are out of
|
|
scope for this file (and for this sweep generally).
|
|
|
|
── All five words are the SAME vm_state transition ─────────────────────
|
|
Each body is: pop u, pop caddr (both via bare `vm_pop`, no upfront `dsp`
|
|
guard -- deferring to `vm_pop`'s own internal underflow check, same
|
|
convention scroll_words.c uses and explains), copy at most 63 bytes from
|
|
`vm->memory[caddr..caddr+u)` into a local buffer (bounds-checked against
|
|
`VM_MEMORY_SIZE`, silently truncated to empty if `caddr` is out of
|
|
range), then `log_message` the extracted name. The five bodies differ
|
|
ONLY in the literal string passed to `log_message` ("BIRTH %s (hosted)"
|
|
vs "KILL %s (hosted)" etc.) -- everything with a vm_state footprint is
|
|
byte-for-byte identical across all five. Modelled ONCE as
|
|
`forth_lifecycle_pop2`, with each word's definition stated as literally
|
|
equal to it.
|
|
|
|
The C does NOT check `vm->error` between the two pops, so on a
|
|
single-element stack the first pop succeeds (consuming it) before the
|
|
second pop discovers the now-empty stack and sets the error -- the same
|
|
partial-pop-then-error shape already seen in physics_pipelining_
|
|
diagnostic_words.c, but here fully mechanised since (unlike that file)
|
|
nothing downstream of the pops needs an unmodelled subsystem: the name
|
|
extraction is a pure, bounds-checked memory READ with no vm_state
|
|
write, and log_message is pure I/O. So this file's entire vm_state
|
|
footprint is exactly captured by the two pops -- no deferred remainder
|
|
at all, the only file in this sweep so far where that's true for every
|
|
registered word. *)
|
|
|
|
definition forth_lifecycle_pop2 :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_lifecycle_pop2 vm =
|
|
(case data_stack vm of
|
|
[] \<Rightarrow> set_error vm
|
|
| [x] \<Rightarrow> set_error (vm\<lparr>data_stack := []\<rparr>)
|
|
| u # caddr # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>)"
|
|
|
|
lemma lifecycle_pop2_underflow_nil:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_lifecycle_pop2 vm)" and "data_stack (forth_lifecycle_pop2 vm) = []"
|
|
by (simp_all add: forth_lifecycle_pop2_def set_error_def assms)
|
|
|
|
lemma lifecycle_pop2_underflow_one:
|
|
\<comment> \<open>Partial pop: the single element IS consumed (it was popped
|
|
successfully as `u`) before the second pop fails.\<close>
|
|
assumes "data_stack vm = [x]"
|
|
shows "vm_error (forth_lifecycle_pop2 vm)" and "data_stack (forth_lifecycle_pop2 vm) = []"
|
|
by (simp_all add: forth_lifecycle_pop2_def set_error_def assms)
|
|
|
|
lemma lifecycle_pop2_normal:
|
|
assumes "data_stack vm = u # caddr # xs"
|
|
shows "data_stack (forth_lifecycle_pop2 vm) = xs"
|
|
and "vm_error (forth_lifecycle_pop2 vm) = vm_error vm"
|
|
by (simp_all add: forth_lifecycle_pop2_def assms)
|
|
|
|
(* ── The five registered words, each literally equal to forth_lifecycle_pop2 ── *)
|
|
|
|
definition forth_birth :: "vm_state \<Rightarrow> vm_state" where "forth_birth = forth_lifecycle_pop2"
|
|
definition forth_kill :: "vm_state \<Rightarrow> vm_state" where "forth_kill = forth_lifecycle_pop2"
|
|
definition forth_pause :: "vm_state \<Rightarrow> vm_state" where "forth_pause = forth_lifecycle_pop2"
|
|
definition forth_resume :: "vm_state \<Rightarrow> vm_state" where "forth_resume = forth_lifecycle_pop2"
|
|
definition forth_use :: "vm_state \<Rightarrow> vm_state" where "forth_use = forth_lifecycle_pop2"
|
|
|
|
lemma birth_is_pop2: "forth_birth vm = forth_lifecycle_pop2 vm" by (simp add: forth_birth_def)
|
|
lemma kill_is_pop2: "forth_kill vm = forth_lifecycle_pop2 vm" by (simp add: forth_kill_def)
|
|
lemma pause_is_pop2: "forth_pause vm = forth_lifecycle_pop2 vm" by (simp add: forth_pause_def)
|
|
lemma resume_is_pop2: "forth_resume vm = forth_lifecycle_pop2 vm" by (simp add: forth_resume_def)
|
|
lemma use_is_pop2: "forth_use vm = forth_lifecycle_pop2 vm" by (simp add: forth_use_def)
|
|
|
|
lemma lifecycle_words_preserve_dictionary:
|
|
"dictionary (forth_lifecycle_pop2 vm) = dictionary vm"
|
|
by (auto simp: forth_lifecycle_pop2_def set_error_def split: list.split)
|
|
|
|
lemma lifecycle_words_preserve_memory:
|
|
"memory (forth_lifecycle_pop2 vm) = memory vm"
|
|
by (auto simp: forth_lifecycle_pop2_def set_error_def split: list.split)
|
|
|
|
lemma lifecycle_name_extraction_and_log_not_modelled: True
|
|
\<comment> \<open>extract_name's memcpy-from-vm-memory is a pure read (no vm_state
|
|
write) and log_message is pure I/O -- neither has any vm_state effect
|
|
to characterise beyond what forth_lifecycle_pop2 already captures.\<close>
|
|
by simp
|
|
|
|
end
|