Robert Allan JamesandClaude Sonnet 5
92474c5219
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 <noreply@anthropic.com>
302 lines
14 KiB
Plaintext
302 lines
14 KiB
Plaintext
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 \<Rightarrow> vm_state" where
|
|
"forth_here vm =
|
|
(if ds_full vm
|
|
then set_error vm
|
|
else vm\<lparr>data_stack := word_of_nat (here vm) # data_stack vm\<rparr>)"
|
|
|
|
lemma here_normal:
|
|
assumes "\<not> 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 \<Rightarrow> 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 \<ge> DICTIONARY_MEMORY_SIZE
|
|
then set_error vm
|
|
else vm\<lparr>here := new_here\<rparr>)"
|
|
|
|
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 \<noteq> 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 \<noteq> 0"
|
|
assumes "here vm + (CELL_BYTES - here vm mod CELL_BYTES) \<ge> 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 \<Rightarrow> vm_state" where
|
|
"forth_allot vm =
|
|
(case data_stack vm of
|
|
[] \<Rightarrow> set_error vm
|
|
| n # xs \<Rightarrow>
|
|
let new_here = (word_of_nat (here vm) :: cell) + n
|
|
in if new_here <s 0 \<or> unat new_here > VM_MEMORY_SIZE
|
|
then set_error (vm\<lparr>data_stack := xs\<rparr>)
|
|
else vm\<lparr>data_stack := xs, here := unat new_here\<rparr>)"
|
|
|
|
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 "\<not> ((word_of_nat (here vm) :: cell) + n <s 0)"
|
|
assumes "unat ((word_of_nat (here vm) :: cell) + n) \<le> 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 <s 0"
|
|
shows "vm_error (forth_allot vm)"
|
|
using assms by (simp add: forth_allot_def set_error_def Let_def)
|
|
|
|
lemma allot_over_limit_errors:
|
|
assumes "data_stack vm = n # xs"
|
|
assumes "\<not> ((word_of_nat (here vm) :: cell) + n <s 0)"
|
|
assumes "unat ((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 \<Rightarrow> vm_state" where
|
|
"forth_comma vm =
|
|
(case data_stack vm of
|
|
[] \<Rightarrow> set_error vm
|
|
| n # xs \<Rightarrow>
|
|
let vm' = forth_align (vm\<lparr>data_stack := xs\<rparr>)
|
|
in if vm_error vm' \<or> here vm' + CELL_BYTES > VM_MEMORY_SIZE
|
|
then set_error vm'
|
|
else vm'\<lparr>memory := mem_write (memory vm') (here vm') n,
|
|
here := here vm' + CELL_BYTES\<rparr>)"
|
|
|
|
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\<lparr>data_stack := xs\<rparr>)"
|
|
assumes "\<not> vm_error vm'"
|
|
assumes "here vm' + CELL_BYTES \<le> 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 \<Rightarrow> vm_state" where
|
|
"forth_c_comma vm =
|
|
(case data_stack vm of
|
|
[] \<Rightarrow> set_error vm
|
|
| c # xs \<Rightarrow>
|
|
if here vm + 1 > VM_MEMORY_SIZE
|
|
then set_error (vm\<lparr>data_stack := xs\<rparr>)
|
|
else vm\<lparr>data_stack := xs,
|
|
memory := mem_write (memory vm) (here vm) (c AND 0xFF),
|
|
here := here vm + 1\<rparr>)"
|
|
|
|
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 \<le> 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 \<Rightarrow> vm_state" where
|
|
"forth_2comma vm =
|
|
(case data_stack vm of
|
|
high # low # xs \<Rightarrow>
|
|
let vm' = forth_align (vm\<lparr>data_stack := xs\<rparr>)
|
|
in if vm_error vm' \<or> here vm' + 2 * CELL_BYTES > VM_MEMORY_SIZE
|
|
then set_error vm'
|
|
else vm'\<lparr>memory := mem_write (mem_write (memory vm') (here vm') low)
|
|
(here vm' + CELL_BYTES) high,
|
|
here := here vm' + 2 * CELL_BYTES\<rparr>
|
|
| _ \<Rightarrow> 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\<lparr>data_stack := xs\<rparr>)"
|
|
assumes "\<not> vm_error vm'"
|
|
assumes "here vm' + 2 * CELL_BYTES \<le> 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 \<Rightarrow> vm_state" where
|
|
"forth_pad vm =
|
|
(if ds_full vm
|
|
then set_error vm
|
|
else vm\<lparr>data_stack := word_of_nat (VM_MEMORY_SIZE - 512) # data_stack vm\<rparr>)"
|
|
|
|
lemma pad_normal:
|
|
assumes "\<not> 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 "\<not> ds_full vm1" "\<not> ds_full vm2"
|
|
assumes "here vm1 \<noteq> 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 \<Rightarrow> 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 "\<not> 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
|
|
\<comment> \<open>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.\<close>
|
|
by simp
|
|
|
|
lemma sp_store_not_modelled: True
|
|
\<comment> \<open>SP! ( sp -- ) is the concrete case that breaks the model: it sets
|
|
vm->dsp to any value \<le> 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.\<close>
|
|
by simp
|
|
|
|
end
|