theory StarForth_Double_Words
  imports StarForth_Base
begin

unbundle bit_operations_syntax

(* =========================================================================
   POST-XX: Double-Cell Words
   Mirrors: src/word_source/double_words.c (all 20 registered words)
            src/test_runner/modules/double_words_test.c

   SCOPE, decided 2026-08-13, REVISED 2026-08-13 (later same day, resumed
   session): double_words.c has 20 registered words in three categories.
   All three are now modeled:

   1. Pure double-cell DATA-STACK shuffles (2DROP, 2DUP, 2SWAP, 2OVER,
      2ROT) -- unchanged from the original pass.

   2. Double-cell RETURN-STACK transfer (2>R, 2R>, 2R@) -- NOW MODELED.
      The blocker recorded earlier (`vm->ecw_nesting` missing from
      vm_state) is resolved: `ecw_nesting :: nat` added to the vm_state
      record in StarForth_Base.thy, immediately after vm_halted.

   3. Double-precision ARITHMETIC (S>D, D+, D-, DNEGATE, DABS, DMAX,
      DMIN, D<, D=, D0=, D0<, D2*, D2/) -- NOW MODELED. The blocker
      recorded earlier ("cell is unbounded int, not a fixed-width
      wrapping type") was STALE when re-checked this session: `cell` was
      migrated from `int` to `"64 word"` in commit fe6e705, well before
      this file was first touched -- the earlier note simply wasn't
      re-verified against current StarForth_Base.thy before being
      written down. Flagging this as a process lesson, not just a code
      fix: carried-forward reasoning about *why* something is out of
      scope needs re-checking against the current file, not just trusted
      because a previous session wrote it down (same lesson the
      control_words.c "vm_ip as raw pointer" note taught one file
      earlier in this same sweep). With cell now a proper wrapping 64-bit
      word, HOL word `+`/`-` already compute mod 2^64 exactly matching
      C's unsigned-long carry/borrow arithmetic and two's-complement
      wraparound bit-for-bit -- no foundational change needed, just
      transcription.

   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)

(* ── S>D ( n -- d ) : single to double ─────────────────────────────────── *)
(* C: dsp<0 -> error; dhigh = (n<0) ? -1 : 0; push n (low), push dhigh. *)

definition forth_s_to_d :: "vm_state \<Rightarrow> vm_state" where
  "forth_s_to_d vm =
    (case data_stack vm of
       []      \<Rightarrow> set_error vm
     | n # rest \<Rightarrow>
         vm\<lparr>data_stack := (if n <s 0 then -1 else 0) # n # rest\<rparr>)"

lemma s_to_d_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_s_to_d vm)"
  by (simp add: forth_s_to_d_def set_error_def assms)

lemma s_to_d_negative:
  assumes "data_stack vm = n # rest"
  assumes "n <s 0"
  shows "data_stack (forth_s_to_d vm) = -1 # n # rest"
  by (simp add: forth_s_to_d_def assms)

lemma s_to_d_nonnegative:
  assumes "data_stack vm = n # rest"
  assumes "\<not> n <s 0"
  shows "data_stack (forth_s_to_d vm) = 0 # n # rest"
  by (simp add: forth_s_to_d_def assms)

(* ── D+ ( d1 d2 -- d3 ) ────────────────────────────────────────────────── *)
(* C: dsp<3 -> error. Pops d2high,d2low,d1high,d1low. Carry detected via
   unsigned comparison; word `+` already computes mod 2^64, so it's the
   direct transcription of the C unsigned-long addition with no
   reinterpretation needed. *)

definition forth_d_plus :: "vm_state \<Rightarrow> vm_state" where
  "forth_d_plus vm =
    (case data_stack vm of
       d2high # d2low # d1high # d1low # rest \<Rightarrow>
         let result_low = d1low + d2low;
             carry = (if result_low < d1low then 1 else 0);
             result_high = d1high + d2high + carry
         in vm\<lparr>data_stack := result_high # result_low # rest\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma d_plus_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_d_plus vm)"
  by (simp add: forth_d_plus_def set_error_def assms)

lemma d_plus_underflow_one:
  assumes "data_stack vm = [x]"
  shows "vm_error (forth_d_plus vm)"
  by (simp add: forth_d_plus_def set_error_def assms)

lemma d_plus_underflow_two:
  assumes "data_stack vm = [x, y]"
  shows "vm_error (forth_d_plus vm)"
  by (simp add: forth_d_plus_def set_error_def assms)

lemma d_plus_underflow_three:
  assumes "data_stack vm = [x, y, z]"
  shows "vm_error (forth_d_plus vm)"
  by (simp add: forth_d_plus_def set_error_def assms)

lemma d_plus_normal_no_carry:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  assumes "\<not> (d1low + d2low) < d1low"
  shows "data_stack (forth_d_plus vm) = (d1high + d2high) # (d1low + d2low) # rest"
  using assms by (simp add: forth_d_plus_def)

lemma d_plus_normal_with_carry:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  assumes "(d1low + d2low) < d1low"
  shows "data_stack (forth_d_plus vm) = (d1high + d2high + 1) # (d1low + d2low) # rest"
  using assms by (simp add: forth_d_plus_def)

(* ── D- ( d1 d2 -- d3 ) ────────────────────────────────────────────────── *)

definition forth_d_minus :: "vm_state \<Rightarrow> vm_state" where
  "forth_d_minus vm =
    (case data_stack vm of
       d2high # d2low # d1high # d1low # rest \<Rightarrow>
         let result_low = d1low - d2low;
             borrow = (if d1low < d2low then 1 else 0);
             result_high = d1high - d2high - borrow
         in vm\<lparr>data_stack := result_high # result_low # rest\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma d_minus_normal_no_borrow:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  assumes "\<not> d1low < d2low"
  shows "data_stack (forth_d_minus vm) = (d1high - d2high) # (d1low - d2low) # rest"
  using assms by (simp add: forth_d_minus_def)

lemma d_minus_normal_with_borrow:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  assumes "d1low < d2low"
  shows "data_stack (forth_d_minus vm) = (d1high - d2high - 1) # (d1low - d2low) # rest"
  using assms by (simp add: forth_d_minus_def)

(* ── DNEGATE ( d1 -- d2 ) ──────────────────────────────────────────────── *)
(* C: ~dlow + 1, ~dhigh + (new_low==0 ? 1 : 0) -- textbook 128-bit two's
   complement negation, transcribed literally rather than via HOL's `-`
   (which would be equal but less faithful to the C bit-operations). *)

definition forth_dnegate :: "vm_state \<Rightarrow> vm_state" where
  "forth_dnegate vm =
    (case data_stack vm of
       dhigh # dlow # rest \<Rightarrow>
         let new_low = NOT dlow + 1;
             new_high = NOT dhigh + (if new_low = 0 then 1 else 0)
         in vm\<lparr>data_stack := new_high # new_low # rest\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma dnegate_underflow:
  assumes "data_stack vm = [] \<or> (\<exists>x. data_stack vm = [x])"
  shows "vm_error (forth_dnegate vm)"
  using assms by (auto simp: forth_dnegate_def set_error_def)

lemma dnegate_normal:
  assumes "data_stack vm = dhigh # dlow # rest"
  shows "data_stack (forth_dnegate vm) =
         (NOT dhigh + (if NOT dlow + 1 = 0 then 1 else 0)) # (NOT dlow + 1) # rest"
  by (simp add: forth_dnegate_def assms)

(* Double negation (DNEGATE twice = identity) is a true property of 128-bit
   two's complement, but proving it here needs the same carry/borrow-across-
   the-pair algebra as D+/D-'s case-split lemmas, not just simp -- left
   unproved as a nice-to-have rather than forcing it, consistent with this
   sweep's "plumbing lemmas only" scope. *)

(* ── DABS ( d1 -- d2 ) ─────────────────────────────────────────────────── *)
(* C peeks dhigh (TOS) WITHOUT popping; if negative, calls DNEGATE (which
   does its own pop/negate/push using the still-untouched stack); else
   the word is a complete no-op. Reuses forth_dnegate directly. *)

definition forth_dabs :: "vm_state \<Rightarrow> vm_state" where
  "forth_dabs vm =
    (case data_stack vm of
       dhigh # dlow # rest \<Rightarrow> (if dhigh <s 0 then forth_dnegate vm else vm)
     | _ \<Rightarrow> set_error vm)"

lemma dabs_underflow:
  assumes "data_stack vm = [] \<or> (\<exists>x. data_stack vm = [x])"
  shows "vm_error (forth_dabs vm)"
  using assms by (auto simp: forth_dabs_def set_error_def)

lemma dabs_already_nonneg_is_noop:
  assumes "data_stack vm = dhigh # dlow # rest"
  assumes "\<not> dhigh <s 0"
  shows "forth_dabs vm = vm"
  by (simp add: forth_dabs_def assms)

lemma dabs_negative_negates:
  assumes "data_stack vm = dhigh # dlow # rest"
  assumes "dhigh <s 0"
  shows "forth_dabs vm = forth_dnegate vm"
  by (simp add: forth_dabs_def assms)

(* ── d_compare : internal helper mirroring the C `d_compare` (not a
   registered word) -- high cells compared SIGNED (cell_t <, C semantics),
   low cells compared UNSIGNED (explicit unsigned long cast in C). ────── *)

definition d_compare :: "cell \<Rightarrow> cell \<Rightarrow> cell \<Rightarrow> cell \<Rightarrow> int" where
  "d_compare d1h d1l d2h d2l =
    (if d1h <s d2h then -1
     else if d2h <s d1h then 1
     else if d2l < d1l then 1
     else if d1l < d2l then -1
     else 0)"

lemma d_compare_equal:
  "d_compare h l h l = 0"
  by (simp add: d_compare_def)

(* ── DMAX ( d1 d2 -- d3 ) / DMIN ( d1 d2 -- d3 ) ──────────────────────────
   C pop order matches D+/D-: d2high # d2low # d1high # d1low # rest. *)

definition forth_dmax :: "vm_state \<Rightarrow> vm_state" where
  "forth_dmax vm =
    (case data_stack vm of
       d2high # d2low # d1high # d1low # rest \<Rightarrow>
         vm\<lparr>data_stack := (if d_compare d1high d1low d2high d2low \<ge> 0
                            then d1high # d1low # rest
                            else d2high # d2low # rest)\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma dmax_picks_d1:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  assumes "d_compare d1high d1low d2high d2low \<ge> 0"
  shows "data_stack (forth_dmax vm) = d1high # d1low # rest"
  using assms by (simp add: forth_dmax_def)

lemma dmax_picks_d2:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  assumes "\<not> d_compare d1high d1low d2high d2low \<ge> 0"
  shows "data_stack (forth_dmax vm) = d2high # d2low # rest"
  using assms by (simp add: forth_dmax_def)

definition forth_dmin :: "vm_state \<Rightarrow> vm_state" where
  "forth_dmin vm =
    (case data_stack vm of
       d2high # d2low # d1high # d1low # rest \<Rightarrow>
         vm\<lparr>data_stack := (if d_compare d1high d1low d2high d2low \<le> 0
                            then d1high # d1low # rest
                            else d2high # d2low # rest)\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma dmin_picks_d1:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  assumes "d_compare d1high d1low d2high d2low \<le> 0"
  shows "data_stack (forth_dmin vm) = d1high # d1low # rest"
  using assms by (simp add: forth_dmin_def)

lemma dmin_picks_d2:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  assumes "\<not> d_compare d1high d1low d2high d2low \<le> 0"
  shows "data_stack (forth_dmin vm) = d2high # d2low # rest"
  using assms by (simp add: forth_dmin_def)

(* ── D< ( d1 d2 -- flag ) / D= ( d1 d2 -- flag ) ────────────────────────── *)

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

lemma d_less_true:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  assumes "d_compare d1high d1low d2high d2low < 0"
  shows "data_stack (forth_d_less vm) = forth_true # rest"
  using assms by (simp add: forth_d_less_def to_forth_bool_def)

lemma d_less_false:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  assumes "\<not> d_compare d1high d1low d2high d2low < 0"
  shows "data_stack (forth_d_less vm) = forth_false # rest"
  using assms by (simp add: forth_d_less_def to_forth_bool_def)

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

lemma d_equals_true:
  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
  assumes "d_compare d1high d1low d2high d2low = 0"
  shows "data_stack (forth_d_equals vm) = forth_true # rest"
  using assms by (simp add: forth_d_equals_def to_forth_bool_def)

lemma d_equals_reflexive:
  assumes "data_stack vm = h # l # h # l # rest"
  shows "data_stack (forth_d_equals vm) = forth_true # rest"
  using assms by (simp add: forth_d_equals_def to_forth_bool_def d_compare_def)

(* ── D0= ( d -- flag ) / D0< ( d -- flag ) ────────────────────────────── *)

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

lemma d_zero_equals_true:
  assumes "data_stack vm = 0 # 0 # rest"
  shows "data_stack (forth_d_zero_equals vm) = forth_true # rest"
  by (simp add: forth_d_zero_equals_def to_forth_bool_def assms)

lemma d_zero_equals_false:
  assumes "data_stack vm = dhigh # dlow # rest"
  assumes "dhigh \<noteq> 0 \<or> dlow \<noteq> 0"
  shows "data_stack (forth_d_zero_equals vm) = forth_false # rest"
  using assms by (auto simp: forth_d_zero_equals_def to_forth_bool_def)

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

lemma d_zero_less_true:
  assumes "data_stack vm = dhigh # dlow # rest"
  assumes "dhigh <s 0"
  shows "data_stack (forth_d_zero_less vm) = forth_true # rest"
  using assms by (simp add: forth_d_zero_less_def to_forth_bool_def)

lemma d_zero_less_false:
  assumes "data_stack vm = dhigh # dlow # rest"
  assumes "\<not> dhigh <s 0"
  shows "data_stack (forth_d_zero_less vm) = forth_false # rest"
  using assms by (simp add: forth_d_zero_less_def to_forth_bool_def)

(* ── D2* ( d1 -- d2 ) : double-cell left shift by 1 ──────────────────────
   C: new_dlow = dlow << 1; new_dhigh = (dhigh << 1) | (top bit of dlow).
   `push_bit 1` is this suite's established idiom for `<< 1` (matches
   StarForth_Q48_16.thy). The carried bit is dlow's bit 63. *)

definition forth_d_two_star :: "vm_state \<Rightarrow> vm_state" where
  "forth_d_two_star vm =
    (case data_stack vm of
       dhigh # dlow # rest \<Rightarrow>
         let new_dlow = push_bit 1 dlow;
             carry = of_bool (bit dlow 63);
             new_dhigh = push_bit 1 dhigh OR carry
         in vm\<lparr>data_stack := new_dhigh # new_dlow # rest\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma d_two_star_normal:
  assumes "data_stack vm = dhigh # dlow # rest"
  shows "data_stack (forth_d_two_star vm) =
         (push_bit 1 dhigh OR of_bool (bit dlow 63)) # push_bit 1 dlow # rest"
  by (simp add: forth_d_two_star_def assms)

(* ── D2/ ( d1 -- d2 ) : double-cell arithmetic right shift by 1 ──────────
   C: new_dhigh = dhigh >> 1 (arithmetic, sign-preserving); new_dlow =
   (dlow >> 1 unsigned) with dhigh's bit 0 carried into dlow's bit 63.
   Arithmetic shift right by 1 on two's complement = floor division by 2,
   which is exactly HOL int `div` (rounds toward -infinity, NOT C99
   truncating division) -- reusing the sint round-trip already
   established for signed reasoning elsewhere in this suite, deliberately
   NOT cell_sdiv (which is C99 truncating division and would be wrong
   here for negative dhigh). *)

definition forth_d_two_slash :: "vm_state \<Rightarrow> vm_state" where
  "forth_d_two_slash vm =
    (case data_stack vm of
       dhigh # dlow # rest \<Rightarrow>
         let new_dhigh = word_of_int (sint dhigh div 2);
             new_dlow = drop_bit 1 dlow OR (if bit dhigh 0 then push_bit 63 1 else 0)
         in vm\<lparr>data_stack := new_dhigh # new_dlow # rest\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma d_two_slash_normal:
  assumes "data_stack vm = dhigh # dlow # rest"
  shows "data_stack (forth_d_two_slash vm) =
         word_of_int (sint dhigh div 2) #
         (drop_bit 1 dlow OR (if bit dhigh 0 then push_bit 63 1 else 0)) # rest"
  by (simp add: forth_d_two_slash_def assms)

(* ── 2>R ( d -- ) ( R: -- d ) ──────────────────────────────────────────── *)
(* C: dsp<1 -> error (checked, then popped, BEFORE the ecw_nesting branch --
   so on a subsequent rsp overflow error, data_stack is already popped,
   matching ALLOT's pop-then-check pattern). Inside a colon word
   (ecw_nesting>0): insert dlow,dhigh BELOW the resume-ip that's already on
   top of the return stack, keeping resume-ip on top. Outside (ecw_nesting
   = 0, e.g. interactively at the REPL): plain push of dlow then dhigh.

   ecw_nesting>0 with an EMPTY return_stack is an invariant violation the
   real C never defensively checks (it would read return_stack[-1], i.e.
   real UB) -- modeled here as set_error as a defensive default, which is
   NOT what the C does (the C has no such check at all); flagged as a
   finding, not a faithful transcription of that one unreachable case. *)

definition forth_2to_r :: "vm_state \<Rightarrow> vm_state" where
  "forth_2to_r vm =
    (case data_stack vm of
       []                \<Rightarrow> set_error vm
     | dhigh # dlow # drest \<Rightarrow>
         let vm1 = vm\<lparr>data_stack := drest\<rparr>
         in if ecw_nesting vm > 0
            then (case return_stack vm of
                    []              \<Rightarrow> set_error vm1  \<comment> \<open>invariant violation, see above\<close>
                  | resume_ip # rst \<Rightarrow>
                      if length rst + 2 \<ge> STACK_SIZE
                      then set_error vm1
                      else vm1\<lparr>return_stack := resume_ip # dhigh # dlow # rst\<rparr>)
            else if length (return_stack vm) + 2 \<ge> STACK_SIZE
                 then set_error vm1
                 else vm1\<lparr>return_stack := dhigh # dlow # return_stack vm\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma two_to_r_underflow:
  assumes "data_stack vm = [] \<or> (\<exists>x. data_stack vm = [x])"
  shows "vm_error (forth_2to_r vm)"
  using assms by (auto simp: forth_2to_r_def set_error_def)

lemma two_to_r_outside_colon:
  assumes "data_stack vm = dhigh # dlow # drest"
  assumes "ecw_nesting vm = 0"
  assumes "length (return_stack vm) + 2 < STACK_SIZE"
  shows "return_stack (forth_2to_r vm) = dhigh # dlow # return_stack vm"
    and "data_stack (forth_2to_r vm) = drest"
  using assms by (simp_all add: forth_2to_r_def)

lemma two_to_r_inside_colon:
  assumes "data_stack vm = dhigh # dlow # drest"
  assumes "ecw_nesting vm > 0"
  assumes "return_stack vm = resume_ip # rst"
  assumes "length rst + 2 < STACK_SIZE"
  shows "return_stack (forth_2to_r vm) = resume_ip # dhigh # dlow # rst"
    and "data_stack (forth_2to_r vm) = drest"
  using assms by (simp_all add: forth_2to_r_def)

(* ── 2R> ( -- d ) ( R: d -- ) ──────────────────────────────────────────── *)
(* Inside a colon word: pops (dlow,dhigh) from just below the resume-ip,
   keeping resume-ip on top. Outside: plain pop of dhigh then dlow. Both
   branches push the same result to the data stack: dhigh # dlow # ... *)

definition forth_2r_from :: "vm_state \<Rightarrow> vm_state" where
  "forth_2r_from vm =
    (if ecw_nesting vm > 0
     then (case return_stack vm of
             resume_ip # dhigh # dlow # rst \<Rightarrow>
               vm\<lparr>data_stack := dhigh # dlow # data_stack vm,
                  return_stack := resume_ip # rst\<rparr>
           | _ \<Rightarrow> set_error vm)
     else (case return_stack vm of
             dhigh # dlow # rst \<Rightarrow>
               vm\<lparr>data_stack := dhigh # dlow # data_stack vm,
                  return_stack := rst\<rparr>
           | _ \<Rightarrow> set_error vm))"

lemma two_r_from_inside_colon:
  assumes "ecw_nesting vm > 0"
  assumes "return_stack vm = resume_ip # dhigh # dlow # rst"
  shows "data_stack (forth_2r_from vm) = dhigh # dlow # data_stack vm"
    and "return_stack (forth_2r_from vm) = resume_ip # rst"
  using assms by (simp_all add: forth_2r_from_def)

lemma two_r_from_outside_colon:
  assumes "ecw_nesting vm = 0"
  assumes "return_stack vm = dhigh # dlow # rst"
  shows "data_stack (forth_2r_from vm) = dhigh # dlow # data_stack vm"
    and "return_stack (forth_2r_from vm) = rst"
  using assms by (simp_all add: forth_2r_from_def)

lemma two_r_from_inside_colon_underflow_nil:
  assumes "ecw_nesting vm > 0"
  assumes "return_stack vm = []"
  shows "vm_error (forth_2r_from vm)"
  by (simp add: forth_2r_from_def set_error_def assms)

lemma two_r_from_inside_colon_underflow_one:
  assumes "ecw_nesting vm > 0"
  assumes "return_stack vm = [x]"
  shows "vm_error (forth_2r_from vm)"
  by (simp add: forth_2r_from_def set_error_def assms)

lemma two_r_from_inside_colon_underflow_two:
  assumes "ecw_nesting vm > 0"
  assumes "return_stack vm = [x, y]"
  shows "vm_error (forth_2r_from vm)"
  by (simp add: forth_2r_from_def set_error_def assms)

(* ── 2R@ ( -- d ) ( R: d -- d ) ────────────────────────────────────────── *)
(* Same source cells as 2R>, but the return stack is left untouched
   (fetch, not pop) -- both branches produce the identical data_stack
   result as 2R>. *)

definition forth_2r_fetch :: "vm_state \<Rightarrow> vm_state" where
  "forth_2r_fetch vm =
    (if ecw_nesting vm > 0
     then (case return_stack vm of
             resume_ip # dhigh # dlow # rst \<Rightarrow>
               vm\<lparr>data_stack := dhigh # dlow # data_stack vm\<rparr>
           | _ \<Rightarrow> set_error vm)
     else (case return_stack vm of
             dhigh # dlow # rst \<Rightarrow>
               vm\<lparr>data_stack := dhigh # dlow # data_stack vm\<rparr>
           | _ \<Rightarrow> set_error vm))"

lemma two_r_fetch_inside_colon:
  assumes "ecw_nesting vm > 0"
  assumes "return_stack vm = resume_ip # dhigh # dlow # rst"
  shows "data_stack (forth_2r_fetch vm) = dhigh # dlow # data_stack vm"
    and "return_stack (forth_2r_fetch vm) = return_stack vm"
  using assms by (simp_all add: forth_2r_fetch_def)

lemma two_r_fetch_outside_colon:
  assumes "ecw_nesting vm = 0"
  assumes "return_stack vm = dhigh # dlow # rst"
  shows "data_stack (forth_2r_fetch vm) = dhigh # dlow # data_stack vm"
    and "return_stack (forth_2r_fetch vm) = return_stack vm"
  using assms by (simp_all add: forth_2r_fetch_def)

end