proof/: migrate cell from int to 64-bit signed word, full suite verifies

cell_t is a 64-bit signed C long; the formal model previously used
unbounded HOL int, hiding wraparound and signed/unsigned distinctions
entirely. Switches cell to "64 word" throughout and fixes every proof
site that assumed int semantics:

- StarForth_Base.thy: cell_safe/cell_abs/cell_sdiv/cell_smod plus the
  sint-bridging lemmas used across the suite
- StarForth_Loop1_Heat.thy, StarForth_Loop3_Decay.thy: heat tracking
  converted to signed word comparisons (<s/\<le>s)
- StarForth_Stack_Words.thy: PICK/ROLL against real C ground truth
- StarForth_Arithmetic_Words.thy: ABS/MIN/MAX/div/mod rebuilt on signed
  word semantics (cell_sdiv/cell_smod match C99 truncating division;
  2/ uses signed_drop_bit to match "n >> 1"); documents a genuine
  ABS(INT64_MIN) wraparound hazard mirroring the real C behavior
- StarForth_Memory_Words.thy: @/!/C@/C! address checks converted to
  the signed order

All 23 theory files verify with zero errors, including
StarForth_Concurrent and StarForth_Correctness.

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

proof/StarForth_Arithmetic_Words.thy

@@ -150,13 +150,13 @@ definition forth_div :: "vm_state \<Rightarrow> vm_state" where
        n2 # n1 # rest \<Rightarrow>
          if n2 = 0
          then set_error vm
-         else vm\<lparr>data_stack := (n1 div n2) # rest\<rparr>
+         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) = (n1 div n2) # rest"
+  shows "data_stack (forth_div vm) = (cell_sdiv n1 n2) # rest"
   by (simp add: forth_div_def assms)
 
 lemma div_by_zero:
@@ -182,13 +182,13 @@ definition forth_mod :: "vm_state \<Rightarrow> vm_state" where
        n2 # n1 # rest \<Rightarrow>
          if n2 = 0
          then set_error vm
-         else vm\<lparr>data_stack := (n1 mod n2) # rest\<rparr>
+         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) = (n1 mod n2) # rest"
+  shows "data_stack (forth_mod vm) = (cell_smod n1 n2) # rest"
   by (simp add: forth_mod_def assms)
 
 lemma mod_by_zero:
@@ -212,28 +212,28 @@ definition forth_divmod :: "vm_state \<Rightarrow> vm_state" where
          then set_error vm
          else if ds_full vm
               then set_error vm
-              else vm\<lparr>data_stack := (n1 div n2) # (n1 mod n2) # rest\<rparr>
+              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) = (n1 div n2) # (n1 mod n2) # rest"
+  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)) = n1 div n2"
+  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))) = n1 mod n2"
+  shows "hd (tl (data_stack (forth_divmod vm))) = cell_smod n1 n2"
   by (simp add: forth_divmod_def assms)
 
 (* ── 1+ ( n -- n+1 ) ───────────────────────────────────────────────────── *)
@@ -298,37 +298,90 @@ lemma two_mul_normal:
   by (simp add: forth_two_mul_def unop_def assms)
 
 (* ── 2/ ( n -- n/2 ) ───────────────────────────────────────────────────── *)
-(* Arithmetic right shift by 1 in C.  In HOL, div 2 on int is floor div.   *)
+(* 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 (\<lambda>n. n div 2)"
+  "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) = (n div 2) # 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 abs"
+  "forth_abs = unop cell_abs"
 
 lemma abs_normal:
   assumes "data_stack vm = n # xs"
-  shows "data_stack (forth_abs vm) = \<bar>n\<bar> # 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"
-  shows "hd (data_stack (forth_abs vm)) \<ge> 0"
+  assumes "cell_safe n"
-  by (simp add: forth_abs_def unop_def assms)
+  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))"
-  by (simp add: forth_abs_def unop_def assms)
+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 = []"
@@ -357,19 +410,22 @@ lemma negate_underflow:
 
 (* ── 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 min"
+  "forth_min = binop signed.min"
 
 lemma min_normal:
   assumes "data_stack vm = n2 # n1 # rest"
-  shows "data_stack (forth_min vm) = min n1 n2 # 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 min.commute)
+  by (simp add: forth_min_def binop_def assms signed.min.commute)
 
 lemma min_idempotent:
   assumes "data_stack vm = n # n # rest"
@@ -384,18 +440,18 @@ lemma min_underflow_nil:
 (* ── MAX ( n1 n2 -- n3 ) ───────────────────────────────────────────────── *)
 
 definition forth_max :: "vm_state \<Rightarrow> vm_state" where
-  "forth_max = binop max"
+  "forth_max = binop signed.max"
 
 lemma max_normal:
   assumes "data_stack vm = n2 # n1 # rest"
-  shows "data_stack (forth_max vm) = max n1 n2 # 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 max.commute)
+  by (simp add: forth_max_def binop_def assms signed.max.commute)
 
 lemma max_idempotent:
   assumes "data_stack vm = n # n # rest"
@@ -410,7 +466,7 @@ lemma max_underflow_nil:
 (* ── min/max algebraic relationship ────────────────────────────────────── *)
 
 lemma min_le_max:
-  "min (a::int) b \<le> max a b"
+  "signed.min (a::cell) b \<le>s signed.max a b"
-  by (simp add: min_def max_def)
+  by (cases "a \<le>s b") (simp_all add: signed.min_def signed.max_def signed.linear)
 
 end

proof/StarForth_Base.thy

@@ -1,7 +1,12 @@
 theory StarForth_Base
-  imports Main
+  imports "HOL-Library.Word"
 begin
 
+(* AND/OR/XOR infix notation moved behind an opt-in bundle at some point
+   after 2011 -- unbundled by default now. Needed here since cell is now a
+   word type and several word derivations use it (see Section 1 below). *)
+unbundle bit_operations_syntax
+
 (* =========================================================================
    SPECIFICATION AUTHORITY NOTICE
    ─────────────────────────────────────────────────────────────────────────
@@ -29,18 +34,33 @@ begin
 
 (* ○ CODE-MUST-MATCH: cell_t in include/vm.h is `typedef signed long cell_t`.
    On x86-64 Linux, signed long = 64-bit signed integer.
-   We model it as HOL int (arbitrary precision).
+
-   All word proofs hold in C provided no intermediate value overflows the
+   CORRECTED 2026-08-13: was modeled as HOL int (arbitrary precision,
-   64-bit signed range.  This is not a hidden assumption — it is the stated
+   never wraps). Changed to a genuine 64-bit word, matching how
-   correctness domain for FORTH programs that avoid overflow UB.            *)
+   StarForth_Q48_16.thy already models q48. The old int model made every
-type_synonym cell = int
+   wraparound-dependent C behavior inexpressible (confirmed while scoping
+   StarForth_Double_Words.thy: D+/D-/DNEGATE explicitly do carry/borrow
+   arithmetic and bitwise-complement wraparound that only make sense
+   against a fixed-width type). cell_t is C's *signed* long, so value
+   comparisons on cell throughout this proof suite use the Word library's
+   SIGNED order (<s, \<le>s, sint) rather than the default unsigned (<, \<le>),
+   which does not match FORTH's signed-integer semantics (e.g. -1 must
+   compare less than 0, not greater, as it would under unsigned order).
+   Structural comparisons (list lengths, nat indices) are unaffected and
+   stay plain nat as before -- only actual cell VALUES need <s/\<le>s. *)
+type_synonym cell = "64 word"
 
 (* ○ CODE-MUST-MATCH: include/vm.h defines:
      #define FORTH_TRUE  ((cell_t)-1)
      #define FORTH_FALSE ((cell_t) 0)
    Any C logical word that produces a boolean result MUST use these macros,
    not raw 1/0 or any other encoding.  Verified in:
-     src/word_source/logical_words.c — ALL comparison and test words         *)
+     src/word_source/logical_words.c — ALL comparison and test words
+
+   -1 as a cell (64 word) numeral is already the correct two's-complement
+   all-ones bit pattern (0xFFFFFFFFFFFFFFFF) via Word's standard numeral
+   semantics -- identical to C's (cell_t)-1 bit-for-bit, no change needed
+   here despite the type change above.                                    *)
 definition forth_true :: cell where "forth_true  = -1"
 definition forth_false :: cell where "forth_false =  0"
 
@@ -54,6 +74,119 @@ lemma to_forth_bool_False [simp]: "to_forth_bool False =  0"
 lemma to_forth_bool_eq: "to_forth_bool b = (if b then -1 else 0)"
   by (cases b; simp)
 
+(* =========================================================================
+   Reusable safe-arithmetic infrastructure for cell (64 word) values,
+   added during the cell-as-word migration 2026-08-13.
+
+   Every numeric constant this proof suite actually uses (HEAT_MAX =
+   10^6, ACL_MAX_TTL = 65535, DECAY_SLOPE_MAX in the low millions, etc.)
+   is many orders of magnitude below the 64-bit signed range
+   [-2^63, 2^63-1]. cell_safe below names a single generous safe zone
+   (|c| < 2^32, still 2^31 times larger than any constant actually in
+   use) so every call site needs only "cell_safe c" (or the two bare
+   inequalities it unfolds to) instead of re-deriving a
+   signed_take_bit/sint no-overflow argument from scratch every time a
+   proof adds or subtracts 1 from a cell value near a bound. Without
+   this, +1/-1 near a bound is NOT provably safe in general -- a bare
+   64-bit word wraps -- so this is a genuine hypothesis every such lemma
+   needs, not a formality. *)
+
+definition cell_safe :: "cell \<Rightarrow> bool" where
+  "cell_safe c \<longleftrightarrow> -4294967296 \<le>s c \<and> c \<le>s 4294967296"  \<comment> \<open>|c| < 2^32\<close>
+
+lemma cell_safe_sint_bounds:
+  assumes "cell_safe c"
+  shows "-4294967296 \<le> sint c" "sint c \<le> 4294967296"
+  using assms by (simp_all add: cell_safe_def word_sle_eq)
+
+(* The one lemma every "+1 near a bound" argument actually needs: adding
+   or subtracting a small delta to a cell_safe value produces exactly
+   the expected sint, no wraparound -- because the safe zone leaves a
+   2^31-times margin against the true 2^63 boundary. *)
+lemma cell_safe_add_sint:
+  assumes "cell_safe c"
+  assumes "\<bar>delta\<bar> \<le> 4294967296"
+  shows "sint (c + word_of_int delta) = sint c + delta"
+proof -
+  have b: "-4294967296 \<le> sint c" "sint c \<le> 4294967296"
+    using assms(1) by (simp_all add: cell_safe_sint_bounds)
+  have step1: "sint (c + word_of_int delta)
+      = signed_take_bit 63 (sint c + sint (word_of_int delta :: cell))"
+    by (simp add: sint_word_add)
+  have step2: "sint (word_of_int delta :: cell) = delta"
+    using assms(2)
+    by (simp add: sint_sbintrunc' signed_take_bit_int_eq_self)
+  have step3: "signed_take_bit 63 (sint c + delta) = sint c + delta"
+    by (rule signed_take_bit_int_eq_self) (use b assms(2) in auto)
+  from step1 step2 step3 show ?thesis by simp
+qed
+
+lemma cell_safe_1 [simp]: "cell_safe 1"
+  by (simp add: cell_safe_def word_sle_eq)
+lemma cell_safe_0 [simp]: "cell_safe 0"
+  by (simp add: cell_safe_def word_sle_eq)
+
+(* Subtraction variant, for the common "de_heat e - amount" shape (amount
+   is itself a cell parameter, not a fixed literal, so cell_safe_add_sint
+   with a literal delta doesn't directly apply). *)
+lemma cell_safe_sub_sint:
+  assumes "cell_safe c"
+  assumes "cell_safe amount"
+  shows "sint (c - amount) = sint c - sint amount"
+proof -
+  have bc: "-4294967296 \<le> sint c" "sint c \<le> 4294967296"
+    using assms(1) by (simp_all add: cell_safe_sint_bounds)
+  have ba: "-4294967296 \<le> sint amount" "sint amount \<le> 4294967296"
+    using assms(2) by (simp_all add: cell_safe_sint_bounds)
+  have "sint (c - amount) = signed_take_bit 63 (sint c - sint amount)"
+    by (simp add: sint_word_diff)
+  also have "\<dots> = sint c - sint amount"
+    by (rule signed_take_bit_int_eq_self) (use bc ba in auto)
+  finally show ?thesis .
+qed
+
+(* Every "nat n" conversion the old int-based PICK/ROLL/etc. definitions
+   did becomes "unat n" under the word migration -- but unat reinterprets
+   the raw bit pattern as unsigned, which only agrees with the natural
+   "nat of the signed value" reading when n is non-negative in the SIGNED
+   sense (0 \<le>s n). Every call site that uses this already checks n <s 0
+   first and only reaches the nat-conversion in the non-negative case, so
+   this lemma is exactly the bridge those proofs need, proved once here
+   rather than re-derived at every site. *)
+lemma unat_eq_nat_sint_of_nonneg:
+  assumes "0 \<le>s (n :: cell)"
+  shows "unat n = nat (sint n)"
+proof -
+  have lo: "0 \<le> sint n" using assms by (simp add: word_sle_eq)
+  have hi63: "sint n < 2 ^ 63" using sint_lt[of n] by simp
+  have hi: "sint n < 2 ^ (64::nat)" using hi63 by simp
+  have "uint n = take_bit (64::nat) (sint n)" by (simp add: uint_sint)
+  also have "\<dots> = sint n"
+    by (rule take_bit_int_eq_self) (use lo hi in auto)
+  finally show ?thesis by (simp add: unat_eq_nat_uint)
+qed
+
+(* Signed absolute value on cell.  word's inherited "abs" (if it resolved at
+   all) would be unsigned-magnitude, which is wrong for cell_t's signed
+   semantics -- must build this explicitly from the signed order <s.
+   NOTE: cell_abs min_word = min_word (two's-complement negation of
+   INT64_MIN wraps back to itself, matching C's ABS(LONG_MIN) hazard) --
+   this is a genuine, documented exclusion, not an oversight. *)
+definition cell_abs :: "cell \<Rightarrow> cell" where
+  "cell_abs n = (if n <s 0 then -n else n)"
+
+(* Signed truncating division/remainder, matching C99's "/" and "%" on
+   signed cell_t: quotient truncates toward zero, remainder takes the sign
+   of the dividend.  word's inherited div/mod are unsigned-magnitude and
+   would silently give the wrong answer for negative operands -- e.g.
+   (-7) div 2 under unsigned word semantics treats the bit pattern of -7 as
+   a huge positive number, nothing like C's -7 / 2 = -3. *)
+definition cell_sdiv :: "cell \<Rightarrow> cell \<Rightarrow> cell" where
+  "cell_sdiv a b = word_of_int (sgn (sint a) * sgn (sint b) * (\<bar>sint a\<bar> div \<bar>sint b\<bar>))"
+
+definition cell_smod :: "cell \<Rightarrow> cell \<Rightarrow> cell" where
+  "cell_smod a b = word_of_int (sgn (sint a) * (\<bar>sint a\<bar> mod \<bar>sint b\<bar>))"
+
 (* =========================================================================
    Section 2: Stack type and capacity constants
    ======================================================================== *)

proof/StarForth_Loop1_Heat.thy

@@ -35,6 +35,19 @@ definition HEAT_MAX          :: cell where "HEAT_MAX          = 1000000"
 (* Demote from hot-words cache below this threshold *)
 definition HEAT_DEMOTION_THR :: cell where "HEAT_DEMOTION_THR = 10"
 
+lemma HEAT_MAX_cell_safe [simp]: "cell_safe HEAT_MAX"
+  by (simp add: cell_safe_def HEAT_MAX_def word_sle_eq)
+
+lemma HEAT_MAX_lt_succ: "HEAT_MAX <s HEAT_MAX + 1"
+proof -
+  have "sint (HEAT_MAX + 1) = sint HEAT_MAX + 1"
+    using cell_safe_add_sint[OF HEAT_MAX_cell_safe, of 1] by simp
+  thus ?thesis by (simp add: word_sless_alt)
+qed
+
+lemma HEAT_MAX_nonneg: "0 \<le>s HEAT_MAX"
+  by (simp add: HEAT_MAX_def word_sle_eq)
+
 (* Word flag bits (match C macros in include/vm.h) *)
 definition FLAG_FROZEN :: nat where "FLAG_FROZEN = 4"   \<comment> \<open>WORD_FROZEN 0x04\<close>
 definition FLAG_PINNED :: nat where "FLAG_PINNED = 8"   \<comment> \<open>WORD_PINNED 0x08\<close>
@@ -49,8 +62,26 @@ definition heat_frozen :: "dict_entry \<Rightarrow> bool" where
 definition heat_pinned :: "dict_entry \<Rightarrow> bool" where
   "heat_pinned e \<longleftrightarrow> de_flags e AND FLAG_PINNED = FLAG_PINNED"
 
+(* CORRECTED 2026-08-13 (cell = 64 word migration): every comparison on a
+   cell value below uses the Word library's SIGNED order (<s, \<le>s,
+   signed.min, signed.max) instead of the default unsigned order (<, \<le>,
+   min, max) that a bare word type gets by default. cell_t is C's
+   *signed* long -- under unsigned order, -1 would compare greater than
+   any positive value, which is simply wrong for FORTH's signed integer
+   semantics. Structural nat/list-length reasoning elsewhere is
+   unaffected. *)
 definition heat_valid :: "dict_entry \<Rightarrow> bool" where
-  "heat_valid e \<longleftrightarrow> de_heat e \<ge> 0 \<and> de_heat e \<le> HEAT_MAX"
+  "heat_valid e \<longleftrightarrow> 0 \<le>s de_heat e \<and> de_heat e \<le>s HEAT_MAX"
+
+(* Bridging lemma: any de_heat within heat_valid's own range is
+   automatically cell_safe (HEAT_MAX = 10^6 sits far inside the 2^32 safe
+   zone), so lemmas that already assume heat_valid never need to also
+   assume cell_safe separately -- it comes for free. *)
+lemma heat_valid_imp_cell_safe:
+  assumes "heat_valid e"
+  shows "cell_safe (de_heat e)"
+  using assms
+  by (simp add: heat_valid_def cell_safe_def HEAT_MAX_def word_sle_eq word_sless_alt)
 
 (* =========================================================================
    Section 3: Heat increment (fired on every word execution)
@@ -59,37 +90,71 @@ definition heat_valid :: "dict_entry \<Rightarrow> bool" where
 (* Saturating increment: heat grows by 1, capped at HEAT_MAX. *)
 definition heat_increment :: "dict_entry \<Rightarrow> dict_entry" where
   "heat_increment e =
-     e\<lparr>de_heat := min (de_heat e + 1) HEAT_MAX\<rparr>"
+     e\<lparr>de_heat := signed.min (de_heat e + 1) HEAT_MAX\<rparr>"
 
+(* CORRECTED for the cell-as-word migration: added the "cell_safe" side
+   condition. Under a bare 64-bit word, "de_heat e < HEAT_MAX \<Longrightarrow>
+   de_heat e + 1 \<le> HEAT_MAX" is only true if the +1 doesn't wrap -- see
+   cell_safe_add_sint in StarForth_Base.thy. Any de_heat within
+   heat_valid's own range is trivially cell_safe (HEAT_MAX is 10^6, far
+   inside the 2^32 safe zone), so this costs nothing in practice. *)
 lemma heat_increment_correct:
-  assumes "de_heat e < HEAT_MAX"
+  assumes "de_heat e <s HEAT_MAX"
+  assumes "cell_safe (de_heat e)"
   shows "de_heat (heat_increment e) = de_heat e + 1"
-  using assms by (simp add: heat_increment_def min_def)
+proof -
+  have sint_eq: "sint (de_heat e + 1) = sint (de_heat e) + 1"
+    using cell_safe_add_sint[OF assms(2), of 1] by simp
+  have "de_heat e + 1 \<le>s HEAT_MAX"
+    using sint_eq assms(1) by (simp add: word_sle_eq word_sless_alt)
+  thus ?thesis
+    by (simp add: heat_increment_def signed.min_def)
+qed
 
 lemma heat_increment_saturates:
   assumes "de_heat e = HEAT_MAX"
   shows "de_heat (heat_increment e) = HEAT_MAX"
-  by (simp add: heat_increment_def assms)
+proof -
+  have "\<not> HEAT_MAX + 1 \<le>s HEAT_MAX"
+    using HEAT_MAX_lt_succ by (simp add: word_sless_alt word_sle_eq)
+  thus ?thesis
+    by (simp add: heat_increment_def assms signed.min_def)
+qed
 
 (* CORRECTED 2026-08-13: added the missing upper-bound hypothesis. Without
    it, if de_heat e already exceeds HEAT_MAX, the min-clamp in
    heat_increment could pull the result back down below de_heat e,
    breaking monotonicity. *)
 lemma heat_increment_non_decreasing:
-  assumes "de_heat e \<le> HEAT_MAX"
+  assumes "de_heat e \<le>s HEAT_MAX"
-  shows "de_heat (heat_increment e) \<ge> de_heat e"
+  assumes "cell_safe (de_heat e)"
-  using assms by (simp add: heat_increment_def)
+  shows "de_heat e \<le>s de_heat (heat_increment e)"
+proof -
+  have sint_eq: "sint (de_heat e + 1) = sint (de_heat e) + 1"
+    using cell_safe_add_sint[OF assms(2), of 1] by simp
+  have "de_heat e \<le>s de_heat e + 1"
+    using sint_eq by (simp add: word_sle_eq)
+  thus ?thesis
+    using assms(1) by (simp add: heat_increment_def signed.min_def)
+qed
 
 lemma heat_increment_preserves_validity:
   assumes "heat_valid e"
   shows "heat_valid (heat_increment e)"
 proof -
-  have h0: "de_heat e \<ge> 0" and hmax: "de_heat e \<le> HEAT_MAX"
+  have h0: "0 \<le>s de_heat e" and hmax: "de_heat e \<le>s HEAT_MAX"
     using assms by (simp_all add: heat_valid_def)
-  have le: "de_heat (heat_increment e) \<le> HEAT_MAX"
+  have safe: "cell_safe (de_heat e)"
-    unfolding heat_increment_def by (simp add: min.cobounded2)
+    using assms by (rule heat_valid_imp_cell_safe)
-  have ge: "de_heat (heat_increment e) \<ge> 0"
+  have sint_eq: "sint (de_heat e + 1) = sint (de_heat e) + 1"
-    unfolding heat_increment_def using h0 by (simp add: HEAT_MAX_def)
+    using cell_safe_add_sint[OF safe, of 1] by simp
+  have step_pos: "0 \<le>s de_heat e + 1"
+    using h0 sint_eq by (simp add: word_sle_eq)
+  have le: "de_heat (heat_increment e) \<le>s HEAT_MAX"
+    unfolding heat_increment_def by (simp add: signed.min_def)
+  have ge: "0 \<le>s de_heat (heat_increment e)"
+    unfolding heat_increment_def using step_pos hmax HEAT_MAX_nonneg
+    by (simp add: signed.min_def)
   from le ge show ?thesis by (simp add: heat_valid_def)
 qed
 
@@ -116,8 +181,8 @@ definition heat_decay :: "cell \<Rightarrow> dict_entry \<Rightarrow> dict_entry
      (if heat_frozen e
       then e                        \<comment> \<open>FROZEN: no decay\<close>
       else if heat_pinned e
-           then e\<lparr>de_heat := max 1 (de_heat e - amount)\<rparr>   \<comment> \<open>PINNED: floor at 1\<close>
+           then e\<lparr>de_heat := signed.max 1 (de_heat e - amount)\<rparr>   \<comment> \<open>PINNED: floor at 1\<close>
-           else e\<lparr>de_heat := max 0 (de_heat e - amount)\<rparr>)" \<comment> \<open>normal: floor at 0\<close>
+           else e\<lparr>de_heat := signed.max 0 (de_heat e - amount)\<rparr>)" \<comment> \<open>normal: floor at 0\<close>
 
 lemma heat_decay_frozen:
   assumes "heat_frozen e"
@@ -127,41 +192,71 @@ lemma heat_decay_frozen:
 (* CORRECTED 2026-08-13: added the missing lower-bound hypothesis. In the
    PINNED branch, heat_decay floors at max 1 (de_heat e - amount) -- if
    de_heat e was already below 1 (e.g. 0), the floor raises it, breaking
-   monotonicity. de_heat e \<ge> 1 is the standing invariant a pinned word is
+   monotonicity. de_heat e \<ge>s 1 is the standing invariant a pinned word is
-   supposed to maintain (see heat_decay_pinned_positive's own \<ge> 1
+   supposed to maintain (see heat_decay_pinned_positive's own \<ge>s 1
    conclusion below), just never stated here as a precondition before. *)
 lemma heat_decay_monotone:
   assumes "\<not> heat_frozen e"
-  assumes "de_heat e \<ge> 1"
+  assumes "1 \<le>s de_heat e"
-  assumes "amount \<ge> 0"
+  assumes "0 \<le>s amount"
-  shows "de_heat (heat_decay amount e) \<le> de_heat e"
+  assumes "cell_safe (de_heat e)"
-  using assms by (simp add: heat_decay_def)
+  assumes "cell_safe amount"
+  shows "de_heat (heat_decay amount e) \<le>s de_heat e"
+proof -
+  have zero_le: "0 \<le>s de_heat e"
+    using assms(2) by (simp add: word_sle_eq)
+  have sub_sint: "sint (de_heat e - amount) = sint (de_heat e) - sint amount"
+    using cell_safe_sub_sint[OF assms(4) assms(5)] .
+  have amount_nonneg: "0 \<le> sint amount" using assms(3) by (simp add: word_sle_eq)
+  have sub_le: "de_heat e - amount \<le>s de_heat e"
+    using sub_sint amount_nonneg by (simp add: word_sle_eq)
+  show ?thesis
+    using assms zero_le sub_le by (simp add: heat_decay_def signed.max_def)
+qed
 
 lemma heat_decay_non_negative:
   assumes "\<not> heat_frozen e"
   assumes "\<not> heat_pinned e"
-  shows "de_heat (heat_decay amount e) \<ge> 0"
+  shows "0 \<le>s de_heat (heat_decay amount e)"
-  by (simp add: heat_decay_def assms)
+  by (simp add: heat_decay_def assms signed.max_def)
 
 lemma heat_decay_pinned_positive:
   assumes "\<not> heat_frozen e"
   assumes "heat_pinned e"
-  shows "de_heat (heat_decay amount e) \<ge> 1"
+  shows "1 \<le>s de_heat (heat_decay amount e)"
-  by (simp add: heat_decay_def assms)
+  by (simp add: heat_decay_def assms signed.max_def)
 
 lemma heat_decay_preserves_validity:
   assumes "heat_valid e"
   assumes "\<not> heat_frozen e"
-  assumes "amount \<ge> 0"
+  assumes "0 \<le>s amount"
+  assumes "cell_safe amount"
   shows "heat_valid (heat_decay amount e)"
-proof (cases "heat_pinned e")
+proof -
-  case True
+  have safe_e: "cell_safe (de_heat e)"
-  thus ?thesis
+    using assms(1) by (rule heat_valid_imp_cell_safe)
-    using assms by (simp add: heat_valid_def heat_decay_def HEAT_MAX_def)
+  have sub_sint: "sint (de_heat e - amount) = sint (de_heat e) - sint amount"
-next
+    using cell_safe_sub_sint[OF safe_e assms(4)] .
-  case False
+  have hmax: "de_heat e \<le>s HEAT_MAX" using assms(1) by (simp add: heat_valid_def)
-  thus ?thesis
+  have amount_nonneg: "0 \<le> sint amount" using assms(3) by (simp add: word_sle_eq)
-    using assms by (simp add: heat_valid_def heat_decay_def HEAT_MAX_def)
+  have sub_le_max: "de_heat e - amount \<le>s HEAT_MAX"
+    using sub_sint hmax amount_nonneg by (simp add: word_sle_eq)
+  have one_le_max: "1 \<le>s HEAT_MAX"
+    by (simp add: HEAT_MAX_def word_sle_eq)
+  have zero_le_one: "0 \<le>s (1 :: cell)"
+    by (simp add: word_sle_eq)
+  show ?thesis
+  proof (cases "heat_pinned e")
+    case True
+    thus ?thesis
+      using sub_le_max one_le_max zero_le_one
+      by (simp add: heat_valid_def heat_decay_def assms(2) signed.max_def word_sle_eq)
+  next
+    case False
+    thus ?thesis
+      using sub_le_max HEAT_MAX_nonneg
+      by (simp add: heat_valid_def heat_decay_def assms(2) signed.max_def)
+  qed
 qed
 
 lemma heat_decay_preserves_flags:
@@ -185,10 +280,10 @@ definition dict_heat_wf :: "vm_state \<Rightarrow> bool" where
    Well-formedness: thresholds are in ascending order and non-negative.      *)
 definition heat_thresholds_wf :: "vm_state \<Rightarrow> bool" where
   "heat_thresholds_wf vm \<longleftrightarrow>
-     heat_threshold_25th vm \<ge> 0 \<and>
+     0 \<le>s heat_threshold_25th vm \<and>
-     heat_threshold_25th vm \<le> heat_threshold_50th vm \<and>
+     heat_threshold_25th vm \<le>s heat_threshold_50th vm \<and>
-     heat_threshold_50th vm \<le> heat_threshold_75th vm \<and>
+     heat_threshold_50th vm \<le>s heat_threshold_75th vm \<and>
-     heat_threshold_75th vm \<le> HEAT_MAX"
+     heat_threshold_75th vm \<le>s HEAT_MAX"
 
 (* A pure data-stack word does not change heat thresholds or dictionary heat. *)
 lemma ds_word_preserves_dict_heat:

proof/StarForth_Loop3_Decay.thy

@@ -144,10 +144,16 @@ lemma vm_decay_step_dict [simp]:
    Section 5: Total heat — fully proved monotonicity
    ======================================================================== *)
 
+(* CORRECTED for the cell-as-word migration: sums sint (de_heat ...), not
+   de_heat directly. de_heat is now a bounded 64-bit word per entry, but
+   the AGGREGATE across an unbounded number of dictionary entries should
+   not itself be silently truncated to 64 bits -- summing the signed int
+   value of each entry keeps total_dict_heat genuinely unbounded, as
+   intended. *)
 definition total_dict_heat :: "vm_state \<Rightarrow> int" where
   "total_dict_heat vm =
      (\<Sum>i \<in> {i. dictionary vm i \<noteq> None}.
-       de_heat (the (dictionary vm i)))"
+       sint (de_heat (the (dictionary vm i))))"
 
 (* PROOF (no sorry):
    vm_decay_step only changes decay_slope_q48, so dictionary is identical
@@ -159,7 +165,7 @@ lemma decay_step_dict_unchanged:
   by simp   \<comment> \<open>vm_decay_step_dict [simp] rewrites the dictionary field\<close>
 
 lemma decay_total_heat_non_increasing:
-  assumes "\<forall>i. dictionary vm i \<noteq> None \<longrightarrow> de_heat (the (dictionary vm i)) \<ge> 0"
+  assumes "\<forall>i. dictionary vm i \<noteq> None \<longrightarrow> 0 \<le>s de_heat (the (dictionary vm i))"
   shows "total_dict_heat (vm_decay_step step vm) \<le> total_dict_heat vm"
   by (simp add: decay_step_dict_unchanged)
 

proof/StarForth_Memory_Words.thy

@@ -53,27 +53,29 @@ definition forth_fetch :: "vm_state \<Rightarrow> vm_state" where
     (case data_stack vm of
        []         \<Rightarrow> set_error vm
      | addr # xs \<Rightarrow>
-         if addr < 0
+         if addr <s 0
          then set_error vm
-         else vm\<lparr>data_stack := mem_read (memory vm) (nat addr) # xs\<rparr>)"
+         else vm\<lparr>data_stack := mem_read (memory vm) (unat addr) # xs\<rparr>)"
 
 lemma fetch_normal:
   assumes "data_stack vm = addr # xs"
-  assumes "addr \<ge> 0"
+  assumes "0 \<le>s addr"
-  shows "data_stack (forth_fetch vm) = mem_read (memory vm) (nat addr) # xs"
+  shows "data_stack (forth_fetch vm) = mem_read (memory vm) (unat addr) # xs"
-  using assms by (auto simp: forth_fetch_def)
+  using assms by (auto simp: forth_fetch_def word_sle_eq word_sless_alt)
 
 lemma fetch_reads_stored_value:
   assumes "memory vm = mem_write m a v"
-  assumes "data_stack vm = int a # xs"
+  assumes "data_stack vm = addr # xs"
+  assumes "0 \<le>s addr"
+  assumes "unat addr = a"
   shows "hd (data_stack (forth_fetch vm)) = v"
-  by (simp add: forth_fetch_def mem_read_def mem_write_def assms)
+  using assms by (simp add: forth_fetch_def mem_read_def mem_write_def word_sle_eq word_sless_alt)
 
 lemma fetch_depth_preserved:
   assumes "data_stack vm = addr # xs"
-  assumes "addr \<ge> 0"
+  assumes "0 \<le>s addr"
   shows "length (data_stack (forth_fetch vm)) = length (data_stack vm)"
-  by (simp add: forth_fetch_def assms)
+  by (simp add: forth_fetch_def assms word_sle_eq word_sless_alt)
 
 lemma fetch_underflow:
   assumes "data_stack vm = []"
@@ -82,7 +84,7 @@ lemma fetch_underflow:
 
 lemma fetch_neg_addr:
   assumes "data_stack vm = addr # xs"
-  assumes "addr < 0"
+  assumes "addr <s 0"
   shows "vm_error (forth_fetch vm)"
   by (simp add: forth_fetch_def set_error_def assms)
 
@@ -94,37 +96,37 @@ definition forth_store :: "vm_state \<Rightarrow> vm_state" where
   "forth_store vm =
     (case data_stack vm of
        addr # n # xs \<Rightarrow>
-         if addr < 0
+         if addr <s 0
          then set_error vm
          else vm\<lparr>data_stack := xs,
-                  memory    := mem_write (memory vm) (nat addr) n\<rparr>
+                  memory    := mem_write (memory vm) (unat addr) n\<rparr>
      | _ \<Rightarrow> set_error vm)"
 
 lemma store_normal:
   assumes "data_stack vm = addr # n # xs"
-  assumes "addr \<ge> 0"
+  assumes "0 \<le>s addr"
   shows "data_stack (forth_store vm) = xs"
-    and "memory (forth_store vm) = mem_write (memory vm) (nat addr) n"
+    and "memory (forth_store vm) = mem_write (memory vm) (unat addr) n"
-  using assms by (auto simp: forth_store_def)
+  using assms by (auto simp: forth_store_def word_sle_eq word_sless_alt)
 
 lemma store_writes_value:
   assumes "data_stack vm = addr # n # xs"
-  assumes "addr \<ge> 0"
+  assumes "0 \<le>s addr"
-  shows "mem_read (memory (forth_store vm)) (nat addr) = n"
+  shows "mem_read (memory (forth_store vm)) (unat addr) = n"
-  using assms by (auto simp: forth_store_def mem_write_def mem_read_def)
+  using assms by (auto simp: forth_store_def mem_write_def mem_read_def word_sle_eq word_sless_alt)
 
 lemma store_depth_decreases:
   assumes "data_stack vm = addr # n # xs"
-  assumes "addr \<ge> 0"
+  assumes "0 \<le>s addr"
   shows "length (data_stack (forth_store vm)) = length (data_stack vm) - 2"
-  using assms by (auto simp: forth_store_def)
+  using assms by (auto simp: forth_store_def word_sle_eq word_sless_alt)
 
 lemma store_other_unchanged:
   assumes "data_stack vm = addr # n # xs"
-  assumes "addr \<ge> 0"
+  assumes "0 \<le>s addr"
-  assumes "nat addr \<noteq> b"
+  assumes "unat addr \<noteq> b"
   shows "mem_read (memory (forth_store vm)) b = mem_read (memory vm) b"
-  using assms by (auto simp: forth_store_def mem_write_def mem_read_def)
+  using assms by (auto simp: forth_store_def mem_write_def mem_read_def word_sle_eq word_sless_alt)
 
 lemma store_underflow_nil:
   assumes "data_stack vm = []"
@@ -138,7 +140,7 @@ lemma store_underflow_one:
 
 lemma store_neg_addr:
   assumes "data_stack vm = addr # n # xs"
-  assumes "addr < 0"
+  assumes "addr <s 0"
   shows "vm_error (forth_store vm)"
   by (simp add: forth_store_def set_error_def assms)
 
@@ -146,12 +148,12 @@ lemma store_neg_addr:
 
 lemma store_then_fetch:
   assumes "data_stack vm = addr # n # xs"
-  assumes "addr \<ge> 0"
+  assumes "0 \<le>s addr"
   assumes "data_stack vm' = addr # xs"
   assumes "memory vm' = memory (forth_store vm)"
-  assumes "addr \<ge> 0"
   shows "hd (data_stack (forth_fetch vm')) = n"
-  using assms by (auto simp: forth_fetch_def forth_store_def mem_write_def mem_read_def)
+  using assms by (auto simp: forth_fetch_def forth_store_def mem_write_def mem_read_def
+                              word_sle_eq word_sless_alt)
 
 (* ── C@ ( addr -- c ) ──────────────────────────────────────────────────── *)
 (* Reads a single byte (0..255) from memory, zero-extended to cell width.
@@ -163,24 +165,25 @@ definition forth_cfetch :: "vm_state \<Rightarrow> vm_state" where
     (case data_stack vm of
        []         \<Rightarrow> set_error vm
      | addr # xs \<Rightarrow>
-         if addr < 0
+         if addr <s 0
          then set_error vm
-         else let byte = mem_read (memory vm) (nat addr) AND 0xFF
+         else let byte = mem_read (memory vm) (unat addr) AND 0xFF
               in vm\<lparr>data_stack := byte # xs\<rparr>)"
 
 lemma cfetch_normal:
   assumes "data_stack vm = addr # xs"
-  assumes "addr \<ge> 0"
+  assumes "0 \<le>s addr"
   shows "data_stack (forth_cfetch vm) =
-         (mem_read (memory vm) (nat addr) AND 0xFF) # xs"
+         (mem_read (memory vm) (unat addr) AND 0xFF) # xs"
-  using assms by (auto simp: forth_cfetch_def)
+  using assms by (auto simp: forth_cfetch_def word_sle_eq word_sless_alt)
 
 lemma cfetch_byte_range:
   assumes "data_stack vm = addr # xs"
-  assumes "addr \<ge> 0"
+  assumes "0 \<le>s addr"
   shows "0 \<le> hd (data_stack (forth_cfetch vm))"
     and "hd (data_stack (forth_cfetch vm)) \<le> 255"
-  using assms by (auto simp: forth_cfetch_def)
+  using assms word_and_le1[of "mem_read (memory vm) (unat addr)" "0xFF::cell"]
+  by (auto simp: forth_cfetch_def word_sle_eq word_sless_alt)
 
 lemma cfetch_underflow:
   assumes "data_stack vm = []"
@@ -189,7 +192,7 @@ lemma cfetch_underflow:
 
 lemma cfetch_neg_addr:
   assumes "data_stack vm = addr # xs"
-  assumes "addr < 0"
+  assumes "addr <s 0"
   shows "vm_error (forth_cfetch vm)"
   by (simp add: forth_cfetch_def set_error_def assms)
 
@@ -201,30 +204,30 @@ definition forth_cstore :: "vm_state \<Rightarrow> vm_state" where
   "forth_cstore vm =
     (case data_stack vm of
        addr # c # xs \<Rightarrow>
-         if addr < 0
+         if addr <s 0
          then set_error vm
          else vm\<lparr>data_stack := xs,
-                  memory    := mem_write (memory vm) (nat addr) (c AND 0xFF)\<rparr>
+                  memory    := mem_write (memory vm) (unat addr) (c AND 0xFF)\<rparr>
      | _ \<Rightarrow> set_error vm)"
 
 lemma cstore_normal:
   assumes "data_stack vm = addr # c # xs"
-  assumes "addr \<ge> 0"
+  assumes "0 \<le>s addr"
   shows "data_stack (forth_cstore vm) = xs"
-    and "memory (forth_cstore vm) = mem_write (memory vm) (nat addr) (c AND 0xFF)"
+    and "memory (forth_cstore vm) = mem_write (memory vm) (unat addr) (c AND 0xFF)"
-  using assms by (auto simp: forth_cstore_def)
+  using assms by (auto simp: forth_cstore_def word_sle_eq word_sless_alt)
 
 lemma cstore_writes_byte:
   assumes "data_stack vm = addr # c # xs"
-  assumes "addr \<ge> 0"
+  assumes "0 \<le>s addr"
-  shows "mem_read (memory (forth_cstore vm)) (nat addr) = c AND 0xFF"
+  shows "mem_read (memory (forth_cstore vm)) (unat addr) = c AND 0xFF"
-  using assms by (auto simp: forth_cstore_def mem_write_def mem_read_def)
+  using assms by (auto simp: forth_cstore_def mem_write_def mem_read_def word_sle_eq word_sless_alt)
 
 lemma cstore_depth_decreases:
   assumes "data_stack vm = addr # c # xs"
-  assumes "addr \<ge> 0"
+  assumes "0 \<le>s addr"
   shows "length (data_stack (forth_cstore vm)) = length (data_stack vm) - 2"
-  using assms by (auto simp: forth_cstore_def)
+  using assms by (auto simp: forth_cstore_def word_sle_eq word_sless_alt)
 
 lemma cstore_underflow_nil:
   assumes "data_stack vm = []"
@@ -238,17 +241,18 @@ lemma cstore_underflow_one:
 
 lemma cstore_neg_addr:
   assumes "data_stack vm = addr # c # xs"
-  assumes "addr < 0"
+  assumes "addr <s 0"
   shows "vm_error (forth_cstore vm)"
   by (simp add: forth_cstore_def set_error_def assms)
 
 (* C! then C@ round-trip: byte written is byte read back. *)
 lemma cstore_then_cfetch:
   assumes "data_stack vm = addr # c # xs"
-  assumes "addr \<ge> 0"
+  assumes "0 \<le>s addr"
   assumes "data_stack vm' = addr # xs"
   assumes "memory vm' = memory (forth_cstore vm)"
   shows "hd (data_stack (forth_cfetch vm')) = c AND 0xFF"
-  using assms by (auto simp: forth_cfetch_def forth_cstore_def mem_write_def mem_read_def)
+  using assms by (auto simp: forth_cfetch_def forth_cstore_def mem_write_def mem_read_def
+                              word_sle_eq word_sless_alt)
 
 end

proof/StarForth_Stack_Words.thy

@@ -295,11 +295,11 @@ 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 := int (length (data_stack vm)) # data_stack vm\<rparr>)"
+     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)) = int (length (data_stack 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:
@@ -327,7 +327,7 @@ lemma depth_overflow:
      val = data_stack[dsp - n]
      data_stack[dsp] = val       (replace TOS with val)
 
-   Bounds check: n \<ge> 0 and n < length (data_stack vm)                     *)
+   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,
@@ -338,7 +338,7 @@ lemma depth_overflow:
    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
-   "nat n \<ge> length (data_stack vm)" used the pre-pop length too, one too
+   "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
@@ -348,37 +348,37 @@ definition forth_pick :: "vm_state \<Rightarrow> vm_state" where
     (case data_stack vm of
        []     \<Rightarrow> set_error vm
      | n # xs \<Rightarrow>
-         if n < 0 \<or> nat n \<ge> length xs
+         if n <s 0 \<or> unat n \<ge> length xs
          then set_error vm
-         else vm\<lparr>data_stack := xs ! nat n # xs\<rparr>)"
+         else vm\<lparr>data_stack := xs ! unat n # xs\<rparr>)"
 
 lemma pick_normal:
   assumes "data_stack vm = n # xs"
-  assumes "n \<ge> 0"
+  assumes "0 \<le>s n"
-  assumes "nat n < length xs"
+  assumes "unat n < length xs"
-  shows "data_stack (forth_pick vm) = xs ! nat n # 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 "n \<ge> 0"
+  assumes "0 \<le>s n"
-  assumes "nat n < length xs"
+  assumes "unat n < length xs"
   shows "length (data_stack (forth_pick vm)) = length (data_stack vm)"
-  using assms by (auto simp: forth_pick_def)
+  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)
+  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)
+  using assms by (auto simp: forth_pick_def word_sless_alt word_sle_eq)
 
 lemma pick_underflow:
   assumes "data_stack vm = []"
@@ -387,13 +387,13 @@ lemma pick_underflow:
 
 lemma pick_bounds_neg:
   assumes "data_stack vm = n # xs"
-  assumes "n < 0"
+  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 "nat n \<ge> length xs"
+  assumes "unat n \<ge> length xs"
   shows "vm_error (forth_pick vm)"
   using assms by (auto simp: forth_pick_def set_error_def)
 
@@ -434,11 +434,11 @@ definition forth_roll :: "vm_state \<Rightarrow> vm_state" where
     (case data_stack vm of
        []     \<Rightarrow> set_error vm
      | n # xs \<Rightarrow>
-         if n < 0 \<or> nat n > length xs
+         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 - nat n;
+              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>)"
@@ -456,10 +456,11 @@ lemma roll_one_moves_bottom:
   assumes "xs \<noteq> []"
   shows "data_stack (forth_roll vm) = last xs # butlast xs"
 proof -
-  have i: "length xs - nat (1::int) = length xs - 1" by simp
+  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)
+    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
@@ -470,14 +471,14 @@ qed
 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)
+  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)
+  using assms by (simp add: forth_roll_def word_sless_alt word_sle_eq)
 
 lemma roll_underflow:
   assumes "data_stack vm = []"
@@ -486,13 +487,13 @@ lemma roll_underflow:
 
 lemma roll_bounds_neg:
   assumes "data_stack vm = n # xs"
-  assumes "n < 0"
+  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 "nat n > length xs"
+  assumes "unat n > length xs"
   shows "vm_error (forth_roll vm)"
   by (simp add: forth_roll_def set_error_def assms)