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