Robert Allan JamesandClaude Sonnet 5
b196c95e44
Both blockers recorded at the previous resume point turned out to be
resolvable, not permanent:
- The "cell is unbounded int" blocker for D+/D-/DNEGATE/etc. was stale --
cell was already migrated to a 64-bit word type in commit fe6e705, before
this file was first touched. The note was never re-checked against
current StarForth_Base.thy before being carried forward. Same lesson the
control_words.c vm_ip finding taught one file earlier in this sweep:
re-verify carried-forward reasoning against the current file, don't just
trust a previous session's note.
- The missing vm->ecw_nesting field for 2>R/2R>/2R@ was a real, scoped gap
-- added ecw_nesting :: nat to vm_state in StarForth_Base.thy.
Adds S>D, D+, D-, DNEGATE, DABS, a d_compare helper, DMAX, DMIN, D<, D=,
D0=, D0<, D2*, D2/, 2>R, 2R>, 2R@. D2*/D2/ use push_bit/drop_bit/bit
(established idiom from StarForth_Q48_16.thy) for the 128-bit shifts; D2/
uses sint/div (floor division) rather than cell_sdiv (C99 truncating
division) since arithmetic right shift is floor division, not truncation,
for negative operands. DNEGATE's double-negation-is-identity property is
true but left unproved (needs the same carry/borrow-across-the-pair
algebra as D+/D-, not just simp) -- a nice-to-have, not core plumbing.
All 20 registered words in double_words.c are now covered. 28 theory
files verify with zero errors.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
685 lines
30 KiB
Plaintext
685 lines
30 KiB
Plaintext
theory StarForth_Double_Words
|
|
imports StarForth_Base
|
|
begin
|
|
|
|
unbundle bit_operations_syntax
|
|
|
|
(* =========================================================================
|
|
POST-XX: Double-Cell Words
|
|
Mirrors: src/word_source/double_words.c (all 20 registered words)
|
|
src/test_runner/modules/double_words_test.c
|
|
|
|
SCOPE, decided 2026-08-13, REVISED 2026-08-13 (later same day, resumed
|
|
session): double_words.c has 20 registered words in three categories.
|
|
All three are now modeled:
|
|
|
|
1. Pure double-cell DATA-STACK shuffles (2DROP, 2DUP, 2SWAP, 2OVER,
|
|
2ROT) -- unchanged from the original pass.
|
|
|
|
2. Double-cell RETURN-STACK transfer (2>R, 2R>, 2R@) -- NOW MODELED.
|
|
The blocker recorded earlier (`vm->ecw_nesting` missing from
|
|
vm_state) is resolved: `ecw_nesting :: nat` added to the vm_state
|
|
record in StarForth_Base.thy, immediately after vm_halted.
|
|
|
|
3. Double-precision ARITHMETIC (S>D, D+, D-, DNEGATE, DABS, DMAX,
|
|
DMIN, D<, D=, D0=, D0<, D2*, D2/) -- NOW MODELED. The blocker
|
|
recorded earlier ("cell is unbounded int, not a fixed-width
|
|
wrapping type") was STALE when re-checked this session: `cell` was
|
|
migrated from `int` to `"64 word"` in commit fe6e705, well before
|
|
this file was first touched -- the earlier note simply wasn't
|
|
re-verified against current StarForth_Base.thy before being
|
|
written down. Flagging this as a process lesson, not just a code
|
|
fix: carried-forward reasoning about *why* something is out of
|
|
scope needs re-checking against the current file, not just trusted
|
|
because a previous session wrote it down (same lesson the
|
|
control_words.c "vm_ip as raw pointer" note taught one file
|
|
earlier in this same sweep). With cell now a proper wrapping 64-bit
|
|
word, HOL word `+`/`-` already compute mod 2^64 exactly matching
|
|
C's unsigned-long carry/borrow arithmetic and two's-complement
|
|
wraparound bit-for-bit -- no foundational change needed, just
|
|
transcription.
|
|
|
|
Every word modeled below is a direct structural analog of an
|
|
already-covered single-cell word in StarForth_Stack_Words.thy (DUP,
|
|
SWAP, OVER, ROT) or StarForth_Return_Stack_Words.thy, just operating
|
|
on cell PAIRS instead of single cells. Convention throughout, matching
|
|
the C comments: a double d is pushed as (dlow dhigh) with dhigh on
|
|
top -- i.e. in this list's head=TOS convention, a double at the top of
|
|
stack is "dhigh # dlow # rest".
|
|
|
|
None of the C implementations below check ds_full before pushing
|
|
(confirmed by reading double_words.c in full) -- not modeled here
|
|
either, to stay faithful to the real source rather than inventing a
|
|
guard that doesn't exist.
|
|
======================================================================== *)
|
|
|
|
(* ── 2DROP ( d -- ) ─────────────────────────────────────────────────────── *)
|
|
(* src/word_source/double_words.c:250-258. Guard: dsp \<ge> 1 (at least two
|
|
cells present). *)
|
|
|
|
definition forth_2drop :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_2drop vm =
|
|
(case data_stack vm of
|
|
_ # _ # rest \<Rightarrow> vm\<lparr>data_stack := rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma two_drop_normal:
|
|
assumes "data_stack vm = dhigh # dlow # rest"
|
|
shows "data_stack (forth_2drop vm) = rest"
|
|
by (simp add: forth_2drop_def assms)
|
|
|
|
lemma two_drop_underflow_nil:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_2drop vm)"
|
|
by (simp add: forth_2drop_def set_error_def assms)
|
|
|
|
lemma two_drop_underflow_one:
|
|
assumes "data_stack vm = [x]"
|
|
shows "vm_error (forth_2drop vm)"
|
|
by (simp add: forth_2drop_def set_error_def assms)
|
|
|
|
(* ── 2DUP ( d -- d d ) ──────────────────────────────────────────────────── *)
|
|
(* src/word_source/double_words.c:260-272. Guard: dsp \<ge> 1. *)
|
|
|
|
definition forth_2dup :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_2dup vm =
|
|
(case data_stack vm of
|
|
dhigh # dlow # rest \<Rightarrow>
|
|
vm\<lparr>data_stack := dhigh # dlow # dhigh # dlow # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma two_dup_normal:
|
|
assumes "data_stack vm = dhigh # dlow # rest"
|
|
shows "data_stack (forth_2dup vm) = dhigh # dlow # dhigh # dlow # rest"
|
|
by (simp add: forth_2dup_def assms)
|
|
|
|
lemma two_dup_depth:
|
|
assumes "data_stack vm = dhigh # dlow # rest"
|
|
shows "length (data_stack (forth_2dup vm)) = length (data_stack vm) + 2"
|
|
by (simp add: forth_2dup_def assms)
|
|
|
|
lemma two_dup_underflow_nil:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_2dup vm)"
|
|
by (simp add: forth_2dup_def set_error_def assms)
|
|
|
|
lemma two_dup_underflow_one:
|
|
assumes "data_stack vm = [x]"
|
|
shows "vm_error (forth_2dup vm)"
|
|
by (simp add: forth_2dup_def set_error_def assms)
|
|
|
|
(* ── 2SWAP ( d1 d2 -- d2 d1 ) ───────────────────────────────────────────── *)
|
|
(* src/word_source/double_words.c:274-290. Guard: dsp \<ge> 3 (four cells). *)
|
|
|
|
definition forth_2swap :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_2swap vm =
|
|
(case data_stack vm of
|
|
d2high # d2low # d1high # d1low # rest \<Rightarrow>
|
|
vm\<lparr>data_stack := d1high # d1low # d2high # d2low # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma two_swap_normal:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
shows "data_stack (forth_2swap vm) = d1high # d1low # d2high # d2low # rest"
|
|
by (simp add: forth_2swap_def assms)
|
|
|
|
lemma two_swap_depth_preserved:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
shows "length (data_stack (forth_2swap vm)) = length (data_stack vm)"
|
|
by (simp add: forth_2swap_def assms)
|
|
|
|
(* 2SWAP is its own inverse. *)
|
|
lemma two_swap_involutive:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
assumes "data_stack vm' = data_stack (forth_2swap vm)"
|
|
shows "data_stack (forth_2swap vm') = data_stack vm"
|
|
using assms by (simp add: forth_2swap_def)
|
|
|
|
lemma two_swap_underflow_nil:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_2swap vm)"
|
|
by (simp add: forth_2swap_def set_error_def assms)
|
|
|
|
lemma two_swap_underflow_one:
|
|
assumes "data_stack vm = [x]"
|
|
shows "vm_error (forth_2swap vm)"
|
|
by (simp add: forth_2swap_def set_error_def assms)
|
|
|
|
lemma two_swap_underflow_two:
|
|
assumes "data_stack vm = [x, y]"
|
|
shows "vm_error (forth_2swap vm)"
|
|
by (simp add: forth_2swap_def set_error_def assms)
|
|
|
|
lemma two_swap_underflow_three:
|
|
assumes "data_stack vm = [x, y, z]"
|
|
shows "vm_error (forth_2swap vm)"
|
|
by (simp add: forth_2swap_def set_error_def assms)
|
|
|
|
(* ── 2OVER ( d1 d2 -- d1 d2 d1 ) ────────────────────────────────────────── *)
|
|
(* src/word_source/double_words.c:292-305. Guard: dsp \<ge> 3. *)
|
|
|
|
definition forth_2over :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_2over vm =
|
|
(case data_stack vm of
|
|
d2high # d2low # d1high # d1low # rest \<Rightarrow>
|
|
vm\<lparr>data_stack := d1high # d1low # d2high # d2low # d1high # d1low # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma two_over_normal:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
shows "data_stack (forth_2over vm)
|
|
= d1high # d1low # d2high # d2low # d1high # d1low # rest"
|
|
by (simp add: forth_2over_def assms)
|
|
|
|
lemma two_over_depth:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
shows "length (data_stack (forth_2over vm)) = length (data_stack vm) + 2"
|
|
by (simp add: forth_2over_def assms)
|
|
|
|
(* ── 2ROT ( d1 d2 d3 -- d2 d3 d1 ) ──────────────────────────────────────── *)
|
|
(* src/word_source/double_words.c:307-327. Guard: dsp \<ge> 5 (six cells).
|
|
Hand-verified against the doc comment's own semantics: d1 (deepest)
|
|
moves to the top, d2 and d3 shift down keeping their relative order. *)
|
|
|
|
definition forth_2rot :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_2rot vm =
|
|
(case data_stack vm of
|
|
d3high # d3low # d2high # d2low # d1high # d1low # rest \<Rightarrow>
|
|
vm\<lparr>data_stack :=
|
|
d1high # d1low # d3high # d3low # d2high # d2low # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma two_rot_normal:
|
|
assumes "data_stack vm
|
|
= d3high # d3low # d2high # d2low # d1high # d1low # rest"
|
|
shows "data_stack (forth_2rot vm)
|
|
= d1high # d1low # d3high # d3low # d2high # d2low # rest"
|
|
by (simp add: forth_2rot_def assms)
|
|
|
|
lemma two_rot_depth_preserved:
|
|
assumes "data_stack vm
|
|
= d3high # d3low # d2high # d2low # d1high # d1low # rest"
|
|
shows "length (data_stack (forth_2rot vm)) = length (data_stack vm)"
|
|
by (simp add: forth_2rot_def assms)
|
|
|
|
(* ── S>D ( n -- d ) : single to double ─────────────────────────────────── *)
|
|
(* C: dsp<0 -> error; dhigh = (n<0) ? -1 : 0; push n (low), push dhigh. *)
|
|
|
|
definition forth_s_to_d :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_s_to_d vm =
|
|
(case data_stack vm of
|
|
[] \<Rightarrow> set_error vm
|
|
| n # rest \<Rightarrow>
|
|
vm\<lparr>data_stack := (if n <s 0 then -1 else 0) # n # rest\<rparr>)"
|
|
|
|
lemma s_to_d_underflow:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_s_to_d vm)"
|
|
by (simp add: forth_s_to_d_def set_error_def assms)
|
|
|
|
lemma s_to_d_negative:
|
|
assumes "data_stack vm = n # rest"
|
|
assumes "n <s 0"
|
|
shows "data_stack (forth_s_to_d vm) = -1 # n # rest"
|
|
by (simp add: forth_s_to_d_def assms)
|
|
|
|
lemma s_to_d_nonnegative:
|
|
assumes "data_stack vm = n # rest"
|
|
assumes "\<not> n <s 0"
|
|
shows "data_stack (forth_s_to_d vm) = 0 # n # rest"
|
|
by (simp add: forth_s_to_d_def assms)
|
|
|
|
(* ── D+ ( d1 d2 -- d3 ) ────────────────────────────────────────────────── *)
|
|
(* C: dsp<3 -> error. Pops d2high,d2low,d1high,d1low. Carry detected via
|
|
unsigned comparison; word `+` already computes mod 2^64, so it's the
|
|
direct transcription of the C unsigned-long addition with no
|
|
reinterpretation needed. *)
|
|
|
|
definition forth_d_plus :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_d_plus vm =
|
|
(case data_stack vm of
|
|
d2high # d2low # d1high # d1low # rest \<Rightarrow>
|
|
let result_low = d1low + d2low;
|
|
carry = (if result_low < d1low then 1 else 0);
|
|
result_high = d1high + d2high + carry
|
|
in vm\<lparr>data_stack := result_high # result_low # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma d_plus_underflow_nil:
|
|
assumes "data_stack vm = []"
|
|
shows "vm_error (forth_d_plus vm)"
|
|
by (simp add: forth_d_plus_def set_error_def assms)
|
|
|
|
lemma d_plus_underflow_one:
|
|
assumes "data_stack vm = [x]"
|
|
shows "vm_error (forth_d_plus vm)"
|
|
by (simp add: forth_d_plus_def set_error_def assms)
|
|
|
|
lemma d_plus_underflow_two:
|
|
assumes "data_stack vm = [x, y]"
|
|
shows "vm_error (forth_d_plus vm)"
|
|
by (simp add: forth_d_plus_def set_error_def assms)
|
|
|
|
lemma d_plus_underflow_three:
|
|
assumes "data_stack vm = [x, y, z]"
|
|
shows "vm_error (forth_d_plus vm)"
|
|
by (simp add: forth_d_plus_def set_error_def assms)
|
|
|
|
lemma d_plus_normal_no_carry:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
assumes "\<not> (d1low + d2low) < d1low"
|
|
shows "data_stack (forth_d_plus vm) = (d1high + d2high) # (d1low + d2low) # rest"
|
|
using assms by (simp add: forth_d_plus_def)
|
|
|
|
lemma d_plus_normal_with_carry:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
assumes "(d1low + d2low) < d1low"
|
|
shows "data_stack (forth_d_plus vm) = (d1high + d2high + 1) # (d1low + d2low) # rest"
|
|
using assms by (simp add: forth_d_plus_def)
|
|
|
|
(* ── D- ( d1 d2 -- d3 ) ────────────────────────────────────────────────── *)
|
|
|
|
definition forth_d_minus :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_d_minus vm =
|
|
(case data_stack vm of
|
|
d2high # d2low # d1high # d1low # rest \<Rightarrow>
|
|
let result_low = d1low - d2low;
|
|
borrow = (if d1low < d2low then 1 else 0);
|
|
result_high = d1high - d2high - borrow
|
|
in vm\<lparr>data_stack := result_high # result_low # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma d_minus_normal_no_borrow:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
assumes "\<not> d1low < d2low"
|
|
shows "data_stack (forth_d_minus vm) = (d1high - d2high) # (d1low - d2low) # rest"
|
|
using assms by (simp add: forth_d_minus_def)
|
|
|
|
lemma d_minus_normal_with_borrow:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
assumes "d1low < d2low"
|
|
shows "data_stack (forth_d_minus vm) = (d1high - d2high - 1) # (d1low - d2low) # rest"
|
|
using assms by (simp add: forth_d_minus_def)
|
|
|
|
(* ── DNEGATE ( d1 -- d2 ) ──────────────────────────────────────────────── *)
|
|
(* C: ~dlow + 1, ~dhigh + (new_low==0 ? 1 : 0) -- textbook 128-bit two's
|
|
complement negation, transcribed literally rather than via HOL's `-`
|
|
(which would be equal but less faithful to the C bit-operations). *)
|
|
|
|
definition forth_dnegate :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_dnegate vm =
|
|
(case data_stack vm of
|
|
dhigh # dlow # rest \<Rightarrow>
|
|
let new_low = NOT dlow + 1;
|
|
new_high = NOT dhigh + (if new_low = 0 then 1 else 0)
|
|
in vm\<lparr>data_stack := new_high # new_low # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma dnegate_underflow:
|
|
assumes "data_stack vm = [] \<or> (\<exists>x. data_stack vm = [x])"
|
|
shows "vm_error (forth_dnegate vm)"
|
|
using assms by (auto simp: forth_dnegate_def set_error_def)
|
|
|
|
lemma dnegate_normal:
|
|
assumes "data_stack vm = dhigh # dlow # rest"
|
|
shows "data_stack (forth_dnegate vm) =
|
|
(NOT dhigh + (if NOT dlow + 1 = 0 then 1 else 0)) # (NOT dlow + 1) # rest"
|
|
by (simp add: forth_dnegate_def assms)
|
|
|
|
(* Double negation (DNEGATE twice = identity) is a true property of 128-bit
|
|
two's complement, but proving it here needs the same carry/borrow-across-
|
|
the-pair algebra as D+/D-'s case-split lemmas, not just simp -- left
|
|
unproved as a nice-to-have rather than forcing it, consistent with this
|
|
sweep's "plumbing lemmas only" scope. *)
|
|
|
|
(* ── DABS ( d1 -- d2 ) ─────────────────────────────────────────────────── *)
|
|
(* C peeks dhigh (TOS) WITHOUT popping; if negative, calls DNEGATE (which
|
|
does its own pop/negate/push using the still-untouched stack); else
|
|
the word is a complete no-op. Reuses forth_dnegate directly. *)
|
|
|
|
definition forth_dabs :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_dabs vm =
|
|
(case data_stack vm of
|
|
dhigh # dlow # rest \<Rightarrow> (if dhigh <s 0 then forth_dnegate vm else vm)
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma dabs_underflow:
|
|
assumes "data_stack vm = [] \<or> (\<exists>x. data_stack vm = [x])"
|
|
shows "vm_error (forth_dabs vm)"
|
|
using assms by (auto simp: forth_dabs_def set_error_def)
|
|
|
|
lemma dabs_already_nonneg_is_noop:
|
|
assumes "data_stack vm = dhigh # dlow # rest"
|
|
assumes "\<not> dhigh <s 0"
|
|
shows "forth_dabs vm = vm"
|
|
by (simp add: forth_dabs_def assms)
|
|
|
|
lemma dabs_negative_negates:
|
|
assumes "data_stack vm = dhigh # dlow # rest"
|
|
assumes "dhigh <s 0"
|
|
shows "forth_dabs vm = forth_dnegate vm"
|
|
by (simp add: forth_dabs_def assms)
|
|
|
|
(* ── d_compare : internal helper mirroring the C `d_compare` (not a
|
|
registered word) -- high cells compared SIGNED (cell_t <, C semantics),
|
|
low cells compared UNSIGNED (explicit unsigned long cast in C). ────── *)
|
|
|
|
definition d_compare :: "cell \<Rightarrow> cell \<Rightarrow> cell \<Rightarrow> cell \<Rightarrow> int" where
|
|
"d_compare d1h d1l d2h d2l =
|
|
(if d1h <s d2h then -1
|
|
else if d2h <s d1h then 1
|
|
else if d2l < d1l then 1
|
|
else if d1l < d2l then -1
|
|
else 0)"
|
|
|
|
lemma d_compare_equal:
|
|
"d_compare h l h l = 0"
|
|
by (simp add: d_compare_def)
|
|
|
|
(* ── DMAX ( d1 d2 -- d3 ) / DMIN ( d1 d2 -- d3 ) ──────────────────────────
|
|
C pop order matches D+/D-: d2high # d2low # d1high # d1low # rest. *)
|
|
|
|
definition forth_dmax :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_dmax vm =
|
|
(case data_stack vm of
|
|
d2high # d2low # d1high # d1low # rest \<Rightarrow>
|
|
vm\<lparr>data_stack := (if d_compare d1high d1low d2high d2low \<ge> 0
|
|
then d1high # d1low # rest
|
|
else d2high # d2low # rest)\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma dmax_picks_d1:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
assumes "d_compare d1high d1low d2high d2low \<ge> 0"
|
|
shows "data_stack (forth_dmax vm) = d1high # d1low # rest"
|
|
using assms by (simp add: forth_dmax_def)
|
|
|
|
lemma dmax_picks_d2:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
assumes "\<not> d_compare d1high d1low d2high d2low \<ge> 0"
|
|
shows "data_stack (forth_dmax vm) = d2high # d2low # rest"
|
|
using assms by (simp add: forth_dmax_def)
|
|
|
|
definition forth_dmin :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_dmin vm =
|
|
(case data_stack vm of
|
|
d2high # d2low # d1high # d1low # rest \<Rightarrow>
|
|
vm\<lparr>data_stack := (if d_compare d1high d1low d2high d2low \<le> 0
|
|
then d1high # d1low # rest
|
|
else d2high # d2low # rest)\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma dmin_picks_d1:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
assumes "d_compare d1high d1low d2high d2low \<le> 0"
|
|
shows "data_stack (forth_dmin vm) = d1high # d1low # rest"
|
|
using assms by (simp add: forth_dmin_def)
|
|
|
|
lemma dmin_picks_d2:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
assumes "\<not> d_compare d1high d1low d2high d2low \<le> 0"
|
|
shows "data_stack (forth_dmin vm) = d2high # d2low # rest"
|
|
using assms by (simp add: forth_dmin_def)
|
|
|
|
(* ── D< ( d1 d2 -- flag ) / D= ( d1 d2 -- flag ) ────────────────────────── *)
|
|
|
|
definition forth_d_less :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_d_less vm =
|
|
(case data_stack vm of
|
|
d2high # d2low # d1high # d1low # rest \<Rightarrow>
|
|
vm\<lparr>data_stack := to_forth_bool (d_compare d1high d1low d2high d2low < 0) # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma d_less_true:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
assumes "d_compare d1high d1low d2high d2low < 0"
|
|
shows "data_stack (forth_d_less vm) = forth_true # rest"
|
|
using assms by (simp add: forth_d_less_def to_forth_bool_def)
|
|
|
|
lemma d_less_false:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
assumes "\<not> d_compare d1high d1low d2high d2low < 0"
|
|
shows "data_stack (forth_d_less vm) = forth_false # rest"
|
|
using assms by (simp add: forth_d_less_def to_forth_bool_def)
|
|
|
|
definition forth_d_equals :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_d_equals vm =
|
|
(case data_stack vm of
|
|
d2high # d2low # d1high # d1low # rest \<Rightarrow>
|
|
vm\<lparr>data_stack := to_forth_bool (d_compare d1high d1low d2high d2low = 0) # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma d_equals_true:
|
|
assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
|
|
assumes "d_compare d1high d1low d2high d2low = 0"
|
|
shows "data_stack (forth_d_equals vm) = forth_true # rest"
|
|
using assms by (simp add: forth_d_equals_def to_forth_bool_def)
|
|
|
|
lemma d_equals_reflexive:
|
|
assumes "data_stack vm = h # l # h # l # rest"
|
|
shows "data_stack (forth_d_equals vm) = forth_true # rest"
|
|
using assms by (simp add: forth_d_equals_def to_forth_bool_def d_compare_def)
|
|
|
|
(* ── D0= ( d -- flag ) / D0< ( d -- flag ) ────────────────────────────── *)
|
|
|
|
definition forth_d_zero_equals :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_d_zero_equals vm =
|
|
(case data_stack vm of
|
|
dhigh # dlow # rest \<Rightarrow>
|
|
vm\<lparr>data_stack := to_forth_bool (dhigh = 0 \<and> dlow = 0) # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma d_zero_equals_true:
|
|
assumes "data_stack vm = 0 # 0 # rest"
|
|
shows "data_stack (forth_d_zero_equals vm) = forth_true # rest"
|
|
by (simp add: forth_d_zero_equals_def to_forth_bool_def assms)
|
|
|
|
lemma d_zero_equals_false:
|
|
assumes "data_stack vm = dhigh # dlow # rest"
|
|
assumes "dhigh \<noteq> 0 \<or> dlow \<noteq> 0"
|
|
shows "data_stack (forth_d_zero_equals vm) = forth_false # rest"
|
|
using assms by (auto simp: forth_d_zero_equals_def to_forth_bool_def)
|
|
|
|
definition forth_d_zero_less :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_d_zero_less vm =
|
|
(case data_stack vm of
|
|
dhigh # dlow # rest \<Rightarrow> vm\<lparr>data_stack := to_forth_bool (dhigh <s 0) # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma d_zero_less_true:
|
|
assumes "data_stack vm = dhigh # dlow # rest"
|
|
assumes "dhigh <s 0"
|
|
shows "data_stack (forth_d_zero_less vm) = forth_true # rest"
|
|
using assms by (simp add: forth_d_zero_less_def to_forth_bool_def)
|
|
|
|
lemma d_zero_less_false:
|
|
assumes "data_stack vm = dhigh # dlow # rest"
|
|
assumes "\<not> dhigh <s 0"
|
|
shows "data_stack (forth_d_zero_less vm) = forth_false # rest"
|
|
using assms by (simp add: forth_d_zero_less_def to_forth_bool_def)
|
|
|
|
(* ── D2* ( d1 -- d2 ) : double-cell left shift by 1 ──────────────────────
|
|
C: new_dlow = dlow << 1; new_dhigh = (dhigh << 1) | (top bit of dlow).
|
|
`push_bit 1` is this suite's established idiom for `<< 1` (matches
|
|
StarForth_Q48_16.thy). The carried bit is dlow's bit 63. *)
|
|
|
|
definition forth_d_two_star :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_d_two_star vm =
|
|
(case data_stack vm of
|
|
dhigh # dlow # rest \<Rightarrow>
|
|
let new_dlow = push_bit 1 dlow;
|
|
carry = of_bool (bit dlow 63);
|
|
new_dhigh = push_bit 1 dhigh OR carry
|
|
in vm\<lparr>data_stack := new_dhigh # new_dlow # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma d_two_star_normal:
|
|
assumes "data_stack vm = dhigh # dlow # rest"
|
|
shows "data_stack (forth_d_two_star vm) =
|
|
(push_bit 1 dhigh OR of_bool (bit dlow 63)) # push_bit 1 dlow # rest"
|
|
by (simp add: forth_d_two_star_def assms)
|
|
|
|
(* ── D2/ ( d1 -- d2 ) : double-cell arithmetic right shift by 1 ──────────
|
|
C: new_dhigh = dhigh >> 1 (arithmetic, sign-preserving); new_dlow =
|
|
(dlow >> 1 unsigned) with dhigh's bit 0 carried into dlow's bit 63.
|
|
Arithmetic shift right by 1 on two's complement = floor division by 2,
|
|
which is exactly HOL int `div` (rounds toward -infinity, NOT C99
|
|
truncating division) -- reusing the sint round-trip already
|
|
established for signed reasoning elsewhere in this suite, deliberately
|
|
NOT cell_sdiv (which is C99 truncating division and would be wrong
|
|
here for negative dhigh). *)
|
|
|
|
definition forth_d_two_slash :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_d_two_slash vm =
|
|
(case data_stack vm of
|
|
dhigh # dlow # rest \<Rightarrow>
|
|
let new_dhigh = word_of_int (sint dhigh div 2);
|
|
new_dlow = drop_bit 1 dlow OR (if bit dhigh 0 then push_bit 63 1 else 0)
|
|
in vm\<lparr>data_stack := new_dhigh # new_dlow # rest\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma d_two_slash_normal:
|
|
assumes "data_stack vm = dhigh # dlow # rest"
|
|
shows "data_stack (forth_d_two_slash vm) =
|
|
word_of_int (sint dhigh div 2) #
|
|
(drop_bit 1 dlow OR (if bit dhigh 0 then push_bit 63 1 else 0)) # rest"
|
|
by (simp add: forth_d_two_slash_def assms)
|
|
|
|
(* ── 2>R ( d -- ) ( R: -- d ) ──────────────────────────────────────────── *)
|
|
(* C: dsp<1 -> error (checked, then popped, BEFORE the ecw_nesting branch --
|
|
so on a subsequent rsp overflow error, data_stack is already popped,
|
|
matching ALLOT's pop-then-check pattern). Inside a colon word
|
|
(ecw_nesting>0): insert dlow,dhigh BELOW the resume-ip that's already on
|
|
top of the return stack, keeping resume-ip on top. Outside (ecw_nesting
|
|
= 0, e.g. interactively at the REPL): plain push of dlow then dhigh.
|
|
|
|
ecw_nesting>0 with an EMPTY return_stack is an invariant violation the
|
|
real C never defensively checks (it would read return_stack[-1], i.e.
|
|
real UB) -- modeled here as set_error as a defensive default, which is
|
|
NOT what the C does (the C has no such check at all); flagged as a
|
|
finding, not a faithful transcription of that one unreachable case. *)
|
|
|
|
definition forth_2to_r :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_2to_r vm =
|
|
(case data_stack vm of
|
|
[] \<Rightarrow> set_error vm
|
|
| dhigh # dlow # drest \<Rightarrow>
|
|
let vm1 = vm\<lparr>data_stack := drest\<rparr>
|
|
in if ecw_nesting vm > 0
|
|
then (case return_stack vm of
|
|
[] \<Rightarrow> set_error vm1 \<comment> \<open>invariant violation, see above\<close>
|
|
| resume_ip # rst \<Rightarrow>
|
|
if length rst + 2 \<ge> STACK_SIZE
|
|
then set_error vm1
|
|
else vm1\<lparr>return_stack := resume_ip # dhigh # dlow # rst\<rparr>)
|
|
else if length (return_stack vm) + 2 \<ge> STACK_SIZE
|
|
then set_error vm1
|
|
else vm1\<lparr>return_stack := dhigh # dlow # return_stack vm\<rparr>
|
|
| _ \<Rightarrow> set_error vm)"
|
|
|
|
lemma two_to_r_underflow:
|
|
assumes "data_stack vm = [] \<or> (\<exists>x. data_stack vm = [x])"
|
|
shows "vm_error (forth_2to_r vm)"
|
|
using assms by (auto simp: forth_2to_r_def set_error_def)
|
|
|
|
lemma two_to_r_outside_colon:
|
|
assumes "data_stack vm = dhigh # dlow # drest"
|
|
assumes "ecw_nesting vm = 0"
|
|
assumes "length (return_stack vm) + 2 < STACK_SIZE"
|
|
shows "return_stack (forth_2to_r vm) = dhigh # dlow # return_stack vm"
|
|
and "data_stack (forth_2to_r vm) = drest"
|
|
using assms by (simp_all add: forth_2to_r_def)
|
|
|
|
lemma two_to_r_inside_colon:
|
|
assumes "data_stack vm = dhigh # dlow # drest"
|
|
assumes "ecw_nesting vm > 0"
|
|
assumes "return_stack vm = resume_ip # rst"
|
|
assumes "length rst + 2 < STACK_SIZE"
|
|
shows "return_stack (forth_2to_r vm) = resume_ip # dhigh # dlow # rst"
|
|
and "data_stack (forth_2to_r vm) = drest"
|
|
using assms by (simp_all add: forth_2to_r_def)
|
|
|
|
(* ── 2R> ( -- d ) ( R: d -- ) ──────────────────────────────────────────── *)
|
|
(* Inside a colon word: pops (dlow,dhigh) from just below the resume-ip,
|
|
keeping resume-ip on top. Outside: plain pop of dhigh then dlow. Both
|
|
branches push the same result to the data stack: dhigh # dlow # ... *)
|
|
|
|
definition forth_2r_from :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_2r_from vm =
|
|
(if ecw_nesting vm > 0
|
|
then (case return_stack vm of
|
|
resume_ip # dhigh # dlow # rst \<Rightarrow>
|
|
vm\<lparr>data_stack := dhigh # dlow # data_stack vm,
|
|
return_stack := resume_ip # rst\<rparr>
|
|
| _ \<Rightarrow> set_error vm)
|
|
else (case return_stack vm of
|
|
dhigh # dlow # rst \<Rightarrow>
|
|
vm\<lparr>data_stack := dhigh # dlow # data_stack vm,
|
|
return_stack := rst\<rparr>
|
|
| _ \<Rightarrow> set_error vm))"
|
|
|
|
lemma two_r_from_inside_colon:
|
|
assumes "ecw_nesting vm > 0"
|
|
assumes "return_stack vm = resume_ip # dhigh # dlow # rst"
|
|
shows "data_stack (forth_2r_from vm) = dhigh # dlow # data_stack vm"
|
|
and "return_stack (forth_2r_from vm) = resume_ip # rst"
|
|
using assms by (simp_all add: forth_2r_from_def)
|
|
|
|
lemma two_r_from_outside_colon:
|
|
assumes "ecw_nesting vm = 0"
|
|
assumes "return_stack vm = dhigh # dlow # rst"
|
|
shows "data_stack (forth_2r_from vm) = dhigh # dlow # data_stack vm"
|
|
and "return_stack (forth_2r_from vm) = rst"
|
|
using assms by (simp_all add: forth_2r_from_def)
|
|
|
|
lemma two_r_from_inside_colon_underflow_nil:
|
|
assumes "ecw_nesting vm > 0"
|
|
assumes "return_stack vm = []"
|
|
shows "vm_error (forth_2r_from vm)"
|
|
by (simp add: forth_2r_from_def set_error_def assms)
|
|
|
|
lemma two_r_from_inside_colon_underflow_one:
|
|
assumes "ecw_nesting vm > 0"
|
|
assumes "return_stack vm = [x]"
|
|
shows "vm_error (forth_2r_from vm)"
|
|
by (simp add: forth_2r_from_def set_error_def assms)
|
|
|
|
lemma two_r_from_inside_colon_underflow_two:
|
|
assumes "ecw_nesting vm > 0"
|
|
assumes "return_stack vm = [x, y]"
|
|
shows "vm_error (forth_2r_from vm)"
|
|
by (simp add: forth_2r_from_def set_error_def assms)
|
|
|
|
(* ── 2R@ ( -- d ) ( R: d -- d ) ────────────────────────────────────────── *)
|
|
(* Same source cells as 2R>, but the return stack is left untouched
|
|
(fetch, not pop) -- both branches produce the identical data_stack
|
|
result as 2R>. *)
|
|
|
|
definition forth_2r_fetch :: "vm_state \<Rightarrow> vm_state" where
|
|
"forth_2r_fetch vm =
|
|
(if ecw_nesting vm > 0
|
|
then (case return_stack vm of
|
|
resume_ip # dhigh # dlow # rst \<Rightarrow>
|
|
vm\<lparr>data_stack := dhigh # dlow # data_stack vm\<rparr>
|
|
| _ \<Rightarrow> set_error vm)
|
|
else (case return_stack vm of
|
|
dhigh # dlow # rst \<Rightarrow>
|
|
vm\<lparr>data_stack := dhigh # dlow # data_stack vm\<rparr>
|
|
| _ \<Rightarrow> set_error vm))"
|
|
|
|
lemma two_r_fetch_inside_colon:
|
|
assumes "ecw_nesting vm > 0"
|
|
assumes "return_stack vm = resume_ip # dhigh # dlow # rst"
|
|
shows "data_stack (forth_2r_fetch vm) = dhigh # dlow # data_stack vm"
|
|
and "return_stack (forth_2r_fetch vm) = return_stack vm"
|
|
using assms by (simp_all add: forth_2r_fetch_def)
|
|
|
|
lemma two_r_fetch_outside_colon:
|
|
assumes "ecw_nesting vm = 0"
|
|
assumes "return_stack vm = dhigh # dlow # rst"
|
|
shows "data_stack (forth_2r_fetch vm) = dhigh # dlow # data_stack vm"
|
|
and "return_stack (forth_2r_fetch vm) = return_stack vm"
|
|
using assms by (simp_all add: forth_2r_fetch_def)
|
|
|
|
end
|