theory StarForth_Double_Words
  imports StarForth_Base
begin

(* =========================================================================
   POST-XX: Double-Cell Stack Manipulation Words
   Mirrors: src/word_source/double_words.c (partial -- see SCOPE below)
            src/test_runner/modules/double_words_test.c

   SCOPE, decided 2026-08-13: double_words.c has 20 registered words in
   three categories. Only the first is modeled here:

   1. Pure double-cell DATA-STACK shuffles (2DROP, 2DUP, 2SWAP, 2OVER,
      2ROT) -- modeled below. These only rearrange data_stack list
      elements; nothing about their correctness depends on cell's exact
      representation or on any vm_state field this theory doesn't already
      track.

   2. Double-cell RETURN-STACK transfer (2>R, 2R>, 2R@) -- NOT modeled.
      The real C (double_words.c:330-382) branches on
      "vm->ecw_nesting > 0" (execute_colon_word re-entrancy depth), a VM
      field that does not exist anywhere in StarForth_Base.thy's
      vm_state record. Modeling these words correctly requires adding
      ecw_nesting to vm_state first -- a model-extension decision, not
      something to add as a side effect of this file.

   3. Double-precision ARITHMETIC (S>D, D+, D-, DNEGATE, DABS, DMAX,
      DMIN, D<, D=, D0=, D0<, D2*, D2/) -- NOT modeled. The real C
      implementations (double_words.c:56-250ish) depend on cell_t being
      a fixed-width (64-bit, "signed long") wrapping integer type --
      D+/D- explicitly do carry/borrow detection via "unsigned long"
      arithmetic and wraparound, DNEGATE uses bitwise complement (~) with
      wraparound. This theory's "type_synonym cell = int" (StarForth_Base)
      is unbounded/arbitrary-precision, not a fixed-width wrapping type,
      so none of this carry/wraparound reasoning is even expressible as
      currently modeled. Correctly formalizing these words needs a
      foundational decision -- change cell's representation to a 64-bit
      word type (matching StarForth_Q48_16.thy's own "64 word" approach)
      or add explicit range side-conditions everywhere -- that ripples
      into all 23 already-verified theories built on today's plain-int
      cell. Not decided or attempted here; flagged for a dedicated pass.

   Every word modeled below is a direct structural analog of an
   already-covered single-cell word in StarForth_Stack_Words.thy (DUP,
   SWAP, OVER, ROT) or StarForth_Return_Stack_Words.thy, just operating
   on cell PAIRS instead of single cells. Convention throughout, matching
   the C comments: a double d is pushed as (dlow dhigh) with dhigh on
   top -- i.e. in this list's head=TOS convention, a double at the top of
   stack is "dhigh # dlow # rest".

   None of the C implementations below check ds_full before pushing
   (confirmed by reading double_words.c in full) -- not modeled here
   either, to stay faithful to the real source rather than inventing a
   guard that doesn't exist.
   ======================================================================== *)

(* ── 2DROP ( d -- ) ─────────────────────────────────────────────────────── *)
(* src/word_source/double_words.c:250-258. Guard: dsp \<ge> 1 (at least two
   cells present). *)

definition forth_2drop :: "vm_state \<Rightarrow> vm_state" where
  "forth_2drop vm =
    (case data_stack vm of
       _ # _ # rest \<Rightarrow> vm\<lparr>data_stack := rest\<rparr>
     | _            \<Rightarrow> set_error vm)"

lemma two_drop_normal:
  assumes "data_stack vm = dhigh # dlow # rest"
  shows "data_stack (forth_2drop vm) = rest"
  by (simp add: forth_2drop_def assms)

lemma two_drop_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_2drop vm)"
  by (simp add: forth_2drop_def set_error_def assms)

lemma two_drop_underflow_one:
  assumes "data_stack vm = [x]"
  shows "vm_error (forth_2drop vm)"
  by (simp add: forth_2drop_def set_error_def assms)

(* ── 2DUP ( d -- d d ) ──────────────────────────────────────────────────── *)
(* src/word_source/double_words.c:260-272. Guard: dsp \<ge> 1. *)

definition forth_2dup :: "vm_state \<Rightarrow> vm_state" where
  "forth_2dup vm =
    (case data_stack vm of
       dhigh # dlow # rest \<Rightarrow>
         vm\<lparr>data_stack := dhigh # dlow # dhigh # dlow # rest\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma two_dup_normal:
  assumes "data_stack vm = dhigh # dlow # rest"
  shows "data_stack (forth_2dup vm) = dhigh # dlow # dhigh # dlow # rest"
  by (simp add: forth_2dup_def assms)

lemma two_dup_depth:
  assumes "data_stack vm = dhigh # dlow # rest"
  shows "length (data_stack (forth_2dup vm)) = length (data_stack vm) + 2"
  by (simp add: forth_2dup_def assms)

lemma two_dup_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_2dup vm)"
  by (simp add: forth_2dup_def set_error_def assms)

lemma two_dup_underflow_one:
  assumes "data_stack vm = [x]"
  shows "vm_error (forth_2dup vm)"
  by (simp add: forth_2dup_def set_error_def assms)

(* ── 2SWAP ( d1 d2 -- d2 d1 ) ───────────────────────────────────────────── *)
(* src/word_source/double_words.c:274-290. Guard: dsp \<ge> 3 (four cells). *)

definition forth_2swap :: "vm_state \<Rightarrow> vm_state" where
  "forth_2swap vm =
    (case data_stack vm of
       d2high # d2low # d1high # d1low # rest \<Rightarrow>
         vm\<lparr>data_stack := d1high # d1low # d2high # d2low # rest\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma two_swap_normal:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  shows "data_stack (forth_2swap vm) = d1high # d1low # d2high # d2low # rest"
  by (simp add: forth_2swap_def assms)

lemma two_swap_depth_preserved:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  shows "length (data_stack (forth_2swap vm)) = length (data_stack vm)"
  by (simp add: forth_2swap_def assms)

(* 2SWAP is its own inverse. *)
lemma two_swap_involutive:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  assumes "data_stack vm' = data_stack (forth_2swap vm)"
  shows "data_stack (forth_2swap vm') = data_stack vm"
  using assms by (simp add: forth_2swap_def)

lemma two_swap_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_2swap vm)"
  by (simp add: forth_2swap_def set_error_def assms)

lemma two_swap_underflow_one:
  assumes "data_stack vm = [x]"
  shows "vm_error (forth_2swap vm)"
  by (simp add: forth_2swap_def set_error_def assms)

lemma two_swap_underflow_two:
  assumes "data_stack vm = [x, y]"
  shows "vm_error (forth_2swap vm)"
  by (simp add: forth_2swap_def set_error_def assms)

lemma two_swap_underflow_three:
  assumes "data_stack vm = [x, y, z]"
  shows "vm_error (forth_2swap vm)"
  by (simp add: forth_2swap_def set_error_def assms)

(* ── 2OVER ( d1 d2 -- d1 d2 d1 ) ────────────────────────────────────────── *)
(* src/word_source/double_words.c:292-305. Guard: dsp \<ge> 3. *)

definition forth_2over :: "vm_state \<Rightarrow> vm_state" where
  "forth_2over vm =
    (case data_stack vm of
       d2high # d2low # d1high # d1low # rest \<Rightarrow>
         vm\<lparr>data_stack := d1high # d1low # d2high # d2low # d1high # d1low # rest\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma two_over_normal:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  shows "data_stack (forth_2over vm)
       = d1high # d1low # d2high # d2low # d1high # d1low # rest"
  by (simp add: forth_2over_def assms)

lemma two_over_depth:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  shows "length (data_stack (forth_2over vm)) = length (data_stack vm) + 2"
  by (simp add: forth_2over_def assms)

(* ── 2ROT ( d1 d2 d3 -- d2 d3 d1 ) ──────────────────────────────────────── *)
(* src/word_source/double_words.c:307-327. Guard: dsp \<ge> 5 (six cells).
   Hand-verified against the doc comment's own semantics: d1 (deepest)
   moves to the top, d2 and d3 shift down keeping their relative order. *)

definition forth_2rot :: "vm_state \<Rightarrow> vm_state" where
  "forth_2rot vm =
    (case data_stack vm of
       d3high # d3low # d2high # d2low # d1high # d1low # rest \<Rightarrow>
         vm\<lparr>data_stack :=
              d1high # d1low # d3high # d3low # d2high # d2low # rest\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma two_rot_normal:
  assumes "data_stack vm
         = d3high # d3low # d2high # d2low # d1high # d1low # rest"
  shows "data_stack (forth_2rot vm)
       = d1high # d1low # d3high # d3low # d2high # d2low # rest"
  by (simp add: forth_2rot_def assms)

lemma two_rot_depth_preserved:
  assumes "data_stack vm
         = d3high # d3low # d2high # d2low # d1high # d1low # rest"
  shows "length (data_stack (forth_2rot vm)) = length (data_stack vm)"
  by (simp add: forth_2rot_def assms)

end