Robert Allan JamesandClaude Sonnet 5
dfdabcc2d7
DECAY-RATE@ (physics_freeze_words.c) pushed to the data stack with no capacity check and no prior pop to make room, unlike its neighbors in the same file -- the one live, unconditional missing-guard bug the Isabelle sweep's ~15 candidate findings reduced to once checked against vm_push()'s real internal bounds check (see proof/FINDINGS.md SS2). Removed dictionary_manipulation_words.c's [ ] STATE and defining_words.c's DEFER IS DEFER@ (plus the now-orphaned defining_runtime_defer helper) -- all confirmed permanently shadowed by later dictionary registrations (defining_words.c and defer_words.c respectively), per FORTH's newest-first lookup. No behavior change: the removed code was already unreachable. Verified: hosted `make` builds clean under -Wall -Werror; the hosted self-test suite passes 965/965 implemented tests with no regressions. Three-architecture QEMU acceptance boot, all clean to ok> with an identical dict_hash=0x24b4279f0670aa3a across amd64/aarch64/riscv64 and identical 1003/965/0/0 test totals -- logs attached. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
212 lines
11 KiB
Plaintext
212 lines
11 KiB
Plaintext
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).
|
|
|
|
── CORRECTED finding: LOG-* words are NOT missing a guard ─────────────
|
|
LOG-ERROR/WARN/INFO/TEST/DEBUG and LOG-LEVEL@ all push via C's
|
|
`vm_push()` (src/stack_management.c:75), which bounds-checks internally
|
|
-- this file's earlier claim of a missing `ds_full` check was a gap in
|
|
this theory's abstract push model, not a real defect in the C.
|
|
Re-verified 2026-08-14; see proof/FINDINGS.md §2 for the full
|
|
correction across every file this pattern was raised against.
|
|
======================================================================== *)
|
|
|
|
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. Push is via vm_push(), which bounds-checks --
|
|
see corrected 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
|