proof/: add StarForth_Mixed_Arithmetic_Words.thy (M+/M-/MOD//MOD/*//*/MOD)

Covers word_source/mixed_arithmetic_words.c. Two genuine findings recorded
in comments rather than fixed:

- register_mixed_arithmetic_words registers MOD and /MOD a second time,
  after arithmetic_words.c's own registrations; vm_create_word links new
  entries at the head of vm->latest and FIND scans from vm->latest forward,
  so arithmetic_words.c's MOD/​/MOD are permanently shadowed, unreachable
  dead code once bootstrap completes (verified against
  dictionary_management.c and the module order in word_registry.c).

- M*, M/MOD, and the "avoids intermediate overflow" claim on */ and */MOD
  are false on 64-bit builds: cell_t and "long long" are the same width
  there, so the long-long intermediate does not actually widen the
  product -- it wraps mod 2^64 like plain cell multiplication before the
  32-bit-style split/reconstruction runs. M*/M/MOD are left undefined
  here (oops-equivalent: documented as not modelled, since formalizing
  "the wrong thing, faithfully" adds no proof value) rather than fixed.

MOD/​/MOD/*//*/MOD reuse cell_sdiv/cell_smod from the arithmetic-words
migration; M+/M- transcribe the C's hand-rolled signed carry/borrow
detection literally, proving only stack-level plumbing (not double-
precision correctness, which needs an interpretation function this
suite doesn't build).

All 24 theory files verify with zero errors.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

proof/ROOT

@@ -6,6 +6,7 @@ session "StarForth" = "HOL-Library" +
     StarForth_Stack_Words
     StarForth_Double_Words
     StarForth_Arithmetic_Words
+    StarForth_Mixed_Arithmetic_Words
     StarForth_Logical_Words
     StarForth_Return_Stack_Words
     StarForth_Memory_Words

proof/StarForth_Mixed_Arithmetic_Words.thy

@@ -0,0 +1,221 @@
+theory StarForth_Mixed_Arithmetic_Words
+  imports StarForth_Base
+begin
+
+(* =========================================================================
+   POST-06: Mixed Arithmetic Words
+   Mirrors: src/word_source/mixed_arithmetic_words.c
+
+   ⚠ GENUINE FINDING: register_mixed_arithmetic_words registers "MOD" and
+   "/MOD" a second time.  register_forth79_words calls register_arithmetic_words
+   (module 4) before register_mixed_arithmetic_words (module 6); vm_create_word
+   links new entries at the head of vm->latest and FIND scans from vm->latest
+   forward, so the later registration wins.  arithmetic_words.c's MOD and /MOD
+   (word_source/arithmetic_words.c) are therefore permanently shadowed,
+   unreachable dead code once bootstrap completes -- confirmed by reading
+   vm_create_word's linked-list insertion in dictionary_management.c and the
+   module order in register_forth79_words (word_registry.c:106-119).  Not
+   fixed here per standing instruction to report, not silently resolve.
+
+   forth_mod/forth_slash_mod below model the WINNING (mixed_arithmetic_words.c)
+   definitions, which are bit-identical in behaviour to arithmetic_words.c's
+   shadowed ones -- both use plain C "%"/"/" on signed cell_t, i.e. the same
+   cell_smod/cell_sdiv already proven for POST-02.
+   ======================================================================== *)
+
+(* ── M+ ( d n -- d ) / M- ( d n -- d ) ────────────────────────────────────
+   Stack effect as coded: pop n, dlow, dhigh (dhigh deepest); push dhigh',
+   dlow' (dlow' TOS).  Carry/borrow propagation is a hand-rolled overflow
+   check on the signed cell_t addition, not a widened-type computation --
+   modelled here literally, including the signed (<s) comparisons the C
+   uses throughout (n compared against 0, dlow' against the pre-add dlow).
+   NOT modelled: whether (dhigh,dlow) as a pair actually represents a
+   correct double-precision integer -- that needs a double_of interpretation
+   function this suite doesn't build; only the stack-level transcription of
+   the C is proved. *)
+
+definition m_plus_carry :: "cell \<Rightarrow> cell \<Rightarrow> cell \<Rightarrow> (cell \<times> cell)" where
+  "m_plus_carry dhigh dlow n =
+     (let dlow' = dlow + n in
+      if 0 <s n \<and> dlow' <s dlow then (dhigh + 1, dlow')
+      else if n <s 0 \<and> dlow <s dlow' then (dhigh - 1, dlow')
+      else (dhigh, dlow'))"
+
+definition forth_m_plus :: "vm_state \<Rightarrow> vm_state" where
+  "forth_m_plus vm =
+    (case data_stack vm of
+       n # dlow # dhigh # rest \<Rightarrow>
+         vm\<lparr>data_stack := snd (m_plus_carry dhigh dlow n)
+                            # fst (m_plus_carry dhigh dlow n) # rest\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma m_plus_normal:
+  assumes "data_stack vm = n # dlow # dhigh # rest"
+  shows "data_stack (forth_m_plus vm) =
+           snd (m_plus_carry dhigh dlow n) # fst (m_plus_carry dhigh dlow n) # rest"
+  by (simp add: forth_m_plus_def assms)
+
+lemma m_plus_no_carry:
+  assumes "\<not> (0 <s n \<and> dlow + n <s dlow)"
+  assumes "\<not> (n <s 0 \<and> dlow <s dlow + n)"
+  shows "m_plus_carry dhigh dlow n = (dhigh, dlow + n)"
+  using assms by (simp add: m_plus_carry_def Let_def)
+
+lemma m_plus_underflow_nil:
+  assumes "data_stack vm = []"
+  shows "vm_error (forth_m_plus vm)"
+  by (simp add: forth_m_plus_def set_error_def assms)
+
+lemma m_plus_underflow_one:
+  assumes "data_stack vm = [x]"
+  shows "vm_error (forth_m_plus vm)"
+  by (simp add: forth_m_plus_def set_error_def assms)
+
+lemma m_plus_underflow_two:
+  assumes "data_stack vm = [x, y]"
+  shows "vm_error (forth_m_plus vm)"
+  by (simp add: forth_m_plus_def set_error_def assms)
+
+definition m_minus_borrow :: "cell \<Rightarrow> cell \<Rightarrow> cell \<Rightarrow> (cell \<times> cell)" where
+  "m_minus_borrow dhigh dlow n =
+     (let dlow' = dlow - n in
+      if 0 <s n \<and> dlow <s dlow' then (dhigh - 1, dlow')
+      else if n <s 0 \<and> dlow' <s dlow then (dhigh + 1, dlow')
+      else (dhigh, dlow'))"
+
+definition forth_m_minus :: "vm_state \<Rightarrow> vm_state" where
+  "forth_m_minus vm =
+    (case data_stack vm of
+       n # dlow # dhigh # rest \<Rightarrow>
+         vm\<lparr>data_stack := snd (m_minus_borrow dhigh dlow n)
+                            # fst (m_minus_borrow dhigh dlow n) # rest\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma m_minus_normal:
+  assumes "data_stack vm = n # dlow # dhigh # rest"
+  shows "data_stack (forth_m_minus vm) =
+           snd (m_minus_borrow dhigh dlow n) # fst (m_minus_borrow dhigh dlow n) # rest"
+  by (simp add: forth_m_minus_def assms)
+
+lemma m_minus_underflow_nil:
+  assumes "data_stack vm = []"
+  shows "vm_error (forth_m_minus vm)"
+  by (simp add: forth_m_minus_def set_error_def assms)
+
+(* ── M* ( n1 n2 -- d ) ─────────────────────────────────────────────────── *
+   ⚠ GENUINE FINDING, not modelled further: on a 64-bit build, cell_t and
+   "long long" are the SAME width, so "(long long) n1 * (long long) n2"
+   does not actually widen the product -- it wraps mod 2^64 exactly like
+   n1*n2 on cell_t would.  M*'s subsequent ">> 32" / "& 0xFFFFFFFF" split
+   then extracts the wrong halves: it produces a 32-bit-style double from
+   a 64-bit product that has ALREADY silently overflowed for any n1,n2
+   whose true product exceeds 2^63.  The doc comment above the C function
+   ("producing a double-cell result") is not true for the general case on
+   64-bit builds; only STAR_SLASH's docstring ("avoids intermediate
+   overflow via long long") shares the same false premise (see below).
+   No forth_m_star definition is given here: the C function does not
+   compute what its name and stack comment claim, and building a formal
+   model of "the wrong thing, faithfully" would misrepresent the intent
+   of M* without adding proof value -- the finding itself is the record. *)
+
+(* ── M/MOD ( d n -- rem quot ) ─────────────────────────────────────────── *
+   Same family of finding as M*: the 64-bit path reconstructs a "dividend"
+   by shifting dhigh left 32 bits and OR-ing in dlow's low 32 bits, which
+   only recovers a genuine double-cell value if dhigh/dlow were produced
+   by a CORRECT M* in the first place -- which they are not (see above).
+   Not modelled for the same reason. *)
+
+(* ── MOD ( n1 n2 -- r ), /MOD ( n1 n2 -- rem quot ) ───────────────────────
+   These are the entries that actually win at runtime (see the shadowing
+   finding at the top of this file).  Identical C body to arithmetic_words.c's
+   shadowed versions: plain signed "%"/"/", i.e. cell_smod/cell_sdiv. *)
+
+definition forth_mod2 :: "vm_state \<Rightarrow> vm_state" where
+  "forth_mod2 vm =
+    (case data_stack vm of
+       n2 # n1 # rest \<Rightarrow>
+         if n2 = 0
+         then set_error vm
+         else vm\<lparr>data_stack := (cell_smod n1 n2) # rest\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma mod2_normal:
+  assumes "data_stack vm = n2 # n1 # rest"
+  assumes "n2 \<noteq> 0"
+  shows "data_stack (forth_mod2 vm) = (cell_smod n1 n2) # rest"
+  by (simp add: forth_mod2_def assms)
+
+lemma mod2_by_zero:
+  assumes "data_stack vm = 0 # n1 # rest"
+  shows "vm_error (forth_mod2 vm)"
+  by (simp add: forth_mod2_def set_error_def assms)
+
+definition forth_slash_mod2 :: "vm_state \<Rightarrow> vm_state" where
+  "forth_slash_mod2 vm =
+    (case data_stack vm of
+       n2 # n1 # rest \<Rightarrow>
+         if n2 = 0
+         then set_error vm
+         else vm\<lparr>data_stack := (cell_sdiv n1 n2) # (cell_smod n1 n2) # rest\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma slash_mod2_normal:
+  assumes "data_stack vm = n2 # n1 # rest"
+  assumes "n2 \<noteq> 0"
+  shows "data_stack (forth_slash_mod2 vm) = (cell_sdiv n1 n2) # (cell_smod n1 n2) # rest"
+  by (simp add: forth_slash_mod2_def assms)
+
+lemma slash_mod2_by_zero:
+  assumes "data_stack vm = 0 # n1 # rest"
+  shows "vm_error (forth_slash_mod2 vm)"
+  by (simp add: forth_slash_mod2_def set_error_def assms)
+
+(* ── */ ( n1 n2 n3 -- quot ), */MOD ( n1 n2 n3 -- rem quot ) ──────────────
+   ⚠ GENUINE FINDING: the docstring claims the long-long intermediate
+   "avoid[s] intermediate overflow" -- false on 64-bit builds for the same
+   reason as M* above (cell_t and long long are the same width there).
+   Modelled here as the C actually computes: n1*n2 wraps at 64 bits exactly
+   like plain cell multiplication, THEN cell_sdiv/cell_smod by n3. *)
+
+definition forth_star_slash :: "vm_state \<Rightarrow> vm_state" where
+  "forth_star_slash vm =
+    (case data_stack vm of
+       n3 # n2 # n1 # rest \<Rightarrow>
+         if n3 = 0
+         then set_error vm
+         else vm\<lparr>data_stack := cell_sdiv (n1 * n2) n3 # rest\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma star_slash_normal:
+  assumes "data_stack vm = n3 # n2 # n1 # rest"
+  assumes "n3 \<noteq> 0"
+  shows "data_stack (forth_star_slash vm) = cell_sdiv (n1 * n2) n3 # rest"
+  by (simp add: forth_star_slash_def assms)
+
+lemma star_slash_by_zero:
+  assumes "data_stack vm = 0 # n2 # n1 # rest"
+  shows "vm_error (forth_star_slash vm)"
+  by (simp add: forth_star_slash_def set_error_def assms)
+
+definition forth_star_slash_mod :: "vm_state \<Rightarrow> vm_state" where
+  "forth_star_slash_mod vm =
+    (case data_stack vm of
+       n3 # n2 # n1 # rest \<Rightarrow>
+         if n3 = 0
+         then set_error vm
+         else vm\<lparr>data_stack := cell_sdiv (n1 * n2) n3 # cell_smod (n1 * n2) n3 # rest\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma star_slash_mod_normal:
+  assumes "data_stack vm = n3 # n2 # n1 # rest"
+  assumes "n3 \<noteq> 0"
+  shows "data_stack (forth_star_slash_mod vm) =
+           cell_sdiv (n1 * n2) n3 # cell_smod (n1 * n2) n3 # rest"
+  by (simp add: forth_star_slash_mod_def assms)
+
+lemma star_slash_mod_by_zero:
+  assumes "data_stack vm = 0 # n2 # n1 # rest"
+  shows "vm_error (forth_star_slash_mod vm)"
+  by (simp add: forth_star_slash_mod_def set_error_def assms)
+
+end