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 <noreply@anthropic.com>
This commit is contained in:
Robert Allan James
co-authored by
Claude Sonnet 5
Claude Sonnet 5
parent
a1d24fdb6f
commit
c1360df2d1
@@ -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
|
||||
|
||||
@@ -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.
|
||||
|
||||
@@ -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 \<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
|
||||
Reference in New Issue
Block a user