admin/LithosAnanake
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

proof/: add StarForth_Inference_Words.thy (inference_words.c coverage)

Browse Source 
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
2026-08-14 16:34:22 -04:00
parent 9d178e0efe
commit 346c793ebc
2 changed files with 253 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
proof/ROOT
+1
View File
@@ -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
proof/StarForth_Inference_Words.thy
+252
View File
@@ -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