Robert Allan JamesandClaude Sonnet 5
ee3a2e57aa
Adds compiling_word_id :: nat option to vm_state, modelling vm->compiling_word (include/vm.h:421). forth_colon_entry_half now sets it from latest_id on success and forces it to None on the pinned-conflict failure path, matching the real C's unconditional `vm->compiling_word = de;` before its own NULL check in vm_enter_compile_mode (src/vm.c:232-264). : is now closed through entry creation + compiling_word tracking, same point as CREATE/VARIABLE/CONSTANT. Remaining gap for : is the same DF write (gap b, vm_align+HERE capture) those three already closed but not yet composed in here. All 52 theories verify clean (isabelle build -D proof/, ~48s). Part of the pre-Artemis closeout pass (FABRIC-2.md 5.2). PROOFS included per Captain Bob's 2026-08-14 instruction. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
905 lines
52 KiB
Plaintext
905 lines
52 KiB
Plaintext
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>
|
|
(* ○ CODE-MUST-MATCH, added 2026-08-15: the entry's data-field (DF) cell
|
|
-- the storage C's `vm_dictionary_get_data_field(entry)` returns a
|
|
pointer into (a single cell_t immediately following the entry's name
|
|
in the arena, per vm_create_word's layout, dictionary_management.c:
|
|
406-410). Modelled here as a plain VALUE (`cell`), not an address --
|
|
this closes gap (b) for every word that only ever reads/writes the DF
|
|
as a value through its OWNING entry (CREATE/VARIABLE/CONSTANT/DEFER
|
|
and their runtimes). It does NOT close >BODY/>NAME-style words in
|
|
StarForth_Dictionary_Manipulation_Words.thy, which need the DF's
|
|
ADDRESS (so a later, unrelated `@`/`!` could target it generically)
|
|
-- this model has no notion of a dict_entry's own address, only its
|
|
word_id, so that remains a distinct, still-open gap. *)
|
|
de_df :: cell
|
|
|
|
(* ── 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
|
|
(* ○ CODE-MUST-MATCH, added 2026-08-15: C `DictEntry* vm->
|
|
current_executing_entry` (include/vm.h:434) -- the entry currently
|
|
executing, read by runtime helpers like `defining_runtime_create`/
|
|
`_variable`/`_constant` via `vm->current_executing_entry` rather than
|
|
a fresh lookup. Modelled word-id-indexed (`nat option`), matching
|
|
`latest_id`'s convention, rather than as a raw pointer. *)
|
|
current_executing_word_id :: "nat option"
|
|
|
|
(* ── Compile-time state ───────────────────────────────────────────────
|
|
Models `vm->compiling_word` (include/vm.h:421, a DictEntry pointer),
|
|
the entry currently under construction by `:` until `;` clears it.
|
|
Word-id-indexed (`nat option`), matching `current_executing_word_id`
|
|
and `latest_id`'s convention, rather than a raw pointer. *)
|
|
compiling_word_id :: "nat option"
|
|
|
|
(* ── 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
|
|
(* ○ CODE-MUST-MATCH: C: vaddr_t state_addr (include/vm.h:452) -- VM
|
|
address of the cell holding STATE (0=interp, -1=compile). Distinct from
|
|
`state_var` (above), which is the host-side mirror cell_t field. Added
|
|
for StarForth_Defining_Words.thy's `[`/`]`/STATE -- these are the LIVE,
|
|
reachable implementations (defining_words.c registers over
|
|
dictionary_manipulation_words.c's `[`/`]`/STATE, which are dead code
|
|
once shadowed; see that file for the shadowed versions and this file
|
|
for the correction). *)
|
|
state_addr :: nat
|
|
|
|
(* ── Input system (TIB), added 2026-08-14 ─────────────────────────────
|
|
○ CODE-MUST-MATCH: C: char input_buffer[INPUT_BUFFER_SIZE] (=1025),
|
|
size_t input_length, size_t input_pos (include/vm.h:415-417). This is
|
|
the REAL, live interpreter input buffer -- vm_interpret's dispatch
|
|
path for both interactive REPL lines and LOAD'd block content (see
|
|
.claude/CLAUDE.md's INPUT_BUFFER_SIZE note) -- distinct from the
|
|
separate `tib_buf`/`tib_cap`/`in_var`/`span_var` fields (vm.h:444-448,
|
|
the C's own comment marks them "legacy; will migrate to VM addr") and
|
|
from `hold_addr`/`hold_pos` above (the pictured-number OUTPUT buffer,
|
|
unrelated). Modelled as `input_buffer :: string` holding exactly the
|
|
meaningful prefix (not the full fixed 1025-byte physical array, which
|
|
has no abstract counterpart -- content past `input_length` in the
|
|
real C is stale/undefined and never read), with `input_length` kept
|
|
as a separate field even though it always equals `length input_buffer`
|
|
here, to mirror the real C's two-field structure precisely. `input_pos`
|
|
is FORTH's `>IN` (parse position), advanced by `vm_parse_word`
|
|
(src/vm.c:137-160, modelled below as `forth_parse_word`). *)
|
|
input_buffer :: string
|
|
input_length :: nat
|
|
input_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 4b: TIB parsing (added 2026-08-14)
|
|
|
|
Closes, for the first time in this suite, the "name parse" dependency
|
|
named as an unmodelled precondition by nearly every name-consuming word
|
|
swept so far (CREATE/VARIABLE/CONSTANT/`:`/DEFER/IS/DEFER@/COMPILE/
|
|
[COMPILE]/FIND/WORD and others -- see StarForth_Defining_Words.thy's
|
|
file header, StarForth_Defer_Words.thy, etc.). `vm_parse_word`
|
|
(src/vm.c:137-160) turns out to be a pure scan over the input_buffer/
|
|
input_length/input_pos fields added above -- no host pointers, no C-
|
|
string tricks, unlike almost everything else this suite has deferred.
|
|
Individual per-word applications (composing this with e.g.
|
|
`dict_insert_entry`) are done in the files that use them, not here --
|
|
this section is only the shared parsing primitive.
|
|
======================================================================== *)
|
|
|
|
definition is_ws :: "char \<Rightarrow> bool" where
|
|
"is_ws c \<longleftrightarrow> c = CHR '' '' \<or> c = char_of (9::nat) \<or> c = char_of (10::nat) \<or> c = char_of (13::nat)"
|
|
\<comment> \<open>space, tab, LF, CR -- matches vm_parse_word's `c==' '||c=='\t'||c=='\n'||c=='\r'` exactly\<close>
|
|
|
|
(* C: `vm_parse_word` skips leading whitespace in input_buffer[input_pos..
|
|
input_length), then copies the following run of non-whitespace
|
|
(truncated to max_len-1 chars) into the caller's buffer, advancing
|
|
input_pos by exactly what was skipped plus what was copied (NOT past
|
|
any untruncated remainder of a token longer than max_len-1 -- the C
|
|
loop's own `len < max_len - 1` condition stops consuming input_pos at
|
|
the same point it stops writing `word`). Returns the parsed token
|
|
(empty string signals the C's `return 0`, matching every caller's
|
|
`nlen <= 0` failure check) and the updated vm_state. *)
|
|
definition forth_parse_word :: "nat \<Rightarrow> vm_state \<Rightarrow> (string \<times> vm_state)" where
|
|
"forth_parse_word max_len vm =
|
|
(let s = drop (input_pos vm) (input_buffer vm);
|
|
s1 = dropWhile is_ws s;
|
|
skipped = length s - length s1;
|
|
pos_ws = input_pos vm + skipped
|
|
in if s1 = []
|
|
then ('''', vm\<lparr>input_pos := pos_ws\<rparr>)
|
|
else
|
|
let tok = take (max_len - 1) (takeWhile (\<lambda>c. \<not> is_ws c) s1)
|
|
in (tok, vm\<lparr>input_pos := pos_ws + length tok\<rparr>))"
|
|
|
|
lemma forth_parse_word_all_whitespace_yields_empty:
|
|
assumes "dropWhile is_ws (drop (input_pos vm) (input_buffer vm)) = []"
|
|
shows "fst (forth_parse_word max_len vm) = ''''"
|
|
using assms by (simp add: forth_parse_word_def Let_def)
|
|
|
|
lemma forth_parse_word_success_nonempty:
|
|
assumes "dropWhile is_ws (drop (input_pos vm) (input_buffer vm)) \<noteq> []"
|
|
assumes "max_len \<ge> 2"
|
|
shows "fst (forth_parse_word max_len vm) \<noteq> ''''"
|
|
proof -
|
|
let ?s1 = "dropWhile is_ws (drop (input_pos vm) (input_buffer vm))"
|
|
from assms(1) obtain c cs where s1_eq: "?s1 = c # cs" by (cases ?s1) auto
|
|
have "\<not> is_ws c" using dropWhile_eq_Cons_conv[of is_ws "drop (input_pos vm) (input_buffer vm)" c cs]
|
|
using s1_eq by auto
|
|
hence "takeWhile (\<lambda>x. \<not> is_ws x) ?s1 = c # takeWhile (\<lambda>x. \<not> is_ws x) cs"
|
|
by (simp add: s1_eq)
|
|
hence "take (max_len - 1) (takeWhile (\<lambda>x. \<not> is_ws x) ?s1) \<noteq> []"
|
|
using assms(2) by simp
|
|
thus ?thesis
|
|
using assms(1) by (simp add: forth_parse_word_def Let_def)
|
|
qed
|
|
|
|
lemma forth_parse_word_input_pos_monotone:
|
|
"input_pos vm \<le> input_pos (snd (forth_parse_word max_len vm))"
|
|
by (simp add: forth_parse_word_def Let_def)
|
|
|
|
lemma forth_parse_word_preserves_buffer:
|
|
"input_buffer (snd (forth_parse_word max_len vm)) = input_buffer vm"
|
|
by (simp add: forth_parse_word_def Let_def)
|
|
|
|
lemma forth_parse_word_preserves_data_stack:
|
|
"data_stack (snd (forth_parse_word max_len vm)) = data_stack vm"
|
|
by (simp add: forth_parse_word_def Let_def)
|
|
|
|
lemma forth_parse_word_preserves_vm_mode:
|
|
"vm_mode (snd (forth_parse_word max_len vm)) = vm_mode vm"
|
|
by (simp add: forth_parse_word_def Let_def)
|
|
|
|
lemma forth_parse_word_preserves_dictionary:
|
|
"dictionary (snd (forth_parse_word max_len vm)) = dictionary vm"
|
|
by (simp add: forth_parse_word_def Let_def)
|
|
|
|
lemma forth_parse_word_preserves_word_id_next:
|
|
"word_id_next (snd (forth_parse_word max_len vm)) = word_id_next vm"
|
|
by (simp add: forth_parse_word_def Let_def)
|
|
|
|
lemma forth_parse_word_never_sets_error: True
|
|
\<comment> \<open>vm_parse_word's own C body never touches vm->error -- callers check
|
|
the returned length themselves and set it. Faithfully NOT set here
|
|
either.\<close>
|
|
by simp
|
|
|
|
(* =========================================================================
|
|
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
|