proof/: all 23 Isabelle theory files now verify under Isabelle2025-2
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.
This commit is contained in:
Robert Allan James
@@ -91,7 +91,7 @@ lemma denied_word_permitted_under_zuse:
|
||||
lemma either_bypass_sufficient:
|
||||
"(emergency_console vm = True \<or> zuse_session vm = True) \<Longrightarrow>
|
||||
acl_check_permits vm e = True"
|
||||
by (simp add: acl_check_permits_def)
|
||||
by (auto simp: acl_check_permits_def)
|
||||
|
||||
(* Without either bypass, the word's own acl_allow is definitive. *)
|
||||
lemma no_bypass_check_follows_allow:
|
||||
|
||||
@@ -57,7 +57,7 @@ definition acl_ttl_compute :: "nat \<Rightarrow> nat" where
|
||||
(* Lower bound: result is always ≥ ACL_BASE_TTL. *)
|
||||
lemma acl_ttl_compute_ge_base:
|
||||
"acl_ttl_compute heat \<ge> ACL_BASE_TTL"
|
||||
by (simp add: acl_ttl_compute_def ACL_BASE_TTL_def)
|
||||
by (simp add: acl_ttl_compute_def ACL_BASE_TTL_def ACL_MAX_TTL_def)
|
||||
|
||||
(* Upper bound: result is always ≤ ACL_MAX_TTL. *)
|
||||
lemma acl_ttl_compute_le_max:
|
||||
|
||||
+42
-21
@@ -135,8 +135,9 @@ record dict_physics =
|
||||
(* ── Dictionary entry ────────────────────────────────────────────────────── *)
|
||||
(* ○ CODE-MUST-MATCH: struct DictEntry in include/vm.h
|
||||
⚠ HUMAN-REVIEW: The C DictEntry stores a function pointer (word_func_t func).
|
||||
This has been moved to word_table (a top-level vm_state field) to avoid the
|
||||
type circularity vm_state → vm_state inside dict_entry.
|
||||
This has been moved to word_table, a free-standing global constant declared
|
||||
after vm_state (see "Word semantics table" section below) -- not a
|
||||
vm_state field at all, which is what actually avoids the type circularity.
|
||||
Implementors: the C code must maintain a SEPARATE lookup table indexed by
|
||||
word_id that maps to word_func_t pointers — this is what word_table models.
|
||||
The dict_entry record here has no func field; look it up via word_table. *)
|
||||
@@ -301,7 +302,9 @@ record inference_outputs_state =
|
||||
□ dictionary / latest_id / here / dict_fence — dictionary state
|
||||
□ dict_lock / word_id_next — dict management
|
||||
□ vm_mode / vm_ip / state_var / vm_base / vm_error / vm_halted
|
||||
□ word_table — function pointer table (C: per-DictEntry func ptr)
|
||||
□ word_table — NOT a field of this record; see the
|
||||
free-standing "consts word_table" declaration after this record,
|
||||
function pointer table (C: per-DictEntry func ptr)
|
||||
□ heat_threshold_25th/50th/75th / last_bucket_reorg_ns / lookup_strategy
|
||||
□ rolling_window — all sub-fields including rw_act_window
|
||||
□ decay_slope_q48 / last_decay_check_ns / total_heat_at_check / ...
|
||||
@@ -358,20 +361,6 @@ record vm_state =
|
||||
vm_error :: bool
|
||||
vm_halted :: bool
|
||||
|
||||
(* ── Word semantics table ───────────────────────────────────────────── *)
|
||||
(* ⚠ CRITICAL DESIGN NOTE: The C DictEntry stores word_func_t func, a function
|
||||
pointer per word. Putting (vm_state ⇒ vm_state) inside dict_entry inside
|
||||
vm_state creates a circular type in HOL. SOLUTION: the word function table
|
||||
is a TOP-LEVEL field of vm_state, indexed by word_id.
|
||||
|
||||
○ CODE-MUST-MATCH: C implementors must maintain a PARALLEL array (or map)
|
||||
from word_id → word_func_t that is logically equivalent to this field.
|
||||
The dict_entry.func pointer in C can remain, but the proof framework
|
||||
treats word_table as the authoritative semantic specification.
|
||||
⚠ HUMAN-REVIEW: Verify that for every word_id i, word_table i matches
|
||||
exactly the behavior of the corresponding word_func_t function. *)
|
||||
word_table :: "nat \<Rightarrow> vm_state \<Rightarrow> vm_state"
|
||||
|
||||
(* ── Physics Loop #1: Execution heat tracking ───────────────────────── *)
|
||||
(* ○ CODE-MUST-MATCH: heat_threshold_{25th,50th,75th} in C VM struct.
|
||||
⚠ HUMAN-REVIEW: Thresholds are recomputed periodically by the heat bucket
|
||||
@@ -439,6 +428,32 @@ record vm_state =
|
||||
non-interference proof breaks. Verify in the SSM implementation. *)
|
||||
ssm_l8 :: ssm_l8_state
|
||||
|
||||
(* =========================================================================
|
||||
Word semantics table — deliberately NOT a vm_state field.
|
||||
|
||||
CORRECTED 2026-08-13: the original design put word_table inside vm_state
|
||||
with type "nat \<Rightarrow> vm_state \<Rightarrow> vm_state" -- self-referential (vm_state
|
||||
naming itself in its own field's type) and rejected by every Isabelle
|
||||
version, not just this one; HOL records have no fixed-point support. The
|
||||
file's own prior comment claimed hoisting it to a "top-level field of
|
||||
vm_state" solved the circularity -- it does not: the field's type still
|
||||
names vm_state before vm_state exists.
|
||||
|
||||
Fix: word_table is a free-standing, uninterpreted global constant,
|
||||
declared here AFTER vm_state so there is no forward reference. This is
|
||||
also more faithful to the C reality it models -- word_func_t dispatch is
|
||||
a fixed table built once at compile time, not per-VM-instance mutable
|
||||
state, so it never belonged inside vm_state's record in the first place.
|
||||
Individual word_id entries are characterised by axioms in the per-word
|
||||
theories (StarForth_Arithmetic_Words.thy etc.), not defined here.
|
||||
|
||||
○ CODE-MUST-MATCH: C implementors maintain the word_id \<rightarrow> word_func_t
|
||||
dispatch table this constant models. See StarForth_Transition.thy's
|
||||
word_physics_transparent axiom for the one property assumed of it: word
|
||||
execution depends only on the exec-visible fields (data_stack,
|
||||
return_stack, memory), never on physics state. *)
|
||||
consts word_table :: "nat \<Rightarrow> vm_state \<Rightarrow> vm_state"
|
||||
|
||||
(* =========================================================================
|
||||
Section 5: Well-formedness, error signalling, capacity predicates
|
||||
======================================================================== *)
|
||||
@@ -515,7 +530,10 @@ definition rs_full :: "vm_state \<Rightarrow> bool" where
|
||||
(* ⚠ CENTRAL CORRECTNESS MECHANISM:
|
||||
HOL record-update syntax vm⦇data_stack := xs⦈ proves that EVERY field
|
||||
not mentioned in the update (rolling_window, heartbeat, decay_slope_q48,
|
||||
pipeline_metrics, dictionary, word_table, etc.) is EXACTLY unchanged.
|
||||
pipeline_metrics, dictionary, etc.) is EXACTLY unchanged. word_table is
|
||||
not in this list since 2026-08-13 -- it is no longer a vm_state field at
|
||||
all (see above), so its independence from any vm_state update is true by
|
||||
construction, stronger than a per-update lemma could state.
|
||||
This is how we mechanise "proof of correctness in totality with no
|
||||
assumptions" — no field is silently assumed unchanged; HOL record algebra
|
||||
guarantees it.
|
||||
@@ -555,8 +573,11 @@ lemma ds_update_preserves_dict:
|
||||
"dictionary (vm\<lparr>data_stack := xs\<rparr>) = dictionary vm"
|
||||
by simp
|
||||
|
||||
lemma ds_update_preserves_word_table:
|
||||
"word_table (vm\<lparr>data_stack := xs\<rparr>) = word_table vm"
|
||||
by simp
|
||||
(* ds_update_preserves_word_table removed 2026-08-13: word_table is no
|
||||
longer a vm_state field (see the "Word semantics table" section above),
|
||||
so "word_table (vm\<lparr>...\<rparr>)" no longer type-checks -- there is nothing
|
||||
left to state. word_table's independence from data_stack updates is now
|
||||
true by construction (it is a fixed global, not read from vm at all),
|
||||
not something requiring its own lemma. *)
|
||||
|
||||
end
|
||||
|
||||
@@ -21,53 +21,72 @@ begin
|
||||
|
||||
theorem heartbeat_noninterference:
|
||||
"\<forall>n k vm.
|
||||
data_stack (word_table (heartbeat_step ^^ k $ vm) n (heartbeat_step ^^ k $ vm))
|
||||
= data_stack (word_table vm n vm)"
|
||||
by (simp add: exec_after_n_heartbeats_eq)
|
||||
data_stack (word_table n ((heartbeat_step ^^ k) vm))
|
||||
= data_stack (word_table n vm)"
|
||||
using exec_after_n_heartbeats_eq exec_equiv_ds by blast
|
||||
|
||||
theorem heartbeat_noninterference_rs:
|
||||
"\<forall>n k vm.
|
||||
return_stack (word_table (heartbeat_step ^^ k $ vm) n (heartbeat_step ^^ k $ vm))
|
||||
= return_stack (word_table vm n vm)"
|
||||
by (simp add: exec_after_n_heartbeats_eq)
|
||||
return_stack (word_table n ((heartbeat_step ^^ k) vm))
|
||||
= return_stack (word_table n vm)"
|
||||
using exec_after_n_heartbeats_eq exec_equiv_rs by blast
|
||||
|
||||
(* =========================================================================
|
||||
Section 2: Trace-level non-interference (proved by induction over ≃)
|
||||
|
||||
foldl_word_table_eq: if two initial states are exec-equivalent (≃), then
|
||||
running any word sequence on each produces identical states. The proof is
|
||||
structural: at each step word_physics_transparent (A4') gives FULL state
|
||||
equality of the successors (not just exec-field agreement), so the remaining
|
||||
foldl is trivially identical — no propagation of equivalence is needed.
|
||||
running any word sequence on each produces exec-equivalent (not
|
||||
identical -- CORRECTED 2026-08-13, see StarForth_Transition.thy's note
|
||||
at word_physics_transparent for why full equality was never provable)
|
||||
states. The proof is structural: at each step word_physics_transparent
|
||||
(A4') gives ≃ of the successors, which is exactly what arbitrary: s1 s2
|
||||
needs to carry the induction through.
|
||||
|
||||
heartbeat_trace_noninterference follows immediately by instantiating with
|
||||
s1 = heartbeat_step ^^ k $ vm, s2 = vm, using heartbeat_n_exec_neutral.
|
||||
s1 = (heartbeat_step ^^ k) vm, s2 = vm, using heartbeat_n_exec_neutral.
|
||||
|
||||
○ CODE-MUST-MATCH: the inductive argument holds only if word_physics_transparent
|
||||
holds for every word — see the audit protocol in StarForth_Transition.thy.
|
||||
======================================================================== *)
|
||||
|
||||
(* Restated 2026-08-13 with explicit object-level \<forall>/\<longrightarrow> instead of
|
||||
assumes/shows + arbitrary: s1 s2 -- the assumes/arbitrary combination
|
||||
was not reliably carrying "s1 \<simeq> s2" into the Nil case as Nil.prems
|
||||
despite multiple tactics (simp, rule, metis with the fact named
|
||||
explicitly all failed identically); this form sidesteps the whole
|
||||
revert-and-generalize mechanism by quantifying s1/s2 in the goal from
|
||||
the start. *)
|
||||
lemma foldl_word_table_eq:
|
||||
assumes "s1 \<simeq> s2"
|
||||
shows "foldl (\<lambda>s n. word_table s n s) s1 ws
|
||||
= foldl (\<lambda>s n. word_table s n s) s2 ws"
|
||||
proof (induction ws arbitrary: s1 s2)
|
||||
case Nil thus ?case by simp
|
||||
"\<forall>s1 s2. s1 \<simeq> s2 \<longrightarrow>
|
||||
foldl (\<lambda>s n. word_table n s) s1 ws \<simeq> foldl (\<lambda>s n. word_table n s) s2 ws"
|
||||
proof (induction ws)
|
||||
case Nil
|
||||
show ?case by simp
|
||||
next
|
||||
case (Cons w ws)
|
||||
(* A4' gives full state equality of the one-step successors *)
|
||||
have heq: "word_table s1 w s1 = word_table s2 w s2"
|
||||
by (rule word_physics_transparent [OF Cons.prems])
|
||||
show ?case by (simp add: heq)
|
||||
show ?case
|
||||
proof (intro allI impI)
|
||||
fix s1 s2 :: vm_state
|
||||
assume h: "s1 \<simeq> s2"
|
||||
have heq: "word_table w s1 \<simeq> word_table w s2"
|
||||
using h word_physics_transparent by blast
|
||||
have "foldl (\<lambda>s n. word_table n s) (word_table w s1) ws
|
||||
\<simeq> foldl (\<lambda>s n. word_table n s) (word_table w s2) ws"
|
||||
using Cons.IH heq by blast
|
||||
thus "foldl (\<lambda>s n. word_table n s) s1 (w # ws)
|
||||
\<simeq> foldl (\<lambda>s n. word_table n s) s2 (w # ws)"
|
||||
by simp
|
||||
qed
|
||||
qed
|
||||
|
||||
theorem heartbeat_trace_noninterference:
|
||||
"\<And> words vm k.
|
||||
data_stack
|
||||
(foldl (\<lambda>s n. word_table s n s) (heartbeat_step ^^ k $ vm) words)
|
||||
(foldl (\<lambda>s n. word_table n s) ((heartbeat_step ^^ k) vm) words)
|
||||
= data_stack
|
||||
(foldl (\<lambda>s n. word_table s n s) vm words)"
|
||||
using foldl_word_table_eq [OF heartbeat_n_exec_neutral] by simp
|
||||
(foldl (\<lambda>s n. word_table n s) vm words)"
|
||||
using foldl_word_table_eq [rule_format, OF heartbeat_n_exec_neutral] exec_equiv_ds
|
||||
by blast
|
||||
|
||||
(* =========================================================================
|
||||
Section 3: Mutex safety (proved from lock_state algebra)
|
||||
@@ -97,12 +116,12 @@ lemma vm_step_preserves_lock_safety:
|
||||
|
||||
lemma word_exec_deterministic:
|
||||
assumes "s1 \<simeq> s2"
|
||||
shows "data_stack (word_table s1 n s1) = data_stack (word_table s2 n s2)"
|
||||
using word_physics_transparent [OF assms] by simp
|
||||
shows "data_stack (word_table n s1) = data_stack (word_table n s2)"
|
||||
using word_physics_transparent [OF assms] exec_equiv_ds by blast
|
||||
|
||||
lemma word_exec_rs_deterministic:
|
||||
assumes "s1 \<simeq> s2"
|
||||
shows "return_stack (word_table s1 n s1) = return_stack (word_table s2 n s2)"
|
||||
using word_physics_transparent [OF assms] by simp
|
||||
shows "return_stack (word_table n s1) = return_stack (word_table n s2)"
|
||||
using word_physics_transparent [OF assms] exec_equiv_rs by blast
|
||||
|
||||
end
|
||||
|
||||
@@ -28,15 +28,20 @@ begin
|
||||
heartbeat_step vm ≃ vm
|
||||
The heartbeat is the identity in vm_state/≃ (exec_equiv).
|
||||
C audit: src/vm_time.c vm_tick() must NOT write to
|
||||
data_stack, return_stack, memory, or word_table.
|
||||
data_stack, return_stack, or memory. (word_table dropped
|
||||
from this list 2026-08-13: it is a free-standing global
|
||||
constant now, not a vm_state field, so vm_tick() cannot
|
||||
write to it at all.)
|
||||
The physics substate is unconstrained — the heartbeat may
|
||||
evolve it freely and non-monotonically.
|
||||
The former 8 field axioms are now proved lemmas from A1.
|
||||
|
||||
A4'×1. word_physics_transparent (StarForth_Transition)
|
||||
s1 ≃ s2 ⟹ word_table s1 n s1 = word_table s2 n s2
|
||||
s1 ≃ s2 ⟹ word_table n s1 ≃ word_table n s2
|
||||
(corrected 2026-08-13: conclusion is ≃, not literal
|
||||
equality -- see the note at its declaration)
|
||||
Word execution is a congruence law for ≃.
|
||||
Word audit: every Level 1 word body must read ONLY the four
|
||||
Word audit: every Level 1 word body must read ONLY the three
|
||||
fields in exec_equiv — never any physics field.
|
||||
|
||||
Physics invariants (A2/A3) remain removed — clamping suffices.
|
||||
@@ -59,14 +64,14 @@ thm swap_normal \<comment> \<open>✓ SWAP exchanges top two\<close>
|
||||
thm over_normal \<comment> \<open>✓ OVER copies second to top\<close>
|
||||
thm rot_normal \<comment> \<open>✓ ROT cycles top 3\<close>
|
||||
thm swap_involutive \<comment> \<open>✓ SWAP ∘ SWAP = identity\<close>
|
||||
thm rot_neg_rot_identity \<comment> \<open>✓ ROT ∘ -ROT = identity\<close>
|
||||
thm rot_nrot_inverse \<comment> \<open>✓ ROT ∘ -ROT = identity (corrected name, 2026-08-13)\<close>
|
||||
thm add_normal \<comment> \<open>✓ + pops 2, pushes sum\<close>
|
||||
thm mul_comm \<comment> \<open>✓ * is commutative\<close>
|
||||
thm mul_commutative \<comment> \<open>✓ * is commutative (corrected name, 2026-08-13)\<close>
|
||||
thm negate_involutive \<comment> \<open>✓ NEGATE ∘ NEGATE = identity\<close>
|
||||
thm abs_non_negative \<comment> \<open>✓ ABS result ≥ 0\<close>
|
||||
thm abs_nonneg \<comment> \<open>✓ ABS result ≥ 0 (corrected name, 2026-08-13)\<close>
|
||||
thm and_normal \<comment> \<open>✓ AND bitwise\<close>
|
||||
thm zero_eq_true \<comment> \<open>✓ 0= of 0 is FORTH_TRUE\<close>
|
||||
thm zero_lt_exhaustion \<comment> \<open>✓ {0=, 0<, 0>} partition ℤ\<close>
|
||||
thm zero_eq_zero \<comment> \<open>✓ 0= of 0 is FORTH_TRUE (corrected name, 2026-08-13)\<close>
|
||||
thm zero_tests_exhaustive \<comment> \<open>✓ {0=, 0<, 0>} partition ℤ (corrected name, 2026-08-13)\<close>
|
||||
thm to_r_then_from_r \<comment> \<open>✓ >R then R> round-trip\<close>
|
||||
thm store_then_fetch \<comment> \<open>✓ ! then @ identity\<close>
|
||||
thm cstore_then_cfetch \<comment> \<open>✓ C! then C@ round-trip\<close>
|
||||
@@ -83,8 +88,10 @@ lemma pure_ds_word_preserves_physics:
|
||||
"last_inference (vm\<lparr>data_stack := xs\<rparr>) = last_inference vm"
|
||||
"ssm_l8 (vm\<lparr>data_stack := xs\<rparr>) = ssm_l8 vm"
|
||||
"dictionary (vm\<lparr>data_stack := xs\<rparr>) = dictionary vm"
|
||||
"word_table (vm\<lparr>data_stack := xs\<rparr>) = word_table vm"
|
||||
by simp_all
|
||||
(* The word_table conjunct here was removed 2026-08-13: word_table is a
|
||||
free-standing global constant now, not a vm_state field, so
|
||||
"word_table (vm\<lparr>...\<rparr>)" no longer type-checks -- true by construction. *)
|
||||
|
||||
(* =========================================================================
|
||||
Section 3: Level 2 — Physics invariants (all ✓ or ○)
|
||||
@@ -125,11 +132,14 @@ theorem starforth_correctness_totality:
|
||||
fixes vm :: vm_state
|
||||
assumes wf: "wf_vm vm"
|
||||
shows
|
||||
(* Level 1: key wf_vm invariants hold *)
|
||||
(* Level 1: key wf_vm invariants hold. Level 2: physics invariants
|
||||
from wf_vm (comment moved out here 2026-08-13 -- it was previously
|
||||
embedded mid-string at the "rw_eff_window" line, which is inside a
|
||||
quoted prop and does not parse as a comment there; genuine syntax
|
||||
error, not a version issue). *)
|
||||
"length (data_stack vm) \<le> STACK_SIZE \<and>
|
||||
length (return_stack vm) \<le> STACK_SIZE \<and>
|
||||
\<not> vm_error vm \<and>
|
||||
(* Level 2: physics invariants from wf_vm *)
|
||||
rw_eff_window (rolling_window vm) \<ge> ADAPTIVE_MIN_WINDOW_SIZE \<and>
|
||||
rw_eff_window (rolling_window vm) \<le> ROLLING_WINDOW_SIZE \<and>
|
||||
rw_act_window (rolling_window vm) \<le> ROLLING_WINDOW_SIZE \<and>
|
||||
@@ -142,15 +152,15 @@ theorem starforth_correctness_totality:
|
||||
(* Corollary: non-interference for a word executed after k heartbeat ticks. *)
|
||||
corollary word_result_heartbeat_independent:
|
||||
"\<forall> n k vm.
|
||||
data_stack (word_table (heartbeat_step ^^ k $ vm) n (heartbeat_step ^^ k $ vm))
|
||||
= data_stack (word_table vm n vm)"
|
||||
data_stack (word_table n ((heartbeat_step ^^ k) vm))
|
||||
= data_stack (word_table n vm)"
|
||||
using heartbeat_noninterference by blast
|
||||
|
||||
(* Corollary: trace-level non-interference (proved theorem). *)
|
||||
corollary trace_result_heartbeat_independent:
|
||||
"\<And> words vm k.
|
||||
data_stack (foldl (\<lambda>s n. word_table s n s) (heartbeat_step ^^ k $ vm) words)
|
||||
= data_stack (foldl (\<lambda>s n. word_table s n s) vm words)"
|
||||
data_stack (foldl (\<lambda>s n. word_table n s) ((heartbeat_step ^^ k) vm) words)
|
||||
= data_stack (foldl (\<lambda>s n. word_table n s) vm words)"
|
||||
using heartbeat_trace_noninterference by blast
|
||||
|
||||
end
|
||||
|
||||
@@ -2,6 +2,10 @@ theory StarForth_Logical_Words
|
||||
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
|
||||
|
||||
(* =========================================================================
|
||||
POST-03: Logical and Comparison Words
|
||||
Mirrors: src/word_source/logical_words.c
|
||||
@@ -194,13 +198,13 @@ lemma zero_lt_negative:
|
||||
assumes "data_stack vm = n # xs"
|
||||
assumes "n < 0"
|
||||
shows "data_stack (forth_zero_lt vm) = (-1) # xs"
|
||||
by (simp add: forth_zero_lt_def to_forth_bool_def forth_true_def assms)
|
||||
using assms by (auto simp: forth_zero_lt_def to_forth_bool_def forth_true_def)
|
||||
|
||||
lemma zero_lt_nonneg:
|
||||
assumes "data_stack vm = n # xs"
|
||||
assumes "n \<ge> 0"
|
||||
shows "data_stack (forth_zero_lt vm) = 0 # xs"
|
||||
by (simp add: forth_zero_lt_def to_forth_bool_def forth_false_def assms)
|
||||
using assms by (auto simp: forth_zero_lt_def to_forth_bool_def forth_false_def)
|
||||
|
||||
lemma zero_lt_underflow:
|
||||
assumes "data_stack vm = []"
|
||||
@@ -220,13 +224,13 @@ lemma zero_gt_positive:
|
||||
assumes "data_stack vm = n # xs"
|
||||
assumes "n > 0"
|
||||
shows "data_stack (forth_zero_gt vm) = (-1) # xs"
|
||||
by (simp add: forth_zero_gt_def to_forth_bool_def forth_true_def assms)
|
||||
using assms by (auto simp: forth_zero_gt_def to_forth_bool_def forth_true_def)
|
||||
|
||||
lemma zero_gt_nonpos:
|
||||
assumes "data_stack vm = n # xs"
|
||||
assumes "n \<le> 0"
|
||||
shows "data_stack (forth_zero_gt vm) = 0 # xs"
|
||||
by (simp add: forth_zero_gt_def to_forth_bool_def forth_false_def assms)
|
||||
using assms by (auto simp: forth_zero_gt_def to_forth_bool_def forth_false_def)
|
||||
|
||||
lemma zero_gt_underflow:
|
||||
assumes "data_stack vm = []"
|
||||
@@ -270,7 +274,7 @@ lemma eq_symmetric:
|
||||
assumes "data_stack vm = n2 # n1 # rest"
|
||||
assumes "data_stack vm' = n1 # n2 # rest"
|
||||
shows "data_stack (forth_eq vm) = data_stack (forth_eq vm')"
|
||||
by (simp add: forth_eq_def assms)
|
||||
by (simp add: forth_eq_def assms eq_commute)
|
||||
|
||||
lemma eq_underflow_nil:
|
||||
assumes "data_stack vm = []"
|
||||
|
||||
@@ -2,6 +2,10 @@ 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)
|
||||
|
||||
@@ -60,25 +64,33 @@ definition heat_increment :: "dict_entry \<Rightarrow> dict_entry" where
|
||||
lemma heat_increment_correct:
|
||||
assumes "de_heat e < HEAT_MAX"
|
||||
shows "de_heat (heat_increment e) = de_heat e + 1"
|
||||
by (simp add: heat_increment_def assms)
|
||||
using assms by (simp add: heat_increment_def min_def)
|
||||
|
||||
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)
|
||||
|
||||
(* 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:
|
||||
"de_heat (heat_increment e) \<ge> de_heat e"
|
||||
by (simp add: heat_increment_def)
|
||||
assumes "de_heat e \<le> HEAT_MAX"
|
||||
shows "de_heat (heat_increment e) \<ge> de_heat e"
|
||||
using assms by (simp add: heat_increment_def)
|
||||
|
||||
lemma heat_increment_preserves_validity:
|
||||
assumes "heat_valid e"
|
||||
shows "heat_valid (heat_increment e)"
|
||||
proof -
|
||||
have "de_heat e \<ge> 0" and "de_heat e \<le> HEAT_MAX"
|
||||
have h0: "de_heat e \<ge> 0" and hmax: "de_heat e \<le> HEAT_MAX"
|
||||
using assms by (simp_all add: heat_valid_def)
|
||||
thus ?thesis
|
||||
by (simp add: heat_valid_def heat_increment_def HEAT_MAX_def)
|
||||
have le: "de_heat (heat_increment e) \<le> HEAT_MAX"
|
||||
unfolding heat_increment_def by (simp add: min.cobounded2)
|
||||
have ge: "de_heat (heat_increment e) \<ge> 0"
|
||||
unfolding heat_increment_def using h0 by (simp add: HEAT_MAX_def)
|
||||
from le ge show ?thesis by (simp add: heat_valid_def)
|
||||
qed
|
||||
|
||||
lemma heat_increment_preserves_flags:
|
||||
@@ -112,10 +124,18 @@ lemma heat_decay_frozen:
|
||||
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> 1 is the standing invariant a pinned word is
|
||||
supposed to maintain (see heat_decay_pinned_positive's own \<ge> 1
|
||||
conclusion below), just never stated here as a precondition before. *)
|
||||
lemma heat_decay_monotone:
|
||||
assumes "\<not> heat_frozen e"
|
||||
assumes "de_heat e \<ge> 1"
|
||||
assumes "amount \<ge> 0"
|
||||
shows "de_heat (heat_decay amount e) \<le> de_heat e"
|
||||
by (simp add: heat_decay_def assms)
|
||||
using assms by (simp add: heat_decay_def)
|
||||
|
||||
lemma heat_decay_non_negative:
|
||||
assumes "\<not> heat_frozen e"
|
||||
@@ -155,7 +175,7 @@ lemma heat_decay_preserves_flags:
|
||||
(* 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"
|
||||
(\<forall>i e. dictionary vm i = Some e \<longrightarrow> heat_valid e)"
|
||||
|
||||
(* =========================================================================
|
||||
Section 6: Heat thresholds
|
||||
|
||||
@@ -78,9 +78,17 @@ lemma window_advance_act_window:
|
||||
"rw_act_window (window_advance w rw) = min (rw_total_exec rw + 1) ROLLING_WINDOW_SIZE"
|
||||
by (simp add: window_advance_def)
|
||||
|
||||
(* CORRECTED 2026-08-13: added the missing window_invariant hypothesis.
|
||||
Without it, rw_act_window rw is an unconstrained field unrelated to
|
||||
rw_total_exec rw, so the claim is not provable -- nothing stops a
|
||||
caller from handing in a state where rw_act_window is already larger
|
||||
than the post-advance value. window_invariant is exactly what ties
|
||||
rw_act_window to rw_total_exec (its defining formula), which is what
|
||||
the proof actually needs. *)
|
||||
lemma window_advance_act_monotone:
|
||||
"rw_act_window (window_advance w rw) \<ge> rw_act_window rw"
|
||||
by (simp add: window_advance_def min_def)
|
||||
assumes "window_invariant rw"
|
||||
shows "rw_act_window (window_advance w rw) \<ge> rw_act_window rw"
|
||||
using assms by (simp add: window_advance_def window_invariant_def min_def)
|
||||
|
||||
lemma window_advance_act_bounded:
|
||||
"rw_act_window (window_advance w rw) \<le> ROLLING_WINDOW_SIZE"
|
||||
@@ -120,29 +128,50 @@ lemma window_shrink_lb:
|
||||
lemma window_shrink_ub:
|
||||
assumes "rw_eff_window rw \<le> ROLLING_WINDOW_SIZE"
|
||||
shows "rw_eff_window (window_shrink rw) \<le> ROLLING_WINDOW_SIZE"
|
||||
using assms by (simp add: window_shrink_def)
|
||||
using assms
|
||||
by (simp add: window_shrink_def ROLLING_WINDOW_SIZE_def ADAPTIVE_MIN_WINDOW_SIZE_def)
|
||||
|
||||
(* CORRECTED 2026-08-13: added the missing lower-bound hypothesis. Without
|
||||
it, rw_eff_window rw could be below ADAPTIVE_MIN_WINDOW_SIZE, in which
|
||||
case window_shrink's max-clamp raises it back up to the floor -- the
|
||||
result would then be \<ge> the input, not \<le>. window_invariant's own lower
|
||||
bound is exactly what rules this out. *)
|
||||
lemma window_shrink_mono:
|
||||
"rw_eff_window (window_shrink rw) \<le> rw_eff_window rw"
|
||||
by (simp add: window_shrink_def)
|
||||
assumes "rw_eff_window rw \<ge> ADAPTIVE_MIN_WINDOW_SIZE"
|
||||
shows "rw_eff_window (window_shrink rw) \<le> rw_eff_window rw"
|
||||
using assms by (simp add: window_shrink_def)
|
||||
|
||||
lemma window_shrink_preserves_invariant:
|
||||
assumes "window_invariant rw"
|
||||
shows "window_invariant (window_shrink rw)"
|
||||
using assms by (simp add: window_invariant_def window_shrink_def)
|
||||
using assms
|
||||
by (auto simp: window_invariant_def window_shrink_def diff_le_self
|
||||
intro: le_trans[OF diff_le_self])
|
||||
|
||||
lemma window_grow_lb:
|
||||
assumes "rw_eff_window rw \<ge> ADAPTIVE_MIN_WINDOW_SIZE"
|
||||
shows "rw_eff_window (window_grow rw) \<ge> ADAPTIVE_MIN_WINDOW_SIZE"
|
||||
using assms by (simp add: window_grow_def)
|
||||
using assms
|
||||
by (simp add: window_grow_def ROLLING_WINDOW_SIZE_def ADAPTIVE_MIN_WINDOW_SIZE_def)
|
||||
|
||||
lemma window_grow_ub:
|
||||
"rw_eff_window (window_grow rw) \<le> ROLLING_WINDOW_SIZE"
|
||||
by (simp add: window_grow_def)
|
||||
proof -
|
||||
have "rw_eff_window (window_grow rw)
|
||||
= min ROLLING_WINDOW_SIZE (rw_eff_window rw + ADAPTIVE_GROWTH_THRESHOLD)"
|
||||
by (simp add: window_grow_def)
|
||||
also have "\<dots> \<le> ROLLING_WINDOW_SIZE" by (rule min.cobounded1)
|
||||
finally show ?thesis .
|
||||
qed
|
||||
|
||||
(* CORRECTED 2026-08-13: added the missing upper-bound hypothesis. Without
|
||||
it, rw_eff_window rw could already exceed ROLLING_WINDOW_SIZE, in which
|
||||
case window_grow's min-clamp would lower it -- the result would then be
|
||||
\<le> the input, not \<ge>. *)
|
||||
lemma window_grow_mono:
|
||||
"rw_eff_window (window_grow rw) \<ge> rw_eff_window rw"
|
||||
by (simp add: window_grow_def)
|
||||
assumes "rw_eff_window rw \<le> ROLLING_WINDOW_SIZE"
|
||||
shows "rw_eff_window (window_grow rw) \<ge> rw_eff_window rw"
|
||||
using assms by (simp add: window_grow_def)
|
||||
|
||||
lemma window_grow_preserves_invariant:
|
||||
assumes "window_invariant rw"
|
||||
|
||||
@@ -21,9 +21,11 @@ begin
|
||||
======================================================================== *)
|
||||
|
||||
(* ○ CODE-MUST-MATCH: Initial slope = 2 × Q48_SCALE = 131072.
|
||||
Matches DECAY_RATE_PER_US_Q16 × 2 in include/vm.h. *)
|
||||
Matches DECAY_RATE_PER_US_Q16 × 2 in include/vm.h.
|
||||
CORRECTED 2026-08-13: was "2 * Q48_SCALE" directly -- Q48_SCALE :: q48
|
||||
(64 word), this constant is nat. Same unat fix as elsewhere. *)
|
||||
definition DECAY_SLOPE_INIT :: nat where
|
||||
"DECAY_SLOPE_INIT = 2 * Q48_SCALE"
|
||||
"DECAY_SLOPE_INIT = 2 * unat Q48_SCALE"
|
||||
|
||||
(* ○ CODE-MUST-MATCH: Never let slope reach zero.
|
||||
⚠ HUMAN-REVIEW: Every C code path that reduces decay_slope_q48 must clamp
|
||||
@@ -33,7 +35,7 @@ definition DECAY_SLOPE_MIN :: nat where
|
||||
"DECAY_SLOPE_MIN = 1"
|
||||
|
||||
definition DECAY_SLOPE_MAX :: nat where
|
||||
"DECAY_SLOPE_MAX = Q48_SCALE * 1000"
|
||||
"DECAY_SLOPE_MAX = unat Q48_SCALE * 1000"
|
||||
|
||||
(* =========================================================================
|
||||
Section 2: Slope well-formedness
|
||||
@@ -69,7 +71,8 @@ lemma slope_decrease_lb:
|
||||
lemma slope_decrease_preserves_wf:
|
||||
assumes "slope_wf s"
|
||||
shows "slope_wf (slope_decrease step s)"
|
||||
using assms by (simp add: slope_wf_def slope_decrease_def DECAY_SLOPE_MIN_def)
|
||||
using assms
|
||||
by (auto simp: slope_wf_def slope_decrease_def intro: le_trans[OF diff_le_self])
|
||||
|
||||
lemma slope_increase_ub:
|
||||
"slope_increase step s \<le> DECAY_SLOPE_MAX"
|
||||
@@ -80,11 +83,20 @@ lemma slope_increase_preserves_wf:
|
||||
shows "slope_wf (slope_increase step s)"
|
||||
using assms by (simp add: slope_wf_def slope_increase_def DECAY_SLOPE_MIN_def DECAY_SLOPE_MAX_def)
|
||||
|
||||
lemma slope_decrease_mono: "slope_decrease step s \<le> s"
|
||||
by (simp add: slope_decrease_def)
|
||||
(* CORRECTED 2026-08-13: added the missing slope_wf hypothesis. Without
|
||||
"s \<ge> DECAY_SLOPE_MIN", slope_decrease's max-clamp can raise a too-small
|
||||
s back up above its own input (e.g. s=0, step=0 gives
|
||||
max DECAY_SLOPE_MIN 0 = 1 > 0 = s), breaking the claim. Symmetric
|
||||
argument for slope_increase_mono below. *)
|
||||
lemma slope_decrease_mono:
|
||||
assumes "s \<ge> DECAY_SLOPE_MIN"
|
||||
shows "slope_decrease step s \<le> s"
|
||||
using assms by (simp add: slope_decrease_def)
|
||||
|
||||
lemma slope_increase_mono: "slope_increase step s \<ge> s"
|
||||
by (simp add: slope_increase_def)
|
||||
lemma slope_increase_mono:
|
||||
assumes "s \<le> DECAY_SLOPE_MAX"
|
||||
shows "slope_increase step s \<ge> s"
|
||||
using assms by (simp add: slope_increase_def)
|
||||
|
||||
(* =========================================================================
|
||||
Section 4: VM decay step
|
||||
@@ -134,8 +146,8 @@ lemma vm_decay_step_dict [simp]:
|
||||
|
||||
definition total_dict_heat :: "vm_state \<Rightarrow> int" where
|
||||
"total_dict_heat vm =
|
||||
\<Sum>i \<in> {i. dictionary vm i \<noteq> None}.
|
||||
de_heat (the (dictionary vm i))"
|
||||
(\<Sum>i \<in> {i. dictionary vm i \<noteq> None}.
|
||||
de_heat (the (dictionary vm i)))"
|
||||
|
||||
(* PROOF (no sorry):
|
||||
vm_decay_step only changes decay_slope_q48, so dictionary is identical
|
||||
@@ -149,7 +161,7 @@ lemma decay_step_dict_unchanged:
|
||||
lemma decay_total_heat_non_increasing:
|
||||
assumes "\<forall>i. dictionary vm i \<noteq> None \<longrightarrow> de_heat (the (dictionary vm i)) \<ge> 0"
|
||||
shows "total_dict_heat (vm_decay_step step vm) \<le> total_dict_heat vm"
|
||||
using decay_step_dict_unchanged by linarith
|
||||
by (simp add: decay_step_dict_unchanged)
|
||||
|
||||
(* =========================================================================
|
||||
Section 6: Well-formedness: slope is positive in wf_vm
|
||||
|
||||
@@ -23,28 +23,40 @@ begin
|
||||
Section 1: Pipeline accuracy
|
||||
======================================================================== *)
|
||||
|
||||
(* CORRECTED 2026-08-13: was "* Q48_SCALE" directly -- Q48_SCALE :: q48
|
||||
(64 word), this function is nat. Same fix as StarForth_Loop5_WinInf.thy's
|
||||
ANOVA_VARIANCE_THRESHOLD: unat Q48_SCALE converts to the equivalent nat. *)
|
||||
definition pm_accuracy_q48 :: "pipeline_metrics_state \<Rightarrow> nat" where
|
||||
"pm_accuracy_q48 pm =
|
||||
(if pm_prefetch_attempts pm = 0
|
||||
then 0
|
||||
else (pm_prefetch_hits pm * Q48_SCALE) div pm_prefetch_attempts pm)"
|
||||
else (pm_prefetch_hits pm * unat Q48_SCALE) div pm_prefetch_attempts pm)"
|
||||
|
||||
lemma pm_accuracy_zero_attempts [simp]:
|
||||
"pm_accuracy_q48 (pm\<lparr>pm_prefetch_attempts := 0\<rparr>) = 0"
|
||||
by (simp add: pm_accuracy_q48_def)
|
||||
|
||||
(* CORRECTED 2026-08-13: "\<le> Q48_ONE" was comparing nat to q48 (64 word) --
|
||||
a type error, could not have type-checked under any Isabelle version.
|
||||
Fixed via unat Q48_ONE, same pattern as pm_accuracy_q48_def above.
|
||||
Internal proof also fixed: Q48_SCALE needs unat for the same reason, and
|
||||
div_le_iff_le_mult doesn't exist under this name any more (same finding
|
||||
as StarForth_Q48_16.thy's q48_accuracy_upper_bound) -- replaced with the
|
||||
same div_le_mono-based argument used there. *)
|
||||
lemma pm_accuracy_upper_bound:
|
||||
assumes "pm_prefetch_hits pm \<le> pm_prefetch_attempts pm"
|
||||
shows "pm_accuracy_q48 pm \<le> Q48_ONE"
|
||||
shows "pm_accuracy_q48 pm \<le> unat Q48_ONE"
|
||||
proof (cases "pm_prefetch_attempts pm = 0")
|
||||
case True thus ?thesis by (simp add: pm_accuracy_q48_def Q48_ONE_def)
|
||||
next
|
||||
case False
|
||||
have "pm_prefetch_hits pm * Q48_SCALE \<le> pm_prefetch_attempts pm * Q48_SCALE"
|
||||
using assms by (simp add: mult_le_mono1)
|
||||
hence "(pm_prefetch_hits pm * Q48_SCALE) div pm_prefetch_attempts pm \<le> Q48_SCALE"
|
||||
using False by (simp add: div_le_iff_le_mult)
|
||||
thus ?thesis by (simp add: pm_accuracy_q48_def Q48_ONE_def False)
|
||||
have "(pm_prefetch_hits pm * unat Q48_SCALE) div pm_prefetch_attempts pm
|
||||
\<le> (pm_prefetch_attempts pm * unat Q48_SCALE) div pm_prefetch_attempts pm"
|
||||
using assms by (intro div_le_mono mult_le_mono1)
|
||||
also have "\<dots> = unat Q48_SCALE"
|
||||
using False by simp
|
||||
finally show ?thesis
|
||||
by (simp add: pm_accuracy_q48_def Q48_ONE_def False)
|
||||
qed
|
||||
|
||||
lemma pm_accuracy_non_negative:
|
||||
@@ -65,8 +77,12 @@ definition pm_wf :: "pipeline_metrics_state \<Rightarrow> bool" where
|
||||
|
||||
lemma pm_wf_accuracy_range:
|
||||
assumes "pm_wf pm"
|
||||
shows "pm_accuracy_q48 pm \<le> Q48_ONE"
|
||||
using assms by (simp add: pm_accuracy_upper_bound pm_wf_def)
|
||||
shows "pm_accuracy_q48 pm \<le> unat Q48_ONE"
|
||||
proof -
|
||||
have "pm_prefetch_hits pm \<le> pm_prefetch_attempts pm"
|
||||
using assms by (simp add: pm_wf_def)
|
||||
thus ?thesis by (rule pm_accuracy_upper_bound)
|
||||
qed
|
||||
|
||||
(* =========================================================================
|
||||
Section 3: Recording a prefetch hit or miss
|
||||
@@ -97,15 +113,26 @@ lemma pm_record_miss_hits_unchanged:
|
||||
"pm_prefetch_hits (pm_record_miss pm) = pm_prefetch_hits pm"
|
||||
by (simp add: pm_record_miss_def)
|
||||
|
||||
(* FLAGGED, NOT FIXED 2026-08-13: pm_wf is not actually closed under
|
||||
pm_record_hit/pm_record_miss as currently defined. pm_wf only requires
|
||||
"pm_last_accuracy_den pm > 0" when pm_prefetch_attempts pm > 0 -- when
|
||||
attempts = 0, den is completely unconstrained (could be 0). Both
|
||||
pm_record_hit and pm_record_miss increment attempts from 0 to 1 without
|
||||
touching pm_last_accuracy_den, so pm_wf's postcondition needs den > 0
|
||||
in a state where nothing in the precondition ever guaranteed it. Not a
|
||||
proof-script issue -- a genuine gap in what pm_wf requires versus what
|
||||
these two operations can establish. Left failing rather than silently
|
||||
strengthening pm_wf's own definition (a design decision, not a
|
||||
mechanical fix) or weakening these lemmas' claim. *)
|
||||
lemma pm_record_hit_preserves_wf:
|
||||
assumes "pm_wf pm"
|
||||
shows "pm_wf (pm_record_hit pm)"
|
||||
using assms by (simp add: pm_wf_def pm_record_hit_def)
|
||||
oops
|
||||
|
||||
lemma pm_record_miss_preserves_wf:
|
||||
assumes "pm_wf pm"
|
||||
shows "pm_wf (pm_record_miss pm)"
|
||||
using assms by (simp add: pm_wf_def pm_record_miss_def)
|
||||
oops
|
||||
|
||||
(* After a hit, hits ≤ attempts still holds. *)
|
||||
lemma pm_record_hit_hits_le_attempts:
|
||||
|
||||
@@ -49,8 +49,14 @@ lemma inf_window_wf_ub:
|
||||
Section 2: ANOVA early-exit threshold
|
||||
======================================================================== *)
|
||||
|
||||
(* CORRECTED 2026-08-13: was "= Q48_SCALE" directly -- Q48_SCALE :: q48
|
||||
(64 word) but this constant is nat (matching io_window_variance_q48's
|
||||
type). A genuine type error, not library drift; this could not have
|
||||
type-checked under any Isabelle version. Fixed via unat to convert the
|
||||
word's value (65536) to the equivalent nat while keeping the same
|
||||
intended numeric meaning (1.0 in Q48.16). *)
|
||||
definition ANOVA_VARIANCE_THRESHOLD :: nat where
|
||||
"ANOVA_VARIANCE_THRESHOLD = Q48_SCALE" \<comment> \<open>1.0 in Q48.16 — matches C default\<close>
|
||||
"ANOVA_VARIANCE_THRESHOLD = unat Q48_SCALE" \<comment> \<open>1.0 in Q48.16 — matches C default\<close>
|
||||
|
||||
definition anova_early_exit :: "inference_outputs_state \<Rightarrow> bool" where
|
||||
"anova_early_exit io \<longleftrightarrow>
|
||||
|
||||
@@ -29,7 +29,8 @@ definition clamp_slope_suggestion :: "nat \<Rightarrow> nat" where
|
||||
|
||||
lemma clamp_slope_wf:
|
||||
"slope_wf (clamp_slope_suggestion s)"
|
||||
by (simp add: slope_wf_def clamp_slope_suggestion_def)
|
||||
by (simp add: slope_wf_def clamp_slope_suggestion_def
|
||||
DECAY_SLOPE_MIN_def DECAY_SLOPE_MAX_def Q48_SCALE_def)
|
||||
|
||||
lemma clamp_slope_pos:
|
||||
"clamp_slope_suggestion s \<ge> DECAY_SLOPE_MIN"
|
||||
|
||||
@@ -86,7 +86,9 @@ lemma hb_shorten_pos:
|
||||
lemma hb_shorten_preserves_wf:
|
||||
assumes "hb_state_wf hb"
|
||||
shows "hb_state_wf (hb_shorten_period delta hb)"
|
||||
using assms by (simp add: hb_state_wf_def hb_shorten_period_def TICK_MAX_NS_def TICK_MIN_NS_def)
|
||||
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"
|
||||
@@ -95,7 +97,7 @@ lemma hb_lengthen_ub:
|
||||
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)
|
||||
using assms by (simp add: hb_lengthen_period_def TICK_MAX_NS_def)
|
||||
|
||||
lemma hb_lengthen_preserves_wf:
|
||||
assumes "hb_state_wf hb"
|
||||
|
||||
@@ -2,6 +2,10 @@ theory StarForth_Memory_Words
|
||||
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
|
||||
|
||||
(* =========================================================================
|
||||
POST-05: Memory Access Words
|
||||
Mirrors: src/word_source/memory_words.c
|
||||
@@ -38,7 +42,7 @@ lemma mem_write_read_same:
|
||||
lemma mem_write_read_other:
|
||||
assumes "a \<noteq> b"
|
||||
shows "mem_read (mem_write mem a v) b = mem_read mem b"
|
||||
by (simp add: mem_read_def mem_write_def assms)
|
||||
using assms by (auto simp: mem_read_def mem_write_def)
|
||||
|
||||
(* ── @ ( addr -- n ) ───────────────────────────────────────────────────── *)
|
||||
(* Pops addr from data stack, reads cell from memory at addr, pushes value.
|
||||
@@ -57,7 +61,7 @@ lemma fetch_normal:
|
||||
assumes "data_stack vm = addr # xs"
|
||||
assumes "addr \<ge> 0"
|
||||
shows "data_stack (forth_fetch vm) = mem_read (memory vm) (nat addr) # xs"
|
||||
by (simp add: forth_fetch_def assms)
|
||||
using assms by (auto simp: forth_fetch_def)
|
||||
|
||||
lemma fetch_reads_stored_value:
|
||||
assumes "memory vm = mem_write m a v"
|
||||
@@ -101,26 +105,26 @@ lemma store_normal:
|
||||
assumes "addr \<ge> 0"
|
||||
shows "data_stack (forth_store vm) = xs"
|
||||
and "memory (forth_store vm) = mem_write (memory vm) (nat addr) n"
|
||||
by (simp add: forth_store_def assms)+
|
||||
using assms by (auto simp: forth_store_def)
|
||||
|
||||
lemma store_writes_value:
|
||||
assumes "data_stack vm = addr # n # xs"
|
||||
assumes "addr \<ge> 0"
|
||||
shows "mem_read (memory (forth_store vm)) (nat addr) = n"
|
||||
by (simp add: forth_store_def mem_write_def mem_read_def assms)
|
||||
using assms by (auto simp: forth_store_def mem_write_def mem_read_def)
|
||||
|
||||
lemma store_depth_decreases:
|
||||
assumes "data_stack vm = addr # n # xs"
|
||||
assumes "addr \<ge> 0"
|
||||
shows "length (data_stack (forth_store vm)) = length (data_stack vm) - 2"
|
||||
by (simp add: forth_store_def assms)
|
||||
using assms by (auto simp: forth_store_def)
|
||||
|
||||
lemma store_other_unchanged:
|
||||
assumes "data_stack vm = addr # n # xs"
|
||||
assumes "addr \<ge> 0"
|
||||
assumes "nat addr \<noteq> b"
|
||||
shows "mem_read (memory (forth_store vm)) b = mem_read (memory vm) b"
|
||||
by (simp add: forth_store_def mem_write_def mem_read_def assms)
|
||||
using assms by (auto simp: forth_store_def mem_write_def mem_read_def)
|
||||
|
||||
lemma store_underflow_nil:
|
||||
assumes "data_stack vm = []"
|
||||
@@ -147,7 +151,7 @@ lemma store_then_fetch:
|
||||
assumes "memory vm' = memory (forth_store vm)"
|
||||
assumes "addr \<ge> 0"
|
||||
shows "hd (data_stack (forth_fetch vm')) = n"
|
||||
by (simp add: forth_fetch_def forth_store_def mem_write_def mem_read_def assms)
|
||||
using assms by (auto simp: forth_fetch_def forth_store_def mem_write_def mem_read_def)
|
||||
|
||||
(* ── C@ ( addr -- c ) ──────────────────────────────────────────────────── *)
|
||||
(* Reads a single byte (0..255) from memory, zero-extended to cell width.
|
||||
@@ -169,14 +173,14 @@ lemma cfetch_normal:
|
||||
assumes "addr \<ge> 0"
|
||||
shows "data_stack (forth_cfetch vm) =
|
||||
(mem_read (memory vm) (nat addr) AND 0xFF) # xs"
|
||||
by (simp add: forth_cfetch_def assms)
|
||||
using assms by (auto simp: forth_cfetch_def)
|
||||
|
||||
lemma cfetch_byte_range:
|
||||
assumes "data_stack vm = addr # xs"
|
||||
assumes "addr \<ge> 0"
|
||||
shows "0 \<le> hd (data_stack (forth_cfetch vm))"
|
||||
and "hd (data_stack (forth_cfetch vm)) \<le> 255"
|
||||
by (simp add: forth_cfetch_def assms)+
|
||||
using assms by (auto simp: forth_cfetch_def)
|
||||
|
||||
lemma cfetch_underflow:
|
||||
assumes "data_stack vm = []"
|
||||
@@ -208,19 +212,19 @@ lemma cstore_normal:
|
||||
assumes "addr \<ge> 0"
|
||||
shows "data_stack (forth_cstore vm) = xs"
|
||||
and "memory (forth_cstore vm) = mem_write (memory vm) (nat addr) (c AND 0xFF)"
|
||||
by (simp add: forth_cstore_def assms)+
|
||||
using assms by (auto simp: forth_cstore_def)
|
||||
|
||||
lemma cstore_writes_byte:
|
||||
assumes "data_stack vm = addr # c # xs"
|
||||
assumes "addr \<ge> 0"
|
||||
shows "mem_read (memory (forth_cstore vm)) (nat addr) = c AND 0xFF"
|
||||
by (simp add: forth_cstore_def mem_write_def mem_read_def assms)
|
||||
using assms by (auto simp: forth_cstore_def mem_write_def mem_read_def)
|
||||
|
||||
lemma cstore_depth_decreases:
|
||||
assumes "data_stack vm = addr # c # xs"
|
||||
assumes "addr \<ge> 0"
|
||||
shows "length (data_stack (forth_cstore vm)) = length (data_stack vm) - 2"
|
||||
by (simp add: forth_cstore_def assms)
|
||||
using assms by (auto simp: forth_cstore_def)
|
||||
|
||||
lemma cstore_underflow_nil:
|
||||
assumes "data_stack vm = []"
|
||||
@@ -245,6 +249,6 @@ lemma cstore_then_cfetch:
|
||||
assumes "data_stack vm' = addr # xs"
|
||||
assumes "memory vm' = memory (forth_cstore vm)"
|
||||
shows "hd (data_stack (forth_cfetch vm')) = c AND 0xFF"
|
||||
by (simp add: forth_cfetch_def forth_cstore_def mem_write_def mem_read_def assms)
|
||||
using assms by (auto simp: forth_cfetch_def forth_cstore_def mem_write_def mem_read_def)
|
||||
|
||||
end
|
||||
|
||||
@@ -104,18 +104,18 @@ lemma lock_wf_held:
|
||||
lemma acquire_preserves_wf:
|
||||
assumes "lock_wf s" "valid_thread t"
|
||||
shows "lock_wf (acquire_lock t s)"
|
||||
by (cases s; simp add: acquire_lock_def lock_wf_def assms)
|
||||
using assms by (cases s; simp add: acquire_lock_def lock_wf_def)
|
||||
|
||||
lemma release_preserves_wf:
|
||||
assumes "lock_wf s"
|
||||
shows "lock_wf (release_lock t s)"
|
||||
by (cases s; simp add: release_lock_def lock_wf_def assms)
|
||||
using assms by (cases s; simp add: release_lock_def lock_wf_def)
|
||||
|
||||
(* Two distinct threads cannot both hold the same lock. *)
|
||||
lemma mutex_exclusive:
|
||||
assumes "lock_held_by t s" "lock_held_by u s"
|
||||
shows "t = u"
|
||||
by (cases s; simp add: lock_held_by_def assms; blast)
|
||||
using assms by (cases s; simp add: lock_held_by_def)
|
||||
|
||||
(* =========================================================================
|
||||
Section 5: VM-level lock accessors
|
||||
|
||||
+76
-23
@@ -2,6 +2,11 @@ theory StarForth_Q48_16
|
||||
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 to avoid clashing with other uses of the
|
||||
same tokens. q48_frac_part below needs it. *)
|
||||
unbundle bit_operations_syntax
|
||||
|
||||
(* =========================================================================
|
||||
StarForth_Q48_16 — Q48.16 Fixed-Point Arithmetic (HOL-Word model)
|
||||
|
||||
@@ -58,9 +63,15 @@ definition q48_to_u64 :: "q48 \<Rightarrow> 64 word" where
|
||||
lemma q48_round_trip:
|
||||
assumes "unat n < 2 ^ 48"
|
||||
shows "q48_to_u64 (q48_from_u64 n) = n"
|
||||
unfolding q48_to_u64_def q48_from_u64_def
|
||||
using assms
|
||||
by (simp add: drop_bit_push_bit word_size)
|
||||
proof -
|
||||
have "unat n * 65536 < 2 ^ 64" using assms by simp
|
||||
hence h: "unat (n * 65536) = unat n * 65536"
|
||||
using unat_mult_lem[of n "65536::q48"] by simp
|
||||
show ?thesis
|
||||
unfolding q48_to_u64_def q48_from_u64_def
|
||||
by (simp add: word_unat_eq_iff push_bit_eq_mult drop_bit_eq_div
|
||||
unat_div_distrib h)
|
||||
qed
|
||||
|
||||
lemma q48_from_u64_zero [simp]: "q48_from_u64 0 = 0"
|
||||
by (simp add: q48_from_u64_def)
|
||||
@@ -68,11 +79,26 @@ lemma q48_from_u64_zero [simp]: "q48_from_u64 0 = 0"
|
||||
lemma q48_to_u64_zero [simp]: "q48_to_u64 0 = 0"
|
||||
by (simp add: q48_to_u64_def)
|
||||
|
||||
(* CORRECTED 2026-08-13: the original statement had no upper bound and is
|
||||
false as such -- push_bit 16 wraps mod 2^64, so e.g. a=1, b=2^48 satisfies
|
||||
unat a \<le> unat b (1 \<le> 2^48) while push_bit 16 a = 65536 and push_bit 16 b
|
||||
wraps to 0, breaking the conclusion. Added the same "unat _ < 2^48
|
||||
overflow-free range" bound this file already uses everywhere else. *)
|
||||
lemma q48_from_u64_mono:
|
||||
assumes "unat a \<le> unat b"
|
||||
assumes "unat a \<le> unat b" and "unat b < 2 ^ 48"
|
||||
shows "unat (q48_from_u64 a) \<le> unat (q48_from_u64 b)"
|
||||
unfolding q48_from_u64_def
|
||||
using assms by (simp add: unat_push_bit)
|
||||
proof -
|
||||
have ha: "unat a < 2 ^ 48" using assms by simp
|
||||
have hb64: "unat b * 65536 < 2 ^ 64" using assms(2) by simp
|
||||
have ha64: "unat a * 65536 < 2 ^ 64" using ha by simp
|
||||
have eb: "unat (b * 65536) = unat b * 65536"
|
||||
using unat_mult_lem[of b "65536::q48"] hb64 by simp
|
||||
have ea: "unat (a * 65536) = unat a * 65536"
|
||||
using unat_mult_lem[of a "65536::q48"] ha64 by simp
|
||||
show ?thesis
|
||||
unfolding q48_from_u64_def
|
||||
by (simp add: push_bit_eq_mult ea eb assms(1))
|
||||
qed
|
||||
|
||||
(* =========================================================================
|
||||
Section 3: Arithmetic operations
|
||||
@@ -117,9 +143,14 @@ lemma q48_mul_zero_left [simp]: "q48_mul 0 a = 0"
|
||||
lemma q48_mul_one_right:
|
||||
assumes "unat a < 2 ^ 48"
|
||||
shows "q48_mul a Q48_ONE = a"
|
||||
unfolding q48_mul_def Q48_ONE_def Q48_SCALE_def
|
||||
using assms
|
||||
by (simp add: drop_bit_push_bit word_size)
|
||||
proof -
|
||||
have "unat a * 65536 < 2 ^ 64" using assms by simp
|
||||
hence h: "unat (a * 65536) = unat a * 65536"
|
||||
using unat_mult_lem[of a "65536::q48"] by simp
|
||||
show ?thesis
|
||||
unfolding q48_mul_def Q48_ONE_def Q48_SCALE_def
|
||||
by (simp add: word_unat_eq_iff drop_bit_eq_div unat_div_distrib h)
|
||||
qed
|
||||
|
||||
(* q48_div: (a << 16) / b
|
||||
C: return ((__uint128_t)a << 16) / b;
|
||||
@@ -130,10 +161,21 @@ definition q48_div :: "q48 \<Rightarrow> q48 \<Rightarrow> q48" where
|
||||
lemma q48_div_zero_denom [simp]: "q48_div a 0 = 0"
|
||||
by (simp add: q48_div_def)
|
||||
|
||||
(* CORRECTED 2026-08-13: the original statement had no bound and is false
|
||||
as such -- push_bit 16 wraps mod 2^64, so e.g. a=2^48 gives push_bit 16 a
|
||||
= 0, so q48_div a Q48_ONE = 0 \<noteq> a. Added the same overflow-free bound
|
||||
used throughout this file. *)
|
||||
lemma q48_div_one:
|
||||
"q48_div a Q48_ONE = a"
|
||||
unfolding q48_div_def Q48_ONE_def Q48_SCALE_def
|
||||
by simp
|
||||
assumes "unat a < 2 ^ 48"
|
||||
shows "q48_div a Q48_ONE = a"
|
||||
proof -
|
||||
have "unat a * 65536 < 2 ^ 64" using assms by simp
|
||||
hence h: "unat (a * 65536) = unat a * 65536"
|
||||
using unat_mult_lem[of a "65536::q48"] by simp
|
||||
show ?thesis
|
||||
unfolding q48_div_def Q48_ONE_def Q48_SCALE_def
|
||||
by (simp add: word_unat_eq_iff push_bit_eq_mult unat_div_distrib h)
|
||||
qed
|
||||
|
||||
(* =========================================================================
|
||||
Section 4: Accuracy ratio in Q48.16 (used by Loop #4 / Loop #5)
|
||||
@@ -142,24 +184,27 @@ lemma q48_div_one:
|
||||
(* Prefetch accuracy: hits / total, represented in Q48.16.
|
||||
Arguments are natural numbers (counters); result is a 64 word. *)
|
||||
definition q48_accuracy :: "nat \<Rightarrow> nat \<Rightarrow> q48" where
|
||||
"q48_accuracy hits total =
|
||||
(if total = 0 then 0
|
||||
else word_of_nat ((hits * 65536) div total))"
|
||||
"q48_accuracy hits tot =
|
||||
(if tot = 0 then 0
|
||||
else word_of_nat ((hits * 65536) div tot))"
|
||||
|
||||
lemma q48_accuracy_zero_total [simp]: "q48_accuracy hits 0 = 0"
|
||||
by (simp add: q48_accuracy_def)
|
||||
|
||||
lemma q48_accuracy_upper_bound:
|
||||
assumes "hits \<le> total"
|
||||
shows "unat (q48_accuracy hits total) \<le> 65536"
|
||||
proof (cases "total = 0")
|
||||
assumes "hits \<le> tot"
|
||||
shows "unat (q48_accuracy hits tot) \<le> 65536"
|
||||
proof (cases "tot = 0")
|
||||
case True thus ?thesis by simp
|
||||
next
|
||||
case False
|
||||
have "(hits * 65536) div total \<le> 65536"
|
||||
using assms False by (simp add: div_le_iff_le_mult)
|
||||
have "(hits * 65536) div tot \<le> (tot * 65536) div tot"
|
||||
using assms by (intro div_le_mono) simp
|
||||
also have "\<dots> = 65536"
|
||||
using False by simp
|
||||
finally have "(hits * 65536) div tot \<le> 65536" .
|
||||
thus ?thesis
|
||||
by (simp add: q48_accuracy_def False unat_word_of_nat)
|
||||
by (simp add: q48_accuracy_def False unat_of_nat)
|
||||
qed
|
||||
|
||||
(* =========================================================================
|
||||
@@ -177,7 +222,15 @@ definition q48_frac_part :: "q48 \<Rightarrow> 64 word" where
|
||||
lemma q48_decompose:
|
||||
"push_bit 16 (q48_int_part q) + q48_frac_part q = q"
|
||||
unfolding q48_int_part_def q48_frac_part_def
|
||||
by (simp add: push_bit_drop_bit_and_not_mask_eq and_mask_eq_iff_shiftr_0
|
||||
bit_push_bit drop_bit_eq_div push_bit_eq_mult)
|
||||
proof -
|
||||
have disj: "push_bit 16 (drop_bit 16 q) AND (q AND mask 16) = 0"
|
||||
by (rule bit_word_eqI) (auto simp: bit_simps)
|
||||
have "push_bit 16 (drop_bit 16 q) + (q AND mask 16)
|
||||
= push_bit 16 (drop_bit 16 q) OR (q AND mask 16)"
|
||||
by (rule disjunctive_add_eq_or) (rule disj)
|
||||
also have "\<dots> = q"
|
||||
by (rule bit_word_eqI) (auto simp: bit_simps)
|
||||
finally show "push_bit 16 (drop_bit 16 q) + (q AND mask 16) = q" .
|
||||
qed
|
||||
|
||||
end
|
||||
|
||||
@@ -152,9 +152,9 @@ proof -
|
||||
have no_ds_full: "\<not> ds_full (forth_to_r vm)"
|
||||
using assms(3) by simp
|
||||
show "data_stack (forth_from_r (forth_to_r vm)) = data_stack vm"
|
||||
by (simp add: forth_from_r_def forth_to_r_def rs ds no_ds_full assms)
|
||||
using rs ds no_ds_full assms by (simp add: forth_from_r_def)
|
||||
show "return_stack (forth_from_r (forth_to_r vm)) = return_stack vm"
|
||||
by (simp add: forth_from_r_def forth_to_r_def rs ds no_ds_full assms)
|
||||
using rs ds no_ds_full assms by (simp add: forth_from_r_def)
|
||||
qed
|
||||
|
||||
(* >R then R@ preserves the return stack and pushes a copy to data stack. *)
|
||||
@@ -168,9 +168,9 @@ proof -
|
||||
have rs: "return_stack (forth_to_r vm) = x # return_stack vm"
|
||||
by (simp add: forth_to_r_def assms)
|
||||
show "hd (data_stack (forth_r_fetch (forth_to_r vm))) = x"
|
||||
by (simp add: forth_r_fetch_def forth_to_r_def rs assms)
|
||||
using rs assms by (simp add: forth_r_fetch_def)
|
||||
show "return_stack (forth_r_fetch (forth_to_r vm)) = x # return_stack vm"
|
||||
by (simp add: forth_r_fetch_def forth_to_r_def rs assms)
|
||||
using rs assms by (simp add: forth_r_fetch_def)
|
||||
qed
|
||||
|
||||
end
|
||||
|
||||
@@ -343,7 +343,7 @@ lemma pick_normal:
|
||||
assumes "n \<ge> 0"
|
||||
assumes "nat n < length (data_stack vm)"
|
||||
shows "data_stack (forth_pick vm) = data_stack vm ! nat n # xs"
|
||||
by (simp add: forth_pick_def assms)
|
||||
using assms by (auto simp: forth_pick_def)
|
||||
|
||||
lemma pick_depth_unchanged:
|
||||
assumes "data_stack vm = n # xs"
|
||||
@@ -380,7 +380,7 @@ lemma pick_bounds_high:
|
||||
assumes "data_stack vm = n # xs"
|
||||
assumes "nat n \<ge> length (data_stack vm)"
|
||||
shows "vm_error (forth_pick vm)"
|
||||
by (simp add: forth_pick_def set_error_def assms)
|
||||
using assms by (auto simp: forth_pick_def set_error_def)
|
||||
|
||||
(* ── ROLL ( +n -- ) ─────────────────────────────────────────────────────── *)
|
||||
(* Pops n, then rotates items.
|
||||
@@ -407,8 +407,8 @@ definition forth_roll :: "vm_state \<Rightarrow> vm_state" where
|
||||
then set_error vm
|
||||
else if n = 0 \<or> n = 1
|
||||
then vm\<lparr>data_stack := xs\<rparr>
|
||||
else let i = nat n
|
||||
item = xs ! (i - 1)
|
||||
else let i = nat n;
|
||||
item = xs ! (i - 1);
|
||||
rest = take (i - 1) xs @ drop i xs
|
||||
in vm\<lparr>data_stack := item # rest\<rparr>)"
|
||||
|
||||
@@ -417,16 +417,37 @@ lemma roll_zero_nop:
|
||||
shows "data_stack (forth_roll vm) = xs"
|
||||
by (simp add: forth_roll_def assms)
|
||||
|
||||
(* CORRECTED 2026-08-13: added the missing "xs non-empty" hypothesis. For
|
||||
n=1 with xs=[], forth_roll_def's own guard (nat n > length xs, i.e.
|
||||
1 > 0) fires BEFORE the n=0\<or>n=1 shortcut is reached, giving set_error
|
||||
instead of the identity -- so the claim is false for xs=[]. *)
|
||||
lemma roll_one_nop:
|
||||
assumes "data_stack vm = 1 # xs"
|
||||
assumes "xs \<noteq> []"
|
||||
shows "data_stack (forth_roll vm) = xs"
|
||||
by (simp add: forth_roll_def assms)
|
||||
using assms by (auto simp: forth_roll_def)
|
||||
|
||||
(* 2 ROLL is equivalent to ROT (bring third item to top). *)
|
||||
(* FLAGGED, NOT FIXED 2026-08-13: this lemma does not hold against
|
||||
forth_roll_def as currently written. Tracing the definition by hand for
|
||||
this exact instantiation (xs = n3#n2#n1#rest after popping the leading
|
||||
2) gives item = xs!(i-1) = xs!1 = n2, rest' = take 1 xs @ drop 2 xs =
|
||||
n3#n1#rest, so forth_roll actually produces n2#n3#n1#rest -- not
|
||||
n1#n3#n2#rest as this lemma (and its own "2 ROLL is equivalent to ROT"
|
||||
comment) claims. Separately, the real C stack_word_roll
|
||||
(src/word_source/stack_words.c:287-320) uses yet a THIRD convention of
|
||||
its own, explicitly commented "1-indexed from bottom: n=1 moves bottom
|
||||
item to top" -- neither this definition nor this lemma's expectation
|
||||
matches it. Three mutually inconsistent conventions (this definition,
|
||||
this lemma, and the C code) -- not a proof-script issue, a genuine
|
||||
unresolved semantic question about what ROLL is supposed to do. This
|
||||
theory's own header asserts the theory is ground truth and the C code
|
||||
must match it, but the theory does not even agree with itself here, so
|
||||
that framing does not resolve which side (if either) is correct.
|
||||
Left failing rather than silently reconciled either direction. *)
|
||||
lemma roll_two_is_rot:
|
||||
assumes "data_stack vm = 2 # n3 # n2 # n1 # rest"
|
||||
shows "data_stack (forth_roll vm) = n1 # n3 # n2 # rest"
|
||||
by (simp add: forth_roll_def assms)
|
||||
oops
|
||||
|
||||
lemma roll_underflow:
|
||||
assumes "data_stack vm = []"
|
||||
|
||||
@@ -49,12 +49,16 @@ type_synonym event = "thread \<times> action"
|
||||
well-defined endomorphism.
|
||||
======================================================================== *)
|
||||
|
||||
(* word_table dropped from exec_equiv 2026-08-13: it is no longer a
|
||||
vm_state field (StarForth_Base.thy fixed the vm_state self-reference by
|
||||
making word_table a free-standing global constant), so "word_table s1 =
|
||||
word_table s2" no longer type-checks -- and would have been vacuously
|
||||
true anyway, since a global constant cannot differ between s1 and s2. *)
|
||||
definition exec_equiv :: "vm_state \<Rightarrow> vm_state \<Rightarrow> bool" (infix "\<simeq>" 50) where
|
||||
"s1 \<simeq> s2 \<longleftrightarrow>
|
||||
data_stack s1 = data_stack s2 \<and>
|
||||
return_stack s1 = return_stack s2 \<and>
|
||||
memory s1 = memory s2 \<and>
|
||||
word_table s1 = word_table s2"
|
||||
memory s1 = memory s2"
|
||||
|
||||
lemma exec_equiv_refl [simp, intro]: "vm \<simeq> vm"
|
||||
by (simp add: exec_equiv_def)
|
||||
@@ -68,7 +72,8 @@ lemma exec_equiv_trans: "s1 \<simeq> s2 \<Longrightarrow> s2 \<simeq> s3 \<Longr
|
||||
lemma exec_equiv_ds: "s1 \<simeq> s2 \<Longrightarrow> data_stack s1 = data_stack s2" by (simp add: exec_equiv_def)
|
||||
lemma exec_equiv_rs: "s1 \<simeq> s2 \<Longrightarrow> return_stack s1 = return_stack s2" by (simp add: exec_equiv_def)
|
||||
lemma exec_equiv_mem:"s1 \<simeq> s2 \<Longrightarrow> memory s1 = memory s2" by (simp add: exec_equiv_def)
|
||||
lemma exec_equiv_wt: "s1 \<simeq> s2 \<Longrightarrow> word_table s1 = word_table s2" by (simp add: exec_equiv_def)
|
||||
(* exec_equiv_wt removed 2026-08-13: word_table is global now, not read
|
||||
from state, so this fact no longer type-checks and is not needed. *)
|
||||
|
||||
(* =========================================================================
|
||||
Section 3: Heartbeat axiom — A1 ×1 (collapsed from ×8)
|
||||
@@ -87,12 +92,14 @@ lemma exec_equiv_wt: "s1 \<simeq> s2 \<Longrightarrow> word_table s1 = word_ta
|
||||
Read every code path reachable from vm_tick() — including
|
||||
vm_tick_window_tuner, vm_tick_slope_validator, and all
|
||||
inference_engine.c callees — and verify that NONE of those paths write
|
||||
to the following four fields:
|
||||
to the following three fields:
|
||||
data_stack (vm->data_stack / vm->ds_top)
|
||||
return_stack (vm->return_stack / vm->rs_top)
|
||||
memory (vm->memory[])
|
||||
word_table (vm->word_table)
|
||||
Those four fields are exactly exec_equiv. Everything else is free.
|
||||
Those three fields are exactly exec_equiv. word_table is no longer
|
||||
among them (2026-08-13: it is a free-standing global constant, not a
|
||||
vm_state field, so it cannot be written by any vm_tick() path at all).
|
||||
Everything else is free.
|
||||
|
||||
○ CODE-MUST-MATCH: if a future refactor moves any of those four fields into
|
||||
the heartbeat's write set, exec_equiv must be updated and a new audit
|
||||
@@ -118,77 +125,100 @@ lemma heartbeat_rs [simp]: "return_stack (heartbeat_step vm) = return_stack vm"
|
||||
lemma heartbeat_mem [simp]: "memory (heartbeat_step vm) = memory vm"
|
||||
using heartbeat_exec_neutral by (simp add: exec_equiv_def)
|
||||
|
||||
lemma heartbeat_wt [simp]: "word_table (heartbeat_step vm) = word_table vm"
|
||||
using heartbeat_exec_neutral by (simp add: exec_equiv_def)
|
||||
(* heartbeat_wt removed 2026-08-13: word_table no longer varies by state. *)
|
||||
|
||||
(* =========================================================================
|
||||
Section 5: n-fold heartbeat exec-neutrality and field preservation
|
||||
======================================================================== *)
|
||||
|
||||
lemma heartbeat_n_exec_neutral: "heartbeat_step ^^ n $ vm \<simeq> vm"
|
||||
lemma heartbeat_n_exec_neutral: "(heartbeat_step ^^ n) vm \<simeq> vm"
|
||||
proof (induction n)
|
||||
case 0 show ?case by simp
|
||||
next
|
||||
case (Suc k)
|
||||
show "heartbeat_step ^^ Suc k $ vm \<simeq> vm"
|
||||
show "(heartbeat_step ^^ Suc k) vm \<simeq> vm"
|
||||
using exec_equiv_trans [OF heartbeat_exec_neutral Suc.IH] by simp
|
||||
qed
|
||||
|
||||
lemma heartbeat_n_steps_ds [simp]: "data_stack (heartbeat_step ^^ n $ vm) = data_stack vm"
|
||||
lemma heartbeat_n_steps_ds [simp]: "data_stack ((heartbeat_step ^^ n) vm) = data_stack vm"
|
||||
using heartbeat_n_exec_neutral by (simp add: exec_equiv_def)
|
||||
|
||||
lemma heartbeat_n_steps_rs [simp]: "return_stack (heartbeat_step ^^ n $ vm) = return_stack vm"
|
||||
lemma heartbeat_n_steps_rs [simp]: "return_stack ((heartbeat_step ^^ n) vm) = return_stack vm"
|
||||
using heartbeat_n_exec_neutral by (simp add: exec_equiv_def)
|
||||
|
||||
lemma heartbeat_n_steps_mem [simp]: "memory (heartbeat_step ^^ n $ vm) = memory vm"
|
||||
lemma heartbeat_n_steps_mem [simp]: "memory ((heartbeat_step ^^ n) vm) = memory vm"
|
||||
using heartbeat_n_exec_neutral by (simp add: exec_equiv_def)
|
||||
|
||||
lemma heartbeat_n_steps_wt [simp]: "word_table (heartbeat_step ^^ n $ vm) = word_table vm"
|
||||
using heartbeat_n_exec_neutral by (simp add: exec_equiv_def)
|
||||
(* heartbeat_n_steps_wt removed 2026-08-13: word_table no longer varies by
|
||||
state -- see the note at heartbeat_wt above. *)
|
||||
|
||||
(* =========================================================================
|
||||
Section 6: Word physics transparency — A4' ×1 (congruence form)
|
||||
|
||||
Word execution is a well-defined endomorphism on the exec quotient: if two
|
||||
states are exec-equivalent, executing any word on each produces identical
|
||||
results. This is the congruence law that makes word sequences independent
|
||||
of interleaved heartbeat ticks.
|
||||
states are exec-equivalent, executing any word on each produces
|
||||
exec-equivalent results. This is the congruence law that makes word
|
||||
sequences independent of interleaved heartbeat ticks.
|
||||
|
||||
CORRECTED 2026-08-13: the conclusion was full state equality
|
||||
("word_table n s1 = word_table n s2"), not \<simeq>-equivalence. That is
|
||||
provably too strong and was never true: two states agreeing only on the
|
||||
three exec_equiv fields can differ in any physics field (rolling_window,
|
||||
heartbeat, etc.), and a word that never reads or writes those physics
|
||||
fields leaves them exactly as it found them -- still different between
|
||||
the two output states. Concretely, this broke
|
||||
StarForth_Concurrent.thy's foldl_word_table_eq at the empty-list base
|
||||
case, which reduced to needing s1 = s2 from s1 \<simeq> s2 alone -- genuinely
|
||||
unprovable. The audit protocol below only ever justified the \<simeq> form:
|
||||
"the word body only reads the three exec_equiv fields" gives identical
|
||||
NEW data_stack/return_stack/memory (since those three inputs agree by
|
||||
\<simeq>), but says nothing about physics fields the word doesn't touch,
|
||||
which simply carry through from s1/s2 respectively and so can still
|
||||
differ. \<simeq> is exactly the right conclusion strength -- it is silent
|
||||
about physics fields, which is what the design has always wanted.
|
||||
|
||||
⚠ AUDIT PROTOCOL: for each word registered in word_table, verify its body
|
||||
only reads data_stack, return_stack, memory, word_table — the four fields
|
||||
of exec_equiv. These are exactly the fields a FORTH word may observe.
|
||||
only reads data_stack, return_stack, memory — the three fields of
|
||||
exec_equiv (word_table itself is no longer one of them since 2026-08-13;
|
||||
it is a fixed global, not part of state to read). These are exactly the
|
||||
fields a FORTH word may observe.
|
||||
|
||||
○ CODE-MUST-MATCH: no word in src/word_source/ may read rolling_window,
|
||||
heartbeat, decay_slope_q48, pipeline_metrics, last_inference, ssm_l8,
|
||||
tuning_lock, dict_lock, heat thresholds, or any other physics field.
|
||||
======================================================================== *)
|
||||
|
||||
(* word_table's arity dropped from 3 to 2 call-site arguments 2026-08-13:
|
||||
it used to be read from a specific state first (word_table s n s -- get
|
||||
s's own copy of the table, apply entry n to s), now it is one fixed
|
||||
global table (word_table n s -- apply entry n directly to s). The
|
||||
mathematical content of this axiom (word execution depends only on the
|
||||
exec-visible fields, not physics state) is unchanged. *)
|
||||
axiomatization where
|
||||
word_physics_transparent:
|
||||
"\<And> (s1 :: vm_state) (s2 :: vm_state) n.
|
||||
s1 \<simeq> s2 \<Longrightarrow> word_table s1 n s1 = word_table s2 n s2"
|
||||
s1 \<simeq> s2 \<Longrightarrow> word_table n s1 \<simeq> word_table n s2"
|
||||
|
||||
(* =========================================================================
|
||||
Section 7: Consequences — all proved from A1 + A4'
|
||||
======================================================================== *)
|
||||
|
||||
lemma exec_after_heartbeat_eq:
|
||||
"word_table (heartbeat_step vm) n (heartbeat_step vm) = word_table vm n vm"
|
||||
"word_table n (heartbeat_step vm) \<simeq> word_table n vm"
|
||||
by (rule word_physics_transparent [OF heartbeat_exec_neutral])
|
||||
|
||||
lemma exec_after_heartbeat_ds:
|
||||
"data_stack (word_table (heartbeat_step vm) n (heartbeat_step vm))
|
||||
= data_stack (word_table vm n vm)"
|
||||
using exec_after_heartbeat_eq by simp
|
||||
"data_stack (word_table n (heartbeat_step vm))
|
||||
= data_stack (word_table n vm)"
|
||||
using exec_after_heartbeat_eq exec_equiv_ds by blast
|
||||
|
||||
lemma exec_after_heartbeat_rs:
|
||||
"return_stack (word_table (heartbeat_step vm) n (heartbeat_step vm))
|
||||
= return_stack (word_table vm n vm)"
|
||||
using exec_after_heartbeat_eq by simp
|
||||
"return_stack (word_table n (heartbeat_step vm))
|
||||
= return_stack (word_table n vm)"
|
||||
using exec_after_heartbeat_eq exec_equiv_rs by blast
|
||||
|
||||
lemma exec_after_n_heartbeats_eq:
|
||||
"word_table (heartbeat_step ^^ k $ vm) n (heartbeat_step ^^ k $ vm)
|
||||
= word_table vm n vm"
|
||||
"word_table n ((heartbeat_step ^^ k) vm) \<simeq> word_table n vm"
|
||||
by (rule word_physics_transparent [OF heartbeat_n_exec_neutral])
|
||||
|
||||
(* =========================================================================
|
||||
@@ -200,7 +230,7 @@ inductive vm_step :: "vm_state \<Rightarrow> event \<Rightarrow> vm_state \<Righ
|
||||
where
|
||||
StepExec:
|
||||
"\<not> vm_error vm \<Longrightarrow> \<not> vm_halted vm \<Longrightarrow>
|
||||
vm' = word_table vm n vm \<Longrightarrow>
|
||||
vm' = word_table n vm \<Longrightarrow>
|
||||
vm \<rightarrow>[(ExecThread, ExecWord n)] vm'"
|
||||
|
||||
| StepHeartTick:
|
||||
|
||||
Reference in New Issue
Block a user