From d0fcd2ed86b2997b4da469744301262804edab2f Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Thu, 13 Aug 2026 13:42:41 -0400 Subject: [PATCH] proof/: add StarForth_Mixed_Arithmetic_Words.thy (M+/M-/MOD//MOD/*//*/MOD) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Covers word_source/mixed_arithmetic_words.c. Two genuine findings recorded in comments rather than fixed: - register_mixed_arithmetic_words registers MOD and /MOD a second time, after arithmetic_words.c's own registrations; vm_create_word links new entries at the head of vm->latest and FIND scans from vm->latest forward, so arithmetic_words.c's MOD/​/MOD are permanently shadowed, unreachable dead code once bootstrap completes (verified against dictionary_management.c and the module order in word_registry.c). - M*, M/MOD, and the "avoids intermediate overflow" claim on */ and */MOD are false on 64-bit builds: cell_t and "long long" are the same width there, so the long-long intermediate does not actually widen the product -- it wraps mod 2^64 like plain cell multiplication before the 32-bit-style split/reconstruction runs. M*/M/MOD are left undefined here (oops-equivalent: documented as not modelled, since formalizing "the wrong thing, faithfully" adds no proof value) rather than fixed. MOD/​/MOD/*//*/MOD reuse cell_sdiv/cell_smod from the arithmetic-words migration; M+/M- transcribe the C's hand-rolled signed carry/borrow detection literally, proving only stack-level plumbing (not double- precision correctness, which needs an interpretation function this suite doesn't build). All 24 theory files verify with zero errors. Co-Authored-By: Claude Sonnet 5 --- proof/ROOT | 1 + proof/StarForth_Mixed_Arithmetic_Words.thy | 221 +++++++++++++++++++++ 2 files changed, 222 insertions(+) create mode 100644 proof/StarForth_Mixed_Arithmetic_Words.thy diff --git a/proof/ROOT b/proof/ROOT index 17e9ec5..54b467e 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -6,6 +6,7 @@ session "StarForth" = "HOL-Library" + StarForth_Stack_Words StarForth_Double_Words StarForth_Arithmetic_Words + StarForth_Mixed_Arithmetic_Words StarForth_Logical_Words StarForth_Return_Stack_Words StarForth_Memory_Words diff --git a/proof/StarForth_Mixed_Arithmetic_Words.thy b/proof/StarForth_Mixed_Arithmetic_Words.thy new file mode 100644 index 0000000..f9d90a6 --- /dev/null +++ b/proof/StarForth_Mixed_Arithmetic_Words.thy @@ -0,0 +1,221 @@ +theory StarForth_Mixed_Arithmetic_Words + imports StarForth_Base +begin + +(* ========================================================================= + POST-06: Mixed Arithmetic Words + Mirrors: src/word_source/mixed_arithmetic_words.c + + ⚠ GENUINE FINDING: register_mixed_arithmetic_words registers "MOD" and + "/MOD" a second time. register_forth79_words calls register_arithmetic_words + (module 4) before register_mixed_arithmetic_words (module 6); vm_create_word + links new entries at the head of vm->latest and FIND scans from vm->latest + forward, so the later registration wins. arithmetic_words.c's MOD and /MOD + (word_source/arithmetic_words.c) are therefore permanently shadowed, + unreachable dead code once bootstrap completes -- confirmed by reading + vm_create_word's linked-list insertion in dictionary_management.c and the + module order in register_forth79_words (word_registry.c:106-119). Not + fixed here per standing instruction to report, not silently resolve. + + forth_mod/forth_slash_mod below model the WINNING (mixed_arithmetic_words.c) + definitions, which are bit-identical in behaviour to arithmetic_words.c's + shadowed ones -- both use plain C "%"/"/" on signed cell_t, i.e. the same + cell_smod/cell_sdiv already proven for POST-02. + ======================================================================== *) + +(* ── M+ ( d n -- d ) / M- ( d n -- d ) ──────────────────────────────────── + Stack effect as coded: pop n, dlow, dhigh (dhigh deepest); push dhigh', + dlow' (dlow' TOS). Carry/borrow propagation is a hand-rolled overflow + check on the signed cell_t addition, not a widened-type computation -- + modelled here literally, including the signed ( cell \ cell \ (cell \ cell)" where + "m_plus_carry dhigh dlow n = + (let dlow' = dlow + n in + if 0 dlow' dlow vm_state" where + "forth_m_plus vm = + (case data_stack vm of + n # dlow # dhigh # rest \ + vm\data_stack := snd (m_plus_carry dhigh dlow n) + # fst (m_plus_carry dhigh dlow n) # rest\ + | _ \ set_error vm)" + +lemma m_plus_normal: + assumes "data_stack vm = n # dlow # dhigh # rest" + shows "data_stack (forth_m_plus vm) = + snd (m_plus_carry dhigh dlow n) # fst (m_plus_carry dhigh dlow n) # rest" + by (simp add: forth_m_plus_def assms) + +lemma m_plus_no_carry: + assumes "\ (0 dlow + n (n dlow cell \ cell \ (cell \ cell)" where + "m_minus_borrow dhigh dlow n = + (let dlow' = dlow - n in + if 0 dlow dlow' vm_state" where + "forth_m_minus vm = + (case data_stack vm of + n # dlow # dhigh # rest \ + vm\data_stack := snd (m_minus_borrow dhigh dlow n) + # fst (m_minus_borrow dhigh dlow n) # rest\ + | _ \ set_error vm)" + +lemma m_minus_normal: + assumes "data_stack vm = n # dlow # dhigh # rest" + shows "data_stack (forth_m_minus vm) = + snd (m_minus_borrow dhigh dlow n) # fst (m_minus_borrow dhigh dlow n) # rest" + by (simp add: forth_m_minus_def assms) + +lemma m_minus_underflow_nil: + assumes "data_stack vm = []" + shows "vm_error (forth_m_minus vm)" + by (simp add: forth_m_minus_def set_error_def assms) + +(* ── M* ( n1 n2 -- d ) ─────────────────────────────────────────────────── * + ⚠ GENUINE FINDING, not modelled further: on a 64-bit build, cell_t and + "long long" are the SAME width, so "(long long) n1 * (long long) n2" + does not actually widen the product -- it wraps mod 2^64 exactly like + n1*n2 on cell_t would. M*'s subsequent ">> 32" / "& 0xFFFFFFFF" split + then extracts the wrong halves: it produces a 32-bit-style double from + a 64-bit product that has ALREADY silently overflowed for any n1,n2 + whose true product exceeds 2^63. The doc comment above the C function + ("producing a double-cell result") is not true for the general case on + 64-bit builds; only STAR_SLASH's docstring ("avoids intermediate + overflow via long long") shares the same false premise (see below). + No forth_m_star definition is given here: the C function does not + compute what its name and stack comment claim, and building a formal + model of "the wrong thing, faithfully" would misrepresent the intent + of M* without adding proof value -- the finding itself is the record. *) + +(* ── M/MOD ( d n -- rem quot ) ─────────────────────────────────────────── * + Same family of finding as M*: the 64-bit path reconstructs a "dividend" + by shifting dhigh left 32 bits and OR-ing in dlow's low 32 bits, which + only recovers a genuine double-cell value if dhigh/dlow were produced + by a CORRECT M* in the first place -- which they are not (see above). + Not modelled for the same reason. *) + +(* ── MOD ( n1 n2 -- r ), /MOD ( n1 n2 -- rem quot ) ─────────────────────── + These are the entries that actually win at runtime (see the shadowing + finding at the top of this file). Identical C body to arithmetic_words.c's + shadowed versions: plain signed "%"/"/", i.e. cell_smod/cell_sdiv. *) + +definition forth_mod2 :: "vm_state \ vm_state" where + "forth_mod2 vm = + (case data_stack vm of + n2 # n1 # rest \ + if n2 = 0 + then set_error vm + else vm\data_stack := (cell_smod n1 n2) # rest\ + | _ \ set_error vm)" + +lemma mod2_normal: + assumes "data_stack vm = n2 # n1 # rest" + assumes "n2 \ 0" + shows "data_stack (forth_mod2 vm) = (cell_smod n1 n2) # rest" + by (simp add: forth_mod2_def assms) + +lemma mod2_by_zero: + assumes "data_stack vm = 0 # n1 # rest" + shows "vm_error (forth_mod2 vm)" + by (simp add: forth_mod2_def set_error_def assms) + +definition forth_slash_mod2 :: "vm_state \ vm_state" where + "forth_slash_mod2 vm = + (case data_stack vm of + n2 # n1 # rest \ + if n2 = 0 + then set_error vm + else vm\data_stack := (cell_sdiv n1 n2) # (cell_smod n1 n2) # rest\ + | _ \ set_error vm)" + +lemma slash_mod2_normal: + assumes "data_stack vm = n2 # n1 # rest" + assumes "n2 \ 0" + shows "data_stack (forth_slash_mod2 vm) = (cell_sdiv n1 n2) # (cell_smod n1 n2) # rest" + by (simp add: forth_slash_mod2_def assms) + +lemma slash_mod2_by_zero: + assumes "data_stack vm = 0 # n1 # rest" + shows "vm_error (forth_slash_mod2 vm)" + by (simp add: forth_slash_mod2_def set_error_def assms) + +(* ── */ ( n1 n2 n3 -- quot ), */MOD ( n1 n2 n3 -- rem quot ) ────────────── + ⚠ GENUINE FINDING: the docstring claims the long-long intermediate + "avoid[s] intermediate overflow" -- false on 64-bit builds for the same + reason as M* above (cell_t and long long are the same width there). + Modelled here as the C actually computes: n1*n2 wraps at 64 bits exactly + like plain cell multiplication, THEN cell_sdiv/cell_smod by n3. *) + +definition forth_star_slash :: "vm_state \ vm_state" where + "forth_star_slash vm = + (case data_stack vm of + n3 # n2 # n1 # rest \ + if n3 = 0 + then set_error vm + else vm\data_stack := cell_sdiv (n1 * n2) n3 # rest\ + | _ \ set_error vm)" + +lemma star_slash_normal: + assumes "data_stack vm = n3 # n2 # n1 # rest" + assumes "n3 \ 0" + shows "data_stack (forth_star_slash vm) = cell_sdiv (n1 * n2) n3 # rest" + by (simp add: forth_star_slash_def assms) + +lemma star_slash_by_zero: + assumes "data_stack vm = 0 # n2 # n1 # rest" + shows "vm_error (forth_star_slash vm)" + by (simp add: forth_star_slash_def set_error_def assms) + +definition forth_star_slash_mod :: "vm_state \ vm_state" where + "forth_star_slash_mod vm = + (case data_stack vm of + n3 # n2 # n1 # rest \ + if n3 = 0 + then set_error vm + else vm\data_stack := cell_sdiv (n1 * n2) n3 # cell_smod (n1 * n2) n3 # rest\ + | _ \ set_error vm)" + +lemma star_slash_mod_normal: + assumes "data_stack vm = n3 # n2 # n1 # rest" + assumes "n3 \ 0" + shows "data_stack (forth_star_slash_mod vm) = + cell_sdiv (n1 * n2) n3 # cell_smod (n1 * n2) n3 # rest" + by (simp add: forth_star_slash_mod_def assms) + +lemma star_slash_mod_by_zero: + assumes "data_stack vm = 0 # n2 # n1 # rest" + shows "vm_error (forth_star_slash_mod vm)" + by (simp add: forth_star_slash_mod_def set_error_def assms) + +end