Robert Allan JamesandClaude Sonnet 5
c1360df2d1
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 <noreply@anthropic.com>
113 lines
6.3 KiB
Plaintext
113 lines
6.3 KiB
Plaintext
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 \<Rightarrow> vm_state" where
|
|
"forth_scr vm = vm\<lparr>data_stack := word_of_nat (scr_addr vm) # data_stack vm\<rparr>"
|
|
|
|
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 \<comment> \<open>BLOCK: block-window cache + blk_get_buffer (disk read).\<close>
|
|
by simp
|
|
lemma buffer_not_modelled: True \<comment> \<open>BUFFER: block-window cache + blk_get_empty_buffer.\<close>
|
|
by simp
|
|
lemma update_not_modelled: True \<comment> \<open>UPDATE: block-window cache + blk_get_buffer + blk_update (disk write).\<close>
|
|
by simp
|
|
lemma blk_confirm_format_not_modelled: True \<comment> \<open>BLK-CONFIRM-FORMAT: blk_subsys_confirm_format, pure disk-container state.\<close>
|
|
by simp
|
|
lemma save_buffers_not_modelled: True \<comment> \<open>SAVE-BUFFERS: block-window cache + blk_update/blk_flush (disk write).\<close>
|
|
by simp
|
|
lemma empty_buffers_not_modelled: True \<comment> \<open>EMPTY-BUFFERS: block-window cache + blk_get_buffer over every user block.\<close>
|
|
by simp
|
|
lemma flush_not_modelled: True \<comment> \<open>FLUSH: same as SAVE-BUFFERS.\<close>
|
|
by simp
|
|
lemma load_not_modelled: True \<comment> \<open>LOAD: blk_get_buffer (disk read) + recursive vm_interpret.\<close>
|
|
by simp
|
|
lemma list_not_modelled: True \<comment> \<open>LIST: blk_get_buffer (disk read) + printf (console I/O).\<close>
|
|
by simp
|
|
lemma thru_not_modelled: True \<comment> \<open>THRU: LOAD in a loop; inherits LOAD's gaps.\<close>
|
|
by simp
|
|
lemma next_block_not_modelled: True \<comment> \<open>-->: blk_get_buffer (disk read) + recursive vm_interpret, line-split.\<close>
|
|
by simp
|
|
|
|
end
|