diff --git a/proof/StarForth_Base.thy b/proof/StarForth_Base.thy
index 84fd05f..444660c 100644
--- a/proof/StarForth_Base.thy
+++ b/proof/StarForth_Base.thy
@@ -509,6 +509,11 @@ record vm_state =
   vm_base       :: cell                           \<comment> \<open>numeric base for I/O (2..36)\<close>
   vm_error      :: bool
   vm_halted     :: bool
+  (* ○ CODE-MUST-MATCH: C: int ecw_nesting (include/vm.h:390) -- depth of
+     execute_colon_word call stack; >0 means inside a colon word. Modeled as
+     nat (C only ever tests ecw_nesting > 0, never negative values in any
+     reachable path) -- see StarForth_Double_Words.thy's 2>R/2R>/2R@. *)
+  ecw_nesting   :: nat
 
   (* ── Physics Loop #1: Execution heat tracking ───────────────────────── *)
   (* ○ CODE-MUST-MATCH: heat_threshold_{25th,50th,75th} in C VM struct.
diff --git a/proof/StarForth_Double_Words.thy b/proof/StarForth_Double_Words.thy
index cadc0ea..b13d441 100644
--- a/proof/StarForth_Double_Words.thy
+++ b/proof/StarForth_Double_Words.thy
@@ -2,43 +2,42 @@ theory StarForth_Double_Words
   imports StarForth_Base
 begin
 
+unbundle bit_operations_syntax
+
 (* =========================================================================
-   POST-XX: Double-Cell Stack Manipulation Words
-   Mirrors: src/word_source/double_words.c (partial -- see SCOPE below)
+   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: double_words.c has 20 registered words in
-   three categories. Only the first is modeled here:
+   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) -- 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.
+      2ROT) -- unchanged from the original pass.
 
-   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.
+   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/) -- 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.
+      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,
@@ -203,4 +202,483 @@ lemma two_rot_depth_preserved:
   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