Robert Allan James
422ef2fa29
Isabelle toolchain replaced (was genuinely 2011, 14+ years stale) and every theory file fixed to actually compile -- most had apparently never been checked under a working Isabelle at all. Fixed the vm_state self-reference in StarForth_Base.thy properly (word_table is now a free-standing global constant, not a circular record field), corrected the word_physics_transparent axiom (was claiming full state equality from mere exec-equivalence, provably too strong), and worked through 14 years of HOL-Library drift plus several missing-hypothesis bugs across the physics-loop and ACL theories. Two genuine (non-tactical) bugs found and left oops-flagged rather than silently resolved: forth_roll's index arithmetic disagrees with both its own test lemma and the real C ROLL implementation (three-way inconsistency), and pm_wf isn't actually preserved by pm_record_hit/pm_record_miss. Both need a decision, not a proof-script fix. Full writeup in FABRIC-2.md item 5.2.
146 lines
5.8 KiB
Plaintext
146 lines
5.8 KiB
Plaintext
theory StarForth_Loop7_Heartrate
|
|
imports StarForth_Base
|
|
begin
|
|
|
|
(* =========================================================================
|
|
StarForth_Loop7_Heartrate — Adaptive Heartrate (Physics Loop #7)
|
|
|
|
Mirrors: src/vm_time.c (heartbeat thread, tick_target_ns updates)
|
|
include/vm.h (HeartbeatState.tick_target_ns)
|
|
|
|
The heartbeat thread wakes on a nanosecond timer (tick_target_ns cadence).
|
|
Loop #7 adjusts tick_target_ns based on observed jitter and load:
|
|
• If ticks are arriving too slowly (jitter > threshold), shorten period.
|
|
• If ticks arrive fast enough, lengthen period to save CPU.
|
|
|
|
Invariants:
|
|
• tick_target_ns > 0 at all times.
|
|
• tick_target_ns ∈ [TICK_MIN_NS, TICK_MAX_NS].
|
|
• hb_tick_count increases monotonically.
|
|
======================================================================== *)
|
|
|
|
(* =========================================================================
|
|
Section 1: Heartrate bounds
|
|
======================================================================== *)
|
|
|
|
(* Minimum tick period: 100 μs = 100,000 ns (matches HEARTBEAT_WINDOW_TUNING_FREQUENCY
|
|
comment: tune every 1000 ticks, implying a ~1ms default tick period). *)
|
|
definition TICK_MIN_NS :: nat where "TICK_MIN_NS = 100000" \<comment> \<open>100 μs\<close>
|
|
definition TICK_MAX_NS :: nat where "TICK_MAX_NS = 100000000" \<comment> \<open>100 ms\<close>
|
|
definition TICK_DEFAULT_NS :: nat where "TICK_DEFAULT_NS = 1000000" \<comment> \<open>1 ms\<close>
|
|
|
|
lemma tick_min_pos: "TICK_MIN_NS > 0"
|
|
by (simp add: TICK_MIN_NS_def)
|
|
|
|
lemma tick_default_in_range:
|
|
"TICK_MIN_NS \<le> TICK_DEFAULT_NS \<and> TICK_DEFAULT_NS \<le> TICK_MAX_NS"
|
|
by (simp add: TICK_MIN_NS_def TICK_DEFAULT_NS_def TICK_MAX_NS_def)
|
|
|
|
(* =========================================================================
|
|
Section 2: Heartbeat state well-formedness
|
|
======================================================================== *)
|
|
|
|
definition hb_state_wf :: "heartbeat_state \<Rightarrow> bool" where
|
|
"hb_state_wf hb \<longleftrightarrow>
|
|
hb_tick_target_ns hb \<ge> TICK_MIN_NS \<and>
|
|
hb_tick_target_ns hb \<le> TICK_MAX_NS \<and>
|
|
hb_tick_target_ns hb > 0"
|
|
|
|
lemma hb_state_wf_pos:
|
|
assumes "hb_state_wf hb"
|
|
shows "hb_tick_target_ns hb > 0"
|
|
using assms by (simp add: hb_state_wf_def)
|
|
|
|
lemma hb_state_wf_lb:
|
|
assumes "hb_state_wf hb"
|
|
shows "hb_tick_target_ns hb \<ge> TICK_MIN_NS"
|
|
using assms by (simp add: hb_state_wf_def)
|
|
|
|
lemma hb_state_wf_ub:
|
|
assumes "hb_state_wf hb"
|
|
shows "hb_tick_target_ns hb \<le> TICK_MAX_NS"
|
|
using assms by (simp add: hb_state_wf_def)
|
|
|
|
(* =========================================================================
|
|
Section 3: Tick period adjustment
|
|
======================================================================== *)
|
|
|
|
(* Shorten tick period (increase tick rate) — saturate at TICK_MIN_NS. *)
|
|
definition hb_shorten_period :: "nat \<Rightarrow> heartbeat_state \<Rightarrow> heartbeat_state" where
|
|
"hb_shorten_period delta hb =
|
|
hb\<lparr>hb_tick_target_ns := max TICK_MIN_NS (hb_tick_target_ns hb - delta)\<rparr>"
|
|
|
|
(* Lengthen tick period (decrease tick rate) — saturate at TICK_MAX_NS. *)
|
|
definition hb_lengthen_period :: "nat \<Rightarrow> heartbeat_state \<Rightarrow> heartbeat_state" where
|
|
"hb_lengthen_period delta hb =
|
|
hb\<lparr>hb_tick_target_ns := min TICK_MAX_NS (hb_tick_target_ns hb + delta)\<rparr>"
|
|
|
|
lemma hb_shorten_lb:
|
|
"hb_tick_target_ns (hb_shorten_period delta hb) \<ge> TICK_MIN_NS"
|
|
by (simp add: hb_shorten_period_def)
|
|
|
|
lemma hb_shorten_pos:
|
|
"hb_tick_target_ns (hb_shorten_period delta hb) > 0"
|
|
using tick_min_pos by (simp add: hb_shorten_period_def)
|
|
|
|
lemma hb_shorten_preserves_wf:
|
|
assumes "hb_state_wf hb"
|
|
shows "hb_state_wf (hb_shorten_period delta hb)"
|
|
using assms
|
|
by (auto simp: hb_state_wf_def hb_shorten_period_def TICK_MAX_NS_def TICK_MIN_NS_def
|
|
intro: le_trans[OF diff_le_self])
|
|
|
|
lemma hb_lengthen_ub:
|
|
"hb_tick_target_ns (hb_lengthen_period delta hb) \<le> TICK_MAX_NS"
|
|
by (simp add: hb_lengthen_period_def)
|
|
|
|
lemma hb_lengthen_preserves_pos:
|
|
assumes "hb_tick_target_ns hb > 0"
|
|
shows "hb_tick_target_ns (hb_lengthen_period delta hb) > 0"
|
|
using assms by (simp add: hb_lengthen_period_def TICK_MAX_NS_def)
|
|
|
|
lemma hb_lengthen_preserves_wf:
|
|
assumes "hb_state_wf hb"
|
|
shows "hb_state_wf (hb_lengthen_period delta hb)"
|
|
using assms by (simp add: hb_state_wf_def hb_lengthen_period_def TICK_MIN_NS_def TICK_MAX_NS_def)
|
|
|
|
(* =========================================================================
|
|
Section 4: Tick counter monotonicity
|
|
======================================================================== *)
|
|
|
|
definition hb_fire_tick :: "heartbeat_state \<Rightarrow> heartbeat_state" where
|
|
"hb_fire_tick hb = hb\<lparr>hb_tick_count := hb_tick_count hb + 1\<rparr>"
|
|
|
|
lemma hb_fire_tick_count_increases:
|
|
"hb_tick_count (hb_fire_tick hb) = hb_tick_count hb + 1"
|
|
by (simp add: hb_fire_tick_def)
|
|
|
|
lemma hb_fire_tick_count_monotone:
|
|
"hb_tick_count (hb_fire_tick hb) \<ge> hb_tick_count hb"
|
|
by (simp add: hb_fire_tick_def)
|
|
|
|
lemma hb_fire_tick_preserves_target:
|
|
"hb_tick_target_ns (hb_fire_tick hb) = hb_tick_target_ns hb"
|
|
by (simp add: hb_fire_tick_def)
|
|
|
|
lemma hb_fire_tick_preserves_wf:
|
|
assumes "hb_state_wf hb"
|
|
shows "hb_state_wf (hb_fire_tick hb)"
|
|
using assms by (simp add: hb_state_wf_def hb_fire_tick_def)
|
|
|
|
(* =========================================================================
|
|
Section 5: VM-level heartbeat well-formedness
|
|
======================================================================== *)
|
|
|
|
lemma wf_vm_hb_pos:
|
|
assumes "wf_vm vm"
|
|
shows "hb_tick_target_ns (heartbeat vm) > 0"
|
|
using assms by (simp add: wf_vm_def)
|
|
|
|
lemma ds_word_preserves_heartbeat_wf:
|
|
assumes "hb_state_wf (heartbeat vm)"
|
|
shows "hb_state_wf (heartbeat (vm\<lparr>data_stack := xs\<rparr>))"
|
|
using assms by simp
|
|
|
|
end
|