proof/: add StarForth_Inference_Words.thy (inference_words.c coverage)
Completes the src/word_source/*.c sweep -- last of the 5 kernel-only files. Five INFER-*@ output accessors fully modelled: they read straight from vm->last_inference_outputs, which is exactly the already-modelled `last_inference :: inference_outputs_state option` field with matching per-field names. Q.VARIANCE/INFER-DECAY-SLOPE/INFER-WINDOW-WIDTH get guard/shape only, capturing a genuine finding: array_ptr sets vm->error AND the caller still pushes a 0 placeholder regardless, unlike the "error or push, never both" shape most guarded words in this sweep follow. L8-UPDATE/L8-TABLE-FORCE get pop-shape only. Second finding: L8-MODE/L8-UPDATE/L8-APPLY/L8-TABLE-FORCE manipulate vm->ssm_l8_state (a legacy 16-mode struct) and, per L8-TABLE-FORCE's own comment, a separate 128-config adaptive table the heartbeat's bandit actually drives -- NEITHER is the `ssm_l8 :: ssm_l8_state` (4-mode C0..C3) field this proof suite has modelled since early in the sweep. Three L8 representations exist in the real system; none of this file's words touch the one the model tracks. Flagged as an open question, not guessed at. WINDOW-DIVERSITY, INFER-RUN, L8-MODE, L8-APPLY, and the six BAYES-* words deferred (unmodelled subsystems: rolling-window diversity algorithm, the whole inference-engine run, legacy L8 state, hot-words cache Bayesian posteriors). Suite now 53 theories, green.
This commit is contained in:
Robert Allan James
@@ -37,6 +37,7 @@ session "StarForth" = "HOL-Library" +
|
||||
StarForth_Defer_Words
|
||||
StarForth_Log_Words
|
||||
StarForth_Q48_Words
|
||||
StarForth_Inference_Words
|
||||
StarForth_Loop1_Heat
|
||||
StarForth_Loop2_Window
|
||||
StarForth_Loop3_Decay
|
||||
|
||||
@@ -0,0 +1,252 @@
|
||||
theory StarForth_Inference_Words
|
||||
imports StarForth_Base
|
||||
begin
|
||||
|
||||
(* =========================================================================
|
||||
Mirrors: src/word_source/inference_words.c
|
||||
Registers: Q.VARIANCE INFER-DECAY-SLOPE INFER-WINDOW-WIDTH
|
||||
WINDOW-DIVERSITY INFER-RUN INFER-WINDOW@ INFER-DECAY@
|
||||
INFER-VARIANCE@ INFER-FIT@ INFER-EARLY-EXIT@ L8-MODE
|
||||
L8-UPDATE L8-APPLY L8-TABLE-FORCE BAYES-CACHE-MEAN/LOWER/UPPER
|
||||
BAYES-BUCKET-MEAN/LOWER/UPPER
|
||||
|
||||
── Scope ─────────────────────────────────────────────────────────────
|
||||
Fully modelled: the five INFER-*@ output accessors, which read straight
|
||||
from `vm->last_inference_outputs` -- exactly `last_inference ::
|
||||
inference_outputs_state option` in vm_state (StarForth_Base.thy),
|
||||
already modelled with matching field names for every value these words
|
||||
read.
|
||||
|
||||
Guard/shape only: Q.VARIANCE, INFER-DECAY-SLOPE, INFER-WINDOW-WIDTH
|
||||
(pop 2, bounds-check the array reference) -- and a genuine finding
|
||||
about that bounds check, see below. L8-UPDATE, L8-TABLE-FORCE (pop
|
||||
shape only; computed/target-subsystem effect not modelled).
|
||||
|
||||
Not modelled: WINDOW-DIVERSITY, L8-MODE, L8-APPLY, the six
|
||||
BAYES-CACHE-*/BAYES-BUCKET-* words, and INFER-RUN. See per-word notes.
|
||||
|
||||
── Finding: array_ptr sets vm->error but the caller pushes anyway ──────
|
||||
`array_ptr` (line 74) sets `vm->error = 1` AND returns NULL on any
|
||||
bounds failure. All three of its callers (Q.VARIANCE/INFER-DECAY-SLOPE/
|
||||
INFER-WINDOW-WIDTH) check only the returned pointer, not `vm->error`,
|
||||
before pushing a 0 placeholder -- so on an invalid array reference the
|
||||
word both sets the error flag AND pushes a value, unlike the "error OR
|
||||
push, never both" shape virtually every other guarded word in this
|
||||
sweep follows. Modelled faithfully: the error and the push both happen.
|
||||
|
||||
── Finding: L8-MODE reads a DIFFERENT L8 representation than vm_state
|
||||
models ──────────────────────────────────────────────────────────
|
||||
`vm->ssm_l8_state` (cast from `void*` to `ssm_l8_state_t*`) is NOT the
|
||||
same field as `ssm_l8 :: ssm_l8_state` already in vm_state
|
||||
(StarForth_Base.thy, used by StarForth_Concurrent.thy/StarForth_
|
||||
Transition.thy) -- that abstract record models a 4-mode `ssm_mode`
|
||||
datatype (`C0`/`C1`/`C2`/`C3`), whereas this file's `current_mode` is
|
||||
documented as a legacy 16-mode int (`L8-MODE` pushes `0-15`), and
|
||||
`L8-TABLE-FORCE`'s own comment additionally describes a THIRD,
|
||||
currently-live representation: a 128-config adaptive table the
|
||||
heartbeat's bandit selection actually drives, which the legacy 16-mode
|
||||
`L8-UPDATE`/`L8-APPLY` path is explicitly said to be overwritten by.
|
||||
So there are (at least) three L8 representations in play across the
|
||||
real system -- the abstract model's 4-mode `ssm_l8`, this file's
|
||||
legacy 16-mode `ssm_l8_state_t`, and the 128-config adaptive table --
|
||||
and none of this file's L8 words touch the one `ssm_l8` field this
|
||||
proof suite actually models. Not modelled as a result; flagged as an
|
||||
open question about which representation `ssm_l8` was originally meant
|
||||
to track, worth raising directly rather than guessing.
|
||||
======================================================================== *)
|
||||
|
||||
(* ── INFER-WINDOW@ / INFER-DECAY@ / INFER-VARIANCE@ / INFER-FIT@ /
|
||||
INFER-EARLY-EXIT@ ( -- n|q|flag ) : read last_inference, 0 if None ──── *)
|
||||
|
||||
definition forth_infer_window_fetch :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_infer_window_fetch vm =
|
||||
vm\<lparr>data_stack :=
|
||||
word_of_nat (case last_inference vm of None \<Rightarrow> 0 | Some io \<Rightarrow> io_adaptive_window_width io)
|
||||
# data_stack vm\<rparr>"
|
||||
|
||||
definition forth_infer_decay_fetch :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_infer_decay_fetch vm =
|
||||
vm\<lparr>data_stack :=
|
||||
word_of_nat (case last_inference vm of None \<Rightarrow> 0 | Some io \<Rightarrow> io_adaptive_decay_slope io)
|
||||
# data_stack vm\<rparr>"
|
||||
|
||||
definition forth_infer_variance_fetch :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_infer_variance_fetch vm =
|
||||
vm\<lparr>data_stack :=
|
||||
word_of_nat (case last_inference vm of None \<Rightarrow> 0 | Some io \<Rightarrow> io_window_variance_q48 io)
|
||||
# data_stack vm\<rparr>"
|
||||
|
||||
definition forth_infer_fit_fetch :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_infer_fit_fetch vm =
|
||||
vm\<lparr>data_stack :=
|
||||
word_of_nat (case last_inference vm of None \<Rightarrow> 0 | Some io \<Rightarrow> io_fit_quality_q48 io)
|
||||
# data_stack vm\<rparr>"
|
||||
|
||||
definition forth_infer_early_exit_fetch :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_infer_early_exit_fetch vm =
|
||||
vm\<lparr>data_stack :=
|
||||
to_forth_bool (case last_inference vm of None \<Rightarrow> False | Some io \<Rightarrow> io_early_exited io)
|
||||
# data_stack vm\<rparr>"
|
||||
|
||||
lemma infer_window_fetch_none:
|
||||
assumes "last_inference vm = None"
|
||||
shows "data_stack (forth_infer_window_fetch vm) = 0 # data_stack vm"
|
||||
using assms by (simp add: forth_infer_window_fetch_def)
|
||||
|
||||
lemma infer_window_fetch_some:
|
||||
assumes "last_inference vm = Some io"
|
||||
shows "data_stack (forth_infer_window_fetch vm) = word_of_nat (io_adaptive_window_width io) # data_stack vm"
|
||||
using assms by (simp add: forth_infer_window_fetch_def)
|
||||
|
||||
lemma infer_decay_fetch_none:
|
||||
assumes "last_inference vm = None"
|
||||
shows "data_stack (forth_infer_decay_fetch vm) = 0 # data_stack vm"
|
||||
using assms by (simp add: forth_infer_decay_fetch_def)
|
||||
|
||||
lemma infer_decay_fetch_some:
|
||||
assumes "last_inference vm = Some io"
|
||||
shows "data_stack (forth_infer_decay_fetch vm) = word_of_nat (io_adaptive_decay_slope io) # data_stack vm"
|
||||
using assms by (simp add: forth_infer_decay_fetch_def)
|
||||
|
||||
lemma infer_variance_fetch_none:
|
||||
assumes "last_inference vm = None"
|
||||
shows "data_stack (forth_infer_variance_fetch vm) = 0 # data_stack vm"
|
||||
using assms by (simp add: forth_infer_variance_fetch_def)
|
||||
|
||||
lemma infer_variance_fetch_some:
|
||||
assumes "last_inference vm = Some io"
|
||||
shows "data_stack (forth_infer_variance_fetch vm) = word_of_nat (io_window_variance_q48 io) # data_stack vm"
|
||||
using assms by (simp add: forth_infer_variance_fetch_def)
|
||||
|
||||
lemma infer_fit_fetch_none:
|
||||
assumes "last_inference vm = None"
|
||||
shows "data_stack (forth_infer_fit_fetch vm) = 0 # data_stack vm"
|
||||
using assms by (simp add: forth_infer_fit_fetch_def)
|
||||
|
||||
lemma infer_fit_fetch_some:
|
||||
assumes "last_inference vm = Some io"
|
||||
shows "data_stack (forth_infer_fit_fetch vm) = word_of_nat (io_fit_quality_q48 io) # data_stack vm"
|
||||
using assms by (simp add: forth_infer_fit_fetch_def)
|
||||
|
||||
lemma infer_early_exit_fetch_none:
|
||||
assumes "last_inference vm = None"
|
||||
shows "data_stack (forth_infer_early_exit_fetch vm) = 0 # data_stack vm"
|
||||
using assms by (simp add: forth_infer_early_exit_fetch_def)
|
||||
|
||||
lemma infer_early_exit_fetch_some_true:
|
||||
assumes "last_inference vm = Some io" "io_early_exited io"
|
||||
shows "data_stack (forth_infer_early_exit_fetch vm) = -1 # data_stack vm"
|
||||
using assms by (simp add: forth_infer_early_exit_fetch_def)
|
||||
|
||||
lemma infer_early_exit_fetch_some_false:
|
||||
assumes "last_inference vm = Some io" "\<not> io_early_exited io"
|
||||
shows "data_stack (forth_infer_early_exit_fetch vm) = 0 # data_stack vm"
|
||||
using assms by (simp add: forth_infer_early_exit_fetch_def)
|
||||
|
||||
lemma infer_fetch_words_no_overflow_guard: True
|
||||
\<comment> \<open>All five push unconditionally, no ds_full check -- another instance
|
||||
of the recurring missing-overflow-guard pattern.\<close>
|
||||
by simp
|
||||
|
||||
(* ── Q.VARIANCE / INFER-DECAY-SLOPE / INFER-WINDOW-WIDTH
|
||||
( addr u -- q|n ) : guard/pop2 shape + the error-and-push quirk ──────── *)
|
||||
(* C: no upfront dsp guard -- relies on VM_POP itself (see StarForth_Q48_
|
||||
Words.thy's build-flag stack-safety finding, same VM_POP/VM_PUSH macro
|
||||
usage here). Pops u then addr; array_ptr validates and, on failure,
|
||||
sets vm->error AND returns NULL, after which the caller pushes 0
|
||||
regardless of the error flag (see file header finding). Modelled here
|
||||
assuming the underlying pop always succeeds (i.e. at least 2 elements
|
||||
present, matching this suite's usual convention of not re-deriving the
|
||||
VM_POP/vm_pop underflow case per word); the array-bounds branch is
|
||||
modelled precisely since it's this word's own logic, not a macro. *)
|
||||
|
||||
definition forth_q_variance_guard :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_q_variance_guard vm =
|
||||
(case data_stack vm of
|
||||
u # addr # xs \<Rightarrow>
|
||||
(if u \<le>s 0 \<or> unat addr \<ge> VM_MEMORY_SIZE \<or> unat addr + unat u * 8 > VM_MEMORY_SIZE
|
||||
then set_error (vm\<lparr>data_stack := 0 # xs\<rparr>)
|
||||
else vm\<lparr>data_stack := xs\<rparr>)
|
||||
| _ \<Rightarrow> set_error vm)"
|
||||
|
||||
lemma q_variance_invalid_array_errors_and_pushes_zero:
|
||||
assumes "data_stack vm = u # addr # xs"
|
||||
assumes "u \<le>s 0 \<or> unat addr \<ge> VM_MEMORY_SIZE \<or> unat addr + unat u * 8 > VM_MEMORY_SIZE"
|
||||
shows "vm_error (forth_q_variance_guard vm)"
|
||||
and "data_stack (forth_q_variance_guard vm) = 0 # xs"
|
||||
using assms by (simp_all add: forth_q_variance_guard_def set_error_def)
|
||||
|
||||
lemma q_variance_valid_array_pops_only:
|
||||
assumes "data_stack vm = u # addr # xs"
|
||||
assumes "\<not> (u \<le>s 0 \<or> unat addr \<ge> VM_MEMORY_SIZE \<or> unat addr + unat u * 8 > VM_MEMORY_SIZE)"
|
||||
shows "data_stack (forth_q_variance_guard vm) = xs"
|
||||
using assms by (simp add: forth_q_variance_guard_def)
|
||||
|
||||
lemma q_variance_result_value_not_modelled: True
|
||||
\<comment> \<open>compute_variance_q48 -- a real variance computation over raw VM
|
||||
memory, not modelled. INFER-DECAY-SLOPE/INFER-WINDOW-WIDTH share this
|
||||
exact guard shape (infer_decay_slope_q48/find_variance_inflection
|
||||
also not modelled) -- one shared guard definition covers all three,
|
||||
matching the file's own `array_ptr` helper being shared.\<close>
|
||||
by simp
|
||||
|
||||
(* ── L8-UPDATE ( entropy cv temporal stability -- ) : pop4 shape only ───── *)
|
||||
(* C: no dsp guard at all; if `l8` is NULL, pops all four anyway (four
|
||||
bare VM_POP calls) and returns; if non-NULL, pops all four via
|
||||
q48_pop_inf (same VM_POP) and calls ssm_l8_update -- either way,
|
||||
exactly four elements are popped whenever the stack has \<ge> 4. *)
|
||||
|
||||
definition forth_l8_update_guard :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_l8_update_guard vm =
|
||||
(case data_stack vm of
|
||||
a # b # c # d # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>
|
||||
| _ \<Rightarrow> set_error vm)"
|
||||
|
||||
lemma l8_update_pops_four:
|
||||
assumes "data_stack vm = a # b # c # d # xs"
|
||||
shows "data_stack (forth_l8_update_guard vm) = xs"
|
||||
by (simp add: forth_l8_update_guard_def assms)
|
||||
|
||||
lemma l8_update_target_not_modelled: True
|
||||
\<comment> \<open>ssm_l8_update mutates *vm->ssm_l8_state -- see file header's L8
|
||||
representation-mismatch finding; not the vm_state field `ssm_l8`.\<close>
|
||||
by simp
|
||||
|
||||
(* ── L8-TABLE-FORCE ( config_idx -- ) : pop1 shape only ─────────────────── *)
|
||||
(* C: pops idx unconditionally BEFORE checking l8/cfg for NULL. *)
|
||||
|
||||
definition forth_l8_table_force_guard :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_l8_table_force_guard vm =
|
||||
(case data_stack vm of
|
||||
idx # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>
|
||||
| _ \<Rightarrow> set_error vm)"
|
||||
|
||||
lemma l8_table_force_pops_one:
|
||||
assumes "data_stack vm = idx # xs"
|
||||
shows "data_stack (forth_l8_table_force_guard vm) = xs"
|
||||
by (simp add: forth_l8_table_force_guard_def assms)
|
||||
|
||||
lemma l8_table_force_target_not_modelled: True
|
||||
\<comment> \<open>ssm_l8_force_config mutates the 128-config adaptive table -- a THIRD
|
||||
L8 representation, see file header finding.\<close>
|
||||
by simp
|
||||
|
||||
(* ── Everything else -- NOT MODELLED ──────────────────────────────────── *)
|
||||
|
||||
lemma window_diversity_not_modelled: True \<comment> \<open>WINDOW-DIVERSITY: rolling_window_measure_diversity computes a fresh value from rw_history (a modelled field, but the diversity ALGORITHM over it is not) -- distinct from the already-stored rw_last_diversity. No overflow guard either.\<close>
|
||||
by simp
|
||||
lemma infer_run_not_modelled: True \<comment> \<open>INFER-RUN: allocates last_inference_outputs on first call, walks the dictionary read-only for heat stats, then runs inference_engine_run -- a whole-subsystem algorithm. This is the ONLY word that writes `last_inference`, so no fetch-after-INFER-RUN lemma can be stated.\<close>
|
||||
by simp
|
||||
lemma l8_mode_not_modelled: True \<comment> \<open>L8-MODE: reads vm->ssm_l8_state's legacy 16-mode int -- see file header's representation-mismatch finding. No overflow guard.\<close>
|
||||
by simp
|
||||
lemma l8_apply_not_modelled: True \<comment> \<open>L8-APPLY: no-op if !l8||!cfg, else ssm_apply_mode -- targets the same unmodelled legacy L8 state as L8-UPDATE.\<close>
|
||||
by simp
|
||||
lemma bayes_cache_mean_not_modelled: True \<comment> \<open>BAYES-CACHE-MEAN: hotwords_posterior_cache_hits over the unmodelled hot-words cache subsystem (StarForth_Physics_Benchmark_Words.thy). No overflow guard.\<close>
|
||||
by simp
|
||||
lemma bayes_cache_lower_not_modelled: True by simp
|
||||
lemma bayes_cache_upper_not_modelled: True by simp
|
||||
lemma bayes_bucket_mean_not_modelled: True by simp
|
||||
lemma bayes_bucket_lower_not_modelled: True by simp
|
||||
lemma bayes_bucket_upper_not_modelled: True by simp
|
||||
|
||||
end
|
||||
Reference in New Issue
Block a user