From fe6e7058678542c68a650d69a0ce1350ce6d1bd1 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Thu, 13 Aug 2026 13:37:07 -0400 Subject: [PATCH] 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) - 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 --- proof/StarForth_Arithmetic_Words.thy | 104 ++++++++++++---- proof/StarForth_Base.thy | 147 +++++++++++++++++++++-- proof/StarForth_Loop1_Heat.thy | 171 +++++++++++++++++++++------ proof/StarForth_Loop3_Decay.thy | 10 +- proof/StarForth_Memory_Words.thy | 100 ++++++++-------- proof/StarForth_Stack_Words.thy | 49 ++++---- 6 files changed, 438 insertions(+), 143 deletions(-) diff --git a/proof/StarForth_Arithmetic_Words.thy b/proof/StarForth_Arithmetic_Words.thy index 55483c3..74e217d 100644 --- a/proof/StarForth_Arithmetic_Words.thy +++ b/proof/StarForth_Arithmetic_Words.thy @@ -150,13 +150,13 @@ definition forth_div :: "vm_state \ vm_state" where n2 # n1 # rest \ if n2 = 0 then set_error vm - else vm\data_stack := (n1 div n2) # rest\ + else vm\data_stack := (cell_sdiv n1 n2) # rest\ | _ \ set_error vm)" lemma div_normal: assumes "data_stack vm = n2 # n1 # rest" assumes "n2 \ 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 \ vm_state" where n2 # n1 # rest \ if n2 = 0 then set_error vm - else vm\data_stack := (n1 mod n2) # rest\ + else vm\data_stack := (cell_smod n1 n2) # rest\ | _ \ set_error vm)" lemma mod_normal: assumes "data_stack vm = n2 # n1 # rest" assumes "n2 \ 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 \ vm_state" where then set_error vm else if ds_full vm then set_error vm - else vm\data_stack := (n1 div n2) # (n1 mod n2) # rest\ + else vm\data_stack := (cell_sdiv n1 n2) # (cell_smod n1 n2) # rest\ | _ \ set_error vm)" lemma divmod_normal: assumes "data_stack vm = n2 # n1 # rest" assumes "n2 \ 0" assumes "\ 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 \ 0" assumes "\ 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 \ 0" assumes "\ 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 \ vm_state" where - "forth_two_div = unop (\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 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) = \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 + \ 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 "\ vm_error vm" - shows "hd (data_stack (forth_abs vm)) \ 0" - by (simp add: forth_abs_def unop_def assms) + assumes "cell_safe n" + shows "0 \s hd (data_stack (forth_abs vm))" +proof (cases "n 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 "\ 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 (-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 \ 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 \ 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 \ max a b" - by (simp add: min_def max_def) + "signed.min (a::cell) b \s signed.max a b" + by (cases "a \s b") (simp_all add: signed.min_def signed.max_def signed.linear) end diff --git a/proof/StarForth_Base.thy b/proof/StarForth_Base.thy index 35a534f..01a5a6e 100644 --- a/proof/StarForth_Base.thy +++ b/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 - 64-bit signed range. This is not a hidden assumption — it is the stated - correctness domain for FORTH programs that avoid overflow UB. *) -type_synonym cell = int + + CORRECTED 2026-08-13: was modeled as HOL int (arbitrary precision, + never wraps). Changed to a genuine 64-bit word, matching how + StarForth_Q48_16.thy already models q48. The old int model made every + 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, sint) rather than the default unsigned (<, \), + 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. *) +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 \ bool" where + "cell_safe c \ -4294967296 \s c \ c \s 4294967296" \ \|c| < 2^32\ + +lemma cell_safe_sint_bounds: + assumes "cell_safe c" + shows "-4294967296 \ sint c" "sint c \ 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 "\delta\ \ 4294967296" + shows "sint (c + word_of_int delta) = sint c + delta" +proof - + have b: "-4294967296 \ sint c" "sint c \ 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 \ sint c" "sint c \ 4294967296" + using assms(1) by (simp_all add: cell_safe_sint_bounds) + have ba: "-4294967296 \ sint amount" "sint amount \ 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 "\ = 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 \s n). Every call site that uses this already checks n s (n :: cell)" + shows "unat n = nat (sint n)" +proof - + have lo: "0 \ 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 "\ = 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 cell" where + "cell_abs n = (if n cell \ cell" where + "cell_sdiv a b = word_of_int (sgn (sint a) * sgn (sint b) * (\sint a\ div \sint b\))" + +definition cell_smod :: "cell \ cell \ cell" where + "cell_smod a b = word_of_int (sgn (sint a) * (\sint a\ mod \sint b\))" + (* ========================================================================= Section 2: Stack type and capacity constants ======================================================================== *) diff --git a/proof/StarForth_Loop1_Heat.thy b/proof/StarForth_Loop1_Heat.thy index b660494..eb53c24 100644 --- a/proof/StarForth_Loop1_Heat.thy +++ b/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" + 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" \ \WORD_FROZEN 0x04\ definition FLAG_PINNED :: nat where "FLAG_PINNED = 8" \ \WORD_PINNED 0x08\ @@ -49,8 +62,26 @@ definition heat_frozen :: "dict_entry \ bool" where definition heat_pinned :: "dict_entry \ bool" where "heat_pinned e \ 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, + signed.min, signed.max) instead of the default unsigned order (<, \, + 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 \ bool" where - "heat_valid e \ de_heat e \ 0 \ de_heat e \ HEAT_MAX" + "heat_valid e \ 0 \s de_heat e \ de_heat e \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 \ bool" where (* Saturating increment: heat grows by 1, capped at HEAT_MAX. *) definition heat_increment :: "dict_entry \ dict_entry" where "heat_increment e = - e\de_heat := min (de_heat e + 1) HEAT_MAX\" + e\de_heat := signed.min (de_heat e + 1) HEAT_MAX\" +(* CORRECTED for the cell-as-word migration: added the "cell_safe" side + condition. Under a bare 64-bit word, "de_heat e < HEAT_MAX \ + de_heat e + 1 \ 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" + 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 "\ HEAT_MAX + 1 \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 \ HEAT_MAX" - shows "de_heat (heat_increment e) \ de_heat e" - using assms by (simp add: heat_increment_def) + assumes "de_heat e \s HEAT_MAX" + assumes "cell_safe (de_heat e)" + shows "de_heat e \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 \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 \ 0" and hmax: "de_heat e \ HEAT_MAX" + have h0: "0 \s de_heat e" and hmax: "de_heat e \s HEAT_MAX" using assms by (simp_all add: heat_valid_def) - have le: "de_heat (heat_increment e) \ HEAT_MAX" - unfolding heat_increment_def by (simp add: min.cobounded2) - have ge: "de_heat (heat_increment e) \ 0" - unfolding heat_increment_def using h0 by (simp add: HEAT_MAX_def) + have safe: "cell_safe (de_heat e)" + using assms by (rule heat_valid_imp_cell_safe) + have sint_eq: "sint (de_heat e + 1) = sint (de_heat e) + 1" + using cell_safe_add_sint[OF safe, of 1] by simp + have step_pos: "0 \s de_heat e + 1" + using h0 sint_eq by (simp add: word_sle_eq) + have le: "de_heat (heat_increment e) \s HEAT_MAX" + unfolding heat_increment_def by (simp add: signed.min_def) + have ge: "0 \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 \ dict_entry \ dict_entry (if heat_frozen e then e \ \FROZEN: no decay\ else if heat_pinned e - then e\de_heat := max 1 (de_heat e - amount)\ \ \PINNED: floor at 1\ - else e\de_heat := max 0 (de_heat e - amount)\)" \ \normal: floor at 0\ + then e\de_heat := signed.max 1 (de_heat e - amount)\ \ \PINNED: floor at 1\ + else e\de_heat := signed.max 0 (de_heat e - amount)\)" \ \normal: floor at 0\ 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 \ 1 is the standing invariant a pinned word is - supposed to maintain (see heat_decay_pinned_positive's own \ 1 + monotonicity. de_heat e \s 1 is the standing invariant a pinned word is + supposed to maintain (see heat_decay_pinned_positive's own \s 1 conclusion below), just never stated here as a precondition before. *) lemma heat_decay_monotone: assumes "\ heat_frozen e" - assumes "de_heat e \ 1" - assumes "amount \ 0" - shows "de_heat (heat_decay amount e) \ de_heat e" - using assms by (simp add: heat_decay_def) + assumes "1 \s de_heat e" + assumes "0 \s amount" + assumes "cell_safe (de_heat e)" + assumes "cell_safe amount" + shows "de_heat (heat_decay amount e) \s de_heat e" +proof - + have zero_le: "0 \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 \ sint amount" using assms(3) by (simp add: word_sle_eq) + have sub_le: "de_heat e - amount \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 "\ heat_frozen e" assumes "\ heat_pinned e" - shows "de_heat (heat_decay amount e) \ 0" - by (simp add: heat_decay_def assms) + shows "0 \s de_heat (heat_decay amount e)" + by (simp add: heat_decay_def assms signed.max_def) lemma heat_decay_pinned_positive: assumes "\ heat_frozen e" assumes "heat_pinned e" - shows "de_heat (heat_decay amount e) \ 1" - by (simp add: heat_decay_def assms) + shows "1 \s de_heat (heat_decay amount e)" + by (simp add: heat_decay_def assms signed.max_def) lemma heat_decay_preserves_validity: assumes "heat_valid e" assumes "\ heat_frozen e" - assumes "amount \ 0" + assumes "0 \s amount" + assumes "cell_safe amount" shows "heat_valid (heat_decay amount e)" -proof (cases "heat_pinned e") - case True - thus ?thesis - using assms by (simp add: heat_valid_def heat_decay_def HEAT_MAX_def) -next - case False - thus ?thesis - using assms by (simp add: heat_valid_def heat_decay_def HEAT_MAX_def) +proof - + have safe_e: "cell_safe (de_heat e)" + using assms(1) by (rule heat_valid_imp_cell_safe) + have sub_sint: "sint (de_heat e - amount) = sint (de_heat e) - sint amount" + using cell_safe_sub_sint[OF safe_e assms(4)] . + have hmax: "de_heat e \s HEAT_MAX" using assms(1) by (simp add: heat_valid_def) + have amount_nonneg: "0 \ sint amount" using assms(3) by (simp add: word_sle_eq) + have sub_le_max: "de_heat e - amount \s HEAT_MAX" + using sub_sint hmax amount_nonneg by (simp add: word_sle_eq) + have one_le_max: "1 \s HEAT_MAX" + by (simp add: HEAT_MAX_def word_sle_eq) + have zero_le_one: "0 \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 \ bool" where Well-formedness: thresholds are in ascending order and non-negative. *) definition heat_thresholds_wf :: "vm_state \ bool" where "heat_thresholds_wf vm \ - heat_threshold_25th vm \ 0 \ - heat_threshold_25th vm \ heat_threshold_50th vm \ - heat_threshold_50th vm \ heat_threshold_75th vm \ - heat_threshold_75th vm \ HEAT_MAX" + 0 \s heat_threshold_25th vm \ + heat_threshold_25th vm \s heat_threshold_50th vm \ + heat_threshold_50th vm \s heat_threshold_75th vm \ + heat_threshold_75th vm \s HEAT_MAX" (* A pure data-stack word does not change heat thresholds or dictionary heat. *) lemma ds_word_preserves_dict_heat: diff --git a/proof/StarForth_Loop3_Decay.thy b/proof/StarForth_Loop3_Decay.thy index c39c4fe..32fec2f 100644 --- a/proof/StarForth_Loop3_Decay.thy +++ b/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 \ int" where "total_dict_heat vm = (\i \ {i. dictionary vm i \ 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 \ \vm_decay_step_dict [simp] rewrites the dictionary field\ lemma decay_total_heat_non_increasing: - assumes "\i. dictionary vm i \ None \ de_heat (the (dictionary vm i)) \ 0" + assumes "\i. dictionary vm i \ None \ 0 \s de_heat (the (dictionary vm i))" shows "total_dict_heat (vm_decay_step step vm) \ total_dict_heat vm" by (simp add: decay_step_dict_unchanged) diff --git a/proof/StarForth_Memory_Words.thy b/proof/StarForth_Memory_Words.thy index 144e6af..2617ed6 100644 --- a/proof/StarForth_Memory_Words.thy +++ b/proof/StarForth_Memory_Words.thy @@ -53,27 +53,29 @@ definition forth_fetch :: "vm_state \ vm_state" where (case data_stack vm of [] \ set_error vm | addr # xs \ - if addr < 0 + if addr data_stack := mem_read (memory vm) (nat addr) # xs\)" + else vm\data_stack := mem_read (memory vm) (unat addr) # xs\)" lemma fetch_normal: assumes "data_stack vm = addr # xs" - assumes "addr \ 0" - shows "data_stack (forth_fetch vm) = mem_read (memory vm) (nat addr) # xs" - using assms by (auto simp: forth_fetch_def) + assumes "0 \s addr" + shows "data_stack (forth_fetch vm) = mem_read (memory vm) (unat addr) # xs" + 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 \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 \ 0" + assumes "0 \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 vm_state" where "forth_store vm = (case data_stack vm of addr # n # xs \ - if addr < 0 + if addr data_stack := xs, - memory := mem_write (memory vm) (nat addr) n\ + memory := mem_write (memory vm) (unat addr) n\ | _ \ set_error vm)" lemma store_normal: assumes "data_stack vm = addr # n # xs" - assumes "addr \ 0" + assumes "0 \s addr" shows "data_stack (forth_store vm) = xs" - and "memory (forth_store vm) = mem_write (memory vm) (nat addr) n" - using assms by (auto simp: forth_store_def) + and "memory (forth_store vm) = mem_write (memory vm) (unat addr) n" + 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 \ 0" - shows "mem_read (memory (forth_store vm)) (nat addr) = n" - using assms by (auto simp: forth_store_def mem_write_def mem_read_def) + assumes "0 \s addr" + shows "mem_read (memory (forth_store vm)) (unat addr) = n" + 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 \ 0" + assumes "0 \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 \ 0" - assumes "nat addr \ b" + assumes "0 \s addr" + assumes "unat addr \ 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 0" + assumes "0 \s addr" assumes "data_stack vm' = addr # xs" assumes "memory vm' = memory (forth_store vm)" - assumes "addr \ 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 \ vm_state" where (case data_stack vm of [] \ set_error vm | addr # xs \ - if addr < 0 + if addr data_stack := byte # xs\)" lemma cfetch_normal: assumes "data_stack vm = addr # xs" - assumes "addr \ 0" + assumes "0 \s addr" shows "data_stack (forth_cfetch vm) = - (mem_read (memory vm) (nat addr) AND 0xFF) # xs" - using assms by (auto simp: forth_cfetch_def) + (mem_read (memory vm) (unat addr) AND 0xFF) # xs" + 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 \ 0" + assumes "0 \s addr" shows "0 \ hd (data_stack (forth_cfetch vm))" and "hd (data_stack (forth_cfetch vm)) \ 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 vm_state" where "forth_cstore vm = (case data_stack vm of addr # c # xs \ - if addr < 0 + if addr data_stack := xs, - memory := mem_write (memory vm) (nat addr) (c AND 0xFF)\ + memory := mem_write (memory vm) (unat addr) (c AND 0xFF)\ | _ \ set_error vm)" lemma cstore_normal: assumes "data_stack vm = addr # c # xs" - assumes "addr \ 0" + assumes "0 \s addr" shows "data_stack (forth_cstore vm) = xs" - and "memory (forth_cstore vm) = mem_write (memory vm) (nat addr) (c AND 0xFF)" - using assms by (auto simp: forth_cstore_def) + and "memory (forth_cstore vm) = mem_write (memory vm) (unat addr) (c AND 0xFF)" + 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 \ 0" - shows "mem_read (memory (forth_cstore vm)) (nat addr) = c AND 0xFF" - using assms by (auto simp: forth_cstore_def mem_write_def mem_read_def) + assumes "0 \s addr" + 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 word_sle_eq word_sless_alt) lemma cstore_depth_decreases: assumes "data_stack vm = addr # c # xs" - assumes "addr \ 0" + assumes "0 \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 0" + assumes "0 \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 diff --git a/proof/StarForth_Stack_Words.thy b/proof/StarForth_Stack_Words.thy index 406ebc9..0eaa0aa 100644 --- a/proof/StarForth_Stack_Words.thy +++ b/proof/StarForth_Stack_Words.thy @@ -295,11 +295,11 @@ definition forth_depth :: "vm_state \ vm_state" where "forth_depth vm = (if ds_full vm then set_error vm - else vm\data_stack := int (length (data_stack vm)) # data_stack vm\)" + else vm\data_stack := word_of_nat (length (data_stack vm)) # data_stack vm\)" lemma depth_pushes_count: assumes "\ 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 \ 0 and n < length (data_stack vm) *) + Bounds check: 0 \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 \ length (data_stack vm)" used the pre-pop length too, one too + "unat n \ 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 \ vm_state" where (case data_stack vm of [] \ set_error vm | n # xs \ - if n < 0 \ nat n \ length xs + if n unat n \ length xs then set_error vm - else vm\data_stack := xs ! nat n # xs\)" + else vm\data_stack := xs ! unat n # xs\)" lemma pick_normal: assumes "data_stack vm = n # xs" - assumes "n \ 0" - assumes "nat n < length xs" - shows "data_stack (forth_pick vm) = xs ! nat n # xs" + assumes "0 \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 "n \ 0" - assumes "nat n < length xs" + assumes "0 \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) + 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 length xs" + assumes "unat n \ 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 \ vm_state" where (case data_stack vm of [] \ set_error vm | n # xs \ - if n < 0 \ nat n > length xs + if n unat n > length xs then set_error vm else if n = 0 then vm\data_stack := xs\ - 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\data_stack := item # rest\)" @@ -456,10 +456,11 @@ lemma roll_one_moves_bottom: assumes "xs \ []" 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 length xs" + assumes "unat n > length xs" shows "vm_error (forth_roll vm)" by (simp add: forth_roll_def set_error_def assms)