LithosAnanake/proof/StarForth_Base.thy

theory StarForth_Base
  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. Needed here since cell is now a
   word type and several word derivations use it (see Section 1 below). *)
unbundle bit_operations_syntax

(* =========================================================================
   SPECIFICATION AUTHORITY NOTICE
   ─────────────────────────────────────────────────────────────────────────
   This file is the GROUND TRUTH specification of the StarForth VM state.
   C code is written TO MATCH this theory, not the other way around.

   HUMAN REVIEW PROTOCOL:
     Every field of vm_state must be audited against include/vm.h.
     Every predicate (wf_vm, ds_full, rs_full) must be audited against the
     corresponding C guard expressions in vm.c, word_source/, and vm_time.c.
     Discrepancies between this theory and the C source are BUGS IN THE C CODE.

   When a C implementation is changed, re-check the corresponding lemma.
   When a lemma is changed, update the C implementation to match.

   PROOF STATUS KEY (used throughout):
     ✓ — fully mechanised, no C review needed beyond initial audit
     ⚠ — sorry/axiom: C code must be manually verified to satisfy this claim
     ○ — proof obligation: C code must implement this specification exactly
   ======================================================================== *)

(* =========================================================================
   Section 1: Cell type and FORTH-79 boolean convention
   ======================================================================== *)

(* ○ CODE-MUST-MATCH: cell_t in include/vm.h is `typedef signed long cell_t`.
   On x86-64 Linux, signed long = 64-bit signed integer.

   CORRECTED 2026-08-13: was modeled as HOL int (arbitrary precision,
   never wraps). Changed to a genuine 64-bit word, matching how
   StarForth_Q48_16.thy already models q48. The old int model made every
   wraparound-dependent C behavior inexpressible (confirmed while scoping
   StarForth_Double_Words.thy: D+/D-/DNEGATE explicitly do carry/borrow
   arithmetic and bitwise-complement wraparound that only make sense
   against a fixed-width type). cell_t is C's *signed* long, so value
   comparisons on cell throughout this proof suite use the Word library's
   SIGNED order (<s, \<le>s, sint) rather than the default unsigned (<, \<le>),
   which does not match FORTH's signed-integer semantics (e.g. -1 must
   compare less than 0, not greater, as it would under unsigned order).
   Structural comparisons (list lengths, nat indices) are unaffected and
   stay plain nat as before -- only actual cell VALUES need <s/\<le>s. *)
type_synonym cell = "64 word"

(* ○ CODE-MUST-MATCH: include/vm.h defines:
     #define FORTH_TRUE  ((cell_t)-1)
     #define FORTH_FALSE ((cell_t) 0)
   Any C logical word that produces a boolean result MUST use these macros,
   not raw 1/0 or any other encoding.  Verified in:
     src/word_source/logical_words.c — ALL comparison and test words

   -1 as a cell (64 word) numeral is already the correct two's-complement
   all-ones bit pattern (0xFFFFFFFFFFFFFFFF) via Word's standard numeral
   semantics -- identical to C's (cell_t)-1 bit-for-bit, no change needed
   here despite the type change above.                                    *)
definition forth_true :: cell where "forth_true  = -1"
definition forth_false :: cell where "forth_false =  0"

definition to_forth_bool :: "bool \<Rightarrow> cell" where
  "to_forth_bool b = (if b then forth_true else forth_false)"

lemma to_forth_bool_True  [simp]: "to_forth_bool True  = -1"
  by (simp add: to_forth_bool_def forth_true_def)
lemma to_forth_bool_False [simp]: "to_forth_bool False =  0"
  by (simp add: to_forth_bool_def forth_false_def)
lemma to_forth_bool_eq: "to_forth_bool b = (if b then -1 else 0)"
  by (cases b; simp)

(* =========================================================================
   Reusable safe-arithmetic infrastructure for cell (64 word) values,
   added during the cell-as-word migration 2026-08-13.

   Every numeric constant this proof suite actually uses (HEAT_MAX =
   10^6, ACL_MAX_TTL = 65535, DECAY_SLOPE_MAX in the low millions, etc.)
   is many orders of magnitude below the 64-bit signed range
   [-2^63, 2^63-1]. cell_safe below names a single generous safe zone
   (|c| < 2^32, still 2^31 times larger than any constant actually in
   use) so every call site needs only "cell_safe c" (or the two bare
   inequalities it unfolds to) instead of re-deriving a
   signed_take_bit/sint no-overflow argument from scratch every time a
   proof adds or subtracts 1 from a cell value near a bound. Without
   this, +1/-1 near a bound is NOT provably safe in general -- a bare
   64-bit word wraps -- so this is a genuine hypothesis every such lemma
   needs, not a formality. *)

definition cell_safe :: "cell \<Rightarrow> bool" where
  "cell_safe c \<longleftrightarrow> -4294967296 \<le>s c \<and> c \<le>s 4294967296"  \<comment> \<open>|c| < 2^32\<close>

lemma cell_safe_sint_bounds:
  assumes "cell_safe c"
  shows "-4294967296 \<le> sint c" "sint c \<le> 4294967296"
  using assms by (simp_all add: cell_safe_def word_sle_eq)

(* The one lemma every "+1 near a bound" argument actually needs: adding
   or subtracting a small delta to a cell_safe value produces exactly
   the expected sint, no wraparound -- because the safe zone leaves a
   2^31-times margin against the true 2^63 boundary. *)
lemma cell_safe_add_sint:
  assumes "cell_safe c"
  assumes "\<bar>delta\<bar> \<le> 4294967296"
  shows "sint (c + word_of_int delta) = sint c + delta"
proof -
  have b: "-4294967296 \<le> sint c" "sint c \<le> 4294967296"
    using assms(1) by (simp_all add: cell_safe_sint_bounds)
  have step1: "sint (c + word_of_int delta)
      = signed_take_bit 63 (sint c + sint (word_of_int delta :: cell))"
    by (simp add: sint_word_add)
  have step2: "sint (word_of_int delta :: cell) = delta"
    using assms(2)
    by (simp add: sint_sbintrunc' signed_take_bit_int_eq_self)
  have step3: "signed_take_bit 63 (sint c + delta) = sint c + delta"
    by (rule signed_take_bit_int_eq_self) (use b assms(2) in auto)
  from step1 step2 step3 show ?thesis by simp
qed

lemma cell_safe_1 [simp]: "cell_safe 1"
  by (simp add: cell_safe_def word_sle_eq)
lemma cell_safe_0 [simp]: "cell_safe 0"
  by (simp add: cell_safe_def word_sle_eq)

(* Subtraction variant, for the common "de_heat e - amount" shape (amount
   is itself a cell parameter, not a fixed literal, so cell_safe_add_sint
   with a literal delta doesn't directly apply). *)
lemma cell_safe_sub_sint:
  assumes "cell_safe c"
  assumes "cell_safe amount"
  shows "sint (c - amount) = sint c - sint amount"
proof -
  have bc: "-4294967296 \<le> sint c" "sint c \<le> 4294967296"
    using assms(1) by (simp_all add: cell_safe_sint_bounds)
  have ba: "-4294967296 \<le> sint amount" "sint amount \<le> 4294967296"
    using assms(2) by (simp_all add: cell_safe_sint_bounds)
  have "sint (c - amount) = signed_take_bit 63 (sint c - sint amount)"
    by (simp add: sint_word_diff)
  also have "\<dots> = sint c - sint amount"
    by (rule signed_take_bit_int_eq_self) (use bc ba in auto)
  finally show ?thesis .
qed

(* Every "nat n" conversion the old int-based PICK/ROLL/etc. definitions
   did becomes "unat n" under the word migration -- but unat reinterprets
   the raw bit pattern as unsigned, which only agrees with the natural
   "nat of the signed value" reading when n is non-negative in the SIGNED
   sense (0 \<le>s n). Every call site that uses this already checks n <s 0
   first and only reaches the nat-conversion in the non-negative case, so
   this lemma is exactly the bridge those proofs need, proved once here
   rather than re-derived at every site. *)
lemma unat_eq_nat_sint_of_nonneg:
  assumes "0 \<le>s (n :: cell)"
  shows "unat n = nat (sint n)"
proof -
  have lo: "0 \<le> sint n" using assms by (simp add: word_sle_eq)
  have hi63: "sint n < 2 ^ 63" using sint_lt[of n] by simp
  have hi: "sint n < 2 ^ (64::nat)" using hi63 by simp
  have "uint n = take_bit (64::nat) (sint n)" by (simp add: uint_sint)
  also have "\<dots> = sint n"
    by (rule take_bit_int_eq_self) (use lo hi in auto)
  finally show ?thesis by (simp add: unat_eq_nat_uint)
qed

(* Signed absolute value on cell.  word's inherited "abs" (if it resolved at
   all) would be unsigned-magnitude, which is wrong for cell_t's signed
   semantics -- must build this explicitly from the signed order <s.
   NOTE: cell_abs min_word = min_word (two's-complement negation of
   INT64_MIN wraps back to itself, matching C's ABS(LONG_MIN) hazard) --
   this is a genuine, documented exclusion, not an oversight. *)
definition cell_abs :: "cell \<Rightarrow> cell" where
  "cell_abs n = (if n <s 0 then -n else n)"

(* Signed truncating division/remainder, matching C99's "/" and "%" on
   signed cell_t: quotient truncates toward zero, remainder takes the sign
   of the dividend.  word's inherited div/mod are unsigned-magnitude and
   would silently give the wrong answer for negative operands -- e.g.
   (-7) div 2 under unsigned word semantics treats the bit pattern of -7 as
   a huge positive number, nothing like C's -7 / 2 = -3. *)
definition cell_sdiv :: "cell \<Rightarrow> cell \<Rightarrow> cell" where
  "cell_sdiv a b = word_of_int (sgn (sint a) * sgn (sint b) * (\<bar>sint a\<bar> div \<bar>sint b\<bar>))"

definition cell_smod :: "cell \<Rightarrow> cell \<Rightarrow> cell" where
  "cell_smod a b = word_of_int (sgn (sint a) * (\<bar>sint a\<bar> mod \<bar>sint b\<bar>))"

(* =========================================================================
   Section 2: Stack type and capacity constants
   ======================================================================== *)

(* Top-of-stack is the head of the list.
   ○ CODE-MUST-MATCH: In C, vm->data_stack[vm->dsp] is TOS.  The list model
   maps directly: head = data_stack[dsp], tail = data_stack[dsp-1..0].      *)
type_synonym forth_stack = "cell list"

(* ○ CODE-MUST-MATCH: #define STACK_SIZE 1024 in include/vm.h.
   ⚠ HUMAN-REVIEW: If STACK_SIZE is ever changed in the C code, this
   definition must be updated and ALL stack overflow/underflow lemmas
   re-proved to ensure they still hold.                                      *)
definition STACK_SIZE :: nat where "STACK_SIZE = 1024"

(* ○ CODE-MUST-MATCH: #define VM_MEMORY_SIZE (5 * 1024 * 1024) in include/vm.h.
   ⚠ HUMAN-REVIEW: If this changes in C, update here and re-check
   StarForth_Dictionary_Words.thy's ALLOT/,/C,/2, bound lemmas.               *)
definition VM_MEMORY_SIZE :: nat where "VM_MEMORY_SIZE = 5242880"

(* ○ CODE-MUST-MATCH: #define BLOCK_SIZE 1024, DICTIONARY_BLOCKS 2048,
   DICTIONARY_MEMORY_SIZE (DICTIONARY_BLOCKS*BLOCK_SIZE) in include/vm.h.
   ⚠ HUMAN-REVIEW: this is a SMALLER bound than VM_MEMORY_SIZE (2MB vs 5MB).
   vm_allot() (src/memory_management.c) -- used by ALIGN via vm_align -- checks
   `here` against THIS bound, but ALLOT/,/C,/2, in dictionary_words.c bypass
   vm_allot and check `here` directly against VM_MEMORY_SIZE instead. Two
   different ceilings for the same pointer -- a real inconsistency in the C
   source, transcribed faithfully here rather than picking one. See
   StarForth_Dictionary_Words.thy.                                            *)
definition DICTIONARY_MEMORY_SIZE :: nat where "DICTIONARY_MEMORY_SIZE = 2097152"

(* ○ CODE-MUST-MATCH: Makefile default parameters for rolling window.
   ⚠ HUMAN-REVIEW: These values appear in multiple C files:
     - ROLLING_WINDOW_SIZE: src/rolling_window_of_truth.c, include/vm.h
     - ADAPTIVE_MIN_WINDOW_SIZE: src/rolling_window_of_truth.c
     - ADAPTIVE_SHRINK_RATE: src/rolling_window_of_truth.c
     - ADAPTIVE_GROWTH_THRESHOLD: src/rolling_window_of_truth.c
   Any change in the C Makefile parameters that alter these values must be
   reflected here and the Loop #2 / Loop #5 invariant proofs re-checked.   *)
definition ROLLING_WINDOW_SIZE      :: nat where "ROLLING_WINDOW_SIZE      = 4096"
definition ADAPTIVE_MIN_WINDOW_SIZE :: nat where "ADAPTIVE_MIN_WINDOW_SIZE = 256"
definition ADAPTIVE_SHRINK_RATE     :: nat where "ADAPTIVE_SHRINK_RATE     = 50"
definition ADAPTIVE_GROWTH_THRESHOLD :: nat where "ADAPTIVE_GROWTH_THRESHOLD = 5"
definition DICTIONARY_SIZE          :: nat where "DICTIONARY_SIZE          = 4096"

(* =========================================================================
   Section 3: Sub-struct types mirroring C structs in include/vm.h
   ======================================================================== *)

(* ── VM mode ────────────────────────────────────────────────────────────── *)
(* ○ CODE-MUST-MATCH: enum vm_mode_t { MODE_INTERPRET = 0, MODE_COMPILE = 1 }
   ⚠ HUMAN-REVIEW: ModeInterpret = 0, ModeCompile = 1.  The C code in
   src/vm.c uses integer comparisons against these values.  Verify that
   no C code uses the raw integer 1 vs 2 or other off-by-one.              *)
datatype vm_mode = ModeInterpret | ModeCompile

(* ── Mutex / lock state ─────────────────────────────────────────────────── *)
(* ○ CODE-MUST-MATCH: sf_mutex_t wraps pthread_mutex_t (Linux) or a bare-metal
   spinlock.  The abstract lock_state here models only the ownership state.
   ⚠ HUMAN-REVIEW: Verify that the C mutex implementation guarantees exactly
   the acquire/release semantics proved in StarForth_Mutex.thy — in
   particular that no thread can observe LockHeld while the lock is logically
   LockFree.  This requires auditing src/platform/linux/mutex.c.            *)
datatype lock_state = LockFree | LockHeld nat   \<comment> \<open>nat = thread ID holder\<close>

(* ── SSM L8 Jacquard mode ────────────────────────────────────────────────── *)
(* ○ CODE-MUST-MATCH: ssm_l8_mode_t { SSM_C0..SSM_C3 } in include/ssm_jacquard.h
   ⚠ HUMAN-REVIEW: Verify the C mode transition logic matches StarForth_Concurrent
   (heartbeat_step does not alter SSM mode during word execution).          *)
datatype ssm_mode = C0 | C1 | C2 | C3

record ssm_l8_state =
  ssm_current_mode       :: ssm_mode
  ssm_hysteresis_counter :: nat
  ssm_pending_mode       :: ssm_mode

(* ── DictPhysics ─────────────────────────────────────────────────────────── *)
(* ○ CODE-MUST-MATCH: struct DictPhysics in include/vm.h
   ⚠ HUMAN-REVIEW: Check that every field listed here has a corresponding field
   in the C DictPhysics struct with the same semantics.
   dp_temperature_q8 → temperature_q8 (uint16_t, Q8 format)
   dp_last_active_ns → last_active_ns  (uint64_t, monotonic ns)
   dp_last_decay_ns  → last_decay_ns   (uint64_t)
   dp_mass_bytes     → mass_bytes      (uint32_t, header+body size)
   dp_avg_latency_ns → avg_latency_ns  (uint64_t, rolling average)
   dp_state_flags    → state_flags     (uint32_t, encoded traits)              *)
record dict_physics =
  dp_temperature_q8   :: nat    \<comment> \<open>Q8 execution-heat hotness\<close>
  dp_last_active_ns   :: nat    \<comment> \<open>monotonic timestamp of last execution\<close>
  dp_last_decay_ns    :: nat
  dp_mass_bytes       :: nat    \<comment> \<open>header + body footprint\<close>
  dp_avg_latency_ns   :: nat    \<comment> \<open>rolling average latency\<close>
  dp_state_flags      :: nat    \<comment> \<open>encoded execution traits\<close>

(* ── 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 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.    *)
record dict_entry =
  de_name     :: string
  de_flags    :: nat
  de_heat     :: cell        \<comment> \<open>execution_heat — drives Loop #1 optimization\<close>
  de_word_id  :: nat
  de_physics  :: dict_physics
  de_acl_ttl     :: nat     \<comment> \<open>acl_ttl: countdown; 0 → ACL-RECHECK\<close>
  de_acl_allow   :: bool    \<comment> \<open>acl_allow: cached decision (True=allow, False=deny)\<close>
  de_acl_mode    :: nat     \<comment> \<open>acl_mode: 0=TTL, 1=STRICT\<close>
  de_acl_pinned  :: bool    \<comment> \<open>acl_pinned: one-way ratchet; True = immutable\<close>

(* ── Word transition metrics ─────────────────────────────────────────────── *)
(* ○ CODE-MUST-MATCH: struct WordTransitionMetrics in include/physics_pipelining_metrics.h
   ⚠ HUMAN-REVIEW: wt_transition_heat and wt_context_window are modeled as HOL
   functions (nat → nat) instead of C arrays.  In C these are fixed-size arrays
   of length DICTIONARY_SIZE / context window size respectively.
   Verify that array accesses in the C code are always in bounds (no UB).
   The abstraction here assumes they are.                                      *)
record word_transition_metrics =
  wt_transition_heat         :: "nat \<Rightarrow> nat"   \<comment> \<open>word_id \<rightarrow> transition count\<close>
  wt_total_transitions       :: nat
  wt_prefetch_attempts       :: nat
  wt_prefetch_hits           :: nat
  wt_prefetch_misses         :: nat
  wt_latency_saved_q48       :: int    \<comment> \<open>Q48.16, signed\<close>
  wt_misprediction_cost_q48  :: int
  wt_max_prob_q48            :: int
  wt_most_likely_next        :: nat    \<comment> \<open>word_id of predicted next word\<close>
  wt_context_window          :: "nat \<Rightarrow> nat"   \<comment> \<open>circular context buffer\<close>
  wt_context_window_pos      :: nat
  wt_actual_window_size      :: nat
  wt_total_context_trans     :: nat

(* ── Rolling Window of Truth ──────────────────────────────────────────────── *)
(* ○ CODE-MUST-MATCH: struct RollingWindowOfTruth in include/rolling_window_of_truth.h
   ⚠ HUMAN-REVIEW: rw_history, rw_snapshot_buf0, rw_snapshot_buf1 model circular
   ring buffers.  In C these are uint32_t arrays of fixed size ROLLING_WINDOW_SIZE.
   Verify that:
     (a) ring buffer write positions always remain < ROLLING_WINDOW_SIZE
     (b) rw_act_window is always set to min(total_executions, ROLLING_WINDOW_SIZE)
         immediately after incrementing rw_total_exec (see src/rolling_window_of_truth.c)
   ⚠ HUMAN-REVIEW: rw_eff_window and rw_act_window are DISTINCT fields.
     rw_eff_window = effective_window_size (adaptive target)
     rw_act_window = actual_window_size = min(total_exec, ROLLING_WINDOW_SIZE)
   Verify the C implementation updates both correctly on every execution.     *)
record rolling_window_state =
  rw_history          :: "nat \<Rightarrow> nat"   \<comment> \<open>circular buffer of word IDs\<close>
  rw_snapshot_buf0    :: "nat \<Rightarrow> nat"   \<comment> \<open>double-buffer slot 0\<close>
  rw_snapshot_buf1    :: "nat \<Rightarrow> nat"   \<comment> \<open>double-buffer slot 1\<close>
  rw_window_pos       :: nat
  rw_total_exec       :: nat
  rw_is_warm          :: bool
  rw_eff_window       :: nat   \<comment> \<open>effective_window_size (adaptive, mutated by Loops 2/5/6)\<close>
  rw_act_window       :: nat   \<comment> \<open>actual_window_size = min(total_exec, ROLLING_WINDOW_SIZE)\<close>
  rw_last_diversity   :: nat
  rw_diversity_checks :: nat
  rw_snap_index       :: nat
  rw_snap_pending     :: bool
  rw_snap_window_pos0 :: nat
  rw_snap_window_pos1 :: nat
  rw_snap_total0      :: nat
  rw_snap_total1      :: nat
  rw_snap_eff0        :: nat
  rw_snap_eff1        :: nat
  rw_snap_warm0       :: bool
  rw_snap_warm1       :: bool
  rw_adapt_accum      :: nat
  rw_adapt_pending    :: bool

(* ── Pipeline global metrics ─────────────────────────────────────────────── *)
(* ○ CODE-MUST-MATCH: struct PipelineGlobalMetrics in include/vm.h
   ⚠ HUMAN-REVIEW: pm_last_accuracy_num / pm_last_accuracy_den model the
   binary-chop accuracy ratio as a fraction.  Verify that the C code stores
   and updates these consistently and that pm_last_accuracy_den > 0 whenever
   pm_last_accuracy_num > 0 (no division by zero in accuracy computation).   *)
record pipeline_metrics_state =
  pm_prefetch_attempts    :: nat
  pm_prefetch_hits        :: nat
  pm_tuning_checks        :: nat
  pm_last_window_size     :: nat
  pm_last_accuracy_num    :: nat   \<comment> \<open>numerator of accuracy ratio\<close>
  pm_last_accuracy_den    :: nat   \<comment> \<open>denominator; den > 0 when num > 0\<close>
  pm_suggested_next_size  :: nat

(* ── Heartbeat tick snapshot ─────────────────────────────────────────────── *)
(* ○ CODE-MUST-MATCH: struct HeartbeatTickSnapshot in include/vm.h
   ⚠ HUMAN-REVIEW: hts_actual_window corresponds to the actual_window_size field
   added in the actual_window_size branch.  Verify that heartbeat_capture_tick_snapshot
   in src/heartbeat_export.c sets this field to min(total_executions, ROLLING_WINDOW_SIZE)
   and NOT to effective_window_size.                                           *)
record hb_tick_snapshot =
  hts_tick_number       :: nat
  hts_elapsed_ns        :: nat
  hts_tick_interval_ns  :: nat
  hts_cache_hits_delta  :: nat
  hts_bucket_hits_delta :: nat
  hts_word_exec_delta   :: nat
  hts_hot_word_count    :: nat
  hts_avg_word_heat_num :: nat   \<comment> \<open>numerator (Q48.16 / 65536 as nat)\<close>
  hts_window_width      :: nat
  hts_actual_window     :: nat
  hts_predicted_labels  :: nat
  hts_jitter_ns_num     :: nat
  hts_l8_mode           :: nat

(* ── Heartbeat state ─────────────────────────────────────────────────────── *)
(* ○ CODE-MUST-MATCH: struct HeartbeatState in include/vm.h
   ⚠ HUMAN-REVIEW: hb_tick_buffer is modeled as a HOL function (nat → hb_tick_snapshot)
   but in C it is a fixed-size ring buffer.  Verify:
     (a) hb_tick_write_idx always wraps modulo hb_tick_buffer_size (ring semantics)
     (b) hb_tick_buffer_size ≤ the actual C array bound (no out-of-bounds write)
   ⚠ HUMAN-REVIEW: hb_enabled must be False when the heartbeat thread is not
   running.  Every code path that accesses heartbeat state must check hb_enabled
   first; the Isabelle theories assume heartbeat is logically active.          *)
record heartbeat_state =
  hb_tick_count         :: nat
  hb_last_infer_tick    :: nat
  hb_check_counter      :: nat
  hb_enabled            :: bool
  hb_tick_target_ns     :: nat
  hb_snap_index         :: nat
  hb_infer_count        :: nat
  hb_early_exit_count   :: nat
  hb_words_executed     :: nat
  hb_dict_lookups       :: nat
  hb_tick_buffer        :: "nat \<Rightarrow> hb_tick_snapshot"
  hb_tick_buffer_size   :: nat
  hb_tick_write_idx     :: nat
  hb_tick_count_total   :: nat
  hb_run_start_ns       :: nat
  hb_tick_number_offset :: nat

(* ── Inference outputs ───────────────────────────────────────────────────── *)
(* ○ CODE-MUST-MATCH: struct InferenceOutputs in include/inference_engine.h
   ⚠ HUMAN-REVIEW: The early-exit flag io_early_exited corresponds to
   InferenceOutputs.early_exited in C.  When this flag is true, the C code
   must NOT update rw_eff_window or decay_slope_q48.  Verify in
   src/inference_engine.c run_inference() and its callers in src/vm_time.c. *)
record inference_outputs_state =
  io_early_exited           :: bool
  io_window_variance_q48    :: nat   \<comment> \<open>pattern variance Q48.16\<close>
  io_adaptive_window_width  :: nat
  io_adaptive_decay_slope   :: nat   \<comment> \<open>Q48.16\<close>
  io_fit_quality_q48        :: nat
  io_window_size_used       :: nat

(* =========================================================================
   Section 4: Full VM state record
   ── ⚠ CRITICAL HUMAN REVIEW REQUIRED ──────────────────────────────────────
   This record must mirror EVERY field of the C VM struct (include/vm.h).
   Any field present in C but absent here is an UNCOVERED STATE that could
   hide a correctness gap.  Similarly, any field present here but not in C
   (or with different semantics) is a SPECIFICATION BUG.

   AUDIT CHECKLIST (compare to include/vm.h struct VM):
     □ data_stack / return_stack — lists, TOS = head
     □ exit_colon / abort_req   — boolean flags
     □ memory / memory_size     — flat address space
     □ 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               — 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 / ...
     □ tuning_lock              — for physics tuning critical section
     □ pipeline_metrics / hb_decay_cursor
     □ heartbeat                — full HeartbeatState
     □ last_inference           — InferenceOutputs option
     □ ssm_l8                   — SSM L8 Jacquard mode
   ======================================================================== *)

record vm_state =
  (* ── Core stacks ────────────────────────────────────────────────────── *)
  (* ○ CODE-MUST-MATCH: C: cell_t data_stack[STACK_SIZE], dsp (index of TOS)
     Stack word proofs rely on head = TOS = data_stack[dsp].               *)
  data_stack    :: forth_stack
  return_stack  :: forth_stack
  (* ○ CODE-MUST-MATCH: exit_colon = return from colon definition flag
     abort_req = ABORT word has been called.  Must be checked by the
     interpreter loop before each word dispatch.                             *)
  exit_colon    :: bool
  abort_req     :: bool
  emergency_console :: bool  \<comment> \<open>True = physical ok> REPL; bypasses all ACL checks (C-only write)\<close>
  zuse_session      :: bool  \<comment> \<open>True = zuse authenticated; god-mode bypass (C-only write via ZUSE-AUTHENTICATE)\<close>

  (* ── Memory ──────────────────────────────────────────────────────────── *)
  (* ○ CODE-MUST-MATCH: C: uint8_t vm_memory[VM_MEMORY_SIZE]
     ⚠ HUMAN-REVIEW: In C, memory is byte-addressed (uint8_t) but cell
     operations (@ !) access aligned cell_t-sized chunks.  The abstract model
     uses nat → cell.  Alignment and bounds are modelled abstractly via
     valid_addr in StarForth_Memory_Words.thy.  A concrete memory model would
     require verifying byte-level alignment in the C vm_load_cell/vm_store_cell
     implementations.                                                        *)
  memory        :: "nat \<Rightarrow> cell"
  memory_size   :: nat

  (* ── Dictionary ──────────────────────────────────────────────────────── *)
  (* ○ CODE-MUST-MATCH: C dictionary is a linked list of DictEntry structs
     allocated in a flat memory arena.  We abstract it as a partial function
     word_id → dict_entry.  This abstracts away the arena layout.
     ⚠ HUMAN-REVIEW: Verify that word ID assignment is injective (no two
     words share a word_id) in src/memory_management.c.                     *)
  dictionary    :: "nat \<Rightarrow> dict_entry option"
  latest_id     :: "nat option"
  here          :: nat                            \<comment> \<open>next free byte offset in arena\<close>
  dict_fence    :: "nat option"                   \<comment> \<open>FENCE word_id for FORGET\<close>
  dict_lock     :: lock_state
  word_id_next  :: nat

  (* ── Execution state ──────────────────────────────────────────────────── *)
  vm_mode       :: vm_mode
  vm_ip         :: nat                            \<comment> \<open>instruction pointer (byte offset)\<close>
  state_var     :: cell                           \<comment> \<open>STATE: 0=interp, -1=compile\<close>
  vm_base       :: cell                           \<comment> \<open>numeric base for I/O (2..36)\<close>
  vm_error      :: bool
  vm_halted     :: bool

  (* ── 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
     reorg.  Verify that heat_thresholds_wf (StarForth_Loop1_Heat.thy) holds
     after every reorg step: 0 ≤ 25th ≤ 50th ≤ 75th ≤ HEAT_MAX.            *)
  heat_threshold_25th       :: cell
  heat_threshold_50th       :: cell
  heat_threshold_75th       :: cell
  last_bucket_reorg_ns      :: nat
  lookup_strategy           :: nat   \<comment> \<open>0=naive 1=heat-aware 2=inference-reorg\<close>

  (* ── Physics Loop #2: Rolling Window of Truth ────────────────────────── *)
  (* ○ CODE-MUST-MATCH: RollingWindowOfTruth vm->rolling_window.
     ⚠ HUMAN-REVIEW: Verify window_invariant (StarForth_Loop2_Window.thy)
     holds after every call to rolling_window_record_execution() in
     src/rolling_window_of_truth.c.  Pay special attention to the boundary
     condition when rw_total_exec wraps around ROLLING_WINDOW_SIZE.          *)
  rolling_window            :: rolling_window_state

  (* ── Physics Loop #3: Linear heat decay ─────────────────────────────── *)
  (* ○ CODE-MUST-MATCH: decay_slope_q48 is a Q48.16 uint64_t.  Its invariant
     (slope > 0) must be preserved by every code path that updates it:
       src/vm_time.c vm_tick_slope_validator()
       src/inference_engine.c run_inference() (slope output)
     ⚠ HUMAN-REVIEW: Check that slope clamping in the C code always results in
     slope ≥ DECAY_SLOPE_MIN (= 1 ulp in Q48.16).                            *)
  decay_slope_q48           :: nat   \<comment> \<open>current decay rate Q48.16; invariant: > 0\<close>
  last_decay_check_ns       :: nat
  total_heat_at_check       :: nat
  hot_word_count_at_check   :: nat
  stale_word_count_at_check :: nat
  word_count_at_check       :: nat
  decay_direction           :: int   \<comment> \<open>-1=decrease 0=stable +1=increase\<close>
  tuning_lock               :: lock_state

  (* ── Physics Loop #4 & #5: Pipelining / prefetch ────────────────────── *)
  (* ○ CODE-MUST-MATCH: PipelineGlobalMetrics vm->pipeline_metrics.
     ⚠ HUMAN-REVIEW: pm_prefetch_hits ≤ pm_prefetch_attempts must hold after
     every pm_record_hit / pm_record_miss call.  Verify in
     src/physics_pipelining_metrics.c.                                        *)
  pipeline_metrics          :: pipeline_metrics_state
  hb_decay_cursor           :: nat   \<comment> \<open>continuation cursor for background decay\<close>

  (* ── Physics Loop #7: Heartbeat ─────────────────────────────────────── *)
  (* ○ CODE-MUST-MATCH: HeartbeatState vm->heartbeat.
     ⚠ HUMAN-REVIEW: hb_tick_target_ns > 0 must hold at all times (enforced
     by hb_shorten_period clamping to TICK_MIN_NS in StarForth_Loop7_Heartrate).
     Verify that src/vm_time.c never sets tick_target_ns to 0 or wraps below
     zero (unsigned underflow).                                               *)
  heartbeat                 :: heartbeat_state

  (* ── Unified Inference Engine (Loops #5 & #6) ───────────────────────── *)
  (* ○ CODE-MUST-MATCH: InferenceOutputs vm->last_inference_outputs (option).
     None = inference has not run yet; Some io = last successful output.
     ⚠ HUMAN-REVIEW: Verify that io_early_exited, io_adaptive_window_width, and
     io_adaptive_decay_slope are always set atomically (under tuning_lock) so
     the concurrent model is not violated.                                    *)
  last_inference            :: "inference_outputs_state option"

  (* ── SSM L8: Jacquard mode selector ─────────────────────────────────── *)
  (* ○ CODE-MUST-MATCH: SSM L8 state from include/ssm_jacquard.h.
     ⚠ HUMAN-REVIEW: The heartbeat_step axioms in StarForth_Transition say
     heartbeat_step does not change vm_mode.  If the SSM L8 selector can
     change vm_mode as a side-effect, that axiom is violated and the
     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
   ======================================================================== *)

(* ⚠ CRITICAL: wf_vm is the formal specification of "the VM is in a valid,
   non-error state."  Every C function that takes a VM* must ensure the VM
   satisfies wf_vm on entry (or restore it on exit).  This is the C-level
   invariant that the Isabelle proofs assume.

   ○ CODE-MUST-MATCH: The C interpreter loop in src/vm.c must check:
     - Stack bounds (dsp, rsp within [0, STACK_SIZE))
     - Error flag clear
     - rolling_window.effective_window_size ∈ [ADAPTIVE_MIN, ROLLING_WINDOW_SIZE]
     - rolling_window.actual_window_size = min(total_exec, ROLLING_WINDOW_SIZE)
     - decay_slope_q48 > 0
     - heartbeat.tick_target_ns > 0
   before entering the main execution loop.                                   *)
definition wf_vm :: "vm_state \<Rightarrow> bool" where
  "wf_vm vm \<longleftrightarrow>
     length (data_stack vm)   \<le> STACK_SIZE \<and>
     length (return_stack vm) \<le> STACK_SIZE \<and>
     \<not> vm_error vm \<and>
     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>
     rw_act_window (rolling_window vm) =
       min (rw_total_exec (rolling_window vm)) ROLLING_WINDOW_SIZE \<and>
     decay_slope_q48 vm > 0 \<and>
     hb_tick_target_ns (heartbeat vm) > 0"

(* ○ CODE-MUST-MATCH: set_error models vm->error = 1.
   Only the vm_error flag changes — ALL other fields remain exactly unchanged.
   ⚠ HUMAN-REVIEW: Verify that every C error path sets ONLY the error flag and
   does NOT accidentally corrupt data_stack, rolling_window, or other physics.
   Particularly check: vm_pop() underflow handlers, vm_push() overflow handlers,
   memory access out-of-bounds handlers.                                      *)
definition set_error :: "vm_state \<Rightarrow> vm_state" where
  "set_error vm = vm\<lparr>vm_error := True\<rparr>"

lemma set_error_error   [simp]: "vm_error   (set_error vm) = True"
  by (simp add: set_error_def)
lemma set_error_ds      [simp]: "data_stack  (set_error vm) = data_stack vm"
  by (simp add: set_error_def)
lemma set_error_rs      [simp]: "return_stack (set_error vm) = return_stack vm"
  by (simp add: set_error_def)
lemma set_error_rolling [simp]: "rolling_window (set_error vm) = rolling_window vm"
  by (simp add: set_error_def)
lemma set_error_hb      [simp]: "heartbeat (set_error vm) = heartbeat vm"
  by (simp add: set_error_def)
lemma set_error_decay   [simp]: "decay_slope_q48 (set_error vm) = decay_slope_q48 vm"
  by (simp add: set_error_def)
lemma set_error_pipeline [simp]: "pipeline_metrics (set_error vm) = pipeline_metrics vm"
  by (simp add: set_error_def)
lemma set_error_infer   [simp]: "last_inference (set_error vm) = last_inference vm"
  by (simp add: set_error_def)
lemma set_error_ssm     [simp]: "ssm_l8 (set_error vm) = ssm_l8 vm"
  by (simp add: set_error_def)
lemma set_error_dict    [simp]: "dictionary (set_error vm) = dictionary vm"
  by (simp add: set_error_def)

(* ── Capacity predicates ──────────────────────────────────────────────── *)
(* ○ CODE-MUST-MATCH: ds_full ↔ dsp + 1 >= STACK_SIZE in C.
   ⚠ HUMAN-REVIEW: Verify that every C word that pushes to the data stack
   checks ds_full BEFORE the push, not after.  Off-by-one here = memory
   corruption in the C stack array.                                          *)
definition ds_full :: "vm_state \<Rightarrow> bool" where
  "ds_full vm \<longleftrightarrow> length (data_stack vm) \<ge> STACK_SIZE"

definition rs_full :: "vm_state \<Rightarrow> bool" where
  "rs_full vm \<longleftrightarrow> length (return_stack vm) \<ge> STACK_SIZE"

(* ── Physics preservation: the key "no assumptions" mechanism ────────── *)

(* ⚠ 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, 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.

   ○ CODE-MUST-MATCH: Any C word implementation that modifies only the data
   stack MUST NOT touch any other VM field.  The C compiler does not enforce
   this; the Isabelle proof framework does.  Each of the lemmas below
   corresponds to a field that must NOT be written by a "pure data stack"
   word.  Violations require adding the field to the word's formal spec and
   re-proving the affected theorems.                                          *)

lemma ds_update_preserves_rolling:
  "rolling_window (vm\<lparr>data_stack := xs\<rparr>) = rolling_window vm"
  by simp

lemma ds_update_preserves_heartbeat:
  "heartbeat (vm\<lparr>data_stack := xs\<rparr>) = heartbeat vm"
  by simp

lemma ds_update_preserves_decay:
  "decay_slope_q48 (vm\<lparr>data_stack := xs\<rparr>) = decay_slope_q48 vm"
  by simp

lemma ds_update_preserves_pipeline:
  "pipeline_metrics (vm\<lparr>data_stack := xs\<rparr>) = pipeline_metrics vm"
  by simp

lemma ds_update_preserves_inference:
  "last_inference (vm\<lparr>data_stack := xs\<rparr>) = last_inference vm"
  by simp

lemma ds_update_preserves_ssm:
  "ssm_l8 (vm\<lparr>data_stack := xs\<rparr>) = ssm_l8 vm"
  by simp

lemma ds_update_preserves_dict:
  "dictionary (vm\<lparr>data_stack := xs\<rparr>) = dictionary 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