theory StarForth_Arithmetic_Words
  imports StarForth_Base
begin

(* =========================================================================
   POST-02: Arithmetic Words
   Mirrors: src/word_source/arithmetic_words.c
            src/test_runner/modules/arithmetic_words_test.c

   All operations use HOL int (arbitrary precision).  Proofs hold in C
   provided no intermediate value overflows 64-bit signed range.
   ======================================================================== *)

(* ── Helper: binary op lifting ─────────────────────────────────────────── *)
(* Most binary arithmetic words: pop two, push result.                      *)

definition binop :: "(cell \<Rightarrow> cell \<Rightarrow> cell) \<Rightarrow> vm_state \<Rightarrow> vm_state" where
  "binop f vm =
    (case data_stack vm of
       n2 # n1 # rest \<Rightarrow> vm\<lparr>data_stack := f n1 n2 # rest\<rparr>
     | _              \<Rightarrow> set_error vm)"

lemma binop_normal:
  assumes "data_stack vm = n2 # n1 # rest"
  shows "data_stack (binop f vm) = f n1 n2 # rest"
  by (simp add: binop_def assms)

lemma binop_depth:
  assumes "data_stack vm = n2 # n1 # rest"
  shows "length (data_stack (binop f vm)) = length (data_stack vm) - 1"
  by (simp add: binop_def assms)

lemma binop_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (binop f vm)"
  by (simp add: binop_def set_error_def assms)

lemma binop_underflow_one:
  assumes "data_stack vm = [x]"
  shows "vm_error (binop f vm)"
  by (simp add: binop_def set_error_def assms)

(* ── Helper: unary op lifting ───────────────────────────────────────────── *)

definition unop :: "(cell \<Rightarrow> cell) \<Rightarrow> vm_state \<Rightarrow> vm_state" where
  "unop f vm =
    (case data_stack vm of
       []     \<Rightarrow> set_error vm
     | x # xs \<Rightarrow> vm\<lparr>data_stack := f x # xs\<rparr>)"

lemma unop_normal:
  assumes "data_stack vm = x # xs"
  shows "data_stack (unop f vm) = f x # xs"
  by (simp add: unop_def assms)

lemma unop_depth_preserved:
  assumes "data_stack vm = x # xs"
  shows "length (data_stack (unop f vm)) = length (data_stack vm)"
  by (simp add: unop_def assms)

lemma unop_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (unop f vm)"
  by (simp add: unop_def set_error_def assms)

(* ── + ( n1 n2 -- n3 ) ─────────────────────────────────────────────────── *)

definition forth_add :: "vm_state \<Rightarrow> vm_state" where
  "forth_add = binop (+)"

lemma add_normal:
  assumes "data_stack vm = n2 # n1 # rest"
  shows "data_stack (forth_add vm) = (n1 + n2) # rest"
  by (simp add: forth_add_def binop_def assms)

lemma add_commutative:
  assumes "data_stack vm = n2 # n1 # rest"
  assumes "data_stack vm' = n1 # n2 # rest"
  shows "data_stack (forth_add vm) = data_stack (forth_add vm')"
  by (simp add: forth_add_def binop_def assms add.commute)

lemma add_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_add vm)"
  by (simp add: forth_add_def binop_def set_error_def assms)

lemma add_underflow_one:
  assumes "data_stack vm = [x]"
  shows "vm_error (forth_add vm)"
  by (simp add: forth_add_def binop_def set_error_def assms)

(* ── - ( n1 n2 -- n3 ) ─────────────────────────────────────────────────── *)
(* Stack effect: n3 = n1 - n2  (n2 = TOS subtracted from n1 = second)      *)

definition forth_sub :: "vm_state \<Rightarrow> vm_state" where
  "forth_sub = binop (-)"

lemma sub_normal:
  assumes "data_stack vm = n2 # n1 # rest"
  shows "data_stack (forth_sub vm) = (n1 - n2) # rest"
  by (simp add: forth_sub_def binop_def assms)

lemma sub_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_sub vm)"
  by (simp add: forth_sub_def binop_def set_error_def assms)

lemma sub_underflow_one:
  assumes "data_stack vm = [x]"
  shows "vm_error (forth_sub vm)"
  by (simp add: forth_sub_def binop_def set_error_def assms)

(* ── * ( n1 n2 -- n3 ) ─────────────────────────────────────────────────── *)

definition forth_mul :: "vm_state \<Rightarrow> vm_state" where
  "forth_mul = binop (*)"

lemma mul_normal:
  assumes "data_stack vm = n2 # n1 # rest"
  shows "data_stack (forth_mul vm) = (n1 * n2) # rest"
  by (simp add: forth_mul_def binop_def assms)

lemma mul_commutative:
  assumes "data_stack vm = n2 # n1 # rest"
  assumes "data_stack vm' = n1 # n2 # rest"
  shows "data_stack (forth_mul vm) = data_stack (forth_mul vm')"
  by (simp add: forth_mul_def binop_def assms mult.commute)

lemma mul_by_zero_tos:
  assumes "data_stack vm = 0 # n1 # rest"
  shows "data_stack (forth_mul vm) = 0 # rest"
  by (simp add: forth_mul_def binop_def assms)

lemma mul_by_zero_second:
  assumes "data_stack vm = n2 # 0 # rest"
  shows "data_stack (forth_mul vm) = 0 # rest"
  by (simp add: forth_mul_def binop_def assms)

lemma mul_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_mul vm)"
  by (simp add: forth_mul_def binop_def set_error_def assms)

(* ── / ( n1 n2 -- n3 ) ─────────────────────────────────────────────────── *)
(* Division by zero sets vm_error (matching C behaviour).                   *)

definition forth_div :: "vm_state \<Rightarrow> vm_state" where
  "forth_div 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) # rest\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma div_normal:
  assumes "data_stack vm = n2 # n1 # rest"
  assumes "n2 \<noteq> 0"
  shows "data_stack (forth_div vm) = (cell_sdiv n1 n2) # rest"
  by (simp add: forth_div_def assms)

lemma div_by_zero:
  assumes "data_stack vm = 0 # n1 # rest"
  shows "vm_error (forth_div vm)"
  by (simp add: forth_div_def set_error_def assms)

lemma div_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_div vm)"
  by (simp add: forth_div_def set_error_def assms)

lemma div_underflow_one:
  assumes "data_stack vm = [x]"
  shows "vm_error (forth_div vm)"
  by (simp add: forth_div_def set_error_def assms)

(* ── MOD ( n1 n2 -- n3 ) ───────────────────────────────────────────────── *)

definition forth_mod :: "vm_state \<Rightarrow> vm_state" where
  "forth_mod 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 mod_normal:
  assumes "data_stack vm = n2 # n1 # rest"
  assumes "n2 \<noteq> 0"
  shows "data_stack (forth_mod vm) = (cell_smod n1 n2) # rest"
  by (simp add: forth_mod_def assms)

lemma mod_by_zero:
  assumes "data_stack vm = 0 # n1 # rest"
  shows "vm_error (forth_mod vm)"
  by (simp add: forth_mod_def set_error_def assms)

lemma mod_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_mod vm)"
  by (simp add: forth_mod_def set_error_def assms)

(* ── /MOD ( n1 n2 -- n3 n4 ) ───────────────────────────────────────────── *)
(* Pushes remainder (n3) then quotient (n4); quotient is TOS.               *)

definition forth_divmod :: "vm_state \<Rightarrow> vm_state" where
  "forth_divmod vm =
    (case data_stack vm of
       n2 # n1 # rest \<Rightarrow>
         if n2 = 0
         then set_error vm
         else if ds_full vm
              then set_error vm
              else vm\<lparr>data_stack := (cell_sdiv n1 n2) # (cell_smod n1 n2) # rest\<rparr>
     | _ \<Rightarrow> set_error vm)"

lemma divmod_normal:
  assumes "data_stack vm = n2 # n1 # rest"
  assumes "n2 \<noteq> 0"
  assumes "\<not> ds_full vm"
  shows "data_stack (forth_divmod vm) = (cell_sdiv n1 n2) # (cell_smod n1 n2) # rest"
  by (simp add: forth_divmod_def assms)

lemma divmod_quotient:
  assumes "data_stack vm = n2 # n1 # rest"
  assumes "n2 \<noteq> 0"
  assumes "\<not> ds_full vm"
  shows "hd (data_stack (forth_divmod vm)) = cell_sdiv n1 n2"
  by (simp add: forth_divmod_def assms)

lemma divmod_remainder:
  assumes "data_stack vm = n2 # n1 # rest"
  assumes "n2 \<noteq> 0"
  assumes "\<not> ds_full vm"
  shows "hd (tl (data_stack (forth_divmod vm))) = cell_smod n1 n2"
  by (simp add: forth_divmod_def assms)

(* ── 1+ ( n -- n+1 ) ───────────────────────────────────────────────────── *)

definition forth_one_plus :: "vm_state \<Rightarrow> vm_state" where
  "forth_one_plus = unop (\<lambda>n. n + 1)"

lemma one_plus_normal:
  assumes "data_stack vm = n # xs"
  shows "data_stack (forth_one_plus vm) = (n + 1) # xs"
  by (simp add: forth_one_plus_def unop_def assms)

lemma one_plus_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_one_plus vm)"
  by (simp add: forth_one_plus_def unop_def set_error_def assms)

(* ── 1- ( n -- n-1 ) ───────────────────────────────────────────────────── *)

definition forth_one_minus :: "vm_state \<Rightarrow> vm_state" where
  "forth_one_minus = unop (\<lambda>n. n - 1)"

lemma one_minus_normal:
  assumes "data_stack vm = n # xs"
  shows "data_stack (forth_one_minus vm) = (n - 1) # xs"
  by (simp add: forth_one_minus_def unop_def assms)

lemma one_minus_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_one_minus vm)"
  by (simp add: forth_one_minus_def unop_def set_error_def assms)

(* ── 2+ ( n -- n+2 ) ───────────────────────────────────────────────────── *)

definition forth_two_plus :: "vm_state \<Rightarrow> vm_state" where
  "forth_two_plus = unop (\<lambda>n. n + 2)"

lemma two_plus_normal:
  assumes "data_stack vm = n # xs"
  shows "data_stack (forth_two_plus vm) = (n + 2) # xs"
  by (simp add: forth_two_plus_def unop_def assms)

(* ── 2- ( n -- n-2 ) ───────────────────────────────────────────────────── *)

definition forth_two_minus :: "vm_state \<Rightarrow> vm_state" where
  "forth_two_minus = unop (\<lambda>n. n - 2)"

lemma two_minus_normal:
  assumes "data_stack vm = n # xs"
  shows "data_stack (forth_two_minus vm) = (n - 2) # xs"
  by (simp add: forth_two_minus_def unop_def assms)

(* ── 2* ( n -- n*2 ) ───────────────────────────────────────────────────── *)
(* Left shift by 1 in C; multiplication by 2 in HOL.                        *)

definition forth_two_mul :: "vm_state \<Rightarrow> vm_state" where
  "forth_two_mul = unop (\<lambda>n. n * 2)"

lemma two_mul_normal:
  assumes "data_stack vm = n # xs"
  shows "data_stack (forth_two_mul vm) = (n * 2) # xs"
  by (simp add: forth_two_mul_def unop_def assms)

(* ── 2/ ( n -- n/2 ) ───────────────────────────────────────────────────── *)
(* CODE-MUST-MATCH: arithmetic_words.c does "n >> 1" on signed cell_t --
   an arithmetic (sign-extending) right shift, i.e. floor division by 2,
   NOT truncating division.  signed_drop_bit is Word's arithmetic shift
   and matches this exactly (unlike plain word div/mod, which are
   unsigned-magnitude and wrong here). *)

definition forth_two_div :: "vm_state \<Rightarrow> vm_state" where
  "forth_two_div = unop (signed_drop_bit 1)"

lemma two_div_normal:
  assumes "data_stack vm = n # xs"
  shows "data_stack (forth_two_div vm) = (signed_drop_bit 1 n) # xs"
  by (simp add: forth_two_div_def unop_def assms)

(* ── ABS ( n -- |n| ) ──────────────────────────────────────────────────── *)
(* word has no signed abs of its own (that error is what forced this whole
   ABS/MIN/MAX section to be revisited) -- cell_abs in StarForth_Base.thy
   supplies it via the signed order <s. *)

definition forth_abs :: "vm_state \<Rightarrow> vm_state" where
  "forth_abs = unop cell_abs"

lemma abs_normal:
  assumes "data_stack vm = n # xs"
  shows "data_stack (forth_abs vm) = cell_abs n # xs"
  by (simp add: forth_abs_def unop_def assms)

(* ⚠ GENUINE FINDING, not an artifact of the proof: ABS(INT64_MIN) is not
   \<ge> 0 -- two's-complement negation of the minimum signed 64-bit value
   overflows and wraps back to itself (identical to C's ABS(LONG_MIN)
   hazard, since cell_t is a plain signed long with no overflow trap).
   cell_safe n excludes exactly this single value (and the rest of the
   far-from-boundary range no real FORTH program should be relying on
   the overflow behaviour of anyway) so the property holds for the
   values arithmetic proofs elsewhere in this suite actually use. *)
lemma abs_nonneg:
  assumes "data_stack vm = n # xs"
  assumes "\<not> vm_error vm"
  assumes "cell_safe n"
  shows "0 \<le>s hd (data_stack (forth_abs vm))"
proof (cases "n <s 0")
  case True
  have sint_negn: "sint (-n) = - sint n"
    using assms(3) cell_safe_0
    by (simp add: cell_safe_sub_sint[of 0 n, simplified])
  have negn_nonneg: "0 \<le>s (-n)"
    using True by (simp add: word_sle_eq word_sless_alt sint_negn)
  have "hd (data_stack (forth_abs vm)) = -n"
    using assms(1) True by (simp add: forth_abs_def unop_def cell_abs_def)
  with negn_nonneg show ?thesis by simp
next
  case False
  then show ?thesis
    using assms(1) by (simp add: forth_abs_def unop_def cell_abs_def word_sle_eq word_sless_alt)
qed

(* cell_safe n again excludes the INT64_MIN self-wrap case: without it,
   idempotence still happens to hold there too (cell_abs wraps INT64_MIN to
   itself both times), but proving that needs the extra double-negation
   self-wrap fact rather than a plain case split, and nothing downstream
   needs that generality. *)
lemma abs_idempotent:
  assumes "data_stack vm = n # xs"
  assumes "\<not> vm_error vm"
  assumes "cell_safe n"
  shows "hd (data_stack (forth_abs (forth_abs vm))) = hd (data_stack (forth_abs vm))"
proof (cases "n <s 0")
  case True
  have sint_negn: "sint (-n) = - sint n"
    using assms(3) cell_safe_0
    by (simp add: cell_safe_sub_sint[of 0 n, simplified])
  have negn_nonneg: "0 \<le>s (-n)"
    using True by (simp add: word_sle_eq word_sless_alt sint_negn)
  have step1: "hd (data_stack (forth_abs vm)) = -n"
    using assms(1) True by (simp add: forth_abs_def unop_def cell_abs_def)
  have step2: "hd (data_stack (forth_abs (forth_abs vm))) = -n"
    using assms(1) True negn_nonneg
    by (simp add: forth_abs_def unop_def cell_abs_def word_sless_alt word_sle_eq)
  from step1 step2 show ?thesis by simp
next
  case False
  then show ?thesis
    using assms(1) by (simp add: forth_abs_def unop_def cell_abs_def)
qed

lemma abs_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_abs vm)"
  by (simp add: forth_abs_def unop_def set_error_def assms)

(* ── NEGATE ( n -- -n ) ─────────────────────────────────────────────────── *)

definition forth_negate :: "vm_state \<Rightarrow> vm_state" where
  "forth_negate = unop uminus"

lemma negate_normal:
  assumes "data_stack vm = n # xs"
  shows "data_stack (forth_negate vm) = (-n) # xs"
  by (simp add: forth_negate_def unop_def assms)

lemma negate_involutive:
  assumes "data_stack vm = n # xs"
  shows "hd (data_stack (forth_negate (forth_negate vm))) = n"
  by (simp add: forth_negate_def unop_def assms)

lemma negate_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_negate vm)"
  by (simp add: forth_negate_def unop_def set_error_def assms)

(* ── MIN ( n1 n2 -- n3 ) ───────────────────────────────────────────────── *)

(* word's inherited min/max (via the default, unsigned <=) is wrong for
   FORTH's signed MIN/MAX -- must use the "signed" locale interpretation
   (Word.thy:1771, linorder over word_sle/word_sless) instead. *)
definition forth_min :: "vm_state \<Rightarrow> vm_state" where
  "forth_min = binop signed.min"

lemma min_normal:
  assumes "data_stack vm = n2 # n1 # rest"
  shows "data_stack (forth_min vm) = signed.min n1 n2 # rest"
  by (simp add: forth_min_def binop_def assms)

lemma min_commutative:
  assumes "data_stack vm = n2 # n1 # rest"
  assumes "data_stack vm' = n1 # n2 # rest"
  shows "data_stack (forth_min vm) = data_stack (forth_min vm')"
  by (simp add: forth_min_def binop_def assms signed.min.commute)

lemma min_idempotent:
  assumes "data_stack vm = n # n # rest"
  shows "data_stack (forth_min vm) = n # rest"
  by (simp add: forth_min_def binop_def assms)

lemma min_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_min vm)"
  by (simp add: forth_min_def binop_def set_error_def assms)

(* ── MAX ( n1 n2 -- n3 ) ───────────────────────────────────────────────── *)

definition forth_max :: "vm_state \<Rightarrow> vm_state" where
  "forth_max = binop signed.max"

lemma max_normal:
  assumes "data_stack vm = n2 # n1 # rest"
  shows "data_stack (forth_max vm) = signed.max n1 n2 # rest"
  by (simp add: forth_max_def binop_def assms)

lemma max_commutative:
  assumes "data_stack vm = n2 # n1 # rest"
  assumes "data_stack vm' = n1 # n2 # rest"
  shows "data_stack (forth_max vm) = data_stack (forth_max vm')"
  by (simp add: forth_max_def binop_def assms signed.max.commute)

lemma max_idempotent:
  assumes "data_stack vm = n # n # rest"
  shows "data_stack (forth_max vm) = n # rest"
  by (simp add: forth_max_def binop_def assms)

lemma max_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_max vm)"
  by (simp add: forth_max_def binop_def set_error_def assms)

(* ── min/max algebraic relationship ────────────────────────────────────── *)

lemma min_le_max:
  "signed.min (a::cell) b \<le>s signed.max a b"
  by (cases "a \<le>s b") (simp_all add: signed.min_def signed.max_def signed.linear)

end