diff --git a/proof/ROOT b/proof/ROOT index 8c5c0ae..1d2de23 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -33,6 +33,9 @@ session "StarForth" = "HOL-Library" + StarForth_Keyboard_Words StarForth_Scroll_Words StarForth_TTF_Words + StarForth_Lifecycle_Words_Hosted + StarForth_Defer_Words + StarForth_Log_Words StarForth_Loop1_Heat StarForth_Loop2_Window StarForth_Loop3_Decay diff --git a/proof/StarForth_Defer_Words.thy b/proof/StarForth_Defer_Words.thy new file mode 100644 index 0000000..727b484 --- /dev/null +++ b/proof/StarForth_Defer_Words.thy @@ -0,0 +1,76 @@ +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 \ 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 + \ \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.\ + by simp + +lemma defer_not_modelled: True \ \DEFER: vm_create_word (gap a) + DF zero-init (gap b).\ + by simp +lemma defer_runtime_not_modelled: True \ \defer_runtime: DF read (gap b) + call-through (gap c).\ + by simp +lemma defer_fetch_not_modelled: True \ \DEFER@: FIND (name-resolution gap) + DF read (gap b).\ + by simp + +end diff --git a/proof/StarForth_Defining_Words.thy b/proof/StarForth_Defining_Words.thy index f35db03..ee1b3b7 100644 --- a/proof/StarForth_Defining_Words.thy +++ b/proof/StarForth_Defining_Words.thy @@ -324,13 +324,13 @@ lemma bracket_compile_not_modelled: True \ \[COMPILE]: identical by simp lemma forget_not_modelled: True \ \FORGET: walks vm->latest's raw linked chain by name, frees C structs, and rewinds `here` from a DF read (gap a/b combined) -- categorically the same class of gap as `block_words.c`'s cache-subsystem deferrals: a whole-subsystem project, not a one-word extension.\ by simp -lemma defer_not_modelled: True \ \DEFER: vm_create_word (gap a) with a zeroed DF slot (gap b).\ +lemma defer_not_modelled: True \ \DEFER: vm_create_word (gap a) with a zeroed DF slot (gap b). CORRECTION (added when src/word_source/defer_words.c was later swept, see StarForth_Defer_Words.thy): word_registry.c registers defer_words.c's DEFER/IS/DEFER@ AFTER this file's (Module 27 vs 17), unconditionally in both builds -- this DEFER is dead, shadowed code, never reachable. The gap analysis below is still accurate as a description of what this dead code would hit, and the live version hits the same gaps anyway, so nothing here needed retracting.\ by simp -lemma defer_runtime_not_modelled: True \ \defining_runtime_defer: reads a DictEntry* out of the DF cell (gap b) and calls through it (gap c).\ +lemma defer_runtime_not_modelled: True \ \defining_runtime_defer: reads a DictEntry* out of the DF cell (gap b) and calls through it (gap c). Also shadowed/dead -- see defer_not_modelled correction above.\ by simp -lemma is_not_modelled: True \ \IS: vm_find_word (parse+lookup) + writes an XT into the target's DF cell (gap b) -- the mutable-dispatch mechanism of gap (c).\ +lemma is_not_modelled: True \ \IS: vm_find_word (parse+lookup) + writes an XT into the target's DF cell (gap b) -- the mutable-dispatch mechanism of gap (c). Also shadowed/dead -- see defer_not_modelled correction above.\ by simp -lemma defer_fetch_not_modelled: True \ \DEFER@: vm_find_word + reads the DF cell (gap b).\ +lemma defer_fetch_not_modelled: True \ \DEFER@: vm_find_word + reads the DF cell (gap b). Also shadowed/dead -- see defer_not_modelled correction above.\ by simp end diff --git a/proof/StarForth_Lifecycle_Words_Hosted.thy b/proof/StarForth_Lifecycle_Words_Hosted.thy new file mode 100644 index 0000000..72ce62c --- /dev/null +++ b/proof/StarForth_Lifecycle_Words_Hosted.thy @@ -0,0 +1,101 @@ +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 \ vm_state" where + "forth_lifecycle_pop2 vm = + (case data_stack vm of + [] \ set_error vm + | [x] \ set_error (vm\data_stack := []\) + | u # caddr # xs \ vm\data_stack := xs\)" + +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: + \ \Partial pop: the single element IS consumed (it was popped + successfully as `u`) before the second pop fails.\ + 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 \ vm_state" where "forth_birth = forth_lifecycle_pop2" +definition forth_kill :: "vm_state \ vm_state" where "forth_kill = forth_lifecycle_pop2" +definition forth_pause :: "vm_state \ vm_state" where "forth_pause = forth_lifecycle_pop2" +definition forth_resume :: "vm_state \ vm_state" where "forth_resume = forth_lifecycle_pop2" +definition forth_use :: "vm_state \ 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 + \ \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.\ + by simp + +end diff --git a/proof/StarForth_Log_Words.thy b/proof/StarForth_Log_Words.thy new file mode 100644 index 0000000..1b83abe --- /dev/null +++ b/proof/StarForth_Log_Words.thy @@ -0,0 +1,210 @@ +theory StarForth_Log_Words + imports StarForth_Base +begin + +(* ========================================================================= + Mirrors: src/word_source/log_words.c + Registers: LOG-ERROR LOG-WARN LOG-INFO LOG-TEST LOG-DEBUG LOG-LEVEL! + LOG-LEVEL@ (do-log-error/warn/info/test/debug) + LOG-ERROR"/WARN"/INFO"/TEST"/DEBUG" (IMMEDIATE) + LOG-ERROR-STR/WARN-STR/INFO-STR/TEST-STR/DEBUG-STR + + ── Scope ───────────────────────────────────────────────────────────── + Fully modelled: the five level-constant pushes (LOG-ERROR..LOG-DEBUG), + LOG-LEVEL!'s guard+clamp (the clamped VALUE is a pure function of the + popped cell, even though where it's stored -- the log subsystem's + active level -- is outside vm_state), and all five LOG-*-STR words + (same "pop2 + bounds-check guard, no further vm_state effect" shape as + StarForth_Lifecycle_Words_Hosted.thy -- log_message is I/O-only, reads + memory but never writes it). + + NOT modelled: LOG-LEVEL@ (pushes the log subsystem's active level, a + value with no vm_state counterpart -- same class of gap as SEED/RANDOM's + g_prng_state, just for a different global); the five (do-log-N) name-family + runtime words (read/advance the return-stack top as a raw C pointer + into inline threaded-code data, the same "raw host pointer, not a VM + address" gap already flagged for LIT in StarForth_Defining_Words.thy); + `log_emit_string` and the five `LOG-*"` immediates built on it (TIB/ + input-buffer dependency in interpret mode, PLUS compile-mode dependency + on vm_find_word + vm_compile_word + vm_allot -- several already-flagged + gaps compounded in one helper). + + ── Finding: three more push-only words with no overflow guard ───────── + LOG-ERROR/WARN/INFO/TEST/DEBUG and LOG-LEVEL@ push unconditionally with + no `ds_full` check -- the pattern first found at DECAY-RATE@ + (physics_freeze_words.c) and repeated across framebuffer_words.c/ + keyboard_words.c keeps recurring specifically in "just returns a + constant/global" words; worth citing log_words.c as further evidence + when this goes to Bob as an aggregated pattern rather than one-offs. + ======================================================================== *) + +definition LOG_ERROR_LEVEL :: cell where "LOG_ERROR_LEVEL = 0" +definition LOG_WARN_LEVEL :: cell where "LOG_WARN_LEVEL = 1" +definition LOG_INFO_LEVEL :: cell where "LOG_INFO_LEVEL = 2" +definition LOG_TEST_LEVEL :: cell where "LOG_TEST_LEVEL = 3" +definition LOG_DEBUG_LEVEL :: cell where "LOG_DEBUG_LEVEL = 4" +definition LOG_LINE_MAX :: nat where "LOG_LINE_MAX = 256" + +(* ── LOG-ERROR / LOG-WARN / LOG-INFO / LOG-TEST / LOG-DEBUG ( -- n ) ────── *) + +definition forth_log_error :: "vm_state \ vm_state" where + "forth_log_error vm = vm\data_stack := LOG_ERROR_LEVEL # data_stack vm\" +definition forth_log_warn :: "vm_state \ vm_state" where + "forth_log_warn vm = vm\data_stack := LOG_WARN_LEVEL # data_stack vm\" +definition forth_log_info :: "vm_state \ vm_state" where + "forth_log_info vm = vm\data_stack := LOG_INFO_LEVEL # data_stack vm\" +definition forth_log_test :: "vm_state \ vm_state" where + "forth_log_test vm = vm\data_stack := LOG_TEST_LEVEL # data_stack vm\" +definition forth_log_debug :: "vm_state \ vm_state" where + "forth_log_debug vm = vm\data_stack := LOG_DEBUG_LEVEL # data_stack vm\" + +lemma log_error_pushes: "data_stack (forth_log_error vm) = 0 # data_stack vm" + by (simp add: forth_log_error_def LOG_ERROR_LEVEL_def) +lemma log_warn_pushes: "data_stack (forth_log_warn vm) = 1 # data_stack vm" + by (simp add: forth_log_warn_def LOG_WARN_LEVEL_def) +lemma log_info_pushes: "data_stack (forth_log_info vm) = 2 # data_stack vm" + by (simp add: forth_log_info_def LOG_INFO_LEVEL_def) +lemma log_test_pushes: "data_stack (forth_log_test vm) = 3 # data_stack vm" + by (simp add: forth_log_test_def LOG_TEST_LEVEL_def) +lemma log_debug_pushes: "data_stack (forth_log_debug vm) = 4 # data_stack vm" + by (simp add: forth_log_debug_def LOG_DEBUG_LEVEL_def) + +lemma log_levels_no_overflow_guard: True + \ \See file header finding -- all five push unconditionally.\ + by simp + +(* ── LOG-LEVEL! ( n -- ) : guard + pure clamp ─────────────────────────── *) +(* C: error if stack empty; else pop n, clamp to [LOG_ERROR, LOG_DEBUG], + call log_set_level(n) -- the STORE target is outside vm_state, but the + clamped value is a pure function of the input, modelled as such. *) + +definition log_level_clamp :: "cell \ cell" where + "log_level_clamp n = + (if n vm_state" where + "forth_log_level_store_guard vm = + (case data_stack vm of + [] \ set_error vm + | n # xs \ vm\data_stack := xs\)" + +lemma log_level_store_underflow: + assumes "data_stack vm = []" + shows "vm_error (forth_log_level_store_guard vm)" + by (simp add: forth_log_level_store_guard_def set_error_def assms) + +lemma log_level_store_pops_one: + assumes "data_stack vm = n # xs" + shows "data_stack (forth_log_level_store_guard vm) = xs" + by (simp add: forth_log_level_store_guard_def assms) + +lemma log_level_clamp_bounds: + "\ (log_level_clamp n (LOG_DEBUG_LEVEL n LOG_DEBUG_LEVEL \log_set_level(n) writes the log subsystem's active level, which has + no vm_state counterpart.\ + by simp + +(* ── LOG-LEVEL@ ( -- n ) -- NOT MODELLED ──────────────────────────────── *) + +lemma log_level_fetch_not_modelled: True + \ \Pushes log_get_level(), reading the same unmodelled global + LOG-LEVEL! writes to. No overflow guard either -- see file header.\ + by simp + +(* ── (do-log-N) runtime words -- NOT MODELLED ─────────────────────────── *) + +lemma do_log_runtime_words_not_modelled: True + \ \All five read/advance vm->return_stack[vm->rsp] as a raw C uint8_t* + into inline threaded-code data -- the same raw-host-pointer gap + already flagged for LIT (StarForth_Defining_Words.thy), not the + IP-as-vaddr usage control_words.c's return-stack addresses already + resolved.\ + by simp + +(* ── LOG-*" (IMMEDIATE) and log_emit_string -- NOT MODELLED ──────────── *) + +lemma log_quote_words_not_modelled: True + \ \log_emit_string: TIB/input-buffer dependency (interpret mode) plus, + in compile mode, vm_find_word + vm_compile_word + vm_allot -- several + already-flagged gaps compounded in one helper shared by all five + LOG-*" immediates.\ + by simp + +(* ── LOG-ERROR-STR / -WARN-STR / -INFO-STR / -TEST-STR / -DEBUG-STR + ( c-addr u -- ) : fully modelled, same shape as lifecycle words ─────── + C: error if dsp<1; pop u, pop addr; if u<=0, no-op (beyond the pops); + if addr out of [0, VM_MEMORY_SIZE - u] range, error; else clamp u to + LOG_LINE_MAX-1 and log_message a READ of vm->memory[addr..addr+u) -- + no vm_state write at all beyond the two pops. All five share this + shape (log_str_emit), differing only in the log level passed through, + which has no vm_state footprint. *) + +definition forth_log_str_emit :: "vm_state \ vm_state" where + "forth_log_str_emit vm = + (case data_stack vm of + u # addr # xs \ + (if u \s 0 then vm\data_stack := xs\ + else if addr unat addr + unat u > VM_MEMORY_SIZE + then set_error (vm\data_stack := xs\) + else vm\data_stack := xs\) + | _ \ set_error vm)" + +lemma log_str_emit_underflow_nil: + assumes "data_stack vm = []" + shows "vm_error (forth_log_str_emit vm)" + by (simp add: forth_log_str_emit_def set_error_def assms) + +lemma log_str_emit_underflow_one: + assumes "data_stack vm = [x]" + shows "vm_error (forth_log_str_emit vm)" + by (simp add: forth_log_str_emit_def set_error_def assms) + +lemma log_str_emit_nonpositive_len_pops_only: + assumes "data_stack vm = u # addr # xs" + assumes "u \s 0" + shows "forth_log_str_emit vm = vm\data_stack := xs\" + using assms by (simp add: forth_log_str_emit_def) + +lemma log_str_emit_out_of_range_errors: + assumes "data_stack vm = u # addr # xs" + assumes "\ u \s 0" + assumes "addr unat addr + unat u > VM_MEMORY_SIZE" + shows "vm_error (forth_log_str_emit vm)" + using assms by (simp add: forth_log_str_emit_def set_error_def) + +lemma log_str_emit_normal: + assumes "data_stack vm = u # addr # xs" + assumes "\ u \s 0" + assumes "\ (addr unat addr + unat u > VM_MEMORY_SIZE)" + shows "forth_log_str_emit vm = vm\data_stack := xs\" + using assms by (simp add: forth_log_str_emit_def) + +lemma log_str_emit_never_writes_memory: + "memory (forth_log_str_emit vm) = memory vm" + by (auto simp: forth_log_str_emit_def set_error_def split: list.split) + +definition forth_log_error_str :: "vm_state \ vm_state" where "forth_log_error_str = forth_log_str_emit" +definition forth_log_warn_str :: "vm_state \ vm_state" where "forth_log_warn_str = forth_log_str_emit" +definition forth_log_info_str :: "vm_state \ vm_state" where "forth_log_info_str = forth_log_str_emit" +definition forth_log_test_str :: "vm_state \ vm_state" where "forth_log_test_str = forth_log_str_emit" +definition forth_log_debug_str :: "vm_state \ vm_state" where "forth_log_debug_str = forth_log_str_emit" + +lemma log_error_str_is_emit: "forth_log_error_str vm = forth_log_str_emit vm" by (simp add: forth_log_error_str_def) +lemma log_warn_str_is_emit: "forth_log_warn_str vm = forth_log_str_emit vm" by (simp add: forth_log_warn_str_def) +lemma log_info_str_is_emit: "forth_log_info_str vm = forth_log_str_emit vm" by (simp add: forth_log_info_str_def) +lemma log_test_str_is_emit: "forth_log_test_str vm = forth_log_str_emit vm" by (simp add: forth_log_test_str_def) +lemma log_debug_str_is_emit: "forth_log_debug_str vm = forth_log_str_emit vm" by (simp add: forth_log_debug_str_def) + +end