Robert Allan James
87cd422957
ROLL: forth_roll_def implemented a third, invented convention matching neither the theory's own test lemma nor the real C stack_word_roll(). Traced the actual C source (src/word_source/stack_words.c:287-320) and its passing tests (stack_words_test.c roll_1/roll_2) to the real semantics -- ROLL is 1-indexed from the BOTTOM of the stack, not top-indexed as the old definition assumed. Rewrote forth_roll_def to match, replaced the false roll_one_nop/roll_two_is_rot with lemmas verified against the actual test vectors. PICK: forth_pick_def indexed into the pre-pop stack (still containing the count n as its own head) instead of the post-pop stack, off by one position, plus a bound check one too permissive. Fixed against src/word_source/ stack_words.c:265-282 and its pick_0/pick_1/pick_2 test vectors. pm_wf: pm_record_hit_preserves_wf/pm_record_miss_preserves_wf were oops-flagged as a genuine invariant gap. Fixed with the minimal added hypothesis (pm_last_accuracy_den pm > 0), matching this session's established discipline. Also documents a deeper finding: pm_last_accuracy_num/den don't correspond to any field in the real PipelineGlobalMetrics C struct (which has a single "double last_checked_accuracy", not a fraction) -- flagged for a separate field-level audit, not attempted here. All 23 theory files verify with zero errors.
195 lines
8.8 KiB
Plaintext
195 lines
8.8 KiB
Plaintext
theory StarForth_Loop4_Pipeline
|
|
imports StarForth_Q48_16 StarForth_Base
|
|
begin
|
|
|
|
(* =========================================================================
|
|
StarForth_Loop4_Pipeline — Prefetch / Pipelining Metrics (Physics Loop #4)
|
|
|
|
Mirrors: src/physics_pipelining_metrics.c
|
|
include/physics_pipelining_metrics.h
|
|
|
|
The pipelining subsystem maintains word-to-word transition probabilities
|
|
(per-word wt_transition_heat arrays) and global pipeline_metrics. On
|
|
every word execution, the most-likely next word is pre-fetched from the
|
|
dictionary; the prefetch is scored as a hit or miss.
|
|
|
|
This theory proves:
|
|
• Prefetch accuracy (hits / (hits + misses)) ∈ [0, 1] as a Q48.16 value.
|
|
• Transition recording increments the correct counter and preserves totals.
|
|
• Global pipeline_metrics totals are consistent with per-step deltas.
|
|
======================================================================== *)
|
|
|
|
(* =========================================================================
|
|
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 * 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> 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 * 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:
|
|
"pm_accuracy_q48 pm \<ge> 0"
|
|
by simp
|
|
|
|
(* =========================================================================
|
|
Section 2: Pipeline metrics well-formedness
|
|
======================================================================== *)
|
|
|
|
definition pm_wf :: "pipeline_metrics_state \<Rightarrow> bool" where
|
|
"pm_wf pm \<longleftrightarrow>
|
|
pm_prefetch_hits pm \<le> pm_prefetch_attempts pm \<and>
|
|
(pm_prefetch_attempts pm = 0 \<longrightarrow>
|
|
pm_last_accuracy_num pm = 0) \<and>
|
|
(pm_prefetch_attempts pm > 0 \<longrightarrow>
|
|
pm_last_accuracy_den pm > 0)"
|
|
|
|
lemma pm_wf_accuracy_range:
|
|
assumes "pm_wf pm"
|
|
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
|
|
======================================================================== *)
|
|
|
|
definition pm_record_hit :: "pipeline_metrics_state \<Rightarrow> pipeline_metrics_state" where
|
|
"pm_record_hit pm =
|
|
pm\<lparr>pm_prefetch_attempts := pm_prefetch_attempts pm + 1,
|
|
pm_prefetch_hits := pm_prefetch_hits pm + 1\<rparr>"
|
|
|
|
definition pm_record_miss :: "pipeline_metrics_state \<Rightarrow> pipeline_metrics_state" where
|
|
"pm_record_miss pm =
|
|
pm\<lparr>pm_prefetch_attempts := pm_prefetch_attempts pm + 1\<rparr>"
|
|
|
|
lemma pm_record_hit_attempts:
|
|
"pm_prefetch_attempts (pm_record_hit pm) = pm_prefetch_attempts pm + 1"
|
|
by (simp add: pm_record_hit_def)
|
|
|
|
lemma pm_record_hit_hits:
|
|
"pm_prefetch_hits (pm_record_hit pm) = pm_prefetch_hits pm + 1"
|
|
by (simp add: pm_record_hit_def)
|
|
|
|
lemma pm_record_miss_attempts:
|
|
"pm_prefetch_attempts (pm_record_miss pm) = pm_prefetch_attempts pm + 1"
|
|
by (simp add: pm_record_miss_def)
|
|
|
|
lemma pm_record_miss_hits_unchanged:
|
|
"pm_prefetch_hits (pm_record_miss pm) = pm_prefetch_hits pm"
|
|
by (simp add: pm_record_miss_def)
|
|
|
|
(* CORRECTED 2026-08-13, in two parts.
|
|
(1) The narrower gap first flagged: pm_wf only requires
|
|
"pm_last_accuracy_den pm > 0" when pm_prefetch_attempts pm > 0 -- when
|
|
attempts = 0, den is 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 the precondition never guaranteed it. Fixed with the minimal,
|
|
honest addition: assume "pm_last_accuracy_den pm > 0" directly, same
|
|
discipline as every other missing-hypothesis fix this session (added,
|
|
not silently invented into pm_wf's own definition, which is a design
|
|
decision for Captain Bob, not a mechanical fix).
|
|
(2) A deeper finding surfaced while chasing this: pm_last_accuracy_num
|
|
and pm_last_accuracy_den do not correspond to anything in the real C
|
|
struct. include/vm.h's PipelineGlobalMetrics has a single
|
|
"double last_checked_accuracy" field (confirmed via
|
|
src/vm_bootstrap.c:290-295 and src/vm_time.c:412-413,627-628) -- there
|
|
is no num/den fraction pair anywhere in the real struct. This theory's
|
|
pipeline_metrics_state record (StarForth_Base.thy) modeled accuracy as
|
|
a fraction that was never audited against the actual C fields it
|
|
claims to mirror. Not re-audited or corrected here -- a full field-level
|
|
pass over pipeline_metrics_state is its own separate task, flagged for
|
|
later, not attempted as a side effect of this fix. *)
|
|
lemma pm_record_hit_preserves_wf:
|
|
assumes "pm_wf pm"
|
|
assumes "pm_last_accuracy_den pm > 0"
|
|
shows "pm_wf (pm_record_hit pm)"
|
|
using assms by (simp add: pm_wf_def pm_record_hit_def)
|
|
|
|
lemma pm_record_miss_preserves_wf:
|
|
assumes "pm_wf pm"
|
|
assumes "pm_last_accuracy_den pm > 0"
|
|
shows "pm_wf (pm_record_miss pm)"
|
|
using assms by (simp add: pm_wf_def pm_record_miss_def)
|
|
|
|
(* After a hit, hits ≤ attempts still holds. *)
|
|
lemma pm_record_hit_hits_le_attempts:
|
|
assumes "pm_prefetch_hits pm \<le> pm_prefetch_attempts pm"
|
|
shows "pm_prefetch_hits (pm_record_hit pm) \<le> pm_prefetch_attempts (pm_record_hit pm)"
|
|
using assms by (simp add: pm_record_hit_def)
|
|
|
|
(* After a miss, hits ≤ attempts still holds. *)
|
|
lemma pm_record_miss_hits_le_attempts:
|
|
assumes "pm_prefetch_hits pm \<le> pm_prefetch_attempts pm"
|
|
shows "pm_prefetch_hits (pm_record_miss pm) \<le> pm_prefetch_attempts (pm_record_miss pm)"
|
|
using assms by (simp add: pm_record_miss_def)
|
|
|
|
(* =========================================================================
|
|
Section 4: Word transition metrics (per-word hot-path transition table)
|
|
======================================================================== *)
|
|
|
|
(* Record a transition from the current context to word_id next. *)
|
|
definition wt_record_transition :: "nat \<Rightarrow> word_transition_metrics \<Rightarrow> word_transition_metrics" where
|
|
"wt_record_transition next wt =
|
|
wt\<lparr>wt_transition_heat :=
|
|
(wt_transition_heat wt)(next := wt_transition_heat wt next + 1),
|
|
wt_total_transitions := wt_total_transitions wt + 1\<rparr>"
|
|
|
|
lemma wt_transition_heat_updated:
|
|
"wt_transition_heat (wt_record_transition n wt) n = wt_transition_heat wt n + 1"
|
|
by (simp add: wt_record_transition_def)
|
|
|
|
lemma wt_transition_heat_other_unchanged:
|
|
assumes "m \<noteq> n"
|
|
shows "wt_transition_heat (wt_record_transition n wt) m = wt_transition_heat wt m"
|
|
by (simp add: wt_record_transition_def assms)
|
|
|
|
lemma wt_total_transitions_increases:
|
|
"wt_total_transitions (wt_record_transition n wt) = wt_total_transitions wt + 1"
|
|
by (simp add: wt_record_transition_def)
|
|
|
|
(* =========================================================================
|
|
Section 5: Pipeline fields are preserved by pure data-stack word execution
|
|
======================================================================== *)
|
|
|
|
lemma ds_word_preserves_pipeline:
|
|
"pipeline_metrics (vm\<lparr>data_stack := xs\<rparr>) = pipeline_metrics vm"
|
|
by simp
|
|
|
|
end
|