admin/LithosAnanake
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
Files
master
LithosAnanake/proof/StarForth_Loop1_Heat.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

299 lines
13 KiB
Plaintext
Raw Permalink Blame History

This file contains ambiguous Unicode characters
This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
theory StarForth_Loop1_Heat
imports StarForth_Base
begin
(* AND/OR/XOR infix notation moved behind an opt-in bundle at some point
after 2011 -- unbundled by default now. Same fix as StarForth_Q48_16.thy. *)
unbundle bit_operations_syntax
(* =========================================================================
StarForth_Loop1_Heat — Execution Heat Tracking (Physics Loop #1)
Mirrors: src/dictionary_heat_optimization.c
src/word_source/ (heat increment on every word execution)
Every time a word executes its de_heat field is incremented. A background
decay sweep (Loop #3) decrements heat over time. Words can be FROZEN
(heat does not decay) or PINNED (heat cannot reach zero).
This theory proves:
• Heat is non-negative throughout its lifecycle.
• Heat increment strictly increases de_heat.
• Heat is bounded above by a MAX_HEAT constant.
• FROZEN words are immune to decay.
• PINNED words' heat stays ≥ 1 after decay.
======================================================================== *)
(* =========================================================================
Section 1: Heat constants
======================================================================== *)
(* Initial heat assigned when a word is first defined *)
definition HEAT_INIT :: cell where "HEAT_INIT = 0"
(* Maximum representable heat (arbitrary upper bound for well-formedness) *)
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>
(* =========================================================================
Section 2: Heat predicates
======================================================================== *)
definition heat_frozen :: "dict_entry \<Rightarrow> bool" where
"heat_frozen e \<longleftrightarrow> de_flags e AND FLAG_FROZEN = FLAG_FROZEN"
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> 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)
======================================================================== *)
(* 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 := 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 <s HEAT_MAX"
assumes "cell_safe (de_heat e)"
shows "de_heat (heat_increment e) = de_heat e + 1"
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"
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>s HEAT_MAX"
assumes "cell_safe (de_heat e)"
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: "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 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 \<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
lemma heat_increment_preserves_flags:
"de_flags (heat_increment e) = de_flags e"
by (simp add: heat_increment_def)
lemma heat_increment_preserves_frozen:
"heat_frozen (heat_increment e) = heat_frozen e"
by (simp add: heat_frozen_def heat_increment_def)
lemma heat_increment_preserves_pinned:
"heat_pinned (heat_increment e) = heat_pinned e"
by (simp add: heat_pinned_def heat_increment_def)
(* =========================================================================
Section 4: Heat decay (fired by heartbeat Loop #3)
======================================================================== *)
(* A decay amount in cell units. The C code uses Q48.16 slope × elapsed time,
truncated to an integer; we abstract the amount as a parameter. *)
definition heat_decay :: "cell \<Rightarrow> dict_entry \<Rightarrow> dict_entry" where
"heat_decay amount e =
(if heat_frozen e
then e \<comment> \<open>FROZEN: no decay\<close>
else if heat_pinned e
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 := signed.max 0 (de_heat e - amount)\<rparr>)" \<comment> \<open>normal: floor at 0\<close>
lemma heat_decay_frozen:
assumes "heat_frozen e"
shows "heat_decay amount e = e"
by (simp add: heat_decay_def assms)
(* 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>s 1 is the standing invariant a pinned word is
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 "1 \<le>s de_heat e"
assumes "0 \<le>s amount"
assumes "cell_safe (de_heat e)"
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 "0 \<le>s de_heat (heat_decay amount e)"
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 "1 \<le>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 "\<not> heat_frozen e"
assumes "0 \<le>s amount"
assumes "cell_safe amount"
shows "heat_valid (heat_decay amount e)"
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 \<le>s HEAT_MAX" using assms(1) by (simp add: heat_valid_def)
have amount_nonneg: "0 \<le> sint amount" using assms(3) by (simp add: word_sle_eq)
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:
"de_flags (heat_decay amount e) = de_flags e"
by (simp add: heat_decay_def)
(* =========================================================================
Section 5: Well-formedness of the dictionary heat state
======================================================================== *)
(* All dict entries reachable via the dictionary have valid heat. *)
definition dict_heat_wf :: "vm_state \<Rightarrow> bool" where
"dict_heat_wf vm \<longleftrightarrow>
(\<forall>i e. dictionary vm i = Some e \<longrightarrow> heat_valid e)"
(* =========================================================================
Section 6: Heat thresholds
======================================================================== *)
(* The VM maintains 25th/50th/75th percentile thresholds for bucket search.
Well-formedness: thresholds are in ascending order and non-negative. *)
definition heat_thresholds_wf :: "vm_state \<Rightarrow> bool" where
"heat_thresholds_wf vm \<longleftrightarrow>
0 \<le>s heat_threshold_25th vm \<and>
heat_threshold_25th vm \<le>s heat_threshold_50th vm \<and>
heat_threshold_50th vm \<le>s heat_threshold_75th vm \<and>
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:
assumes "dictionary (vm\<lparr>data_stack := xs\<rparr>) = dictionary vm"
shows "dict_heat_wf (vm\<lparr>data_stack := xs\<rparr>) = dict_heat_wf vm"
by (simp add: dict_heat_wf_def assms)
lemma ds_word_preserves_heat_thresholds:
"heat_thresholds_wf (vm\<lparr>data_stack := xs\<rparr>) = heat_thresholds_wf vm"
by (simp add: heat_thresholds_wf_def)
end
Reference in New Issue View Git Blame Copy Permalink