From c1360df2d15bd46e02151d2a94ad245475bcf082 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Thu, 13 Aug 2026 23:14:24 -0400 Subject: [PATCH] proof/: add StarForth_Block_Words.thy (SCR only) block_words.c is categorically different from every file covered so far in this sweep: every other word_source file operates on pure per-VM internal state already in vm_state (data_stack/return_stack/memory/dictionary). block_words.c sits on top of a real disk-backed I/O subsystem (block_subsystem.h) plus a per-VM in-memory cache of it (vm->blk_vm_lbn/blk_vm_cbuf/blk_vm_dirty/blk_vm_next), none of which are in vm_state. Only SCR is self-contained (just needs vm->scr_addr, added to vm_state the same way here/ecw_nesting were for earlier files). The other 11 words are deferred for three reasons documented in the theory header: the block-window cache subsystem (a modeling project on the scale of the deferred TIB input subsystem, not a one-word extension), real disk I/O via block_subsystem.h, and recursive vm_interpret()/printf() in LOAD/LIST/ THRU/-->. Noted in passing: blk_vm_evict/blk_vm_flush_all's own comments document a real raw-pointer-lifetime bug (stale C buffer pointers after block- subsystem struct-copy eviction) that was already found and fixed by hand in the C, before this suite ever looked at the file -- not an open issue, just worth recording as prior art for exactly the class of bug this sweep exists to catch. 30 theory files verify with zero errors. Co-Authored-By: Claude Sonnet 5 --- proof/ROOT | 1 + proof/StarForth_Base.thy | 5 ++ proof/StarForth_Block_Words.thy | 112 ++++++++++++++++++++++++++++++++ 3 files changed, 118 insertions(+) create mode 100644 proof/StarForth_Block_Words.thy diff --git a/proof/ROOT b/proof/ROOT index 71ff2ce..1367c27 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -14,6 +14,7 @@ session "StarForth" = "HOL-Library" + StarForth_Dictionary_Manipulation_Words StarForth_Control_Words StarForth_String_Words + StarForth_Block_Words StarForth_Mutex StarForth_Transition StarForth_Loop1_Heat diff --git a/proof/StarForth_Base.thy b/proof/StarForth_Base.thy index 444660c..d46fea1 100644 --- a/proof/StarForth_Base.thy +++ b/proof/StarForth_Base.thy @@ -514,6 +514,11 @@ record vm_state = nat (C only ever tests ecw_nesting > 0, never negative values in any reachable path) -- see StarForth_Double_Words.thy's 2>R/2R>/2R@. *) ecw_nesting :: nat + (* ○ CODE-MUST-MATCH: C: vaddr_t scr_addr (include/vm.h:451, vaddr_t = + uint64_t) -- VM address of the SCR variable cell holding the current + block number. Modeled as nat, matching `here`'s convention for VM + addresses. See StarForth_Block_Words.thy's SCR. *) + scr_addr :: nat (* ── Physics Loop #1: Execution heat tracking ───────────────────────── *) (* ○ CODE-MUST-MATCH: heat_threshold_{25th,50th,75th} in C VM struct. diff --git a/proof/StarForth_Block_Words.thy b/proof/StarForth_Block_Words.thy new file mode 100644 index 0000000..80d095c --- /dev/null +++ b/proof/StarForth_Block_Words.thy @@ -0,0 +1,112 @@ +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