From 92474c521936361fcb98aa0eacbf3a64a5988175 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Thu, 13 Aug 2026 18:12:54 -0400 Subject: [PATCH] proof/: add StarForth_Dictionary_Words.thy (HERE/ALIGN/ALLOT/,/C,/2,/PAD/LATEST) Adds VM_MEMORY_SIZE and DICTIONARY_MEMORY_SIZE constants to StarForth_Base.thy (previously only STACK_SIZE existed). SP@/SP! left unmodelled (oops-flagged with explanation) -- the list-based data_stack model has no independent dsp register distinct from list length, which is exactly what SP! manipulates. Genuine findings recorded in comments, not fixed: - LATEST has an identical body to HERE (both just push vm->here) rather than consulting vm->latest -- doesn't return what its own doc comment claims. - ALIGN (via vm_align/vm_allot) bounds-checks here against DICTIONARY_MEMORY_SIZE (2MB), while ALLOT/,/C,/2, bound-check directly against VM_MEMORY_SIZE (5MB) instead -- two different ceilings for the same dictionary pointer. Full suite (26 theory files) verifies with zero errors. Co-Authored-By: Claude Sonnet 5 --- proof/ROOT | 1 + proof/StarForth_Base.thy | 16 ++ proof/StarForth_Dictionary_Words.thy | 301 +++++++++++++++++++++++++++ 3 files changed, 318 insertions(+) create mode 100644 proof/StarForth_Dictionary_Words.thy diff --git a/proof/ROOT b/proof/ROOT index 54b467e..43a57c6 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -10,6 +10,7 @@ session "StarForth" = "HOL-Library" + StarForth_Logical_Words StarForth_Return_Stack_Words StarForth_Memory_Words + StarForth_Dictionary_Words StarForth_Mutex StarForth_Transition StarForth_Loop1_Heat diff --git a/proof/StarForth_Base.thy b/proof/StarForth_Base.thy index 01a5a6e..84fd05f 100644 --- a/proof/StarForth_Base.thy +++ b/proof/StarForth_Base.thy @@ -202,6 +202,22 @@ type_synonym forth_stack = "cell list" re-proved to ensure they still hold. *) definition STACK_SIZE :: nat where "STACK_SIZE = 1024" +(* ○ CODE-MUST-MATCH: #define VM_MEMORY_SIZE (5 * 1024 * 1024) in include/vm.h. + ⚠ HUMAN-REVIEW: If this changes in C, update here and re-check + StarForth_Dictionary_Words.thy's ALLOT/,/C,/2, bound lemmas. *) +definition VM_MEMORY_SIZE :: nat where "VM_MEMORY_SIZE = 5242880" + +(* ○ CODE-MUST-MATCH: #define BLOCK_SIZE 1024, DICTIONARY_BLOCKS 2048, + DICTIONARY_MEMORY_SIZE (DICTIONARY_BLOCKS*BLOCK_SIZE) in include/vm.h. + ⚠ HUMAN-REVIEW: this is a SMALLER bound than VM_MEMORY_SIZE (2MB vs 5MB). + vm_allot() (src/memory_management.c) -- used by ALIGN via vm_align -- checks + `here` against THIS bound, but ALLOT/,/C,/2, in dictionary_words.c bypass + vm_allot and check `here` directly against VM_MEMORY_SIZE instead. Two + different ceilings for the same pointer -- a real inconsistency in the C + source, transcribed faithfully here rather than picking one. See + StarForth_Dictionary_Words.thy. *) +definition DICTIONARY_MEMORY_SIZE :: nat where "DICTIONARY_MEMORY_SIZE = 2097152" + (* ○ CODE-MUST-MATCH: Makefile default parameters for rolling window. ⚠ HUMAN-REVIEW: These values appear in multiple C files: - ROLLING_WINDOW_SIZE: src/rolling_window_of_truth.c, include/vm.h diff --git a/proof/StarForth_Dictionary_Words.thy b/proof/StarForth_Dictionary_Words.thy new file mode 100644 index 0000000..44bb722 --- /dev/null +++ b/proof/StarForth_Dictionary_Words.thy @@ -0,0 +1,301 @@ +theory StarForth_Dictionary_Words + imports StarForth_Base StarForth_Memory_Words +begin + +(* ========================================================================= + POST-06: Dictionary Pointer Words + Mirrors: src/word_source/dictionary_words.c + + These words manipulate `here` (next free byte offset in the dictionary + arena) and the memory bytes at/around it. `here` is modelled as the + existing `here :: nat` field of vm_state (StarForth_Base.thy:484). + + ── Genuine finding, not modelled as a bug, just noted ────────────────── + `dictionary_word_latest` (LATEST) has an identical body to + `dictionary_word_here` (HERE) -- both simply `vm_push(vm, vm->here)`. + LATEST is documented ("Get latest definition address") as returning the + address of the most recently compiled word, but it does not consult + `vm->latest` (the actual dictionary head pointer) at all; it returns the + free-space pointer instead. Modelled faithfully below as identical to + HERE -- this is what the C code does, not what its doc comment claims. + + ── SP@ / SP! -- NOT MODELLED, see `oops` lemmas at the end ───────────── + Both read/write `vm->dsp` directly as a register distinct from stack + *contents*. The list-based `data_stack` model used throughout this proof + suite has no such register -- depth is `length (data_stack vm)`, always + in lockstep with content. SP! explicitly breaks that lockstep (it can + shrink dsp without popping the now out-of-view elements, leaving them as + C describes "garbage/unused" above the new top). This cannot be expressed + without extending vm_state with a genuine dsp field distinct from list + length -- flagged here, not attempted. + ======================================================================== *) + +(* ── HERE ( -- addr ) ──────────────────────────────────────────────────── *) +(* C: vm_push(vm, vm->here). Unconditional push of the dictionary pointer. *) + +definition forth_here :: "vm_state \ vm_state" where + "forth_here vm = + (if ds_full vm + then set_error vm + else vm\data_stack := word_of_nat (here vm) # data_stack vm\)" + +lemma here_normal: + assumes "\ ds_full vm" + shows "data_stack (forth_here vm) = word_of_nat (here vm) # data_stack vm" + by (simp add: forth_here_def assms) + +lemma here_overflow: + assumes "ds_full vm" + shows "vm_error (forth_here vm)" + by (simp add: forth_here_def set_error_def assms) + +lemma here_preserves_here: + "here (forth_here vm) = here vm" + by (simp add: forth_here_def set_error_def) + +(* ── ALIGN ( -- ) ──────────────────────────────────────────────────────── *) +(* C: vm_align(vm) -- rounds `here` up to the next sizeof(cell_t)=8 boundary + via vm_allot(vm, padding), which bounds-checks against + DICTIONARY_MEMORY_SIZE (see StarForth_Base.thy note above), NOT + VM_MEMORY_SIZE. No stack effect either way. *) + +definition CELL_BYTES :: nat where "CELL_BYTES = 8" + +definition forth_align :: "vm_state \ vm_state" where + "forth_align vm = + (let m = here vm mod CELL_BYTES + in if m = 0 + then vm + else let new_here = here vm + (CELL_BYTES - m) + in if new_here \ DICTIONARY_MEMORY_SIZE + then set_error vm + else vm\here := new_here\)" + +lemma align_already_aligned: + assumes "here vm mod CELL_BYTES = 0" + shows "forth_align vm = vm" + by (simp add: forth_align_def assms) + +lemma align_result_aligned: + assumes "here vm mod CELL_BYTES \ 0" + assumes "here vm + (CELL_BYTES - here vm mod CELL_BYTES) < DICTIONARY_MEMORY_SIZE" + shows "here (forth_align vm) mod CELL_BYTES = 0" + using assms by (simp add: forth_align_def CELL_BYTES_def) presburger + +lemma align_data_stack_unchanged: + "data_stack (forth_align vm) = data_stack vm" + by (auto simp: forth_align_def set_error_def Let_def) + +lemma align_overflow: + assumes "here vm mod CELL_BYTES \ 0" + assumes "here vm + (CELL_BYTES - here vm mod CELL_BYTES) \ DICTIONARY_MEMORY_SIZE" + shows "vm_error (forth_align vm)" + using assms by (simp add: forth_align_def set_error_def) + +(* ── ALLOT ( n -- ) ────────────────────────────────────────────────────── *) +(* C: guards dsp<0 first (empty-stack check), pops n, computes + new_here = vm->here + n as cell_t (add BEFORE checking), errors if + new_here < 0 or new_here > VM_MEMORY_SIZE, else vm->here = new_here. + Note the bound here is VM_MEMORY_SIZE, not DICTIONARY_MEMORY_SIZE -- + ALLOT bypasses vm_allot()/vm_align()'s smaller ceiling entirely. *) + +definition forth_allot :: "vm_state \ vm_state" where + "forth_allot vm = + (case data_stack vm of + [] \ set_error vm + | n # xs \ + let new_here = (word_of_nat (here vm) :: cell) + n + in if new_here unat new_here > VM_MEMORY_SIZE + then set_error (vm\data_stack := xs\) + else vm\data_stack := xs, here := unat new_here\)" + +lemma allot_underflow: + assumes "data_stack vm = []" + shows "vm_error (forth_allot vm)" + by (simp add: forth_allot_def set_error_def assms) + +lemma allot_pops_one: + assumes "data_stack vm = n # xs" + shows "data_stack (forth_allot vm) = xs" + by (simp add: forth_allot_def assms Let_def split: if_split) + +lemma allot_normal: + assumes "data_stack vm = n # xs" + assumes "\ ((word_of_nat (here vm) :: cell) + n VM_MEMORY_SIZE" + shows "here (forth_allot vm) = unat ((word_of_nat (here vm) :: cell) + n)" + using assms by (simp add: forth_allot_def Let_def) + +lemma allot_neg_result_errors: + assumes "data_stack vm = n # xs" + assumes "(word_of_nat (here vm) :: cell) + n ((word_of_nat (here vm) :: cell) + n VM_MEMORY_SIZE" + shows "vm_error (forth_allot vm)" + using assms by (simp add: forth_allot_def set_error_def Let_def) + +(* ── , ( n -- ) : compile a cell at HERE, then here += CELL_BYTES ──────── + ── C, ( c -- ) : compile a byte at HERE, then here += 1 ──────────────── + ── 2, ( d -- ) : compile a double (low then high) at HERE, here += 2*CELL_BYTES + All three: ALIGN first (comma/2comma only -- C, does not align), bound + `here + width > VM_MEMORY_SIZE` -> error (checked AFTER align, before + write). Memory write itself modelled via mem_write (StarForth_Memory_Words + pattern); vm_addr_ok is redundant with the explicit bound check here since + both check the same VM_MEMORY_SIZE ceiling, so we don't duplicate it. *) + +definition forth_comma :: "vm_state \ vm_state" where + "forth_comma vm = + (case data_stack vm of + [] \ set_error vm + | n # xs \ + let vm' = forth_align (vm\data_stack := xs\) + in if vm_error vm' \ here vm' + CELL_BYTES > VM_MEMORY_SIZE + then set_error vm' + else vm'\memory := mem_write (memory vm') (here vm') n, + here := here vm' + CELL_BYTES\)" + +lemma comma_underflow: + assumes "data_stack vm = []" + shows "vm_error (forth_comma vm)" + by (simp add: forth_comma_def set_error_def assms) + +lemma comma_pops_and_writes: + assumes "data_stack vm = n # xs" + assumes "vm' = forth_align (vm\data_stack := xs\)" + assumes "\ vm_error vm'" + assumes "here vm' + CELL_BYTES \ VM_MEMORY_SIZE" + shows "data_stack (forth_comma vm) = xs" + and "mem_read (memory (forth_comma vm)) (here vm') = n" + and "here (forth_comma vm) = here vm' + CELL_BYTES" + using assms by (simp_all add: forth_comma_def mem_write_def mem_read_def Let_def + align_data_stack_unchanged) + +definition forth_c_comma :: "vm_state \ vm_state" where + "forth_c_comma vm = + (case data_stack vm of + [] \ set_error vm + | c # xs \ + if here vm + 1 > VM_MEMORY_SIZE + then set_error (vm\data_stack := xs\) + else vm\data_stack := xs, + memory := mem_write (memory vm) (here vm) (c AND 0xFF), + here := here vm + 1\)" + +lemma c_comma_underflow: + assumes "data_stack vm = []" + shows "vm_error (forth_c_comma vm)" + by (simp add: forth_c_comma_def set_error_def assms) + +lemma c_comma_normal: + assumes "data_stack vm = c # xs" + assumes "here vm + 1 \ VM_MEMORY_SIZE" + shows "data_stack (forth_c_comma vm) = xs" + and "mem_read (memory (forth_c_comma vm)) (here vm) = c AND 0xFF" + and "here (forth_c_comma vm) = here vm + 1" + using assms by (simp_all add: forth_c_comma_def mem_write_def mem_read_def) + +definition forth_2comma :: "vm_state \ vm_state" where + "forth_2comma vm = + (case data_stack vm of + high # low # xs \ + let vm' = forth_align (vm\data_stack := xs\) + in if vm_error vm' \ here vm' + 2 * CELL_BYTES > VM_MEMORY_SIZE + then set_error vm' + else vm'\memory := mem_write (mem_write (memory vm') (here vm') low) + (here vm' + CELL_BYTES) high, + here := here vm' + 2 * CELL_BYTES\ + | _ \ set_error vm)" + +lemma comma2_underflow_nil: + assumes "data_stack vm = []" + shows "vm_error (forth_2comma vm)" + by (simp add: forth_2comma_def set_error_def assms) + +lemma comma2_underflow_one: + assumes "data_stack vm = [x]" + shows "vm_error (forth_2comma vm)" + by (simp add: forth_2comma_def set_error_def assms) + +lemma comma2_normal: + assumes "data_stack vm = high # low # xs" + assumes "vm' = forth_align (vm\data_stack := xs\)" + assumes "\ vm_error vm'" + assumes "here vm' + 2 * CELL_BYTES \ VM_MEMORY_SIZE" + shows "data_stack (forth_2comma vm) = xs" + and "mem_read (memory (forth_2comma vm)) (here vm') = low" + and "mem_read (memory (forth_2comma vm)) (here vm' + CELL_BYTES) = high" + and "here (forth_2comma vm) = here vm' + 2 * CELL_BYTES" + using assms by (simp_all add: forth_2comma_def mem_write_def mem_read_def Let_def + align_data_stack_unchanged CELL_BYTES_def) + +(* ── PAD ( -- addr ) ───────────────────────────────────────────────────── *) +(* C: vm_push(vm, VM_MEMORY_SIZE - 512). A fixed constant, independent of + `here` -- the scratch buffer lives at the top of VM memory, not the + dictionary arena. *) + +definition forth_pad :: "vm_state \ vm_state" where + "forth_pad vm = + (if ds_full vm + then set_error vm + else vm\data_stack := word_of_nat (VM_MEMORY_SIZE - 512) # data_stack vm\)" + +lemma pad_normal: + assumes "\ ds_full vm" + shows "data_stack (forth_pad vm) = word_of_nat (VM_MEMORY_SIZE - 512) # data_stack vm" + by (simp add: forth_pad_def assms) + +lemma pad_overflow: + assumes "ds_full vm" + shows "vm_error (forth_pad vm)" + by (simp add: forth_pad_def set_error_def assms) + +lemma pad_constant_regardless_of_here: + assumes "\ ds_full vm1" "\ ds_full vm2" + assumes "here vm1 \ here vm2" + shows "hd (data_stack (forth_pad vm1)) = hd (data_stack (forth_pad vm2))" + using assms by (simp add: forth_pad_def) + +(* ── LATEST ( -- addr ) ────────────────────────────────────────────────── *) +(* C body is byte-for-byte identical to HERE -- see the top-of-file note. + Modelled as literally the same transition function. *) + +definition forth_latest :: "vm_state \ vm_state" where + "forth_latest = forth_here" + +lemma latest_is_here: + "forth_latest vm = forth_here vm" + by (simp add: forth_latest_def) + +lemma latest_normal: + assumes "\ ds_full vm" + shows "data_stack (forth_latest vm) = word_of_nat (here vm) # data_stack vm" + using assms by (simp add: forth_latest_def forth_here_def) + +(* ── SP@ / SP! -- unmodellable under the list-based stack, see header note ── *) + +lemma sp_fetch_not_modelled: True + \ \SP@ ( -- sp ) pushes vm->dsp, a register the list-based data_stack model + has no independent representation of (dsp is always `length data_stack - + 1` here by construction). Nothing to prove wrong; the model simply + cannot distinguish "SP@ implemented" from "not implemented" since there + is no separate register to read. Left as a documented gap, not a lemma.\ + by simp + +lemma sp_store_not_modelled: True + \ \SP! ( sp -- ) is the concrete case that breaks the model: it sets + vm->dsp to any value \ the current dsp, WITHOUT popping/clearing the + list elements above the new top ("garbage/unused" per the C comment at + src/word_source/dictionary_words.c:196). A list-based data_stack cannot + have a length that disagrees with its own element count -- expressing + SP! faithfully would require splitting `dsp :: nat` out as its own + vm_state field, independent of `length data_stack`, which no other word + in this proof suite needs or uses. Left unmodelled rather than forcing + an incompatible extension onto every other word's proofs.\ + by simp + +end