theory StarForth_Stack_Words
  imports StarForth_Base
begin

(* =========================================================================
   POST-01: Stack Manipulation Words
   Mirrors: src/word_source/stack_words.c
            src/test_runner/modules/stack_words_test.c
   ======================================================================== *)

(* ── DROP ( n -- ) ──────────────────────────────────────────────────────── *)

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

lemma drop_normal:
  assumes "data_stack vm = x # xs"
  shows "data_stack (forth_drop vm) = xs \<and> vm_error (forth_drop vm) = vm_error vm"
  by (simp add: forth_drop_def assms)

lemma drop_depth:
  assumes "data_stack vm = x # xs"
  shows "length (data_stack (forth_drop vm)) = length (data_stack vm) - 1"
  by (simp add: forth_drop_def assms)

lemma drop_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_drop vm)"
  by (simp add: forth_drop_def set_error_def assms)

(* ── DUP ( n -- n n ) ───────────────────────────────────────────────────── *)

definition forth_dup :: "vm_state \<Rightarrow> vm_state" where
  "forth_dup vm =
    (case data_stack vm of
       []     \<Rightarrow> set_error vm
     | x # xs \<Rightarrow>
         if ds_full vm
         then set_error vm
         else vm\<lparr>data_stack := x # x # xs\<rparr>)"

lemma dup_normal:
  assumes "data_stack vm = x # xs"
  assumes "\<not> ds_full vm"
  shows "data_stack (forth_dup vm) = x # x # xs"
  by (simp add: forth_dup_def assms)

lemma dup_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_dup vm)"
  by (simp add: forth_dup_def set_error_def assms)

lemma dup_overflow:
  assumes "data_stack vm = x # xs"
  assumes "ds_full vm"
  shows "vm_error (forth_dup vm)"
  by (simp add: forth_dup_def set_error_def assms)

lemma dup_increases_depth:
  assumes "data_stack vm = x # xs"
  assumes "\<not> ds_full vm"
  shows "length (data_stack (forth_dup vm)) = length (data_stack vm) + 1"
  by (simp add: forth_dup_def assms)

(* ── ?DUP ( n -- n n | 0 ) ─────────────────────────────────────────────── *)
(* Duplicates top if non-zero; leaves zero unchanged.                        *)

definition forth_qdup :: "vm_state \<Rightarrow> vm_state" where
  "forth_qdup vm =
    (case data_stack vm of
       []     \<Rightarrow> set_error vm
     | x # xs \<Rightarrow>
         if x = 0
         then vm
         else if ds_full vm
              then set_error vm
              else vm\<lparr>data_stack := x # x # xs\<rparr>)"

lemma qdup_zero:
  assumes "data_stack vm = 0 # xs"
  shows "data_stack (forth_qdup vm) = 0 # xs"
  by (simp add: forth_qdup_def assms)

lemma qdup_zero_noop:
  assumes "data_stack vm = 0 # xs"
  shows "forth_qdup vm = vm"
  by (simp add: forth_qdup_def assms)

lemma qdup_nonzero:
  assumes "data_stack vm = x # xs"
  assumes "x \<noteq> 0"
  assumes "\<not> ds_full vm"
  shows "data_stack (forth_qdup vm) = x # x # xs"
  by (simp add: forth_qdup_def assms)

lemma qdup_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_qdup vm)"
  by (simp add: forth_qdup_def set_error_def assms)

lemma qdup_overflow:
  assumes "data_stack vm = x # xs"
  assumes "x \<noteq> 0"
  assumes "ds_full vm"
  shows "vm_error (forth_qdup vm)"
  by (simp add: forth_qdup_def set_error_def assms)

(* ── SWAP ( n1 n2 -- n2 n1 ) ───────────────────────────────────────────── *)
(* Stack effect (right = TOS): n1=second, n2=TOS.
   In list notation (head = TOS): [n2, n1, rest] \<rightarrow> [n1, n2, rest]         *)

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

lemma swap_normal:
  assumes "data_stack vm = n2 # n1 # rest"
  shows "data_stack (forth_swap vm) = n1 # n2 # rest"
  by (simp add: forth_swap_def assms)

lemma swap_depth_preserved:
  assumes "data_stack vm = n2 # n1 # rest"
  shows "length (data_stack (forth_swap vm)) = length (data_stack vm)"
  by (simp add: forth_swap_def assms)

lemma swap_involutive:
  assumes "data_stack vm = n2 # n1 # rest"
  shows "data_stack (forth_swap (forth_swap vm)) = data_stack vm"
  by (simp add: forth_swap_def assms)

lemma swap_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_swap vm)"
  by (simp add: forth_swap_def set_error_def assms)

lemma swap_underflow_one:
  assumes "data_stack vm = [x]"
  shows "vm_error (forth_swap vm)"
  by (simp add: forth_swap_def set_error_def assms)

(* ── OVER ( n1 n2 -- n1 n2 n1 ) ───────────────────────────────────────── *)
(* n2=TOS, n1=second. Copies n1 (second) to new TOS.
   In list: [n2, n1, rest] \<rightarrow> [n1, n2, n1, rest]                           *)

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

lemma over_normal:
  assumes "data_stack vm = n2 # n1 # rest"
  assumes "\<not> ds_full vm"
  shows "data_stack (forth_over vm) = n1 # n2 # n1 # rest"
  by (simp add: forth_over_def assms)

lemma over_second_preserved:
  assumes "data_stack vm = n2 # n1 # rest"
  assumes "\<not> ds_full vm"
  shows "hd (data_stack (forth_over vm)) = n1"
  by (simp add: forth_over_def assms)

lemma over_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_over vm)"
  by (simp add: forth_over_def set_error_def assms)

lemma over_underflow_one:
  assumes "data_stack vm = [x]"
  shows "vm_error (forth_over vm)"
  by (simp add: forth_over_def set_error_def assms)

lemma over_overflow:
  assumes "data_stack vm = n2 # n1 # rest"
  assumes "ds_full vm"
  shows "vm_error (forth_over vm)"
  by (simp add: forth_over_def set_error_def assms)

(* ── ROT ( n1 n2 n3 -- n2 n3 n1 ) ─────────────────────────────────────── *)
(* n3=TOS, n2=second, n1=third.  Brings n1 (third) to TOS.
   In list: [n3, n2, n1, rest] \<rightarrow> [n1, n3, n2, rest]

   Verified against C:
     n3 = data_stack[dsp]       (TOS)
     n2 = data_stack[dsp-1]     (second)
     n1 = data_stack[dsp-2]     (third)
     data_stack[dsp]   = n1     (new TOS)
     data_stack[dsp-1] = n3
     data_stack[dsp-2] = n2                                                *)

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

lemma rot_normal:
  assumes "data_stack vm = n3 # n2 # n1 # rest"
  shows "data_stack (forth_rot vm) = n1 # n3 # n2 # rest"
  by (simp add: forth_rot_def assms)

lemma rot_depth_preserved:
  assumes "data_stack vm = n3 # n2 # n1 # rest"
  shows "length (data_stack (forth_rot vm)) = length (data_stack vm)"
  by (simp add: forth_rot_def assms)

lemma rot_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_rot vm)"
  by (simp add: forth_rot_def set_error_def assms)

lemma rot_underflow_one:
  assumes "data_stack vm = [x]"
  shows "vm_error (forth_rot vm)"
  by (simp add: forth_rot_def set_error_def assms)

lemma rot_underflow_two:
  assumes "data_stack vm = [x, y]"
  shows "vm_error (forth_rot vm)"
  by (simp add: forth_rot_def set_error_def assms)

(* ── -ROT ( n1 n2 n3 -- n3 n1 n2 ) ─────────────────────────────────────── *)
(* Reverse rotation: brings TOS (n3) to third position.
   In list: [n3, n2, n1, rest] \<rightarrow> [n2, n1, n3, rest]

   Verified against C:
     data_stack[dsp]   = n2     (new TOS)
     data_stack[dsp-1] = n1
     data_stack[dsp-2] = n3                                                *)

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

lemma nrot_normal:
  assumes "data_stack vm = n3 # n2 # n1 # rest"
  shows "data_stack (forth_nrot vm) = n2 # n1 # n3 # rest"
  by (simp add: forth_nrot_def assms)

lemma nrot_depth_preserved:
  assumes "data_stack vm = n3 # n2 # n1 # rest"
  shows "length (data_stack (forth_nrot vm)) = length (data_stack vm)"
  by (simp add: forth_nrot_def assms)

(* ROT and -ROT are mutual inverses on the data stack. *)
lemma rot_nrot_inverse:
  assumes "data_stack vm = n3 # n2 # n1 # rest"
  shows "data_stack (forth_nrot (forth_rot vm)) = data_stack vm"
  by (simp add: forth_nrot_def forth_rot_def assms)

lemma nrot_rot_inverse:
  assumes "data_stack vm = n3 # n2 # n1 # rest"
  shows "data_stack (forth_rot (forth_nrot vm)) = data_stack vm"
  by (simp add: forth_nrot_def forth_rot_def assms)

lemma nrot_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_nrot vm)"
  by (simp add: forth_nrot_def set_error_def assms)

lemma nrot_underflow_one:
  assumes "data_stack vm = [x]"
  shows "vm_error (forth_nrot vm)"
  by (simp add: forth_nrot_def set_error_def assms)

lemma nrot_underflow_two:
  assumes "data_stack vm = [x, y]"
  shows "vm_error (forth_nrot vm)"
  by (simp add: forth_nrot_def set_error_def assms)

(* ── DROP \<circ> DUP = identity ─────────────────────────────────────────────── *)

lemma dup_then_drop:
  assumes "data_stack vm = x # xs"
  assumes "\<not> ds_full vm"
  assumes "\<not> vm_error vm"
  shows "data_stack (forth_drop (forth_dup vm)) = data_stack vm"
  by (simp add: forth_dup_def forth_drop_def assms)

(* ── DEPTH ( -- n ) ─────────────────────────────────────────────────────── *)
(* Pushes the current stack depth (number of items before DEPTH executes).
   C impl: depth = dsp + 1; data_stack[++dsp] = depth.                     *)

definition forth_depth :: "vm_state \<Rightarrow> vm_state" where
  "forth_depth vm =
    (if ds_full vm
     then set_error vm
     else vm\<lparr>data_stack := word_of_nat (length (data_stack vm)) # data_stack vm\<rparr>)"

lemma depth_pushes_count:
  assumes "\<not> ds_full vm"
  shows "hd (data_stack (forth_depth vm)) = word_of_nat (length (data_stack vm))"
  by (simp add: forth_depth_def assms)

lemma depth_rest_preserved:
  assumes "\<not> ds_full vm"
  shows "tl (data_stack (forth_depth vm)) = data_stack vm"
  by (simp add: forth_depth_def assms)

lemma depth_increases_by_one:
  assumes "\<not> ds_full vm"
  shows "length (data_stack (forth_depth vm)) = length (data_stack vm) + 1"
  by (simp add: forth_depth_def assms)

lemma depth_overflow:
  assumes "ds_full vm"
  shows "vm_error (forth_depth vm)"
  by (simp add: forth_depth_def set_error_def assms)

(* ── PICK ( n -- x ) ───────────────────────────────────────────────────── *)
(* Replaces TOS (n) with the element at index n in the current stack.
   Index 0 = TOS itself; index 1 = second item; etc.
   In-place replacement — depth unchanged.

   Verified against C:
     n   = data_stack[dsp]       (TOS, not popped)
     val = data_stack[dsp - n]
     data_stack[dsp] = val       (replace TOS with val)

   Bounds check: 0 \<le>s n and n < length (data_stack vm)                     *)

(* CORRECTED 2026-08-13, against src/word_source/stack_words.c:265-282 and
   its passing tests (test_runner/modules/stack_words_test.c: pick_0,
   pick_1, pick_2). The C code pops n FIRST (vm_pop), THEN indexes into
   the REMAINING stack: "cell_t value = vm->data_stack[vm->dsp - n]" where
   vm->dsp is already the post-pop top-of-stack index -- i.e. value = the
   post-pop stack's n'th-from-top item, xs!n in this list's head=TOS
   convention. The theory's original definition indexed into
   "data_stack vm" (the PRE-pop stack, still containing n as its own head)
   instead of "xs" (post-pop) -- off by one position, and its bound check
   "unat n \<ge> length (data_stack vm)" used the pre-pop length too, one too
   permissive (C's own bound is against post-pop depth, vm->dsp+1 = length
   xs). Confirmed against the real test vectors: "1 2 3 0 PICK" expects
   TOS=3 (xs!0), "1 2 3 1 PICK" expects 2 (xs!1), "1 2 3 2 PICK" expects 1
   (xs!2) -- all match xs!n, none match the old (data_stack vm)!n. *)
definition forth_pick :: "vm_state \<Rightarrow> vm_state" where
  "forth_pick vm =
    (case data_stack vm of
       []     \<Rightarrow> set_error vm
     | n # xs \<Rightarrow>
         if n <s 0 \<or> unat n \<ge> length xs
         then set_error vm
         else vm\<lparr>data_stack := xs ! unat n # xs\<rparr>)"

lemma pick_normal:
  assumes "data_stack vm = n # xs"
  assumes "0 \<le>s n"
  assumes "unat n < length xs"
  shows "data_stack (forth_pick vm) = xs ! unat n # xs"
  using assms by (auto simp: forth_pick_def)

lemma pick_depth_unchanged:
  assumes "data_stack vm = n # xs"
  assumes "0 \<le>s n"
  assumes "unat n < length xs"
  shows "length (data_stack (forth_pick vm)) = length (data_stack vm)"
  using assms by (auto simp: forth_pick_def word_sless_alt word_sle_eq)

(* 0 PICK: pushes a copy of the post-pop TOS (xs!0) -- equivalent to DUP.
   Matches the real test vector "1 2 3 0 PICK" => prints 3. *)
lemma pick_zero_dup:
  assumes "data_stack vm = 0 # x # xs"
  shows "data_stack (forth_pick vm) = x # x # xs"
  using assms by (auto simp: forth_pick_def word_sless_alt word_sle_eq)

(* 1 PICK: pushes a copy of the item one below TOS (xs!1).
   Matches the real test vector "1 2 3 1 PICK" => prints 2. *)
lemma pick_one:
  assumes "data_stack vm = 1 # x # y # xs"
  shows "data_stack (forth_pick vm) = y # x # y # xs"
  using assms by (auto simp: forth_pick_def word_sless_alt word_sle_eq)

lemma pick_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_pick vm)"
  by (simp add: forth_pick_def set_error_def assms)

lemma pick_bounds_neg:
  assumes "data_stack vm = n # xs"
  assumes "n <s 0"
  shows "vm_error (forth_pick vm)"
  by (simp add: forth_pick_def set_error_def assms)

lemma pick_bounds_high:
  assumes "data_stack vm = n # xs"
  assumes "unat n \<ge> length xs"
  shows "vm_error (forth_pick vm)"
  using assms by (auto simp: forth_pick_def set_error_def)

(* ── ROLL ( +n -- ) ─────────────────────────────────────────────────────── *)
(* REWRITTEN 2026-08-13 to match real, ground-truth semantics -- the
   previous version implemented a THIRD convention that matched neither
   the real C code nor its own test lemma (see git history for the
   original oops-flagged finding). Resolved by tracing the actual C
   source and its passing tests:

   src/word_source/stack_words.c:291-320 (stack_word_roll): n is popped
   FIRST. n=0 is a no-op. For n\<ge>1, the comment is explicit and the code
   matches it exactly: "1-indexed from bottom: n=1 moves bottom item to
   top" -- target = bottom + (n-1) (C array index, bottom=0); the item at
   that index is removed, everything above it shifts down one slot, and
   the removed item is placed on top. This is NOT the standard/gforth
   "count from top" ROLL (which would make "2 ROLL" a ROT) -- it is a
   different, deliberately bottom-indexed operation in this codebase.

   Verified against the real passing tests (stack_words_test.c):
     "1 2 3 1 ROLL . . . CR" => prints "1 3 2"
     "1 2 3 2 ROLL . . . CR" => prints "2 3 1"
   In this list's head=TOS convention, after popping n the remaining xs
   has xs!0 = TOS ... xs!(length xs - 1) = bottom. "n=1 moves bottom to
   top" means: target index = length xs - n (n=1 -> last index = bottom,
   n=length xs -> index 0 = TOS itself, a full-depth roll). Hand-checked
   both test vectors against this formula -- both match exactly (worked
   in the discovering session's transcript, not reproduced in-line here).

   Bound: n=0 is a no-op (checked first, no shift). For n\<ge>1, valid range
   is 1 \<le> n \<le> length xs (C: "n >= vm->dsp + 1" is the error condition,
   vm->dsp+1 = length xs after the pop) -- n = length xs is a valid
   full-depth roll (brings the very bottom item to top when the whole
   remaining stack is rolled), not an error. *)

definition forth_roll :: "vm_state \<Rightarrow> vm_state" where
  "forth_roll vm =
    (case data_stack vm of
       []     \<Rightarrow> set_error vm
     | n # xs \<Rightarrow>
         if n <s 0 \<or> unat n > length xs
         then set_error vm
         else if n = 0
              then vm\<lparr>data_stack := xs\<rparr>
              else let i    = length xs - unat n;
                       item = xs ! i;
                       rest = take i xs @ drop (i + 1) xs
                   in vm\<lparr>data_stack := item # rest\<rparr>)"

lemma roll_zero_nop:
  assumes "data_stack vm = 0 # xs"
  shows "data_stack (forth_roll vm) = xs"
  by (simp add: forth_roll_def assms)

(* n=1 moves the BOTTOM item to the top -- NOT a no-op in general (only
   coincidentally a no-op when xs has length \<le> 1). Renamed from the old,
   now-false "roll_one_nop" name. *)
lemma roll_one_moves_bottom:
  assumes "data_stack vm = 1 # xs"
  assumes "xs \<noteq> []"
  shows "data_stack (forth_roll vm) = last xs # butlast xs"
proof -
  have i: "length xs - unat (1::cell) = length xs - 1" by simp
  show ?thesis
    using assms
    by (simp add: forth_roll_def Let_def i last_conv_nth butlast_conv_take
                  word_sless_alt word_sle_eq)
qed

(* Ground-truth test vectors, proved symbolically (no need to construct a
   concrete vm_state -- data_stack alone determines forth_roll's result).
   "1 2 3 1 ROLL . . . CR" => prints "1 3 2": push 1,2,3 gives
   data_stack=[3,2,1] (head=TOS), push count 1 gives [1,3,2,1]; xs=[3,2,1]
   after popping the count; 1 ROLL moves the bottom item (1) to top. *)
lemma roll_test_vector_1:
  assumes "data_stack vm = [1, 3, 2, 1]"
  shows "data_stack (forth_roll vm) = [1, 3, 2]"
  using assms by (simp add: forth_roll_def word_sless_alt word_sle_eq)

(* "1 2 3 2 ROLL . . . CR" => prints "2 3 1": xs=[3,2,1] after popping the
   count 2; 2 ROLL moves the 2nd-from-bottom item (2) to top. *)
lemma roll_test_vector_2:
  assumes "data_stack vm = [2, 3, 2, 1]"
  shows "data_stack (forth_roll vm) = [2, 3, 1]"
  using assms by (simp add: forth_roll_def word_sless_alt word_sle_eq)

lemma roll_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_roll vm)"
  by (simp add: forth_roll_def set_error_def assms)

lemma roll_bounds_neg:
  assumes "data_stack vm = n # xs"
  assumes "n <s 0"
  shows "vm_error (forth_roll vm)"
  by (simp add: forth_roll_def set_error_def assms)

lemma roll_bounds_high:
  assumes "data_stack vm = n # xs"
  assumes "unat n > length xs"
  shows "vm_error (forth_roll vm)"
  by (simp add: forth_roll_def set_error_def assms)

end