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>CORRECTED 2026-08-14: all five push via VM_PUSH (include/vm.h:706-719),
     which resolves to the bounds-checked vm_push() in every build except one
     defining STARFORTH_PERFORMANCE -- confirmed by repo-wide grep to never be
     defined by any Makefile/Kconfig target here. Real but dormant hazard, not
     a live per-word bug; same finding as StarForth_Q48_Words.thy's header.
     See proof/FINDINGS.md \<section>2.\<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. Push is via VM_PUSH -- see corrected header note near infer_fetch_words_no_overflow_guard.\<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. Push is via VM_PUSH -- see corrected header note near infer_fetch_words_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). Push is via VM_PUSH -- see corrected header note near infer_fetch_words_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