admin/LithosAnanake
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
Files
4dd1321ea4176bccbfb1d5fd218c5062536573c2
LithosAnanake/proof/StarForth_Arithmetic_Words.thy
T
Robert Allan JamesandClaude Sonnet 5 fe6e705867 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>
2026-08-13 13:37:07 -04:00

473 lines
19 KiB
Plaintext
Raw Blame History

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
Reference in New Issue View Git Blame Copy Permalink