From 9d178e0efe4f66552ce1b15957b59cf384db9d15 Mon Sep 17 00:00:00 2001
From: Robert Allan James <robert.allan.james@gmail.com>
Date: Fri, 14 Aug 2026 16:31:39 -0400
Subject: [PATCH] proof/: add StarForth_Q48_Words.thy (q48_words.c coverage)

17 of 23 words fully modelled (Q.+/-/*//,  Q.ABS/NEG, Q.FROM-INT/TO-INT,
Q.1/0/SCALE, Q.=/</>/0=, Q.MAX/MIN), reusing q48_add/q48_mul/q48_div/
q48_from_u64/q48_to_u64 already in StarForth_Q48_16.thy and cell_abs
(Q.ABS's raw sign-bit test is bit-for-bit cell_abs's `n <s 0`). Added
q48_sub there alongside, the one missing arithmetic primitive.
Q.LOG/EXP/SQRT/SIN/COS deferred (same transcendental-approximation class
already excluded from the sweep at q48_16_words.c). Q.PRINT deferred
(stdout only).

Finding: every word in this file pops/pushes via the VM_POP/VM_PUSH
macros, which resolve to completely unchecked vm_pop_fast/vm_push_fast
when STARFORTH_PERFORMANCE is defined -- a build-flag-gated stack-safety
hazard distinct from (and broader than) the individual missing-guard
instances found elsewhere in the sweep, since it silently disables every
guard in the entire file at once. Modelled assuming the safe path.

Suite now 52 theories, green.
---
 proof/ROOT                    |   1 +
 proof/StarForth_Q48_16.thy    |  23 +++
 proof/StarForth_Q48_Words.thy | 321 ++++++++++++++++++++++++++++++++++
 3 files changed, 345 insertions(+)
 create mode 100644 proof/StarForth_Q48_Words.thy

diff --git a/proof/ROOT b/proof/ROOT
index 1d2de23..7bbaac4 100644
--- a/proof/ROOT
+++ b/proof/ROOT
@@ -36,6 +36,7 @@ session "StarForth" = "HOL-Library" +
     StarForth_Lifecycle_Words_Hosted
     StarForth_Defer_Words
     StarForth_Log_Words
+    StarForth_Q48_Words
     StarForth_Loop1_Heat
     StarForth_Loop2_Window
     StarForth_Loop3_Decay
diff --git a/proof/StarForth_Q48_16.thy b/proof/StarForth_Q48_16.thy
index 46a5f50..9d71556 100644
--- a/proof/StarForth_Q48_16.thy
+++ b/proof/StarForth_Q48_16.thy
@@ -121,6 +121,29 @@ lemma q48_add_zero_right [simp]: "q48_add a 0 = a"
 lemma q48_add_zero_left [simp]: "q48_add 0 a = a"
   by (simp add: q48_add_def)
 
+(* q48_sub: pointwise subtraction, wrapping on underflow (matches C - on
+   uint64_t). Added for src/word_source/q48_words.c's Q.- (StarForth_Q48_
+   Words.thy).
+   C: static inline q48_16_t q48_sub(q48_16_t a, q48_16_t b) { return a-b; } *)
+definition q48_sub :: "q48 \<Rightarrow> q48 \<Rightarrow> q48" where
+  "q48_sub a b = a - b"
+
+lemma q48_sub_zero_right [simp]: "q48_sub a 0 = a"
+  by (simp add: q48_sub_def)
+
+lemma q48_sub_self [simp]: "q48_sub a a = 0"
+  by (simp add: q48_sub_def)
+
+lemma q48_add_sub_cancel [simp]: "q48_sub (q48_add a b) b = a"
+  by (simp add: q48_sub_def q48_add_def)
+
+(* q48_abs: C compares the raw uint64 bit pattern against 0x8000...0 (the
+   sign bit threshold) rather than using a signed comparison operator, but
+   this is bit-for-bit the same test as `cell_abs`'s `n <s 0`
+   (StarForth_Base.thy) -- both are exactly "is the sign bit set". q48_abs
+   is therefore not modelled as a separate definition here: StarForth_Q48_
+   Words.thy's Q.ABS uses `cell_abs` directly under the `q48` type synonym. *)
+
 (* q48_mul: (a * b) >> 16, wrapping.
    C: q48_16_t q48_mul(q48_16_t a, q48_16_t b) { return ((__uint128_t)a*b) >> 16; }
    ⚠ HUMAN-REVIEW: The C implementation uses __uint128_t for the intermediate
diff --git a/proof/StarForth_Q48_Words.thy b/proof/StarForth_Q48_Words.thy
new file mode 100644
index 0000000..10418ab
--- /dev/null
+++ b/proof/StarForth_Q48_Words.thy
@@ -0,0 +1,321 @@
+theory StarForth_Q48_Words
+  imports StarForth_Base StarForth_Q48_16
+begin
+
+(* =========================================================================
+   Mirrors: src/word_source/q48_words.c
+   Registers: Q.+ Q.- Q.* Q./ Q.ABS Q.NEG Q.LOG Q.EXP Q.SQRT Q.SIN Q.COS
+              Q.FROM-INT Q.TO-INT Q.1 Q.0 Q.SCALE Q.= Q.< Q.> Q.0=
+              Q.MAX Q.MIN Q.PRINT
+
+   Thin FORTH stack wrappers around the q48_16.h math library. `q48_16_t`
+   is the same 64-bit representation as `cell`/`q48` (StarForth_Base.thy/
+   StarForth_Q48_16.thy) reinterpreted, so most of these words reduce
+   directly to already-modelled q48 operations.
+
+   ── Build-flag stack-safety hazard, distinct from the rest of the sweep ──
+   Every word here pops/pushes via the `VM_POP`/`VM_PUSH` MACROS (include/
+   vm.h:706-719), not a direct `vm_pop`/`vm_push` call the way virtually
+   every other file in this sweep does. Those macros resolve to
+   `vm_pop_fast`/`vm_push_fast` (raw `vm->data_stack[vm->dsp--/++]`, NO
+   bounds check at all) when `STARFORTH_PERFORMANCE` is defined, and to
+   the safe, bounds-checked `vm_pop`/`vm_push` otherwise. This is a
+   genuinely different hazard shape from anything else in the sweep: it
+   isn't a missing guard in this file's own code (the missing-guard
+   pattern from DECAY-RATE@ onward), it's that EVERY guard in this ENTIRE
+   FILE is conditionally compiled away by a build flag most other word
+   files never consult. Modelled below assuming the safe (non-
+   `STARFORTH_PERFORMANCE`) path, consistent with this suite's general
+   assumption that stack words check bounds; the fast-path variant is
+   flagged, not modelled, since "no check at all" has no useful lemma to
+   state beyond "anything can happen."
+
+   ── Q48 operations reused from StarForth_Q48_16.thy ─────────────────────
+   q48_add/q48_sub/q48_mul/q48_div/q48_from_u64/q48_to_u64 were already
+   modelled (q48_sub added there alongside this file, since it's a genuine
+   Q48 arithmetic primitive, not FORTH-word-specific). Q.ABS uses
+   `cell_abs` directly (StarForth_Base.thy) -- q48_abs's raw-bit sign-bit
+   test is bit-for-bit identical to `cell_abs`'s `n <s 0` test, see
+   StarForth_Q48_16.thy's note. Q.=/Q.</Q.>/Q.0=/Q.MAX/Q.MIN use PLAIN
+   (unsigned) word comparison operators, matching the C's direct
+   `uint64_t` `==`/`<`/`>` -- Q48.16 in this codebase is fundamentally an
+   unsigned fixed-point format, unlike `cell`'s general signed
+   two's-complement use elsewhere in this suite.
+
+   ── Scope ─────────────────────────────────────────────────────────────
+   Fully modelled: Q.+, Q.-, Q.*, Q./, Q.ABS, Q.NEG, Q.FROM-INT, Q.TO-INT,
+   Q.1, Q.0, Q.SCALE, Q.=, Q.<, Q.>, Q.0=, Q.MAX, Q.MIN (17 of 23 words).
+   Not modelled: Q.LOG/Q.EXP/Q.SQRT/Q.SIN/Q.COS (the same transcendental
+   approximation functions already excluded from this sweep entirely at
+   q48_16_words.c -- Newton-Raphson/Taylor-series numerical algorithms
+   needing error-bound proofs, a different kind of work than this sweep's
+   plumbing-lemma style) and Q.PRINT (stdout formatting only, no vm_state
+   write beyond its pop).
+   ======================================================================== *)
+
+(* ── Q.+ / Q.- / Q.* / Q./ ( q1 q2 -- q_result ) ──────────────────────── *)
+(* C pops b then a (b is TOS); data_stack list convention: b # a # xs. *)
+
+definition forth_q_add :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_add vm =
+    (case data_stack vm of
+       b # a # xs \<Rightarrow> vm\<lparr>data_stack := q48_add a b # xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+definition forth_q_sub :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_sub vm =
+    (case data_stack vm of
+       b # a # xs \<Rightarrow> vm\<lparr>data_stack := q48_sub a b # xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+definition forth_q_mul :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_mul vm =
+    (case data_stack vm of
+       b # a # xs \<Rightarrow> vm\<lparr>data_stack := q48_mul a b # xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+definition forth_q_div :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_div vm =
+    (case data_stack vm of
+       b # a # xs \<Rightarrow> vm\<lparr>data_stack := q48_div a b # xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma q_add_underflow_nil: "data_stack vm = [] \<Longrightarrow> vm_error (forth_q_add vm)"
+  by (simp add: forth_q_add_def set_error_def)
+lemma q_add_underflow_one: "data_stack vm = [x] \<Longrightarrow> vm_error (forth_q_add vm)"
+  by (simp add: forth_q_add_def set_error_def)
+lemma q_add_normal:
+  assumes "data_stack vm = b # a # xs"
+  shows "data_stack (forth_q_add vm) = q48_add a b # xs"
+  by (simp add: forth_q_add_def assms)
+
+lemma q_sub_normal:
+  assumes "data_stack vm = b # a # xs"
+  shows "data_stack (forth_q_sub vm) = q48_sub a b # xs"
+  by (simp add: forth_q_sub_def assms)
+
+lemma q_mul_normal:
+  assumes "data_stack vm = b # a # xs"
+  shows "data_stack (forth_q_mul vm) = q48_mul a b # xs"
+  by (simp add: forth_q_mul_def assms)
+
+lemma q_div_normal:
+  assumes "data_stack vm = b # a # xs"
+  shows "data_stack (forth_q_div vm) = q48_div a b # xs"
+  by (simp add: forth_q_div_def assms)
+
+lemma q_div_by_zero_is_zero:
+  assumes "data_stack vm = 0 # a # xs"
+  shows "data_stack (forth_q_div vm) = 0 # xs"
+  using assms by (simp add: forth_q_div_def q48_div_def)
+
+(* ── Q.ABS / Q.NEG ( q -- q' ) ─────────────────────────────────────────── *)
+
+definition forth_q_abs :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_abs vm =
+    (case data_stack vm of
+       a # xs \<Rightarrow> vm\<lparr>data_stack := cell_abs a # xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+definition forth_q_neg :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_neg vm =
+    (case data_stack vm of
+       a # xs \<Rightarrow> vm\<lparr>data_stack := -a # xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma q_abs_underflow: "data_stack vm = [] \<Longrightarrow> vm_error (forth_q_abs vm)"
+  by (simp add: forth_q_abs_def set_error_def)
+lemma q_abs_normal:
+  assumes "data_stack vm = a # xs"
+  shows "data_stack (forth_q_abs vm) = cell_abs a # xs"
+  by (simp add: forth_q_abs_def assms)
+
+lemma q_neg_underflow: "data_stack vm = [] \<Longrightarrow> vm_error (forth_q_neg vm)"
+  by (simp add: forth_q_neg_def set_error_def)
+lemma q_neg_normal:
+  assumes "data_stack vm = a # xs"
+  shows "data_stack (forth_q_neg vm) = -a # xs"
+  by (simp add: forth_q_neg_def assms)
+lemma q_neg_involutive:
+  assumes "data_stack vm = a # xs"
+  shows "data_stack (forth_q_neg (forth_q_neg vm)) = a # xs"
+  by (simp add: forth_q_neg_def assms)
+
+(* ── Q.FROM-INT ( n -- q ) / Q.TO-INT ( q -- n ) ──────────────────────── *)
+(* C: Q.FROM-INT clamps negative n to 0 before q48_from_u64 (the C source
+   pops via bare VM_POP, a signed cell_t, then treats negative as 0). *)
+
+definition forth_q_from_int :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_from_int vm =
+    (case data_stack vm of
+       n # xs \<Rightarrow> vm\<lparr>data_stack := q48_from_u64 (if n <s 0 then 0 else n) # xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+definition forth_q_to_int :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_to_int vm =
+    (case data_stack vm of
+       q # xs \<Rightarrow> vm\<lparr>data_stack := q48_to_u64 q # xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma q_from_int_underflow: "data_stack vm = [] \<Longrightarrow> vm_error (forth_q_from_int vm)"
+  by (simp add: forth_q_from_int_def set_error_def)
+lemma q_from_int_negative_clamped:
+  assumes "data_stack vm = n # xs" "n <s 0"
+  shows "data_stack (forth_q_from_int vm) = 0 # xs"
+  using assms by (simp add: forth_q_from_int_def)
+lemma q_from_int_nonneg:
+  assumes "data_stack vm = n # xs" "\<not> n <s 0"
+  shows "data_stack (forth_q_from_int vm) = q48_from_u64 n # xs"
+  using assms by (simp add: forth_q_from_int_def)
+
+lemma q_to_int_underflow: "data_stack vm = [] \<Longrightarrow> vm_error (forth_q_to_int vm)"
+  by (simp add: forth_q_to_int_def set_error_def)
+lemma q_to_int_normal:
+  assumes "data_stack vm = q # xs"
+  shows "data_stack (forth_q_to_int vm) = q48_to_u64 q # xs"
+  by (simp add: forth_q_to_int_def assms)
+
+(* ── Q.1 / Q.0 / Q.SCALE ( -- q ) : constants, no capacity guard ─────────── *)
+(* Like DECAY-RATE@/LOG-ERROR etc, these push with no ds_full check --
+   another instance of the recurring missing-overflow-guard pattern. *)
+
+definition forth_q_one :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_one vm = vm\<lparr>data_stack := Q48_ONE # data_stack vm\<rparr>"
+definition forth_q_zero :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_zero vm = vm\<lparr>data_stack := 0 # data_stack vm\<rparr>"
+definition forth_q_scale :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_scale vm = vm\<lparr>data_stack := Q48_SCALE # data_stack vm\<rparr>"
+
+lemma q_one_pushes: "data_stack (forth_q_one vm) = 65536 # data_stack vm"
+  by (simp add: forth_q_one_def Q48_ONE_def Q48_SCALE_def)
+lemma q_zero_pushes: "data_stack (forth_q_zero vm) = 0 # data_stack vm"
+  by (simp add: forth_q_zero_def)
+lemma q_scale_pushes: "data_stack (forth_q_scale vm) = 65536 # data_stack vm"
+  by (simp add: forth_q_scale_def Q48_SCALE_def)
+lemma q_one_scale_agree: "forth_q_one vm = forth_q_scale vm"
+  by (simp add: forth_q_one_def forth_q_scale_def Q48_ONE_def Q48_SCALE_def)
+
+(* ── Q.= / Q.< / Q.> / Q.0= ( q1 q2 -- flag ) : unsigned comparison ───────── *)
+
+definition forth_q_eq :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_eq vm =
+    (case data_stack vm of
+       b # a # xs \<Rightarrow> vm\<lparr>data_stack := to_forth_bool (a = b) # xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+definition forth_q_lt :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_lt vm =
+    (case data_stack vm of
+       b # a # xs \<Rightarrow> vm\<lparr>data_stack := to_forth_bool (a < b) # xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+definition forth_q_gt :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_gt vm =
+    (case data_stack vm of
+       b # a # xs \<Rightarrow> vm\<lparr>data_stack := to_forth_bool (b < a) # xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+definition forth_q_zero_eq :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_zero_eq vm =
+    (case data_stack vm of
+       a # xs \<Rightarrow> vm\<lparr>data_stack := to_forth_bool (a = 0) # xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma q_eq_normal:
+  assumes "data_stack vm = b # a # xs"
+  shows "data_stack (forth_q_eq vm) = to_forth_bool (a = b) # xs"
+  by (simp add: forth_q_eq_def assms)
+
+lemma q_lt_normal:
+  assumes "data_stack vm = b # a # xs"
+  shows "data_stack (forth_q_lt vm) = to_forth_bool (a < b) # xs"
+  by (simp add: forth_q_lt_def assms)
+
+lemma q_gt_normal:
+  assumes "data_stack vm = b # a # xs"
+  shows "data_stack (forth_q_gt vm) = to_forth_bool (b < a) # xs"
+  by (simp add: forth_q_gt_def assms)
+
+lemma q_zero_eq_normal:
+  assumes "data_stack vm = a # xs"
+  shows "data_stack (forth_q_zero_eq vm) = to_forth_bool (a = 0) # xs"
+  by (simp add: forth_q_zero_eq_def assms)
+
+lemma q_lt_gt_antisymmetric:
+  assumes "data_stack vm1 = b # a # xs" "data_stack vm2 = a # b # xs"
+  shows "data_stack (forth_q_lt vm1) = data_stack (forth_q_gt vm2)"
+  using assms by (simp add: forth_q_lt_def forth_q_gt_def)
+
+(* ── Q.MAX / Q.MIN ( q1 q2 -- q_result ) : unsigned comparison ──────────── *)
+
+definition forth_q_max :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_max vm =
+    (case data_stack vm of
+       b # a # xs \<Rightarrow> vm\<lparr>data_stack := (if b \<le> a then a else b) # xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+definition forth_q_min :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_min vm =
+    (case data_stack vm of
+       b # a # xs \<Rightarrow> vm\<lparr>data_stack := (if a \<le> b then a else b) # xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma q_max_normal:
+  assumes "data_stack vm = b # a # xs"
+  shows "data_stack (forth_q_max vm) = (if b \<le> a then a else b) # xs"
+  by (simp add: forth_q_max_def assms)
+
+lemma q_min_normal:
+  assumes "data_stack vm = b # a # xs"
+  shows "data_stack (forth_q_min vm) = (if a \<le> b then a else b) # xs"
+  by (simp add: forth_q_min_def assms)
+
+lemma q_max_ge_both:
+  assumes "data_stack vm = b # a # xs"
+  shows "a \<le> hd (data_stack (forth_q_max vm))" "b \<le> hd (data_stack (forth_q_max vm))"
+  using assms by (auto simp add: forth_q_max_def)
+
+lemma q_min_le_both:
+  assumes "data_stack vm = b # a # xs"
+  shows "hd (data_stack (forth_q_min vm)) \<le> a" "hd (data_stack (forth_q_min vm)) \<le> b"
+  using assms by (auto simp add: forth_q_min_def)
+
+(* ── Q.LOG / Q.EXP / Q.SQRT / Q.SIN / Q.COS -- NOT MODELLED ──────────────── *)
+
+lemma q_log_not_modelled: True  \<comment> \<open>q48_log_approx: Newton-Raphson, same excluded class as q48_16_words.c's transcendentals (see that file's sweep-skip note).\<close>
+  by simp
+lemma q_exp_not_modelled: True  \<comment> \<open>q48_exp_approx: Taylor series.\<close>
+  by simp
+lemma q_sqrt_not_modelled: True \<comment> \<open>q48_sqrt_approx: Newton-Raphson.\<close>
+  by simp
+lemma q_sin_not_modelled: True  \<comment> \<open>q48_sin_approx: Taylor series.\<close>
+  by simp
+lemma q_cos_not_modelled: True  \<comment> \<open>q48_cos_approx: Taylor series.\<close>
+  by simp
+
+(* ── Q.PRINT ( q -- ) : pop + stdout, no further vm_state effect ────────── *)
+
+definition forth_q_print :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_print vm =
+    (case data_stack vm of
+       q # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma q_print_underflow: "data_stack vm = [] \<Longrightarrow> vm_error (forth_q_print vm)"
+  by (simp add: forth_q_print_def set_error_def)
+lemma q_print_pops_one:
+  assumes "data_stack vm = q # xs"
+  shows "data_stack (forth_q_print vm) = xs"
+  by (simp add: forth_q_print_def assms)
+
+(* ── Fast-path (STARFORTH_PERFORMANCE) variant -- NOT MODELLED ───────────── *)
+
+lemma fast_path_variant_not_modelled: True
+  \<comment> \<open>See file header -- when STARFORTH_PERFORMANCE is defined, every word
+     above uses vm_pop_fast/vm_push_fast with NO bounds check at all, so
+     none of the underflow lemmas above apply; there is no meaningful
+     positive statement to make about that build configuration beyond
+     "unchecked".\<close>
+  by simp
+
+end