theory StarForth_Block_Words imports StarForth_Base StarForth_Dictionary_Words begin (* ========================================================================= POST-10: Block Words Mirrors: src/word_source/block_words.c (12 registered words) SCOPE, decided 2026-08-14: this file is categorically different from every other file covered in this sweep so far. Every other word_source file operates on pure, deterministic, per-VM internal state (data_stack, return_stack, memory, dictionary) -- exactly what the abstract vm_state already represents. block_words.c instead sits on top of a real, stateful I/O subsystem (block_subsystem.h's blk_get_buffer/blk_update/ blk_flush/blk_subsys_confirm_format/blk_is_valid), backed by an actual disk (per the repo's Artemis storage architecture) -- and a per-VM in-memory CACHE of that subsystem, `vm->blk_vm_lbn`/`blk_vm_cbuf`/ `blk_vm_dirty`/`blk_vm_next` (include/vm.h:459-462), none of which are in vm_state. Only ONE of the 12 registered words is self-contained enough to model: - SCR ( -- addr ): `vm_push(vm, CELL(vm->scr_addr))`. Needs only `scr_addr`, now added to vm_state (StarForth_Base.thy, after ecw_nesting) the same way `here`/`ecw_nesting` were added for earlier files -- a real, simply-scoped field, not a placeholder. The other 11 (BLOCK, BUFFER, UPDATE, BLK-CONFIRM-FORMAT, SAVE-BUFFERS, EMPTY-BUFFERS, FLUSH, LOAD, LIST, THRU, -->) are NOT modeled, each for at least one of three reasons, most for more than one: a. Block-window CACHE dependency (BLOCK/BUFFER/UPDATE/SAVE-BUFFERS/ EMPTY-BUFFERS/FLUSH/-->): read/write `vm->blk_vm_lbn`/`blk_vm_cbuf`/ `blk_vm_dirty`/`blk_vm_next`, a 4-slot LRU-ish cache correlating a VM memory window (BLK_VM_WINDOW_BASE) with C-layer block buffers. Modeling this faithfully means modeling the cache's slot-assignment and eviction policy (`blk_vm_find`/`blk_vm_evict`/`blk_vm_load`/ `blk_vm_assign`) as vm_state too -- a real subsystem-modeling project on the scale of the deferred TIB input subsystem (StarForth_String_Words.thy), not a one-word extension. b. Real external I/O (BLOCK/BUFFER/UPDATE/BLK-CONFIRM-FORMAT/ SAVE-BUFFERS/EMPTY-BUFFERS/FLUSH/LOAD/LIST/THRU/-->, i.e. all 11): every one of them calls into block_subsystem.h (blk_get_buffer/blk_get_empty_buffer/blk_update/blk_flush/ blk_subsys_confirm_format/blk_is_valid/blk_get_total_blocks) -- genuine disk-backed state outside the VM entirely, the same category of gap as string_words.c's stdio calls, just at the block-storage layer instead of the terminal. c. Recursive interpretation / console output (LOAD/THRU/-->/LIST): LOAD and --> call `vm_interpret()` on block content (arbitrary recursive FORTH execution, not a leaf-level stack/memory effect); THRU calls LOAD in a loop; LIST calls `printf()` directly. None of these are single-step vm_state transitions in any sense this proof suite's other words are. ── Genuine finding, not fixed ─────────────────────────────────────────── `blk_vm_evict`'s and `blk_vm_flush_all`'s own comments (lines 180-184, 241-243) document a real, previously-hit bug class being defended against here: "the block-subsystem's own devblock cache may have shifted (struct-copy eviction) since this slot was populated, which silently invalidates any raw pointer captured earlier" -- i.e. C buffer pointers cached in `vm->blk_vm_cbuf[]` can go stale out from under the VM, and both functions now defensively re-resolve by LBN instead of trusting the stored pointer. This reads as already-fixed (the code re-resolves), not an open bug -- noted here only because it is exactly the kind of raw-pointer-lifetime hazard this proof suite exists to catch, and it's worth knowing it was already found and fixed by hand once, in the C, before this suite ever looked at this file. ======================================================================== *) (* ── SCR ( -- addr ) ───────────────────────────────────────────────────── *) definition forth_scr :: "vm_state \ vm_state" where "forth_scr vm = vm\data_stack := word_of_nat (scr_addr vm) # data_stack vm\" lemma scr_pushes_scr_addr: "data_stack (forth_scr vm) = word_of_nat (scr_addr vm) # data_stack vm" by (simp add: forth_scr_def) lemma scr_preserves_scr_addr: "scr_addr (forth_scr vm) = scr_addr vm" by (simp add: forth_scr_def) lemma scr_never_errors: "vm_error (forth_scr vm) = vm_error vm" by (simp add: forth_scr_def) (* ── The other 11 words -- NOT MODELLED, see SCOPE above ────────────────── *) lemma block_not_modelled: True \ \BLOCK: block-window cache + blk_get_buffer (disk read).\ by simp lemma buffer_not_modelled: True \ \BUFFER: block-window cache + blk_get_empty_buffer.\ by simp lemma update_not_modelled: True \ \UPDATE: block-window cache + blk_get_buffer + blk_update (disk write).\ by simp lemma blk_confirm_format_not_modelled: True \ \BLK-CONFIRM-FORMAT: blk_subsys_confirm_format, pure disk-container state.\ by simp lemma save_buffers_not_modelled: True \ \SAVE-BUFFERS: block-window cache + blk_update/blk_flush (disk write).\ by simp lemma empty_buffers_not_modelled: True \ \EMPTY-BUFFERS: block-window cache + blk_get_buffer over every user block.\ by simp lemma flush_not_modelled: True \ \FLUSH: same as SAVE-BUFFERS.\ by simp lemma load_not_modelled: True \ \LOAD: blk_get_buffer (disk read) + recursive vm_interpret.\ by simp lemma list_not_modelled: True \ \LIST: blk_get_buffer (disk read) + printf (console I/O).\ by simp lemma thru_not_modelled: True \ \THRU: LOAD in a loop; inherits LOAD's gaps.\ by simp lemma next_block_not_modelled: True \ \-->: blk_get_buffer (disk read) + recursive vm_interpret, line-split.\ by simp end