admin/LithosAnanake
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
Files
cf205ca04a1c3c840001bd95b003a47ba38d65f8
LithosAnanake/proof/StarForth_Base.thy
T
Robert Allan James cf205ca04a proof/: add StarForth_Editor_Words.thy and StarForth_Format_Words.thy 
editor_words.c: zero tractable words (first such file in this sweep) --
every word routes through the same deferred block-window cache as
block_words.c, and EDIT is an interactive stdin/stdout REPL loop, not a
single-step transition.

format_words.c: 17 of 19 registered words modeled (# and #S deferred,
multi-precision division out of scope). Two genuine C findings recorded:
(1) DECIMAL/HEX/OCTAL write only the FORTH-visible memory cell at
base_addr, never the separate vm->base host-mirror field that number
OUTPUT words actually read -- proved formally
(decimal_does_not_change_vm_base et al.), so HEX/OCTAL/DECIMAL silently
never affect printed output, only parsed input. (2) ? and DUMP cast the
popped cell directly to a host pointer and dereference it, bypassing
vm_addr_ok entirely -- an out-of-VM-bounds read, not modeled since it
isn't a vm->memory access at all.

Adds base_addr/hold_addr/hold_pos to vm_state (StarForth_Base.thy),
matching the scr_addr/here pattern from earlier files.
2026-08-14 14:03:05 -04:00

755 lines
43 KiB
Plaintext
Raw Blame History

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
(* ○ CODE-MUST-MATCH: C: int ecw_nesting (include/vm.h:390) -- depth of
execute_colon_word call stack; >0 means inside a colon word. Modeled as
nat (C only ever tests ecw_nesting > 0, never negative values in any
reachable path) -- see StarForth_Double_Words.thy's 2>R/2R>/2R@. *)
ecw_nesting :: nat
(* ○ CODE-MUST-MATCH: C: vaddr_t scr_addr (include/vm.h:451, vaddr_t =
uint64_t) -- VM address of the SCR variable cell holding the current
block number. Modeled as nat, matching `here`'s convention for VM
addresses. See StarForth_Block_Words.thy's SCR. *)
scr_addr :: nat
(* ○ CODE-MUST-MATCH: C: vaddr_t base_addr (include/vm.h:453) -- VM address
of the FORTH BASE variable cell; vaddr_t hold_addr (include/vm.h:454) --
VM address of the 64-byte pictured-number hold buffer; int hold_pos
(include/vm.h:455) -- current fill count in that buffer, 0..63.
`vm_base` (above) is the SEPARATE host-mirror cell_t field C reads for
number *output* formatting (format_words.c's current_base()); the cell
at `base_addr` is what number *parsing* reads (vm.c's vm_get_base()).
See StarForth_Format_Words.thy for the finding that these two can
desync. *)
base_addr :: nat
hold_addr :: nat
hold_pos :: nat
(* ── 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
Reference in New Issue View Git Blame Copy Permalink