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