Robert Allan James
283c4780e4
10 of 16 registered words modeled (COLD/WARM/BYE/WORDS/VLIST/PAGE/NOP/ QUIT/ABORT/EXECUTE guard-shape), plus the internal (ABORT") runtime helper. Deferred: ( and \ (TIB dependency), SAVE-SYSTEM (real file I/O), 79-STANDARD (reads a non-per-VM global), ABORT" compile-time half (TIB + codegen), SEE (TIB + raw threaded-code pointer walk). Two findings. (1) system_running/forth_79_standard are file-scope C statics doing per-VM-shaped work -- the 5th and 6th occurrence of this bug pattern in the sweep (previously: control_words.c's cf_stack, dictionary_manipulation_words.c's state_variable, string_words.c's word_scratch_addr). (2) EXECUTE casts a popped FORTH cell straight to a DictEntry host pointer and calls through it (entry->func(vm)), gated only by a null check -- same hazard class as format_words.c's ?/DUMP but far more consequential since EXECUTE is a core, ubiquitous primitive rather than a diagnostic word. Flagged as the highest-severity finding this sweep has produced.
38 lines
1.1 KiB
Plaintext
38 lines
1.1 KiB
Plaintext
session "StarForth" = "HOL-Library" +
|
|
description "Formal proofs of StarForth FORTH-79 primitive correctness and physics-loop invariants"
|
|
theories [document = false]
|
|
StarForth_Base
|
|
StarForth_Q48_16
|
|
StarForth_Stack_Words
|
|
StarForth_Double_Words
|
|
StarForth_Arithmetic_Words
|
|
StarForth_Mixed_Arithmetic_Words
|
|
StarForth_Logical_Words
|
|
StarForth_Return_Stack_Words
|
|
StarForth_Memory_Words
|
|
StarForth_Dictionary_Words
|
|
StarForth_Dictionary_Manipulation_Words
|
|
StarForth_Control_Words
|
|
StarForth_String_Words
|
|
StarForth_Block_Words
|
|
StarForth_IO_Words
|
|
StarForth_Editor_Words
|
|
StarForth_Format_Words
|
|
StarForth_System_Words
|
|
StarForth_Mutex
|
|
StarForth_Transition
|
|
StarForth_Loop1_Heat
|
|
StarForth_Loop2_Window
|
|
StarForth_Loop3_Decay
|
|
StarForth_Loop4_Pipeline
|
|
StarForth_Loop5_WinInf
|
|
StarForth_Loop6_DecayInf
|
|
StarForth_Loop7_Heartrate
|
|
StarForth_Concurrent
|
|
StarForth_Correctness
|
|
ACL_Pin_Monotone
|
|
ACL_Inherit_Clears_Pin
|
|
ACL_TTL_Bounded
|
|
ACL_Emergency_Bypass
|
|
ACL_No_Escalation
|