admin/LithosAnanake
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

proof/: complete StarForth_Double_Words.thy (arithmetic + 2>R/2R>/2R@)

Browse Source 
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>
This commit is contained in:
Robert Allan James
2026-08-13 22:23:47 -04:00
co-authored by Claude Sonnet 5
parent 45c381ca6c
commit b196c95e44
2 changed files with 512 additions and 29 deletions
Download Patch File Download Diff File Expand all files Collapse all files
proof/StarForth_Base.thy
+5
View File
@@ -509,6 +509,11 @@ record vm_state =
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
(* ── Physics Loop #1: Execution heat tracking ───────────────────────── *)
(* ○ CODE-MUST-MATCH: heat_threshold_{25th,50th,75th} in C VM struct.
proof/StarForth_Double_Words.thy
+507 -29
View File
@@ -2,43 +2,42 @@ theory StarForth_Double_Words
imports StarForth_Base
begin
unbundle bit_operations_syntax
(* =========================================================================
POST-XX: Double-Cell Stack Manipulation Words
Mirrors: src/word_source/double_words.c (partial -- see SCOPE below)
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: double_words.c has 20 registered words in
three categories. Only the first is modeled here:
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) -- modeled below. These only rearrange data_stack list
elements; nothing about their correctness depends on cell's exact
representation or on any vm_state field this theory doesn't already
track.
2ROT) -- unchanged from the original pass.
2. Double-cell RETURN-STACK transfer (2>R, 2R>, 2R@) -- NOT modeled.
The real C (double_words.c:330-382) branches on
"vm->ecw_nesting > 0" (execute_colon_word re-entrancy depth), a VM
field that does not exist anywhere in StarForth_Base.thy's
vm_state record. Modeling these words correctly requires adding
ecw_nesting to vm_state first -- a model-extension decision, not
something to add as a side effect of this file.
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/) -- NOT modeled. The real C
implementations (double_words.c:56-250ish) depend on cell_t being
a fixed-width (64-bit, "signed long") wrapping integer type --
D+/D- explicitly do carry/borrow detection via "unsigned long"
arithmetic and wraparound, DNEGATE uses bitwise complement (~) with
wraparound. This theory's "type_synonym cell = int" (StarForth_Base)
is unbounded/arbitrary-precision, not a fixed-width wrapping type,
so none of this carry/wraparound reasoning is even expressible as
currently modeled. Correctly formalizing these words needs a
foundational decision -- change cell's representation to a 64-bit
word type (matching StarForth_Q48_16.thy's own "64 word" approach)
or add explicit range side-conditions everywhere -- that ripples
into all 23 already-verified theories built on today's plain-int
cell. Not decided or attempted here; flagged for a dedicated pass.
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,
@@ -203,4 +202,483 @@ lemma two_rot_depth_preserved:
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