proof/: add lifecycle_words_hosted.c, defer_words.c, log_words.c coverage
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.
This commit is contained in:
Robert Allan James
@@ -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
|
||||
|
||||
@@ -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 \<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
|
||||
@@ -324,13 +324,13 @@ lemma bracket_compile_not_modelled: True \<comment> \<open>[COMPILE]: identical
|
||||
by simp
|
||||
lemma forget_not_modelled: True \<comment> \<open>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.\<close>
|
||||
by simp
|
||||
lemma defer_not_modelled: True \<comment> \<open>DEFER: vm_create_word (gap a) with a zeroed DF slot (gap b).\<close>
|
||||
lemma defer_not_modelled: True \<comment> \<open>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.\<close>
|
||||
by simp
|
||||
lemma defer_runtime_not_modelled: True \<comment> \<open>defining_runtime_defer: reads a DictEntry* out of the DF cell (gap b) and calls through it (gap c).\<close>
|
||||
lemma defer_runtime_not_modelled: True \<comment> \<open>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.\<close>
|
||||
by simp
|
||||
lemma is_not_modelled: True \<comment> \<open>IS: vm_find_word (parse+lookup) + writes an XT into the target's DF cell (gap b) -- the mutable-dispatch mechanism of gap (c).\<close>
|
||||
lemma is_not_modelled: True \<comment> \<open>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.\<close>
|
||||
by simp
|
||||
lemma defer_fetch_not_modelled: True \<comment> \<open>DEFER@: vm_find_word + reads the DF cell (gap b).\<close>
|
||||
lemma defer_fetch_not_modelled: True \<comment> \<open>DEFER@: vm_find_word + reads the DF cell (gap b). Also shadowed/dead -- see defer_not_modelled correction above.\<close>
|
||||
by simp
|
||||
|
||||
end
|
||||
|
||||
@@ -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 \<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
|
||||
@@ -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 \<Rightarrow> vm_state" where
|
||||
"forth_log_error vm = vm\<lparr>data_stack := LOG_ERROR_LEVEL # data_stack vm\<rparr>"
|
||||
definition forth_log_warn :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_log_warn vm = vm\<lparr>data_stack := LOG_WARN_LEVEL # data_stack vm\<rparr>"
|
||||
definition forth_log_info :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_log_info vm = vm\<lparr>data_stack := LOG_INFO_LEVEL # data_stack vm\<rparr>"
|
||||
definition forth_log_test :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_log_test vm = vm\<lparr>data_stack := LOG_TEST_LEVEL # data_stack vm\<rparr>"
|
||||
definition forth_log_debug :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_log_debug vm = vm\<lparr>data_stack := LOG_DEBUG_LEVEL # data_stack vm\<rparr>"
|
||||
|
||||
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
|
||||
\<comment> \<open>See file header finding -- all five push unconditionally.\<close>
|
||||
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 \<Rightarrow> cell" where
|
||||
"log_level_clamp n =
|
||||
(if n <s LOG_ERROR_LEVEL then LOG_ERROR_LEVEL
|
||||
else if LOG_DEBUG_LEVEL <s n then LOG_DEBUG_LEVEL
|
||||
else n)"
|
||||
|
||||
definition forth_log_level_store_guard :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_log_level_store_guard vm =
|
||||
(case data_stack vm of
|
||||
[] \<Rightarrow> set_error vm
|
||||
| n # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>)"
|
||||
|
||||
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:
|
||||
"\<not> (log_level_clamp n <s LOG_ERROR_LEVEL)"
|
||||
"\<not> (LOG_DEBUG_LEVEL <s log_level_clamp n)"
|
||||
by (auto simp: log_level_clamp_def LOG_ERROR_LEVEL_def LOG_DEBUG_LEVEL_def
|
||||
word_sle_eq word_sless_alt)
|
||||
|
||||
lemma log_level_clamp_identity_in_range:
|
||||
assumes "\<not> n <s LOG_ERROR_LEVEL" "\<not> LOG_DEBUG_LEVEL <s n"
|
||||
shows "log_level_clamp n = n"
|
||||
using assms by (simp add: log_level_clamp_def)
|
||||
|
||||
lemma log_level_store_target_not_modelled: True
|
||||
\<comment> \<open>log_set_level(n) writes the log subsystem's active level, which has
|
||||
no vm_state counterpart.\<close>
|
||||
by simp
|
||||
|
||||
(* ── LOG-LEVEL@ ( -- n ) -- NOT MODELLED ──────────────────────────────── *)
|
||||
|
||||
lemma log_level_fetch_not_modelled: True
|
||||
\<comment> \<open>Pushes log_get_level(), reading the same unmodelled global
|
||||
LOG-LEVEL! writes to. No overflow guard either -- see file header.\<close>
|
||||
by simp
|
||||
|
||||
(* ── (do-log-N) runtime words -- NOT MODELLED ─────────────────────────── *)
|
||||
|
||||
lemma do_log_runtime_words_not_modelled: True
|
||||
\<comment> \<open>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.\<close>
|
||||
by simp
|
||||
|
||||
(* ── LOG-*" (IMMEDIATE) and log_emit_string -- NOT MODELLED ──────────── *)
|
||||
|
||||
lemma log_quote_words_not_modelled: True
|
||||
\<comment> \<open>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.\<close>
|
||||
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 \<Rightarrow> vm_state" where
|
||||
"forth_log_str_emit vm =
|
||||
(case data_stack vm of
|
||||
u # addr # xs \<Rightarrow>
|
||||
(if u \<le>s 0 then vm\<lparr>data_stack := xs\<rparr>
|
||||
else if addr <s 0 \<or> unat addr + unat u > VM_MEMORY_SIZE
|
||||
then set_error (vm\<lparr>data_stack := xs\<rparr>)
|
||||
else vm\<lparr>data_stack := xs\<rparr>)
|
||||
| _ \<Rightarrow> 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 \<le>s 0"
|
||||
shows "forth_log_str_emit vm = vm\<lparr>data_stack := xs\<rparr>"
|
||||
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 "\<not> u \<le>s 0"
|
||||
assumes "addr <s 0 \<or> 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 "\<not> u \<le>s 0"
|
||||
assumes "\<not> (addr <s 0 \<or> unat addr + unat u > VM_MEMORY_SIZE)"
|
||||
shows "forth_log_str_emit vm = vm\<lparr>data_stack := xs\<rparr>"
|
||||
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 \<Rightarrow> vm_state" where "forth_log_error_str = forth_log_str_emit"
|
||||
definition forth_log_warn_str :: "vm_state \<Rightarrow> vm_state" where "forth_log_warn_str = forth_log_str_emit"
|
||||
definition forth_log_info_str :: "vm_state \<Rightarrow> vm_state" where "forth_log_info_str = forth_log_str_emit"
|
||||
definition forth_log_test_str :: "vm_state \<Rightarrow> vm_state" where "forth_log_test_str = forth_log_str_emit"
|
||||
definition forth_log_debug_str :: "vm_state \<Rightarrow> 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
|
||||
Reference in New Issue
Block a user