proof/: add StarForth_Control_Words.thy (runtime branch/loop/EXIT words)
Covers the runtime half of control_words.c fully: (BRANCH), (0BRANCH), (?DO), (DO), (LOOP), (+LOOP), (LEAVE), UNLOOP, I, J, EXIT. The "vm_ip as raw pointer" gap flagged at every earlier resume point turns out not to need a new model extension -- return_stack-held addresses dereference into vm->memory exactly like @/! addresses from the data stack, so the existing mem_read/unat machinery from StarForth_Memory_Words covers it directly. The compile-time half (IF/ELSE/THEN, BEGIN/WHILE/REPEAT/AGAIN/UNTIL, the compiling halves of ?DO/DO/LOOP/+LOOP/LEAVE, CASE/OF/ENDOF/ENDCASE) is left unmodelled, not from a model gap but a genuine architectural finding: Headline finding, not fixed: every compile-time control-flow word operates on FILE-SCOPE C statics (cf_stack/cf_sp, cf_last_mode, leave_addrs/leave_sp, endof_addrs/endof_sp, and their mark-stacks) -- none are struct VM fields, none are keyed by VM instance. In the Tripod multi-VM fleet, two VMs compiling control structures at overlapping times corrupt each other's IF/DO/CASE nesting through this shared global state, and a VM whose compilation aborts mid-structure leaves stale cf_sp/leave_sp/endof_sp state for whichever VM compiles next. cf_epoch_sync's mode-transition reset heuristic is itself keyed off a single global (cf_last_mode), not per-VM, so it can neither reliably detect nor reliably avoid false resets across VMs. Modelling these words against vm_state would require either inventing a field the real implementation doesn't have (silently fixing the bug in the proof) or modelling a bare global with no plumbing precedent in this suite -- both out of scope, left as documented gaps. 28 theory files verify with zero errors. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
Robert Allan James
co-authored by
Claude Sonnet 5
Claude Sonnet 5
parent
77d8f0606a
commit
45c381ca6c
@@ -12,6 +12,7 @@ session "StarForth" = "HOL-Library" +
|
||||
StarForth_Memory_Words
|
||||
StarForth_Dictionary_Words
|
||||
StarForth_Dictionary_Manipulation_Words
|
||||
StarForth_Control_Words
|
||||
StarForth_Mutex
|
||||
StarForth_Transition
|
||||
StarForth_Loop1_Heat
|
||||
|
||||
@@ -0,0 +1,525 @@
|
||||
theory StarForth_Control_Words
|
||||
imports StarForth_Base StarForth_Dictionary_Words
|
||||
begin
|
||||
|
||||
(* =========================================================================
|
||||
POST-08: Control Flow Words
|
||||
Mirrors: src/word_source/control_words.c
|
||||
|
||||
This file splits sharply into two classes, unlike any prior file in this
|
||||
sweep:
|
||||
|
||||
1. RUNTIME words ((BRANCH), (0BRANCH), (?DO), (DO), (LOOP), (+LOOP),
|
||||
(LEAVE), UNLOOP, I, J, EXIT) execute per-VM, inside `vm->return_stack`
|
||||
-- which IS in the abstract model. The "vm_ip as raw pointer" gap
|
||||
flagged at every earlier resume point turns out NOT to need a new
|
||||
model extension: the top of `return_stack` holds a `cell` that is a
|
||||
byte address into `vm->memory`, exactly like an `@`/`!` address taken
|
||||
from the data stack. Reusing `mem_read`/`unat` from
|
||||
StarForth_Memory_Words (imported transitively via
|
||||
StarForth_Dictionary_Words) models it directly. Fully covered below.
|
||||
|
||||
2. COMPILE-TIME words (IF/ELSE/THEN, BEGIN/WHILE/REPEAT/AGAIN/UNTIL,
|
||||
?DO/DO/LOOP/+LOOP/LEAVE's compiling halves, CASE/OF/ENDOF/ENDCASE) are
|
||||
NOT modelled -- not because the model is missing a piece, but because
|
||||
of a genuine architectural finding (below) that makes modelling them
|
||||
against `vm_state` actively misleading: their real state does not
|
||||
live in the VM at all.
|
||||
|
||||
── Headline finding, not fixed ──────────────────────────────────────────
|
||||
EVERY compile-time control-flow word in this file operates on FILE-SCOPE
|
||||
C statics, not `struct VM` fields: `cf_stack`/`cf_sp` (the IF/BEGIN/DO/
|
||||
CASE/OF nesting stack), `cf_last_mode` (the mode-transition heuristic
|
||||
`cf_epoch_sync` uses to decide when to reset `cf_stack`), `leave_addrs`/
|
||||
`leave_sp`/`leave_mark_stack`/`leave_mark_sp` (LEAVE patch sites), and
|
||||
`endof_addrs`/`endof_sp`/`endof_mark_stack`/`endof_mark_sp` (ENDOF patch
|
||||
sites) -- all declared `static` at file scope (lines 115-183), shared by
|
||||
every `VM*` in the process. There is no VM-id key anywhere in any of
|
||||
them.
|
||||
|
||||
Concretely, in the Tripod multi-VM fleet this repo is built around: if
|
||||
two VMs ever compile colon definitions containing control structures at
|
||||
overlapping times, their IF/DO/CASE nesting corrupts across VMs, since
|
||||
both write through the same `cf_stack`/`cf_sp`. Even without true
|
||||
concurrency, if one VM's compilation aborts mid-structure (a syntax
|
||||
error, an ACL denial, a capsule birth interrupted) leaving `cf_sp`/
|
||||
`leave_sp`/`endof_sp` non-reset, that leftover state is silently
|
||||
inherited by whichever VM compiles the next colon definition, in the
|
||||
same process, regardless of which VM it is. The only guard,
|
||||
`cf_epoch_sync` (lines 121-132), resets `cf_stack` when it observes a
|
||||
*mode* transition -- but it compares against `cf_last_mode`, itself a
|
||||
single global, not keyed per VM either: it can neither reliably detect
|
||||
"this VM's mode changed" (another VM's mode flip can mask this one's)
|
||||
nor avoid falsely resetting genuine in-progress nesting (this VM's own
|
||||
legitimate COMPILE-mode session, interrupted by another VM's transition
|
||||
observed first).
|
||||
|
||||
None of `cf_stack`, `leave_addrs`, `endof_addrs`, or their mark-stacks
|
||||
and cursors have any representation in `vm_state` (StarForth_Base.thy) --
|
||||
correctly so, since giving them one would misrepresent what the C code
|
||||
actually does (global, not per-VM). Modelling the compile-time words
|
||||
would therefore mean either (a) inventing a vm_state field the real
|
||||
implementation doesn't have, silently "fixing" the bug in the proof
|
||||
while the C stays broken, or (b) modelling a bare global outside
|
||||
vm_state, which this proof suite has no precedent or plumbing for. Both
|
||||
are out of scope; the words are left as documented gaps below.
|
||||
======================================================================== *)
|
||||
|
||||
definition CELL_BYTES_W :: cell where "CELL_BYTES_W = word_of_nat CELL_BYTES"
|
||||
|
||||
(* ── (BRANCH) ( -- ) : unconditional branch ───────────────────────────────
|
||||
C: ip = return_stack[rsp] (TOS); rel = *ip; ip += rel (bytes); store back. *)
|
||||
|
||||
definition forth_branch :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_branch vm =
|
||||
(case return_stack vm of
|
||||
[] \<Rightarrow> set_error vm
|
||||
| ip # rst \<Rightarrow>
|
||||
let rel = mem_read (memory vm) (unat ip)
|
||||
in vm\<lparr>return_stack := (ip + rel) # rst\<rparr>)"
|
||||
|
||||
lemma branch_underflow:
|
||||
assumes "return_stack vm = []"
|
||||
shows "vm_error (forth_branch vm)"
|
||||
by (simp add: forth_branch_def set_error_def assms)
|
||||
|
||||
lemma branch_normal:
|
||||
assumes "return_stack vm = ip # rst"
|
||||
shows "return_stack (forth_branch vm) = (ip + mem_read (memory vm) (unat ip)) # rst"
|
||||
by (simp add: forth_branch_def assms)
|
||||
|
||||
lemma branch_data_stack_unchanged:
|
||||
"data_stack (forth_branch vm) = data_stack vm"
|
||||
by (auto simp: forth_branch_def set_error_def Let_def split: list.split)
|
||||
|
||||
(* ── (0BRANCH) ( f -- ) : conditional branch ──────────────────────────────
|
||||
C: checks rsp<0 THEN dsp<0 (in that order); pops flag; if flag=0 take the
|
||||
branch (ip+=rel), else fall through (ip+=1 cell, skipping the literal). *)
|
||||
|
||||
definition forth_zero_branch :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_zero_branch vm =
|
||||
(case return_stack vm of
|
||||
[] \<Rightarrow> set_error vm
|
||||
| ip # rst \<Rightarrow>
|
||||
(case data_stack vm of
|
||||
[] \<Rightarrow> set_error vm
|
||||
| flag # drst \<Rightarrow>
|
||||
let rel = mem_read (memory vm) (unat ip);
|
||||
new_ip = if flag = 0 then ip + rel else ip + CELL_BYTES_W
|
||||
in vm\<lparr>data_stack := drst, return_stack := new_ip # rst\<rparr>))"
|
||||
|
||||
lemma zero_branch_rsp_underflow:
|
||||
assumes "return_stack vm = []"
|
||||
shows "vm_error (forth_zero_branch vm)"
|
||||
by (simp add: forth_zero_branch_def set_error_def assms)
|
||||
|
||||
lemma zero_branch_dsp_underflow:
|
||||
assumes "return_stack vm = ip # rst"
|
||||
assumes "data_stack vm = []"
|
||||
shows "vm_error (forth_zero_branch vm)"
|
||||
by (simp add: forth_zero_branch_def set_error_def assms)
|
||||
|
||||
lemma zero_branch_taken:
|
||||
assumes "return_stack vm = ip # rst"
|
||||
assumes "data_stack vm = 0 # drst"
|
||||
shows "return_stack (forth_zero_branch vm) = (ip + mem_read (memory vm) (unat ip)) # rst"
|
||||
and "data_stack (forth_zero_branch vm) = drst"
|
||||
using assms by (simp_all add: forth_zero_branch_def)
|
||||
|
||||
lemma zero_branch_not_taken:
|
||||
assumes "return_stack vm = ip # rst"
|
||||
assumes "data_stack vm = flag # drst"
|
||||
assumes "flag \<noteq> 0"
|
||||
shows "return_stack (forth_zero_branch vm) = (ip + CELL_BYTES_W) # rst"
|
||||
and "data_stack (forth_zero_branch vm) = drst"
|
||||
using assms by (simp_all add: forth_zero_branch_def)
|
||||
|
||||
(* ── (?DO) ( limit index -- ) ──────────────────────────────────────────────
|
||||
C: checks rsp<0 THEN dsp<1; pops index then limit. If index=limit, skips
|
||||
the whole loop body (ip+=rel from the fwd-branch literal). Otherwise
|
||||
enters: ip+=1 cell (skip literal), push (limit,index) under ip, checking
|
||||
the same rsp+2>=STACK_SIZE overflow DO itself checks. *)
|
||||
|
||||
definition forth_qdo_runtime :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_qdo_runtime vm =
|
||||
(case return_stack vm of
|
||||
[] \<Rightarrow> set_error vm
|
||||
| ip # rst \<Rightarrow>
|
||||
(case data_stack vm of
|
||||
index # limit # drst \<Rightarrow>
|
||||
let rel = mem_read (memory vm) (unat ip)
|
||||
in if index = limit
|
||||
then vm\<lparr>data_stack := drst, return_stack := (ip + rel) # rst\<rparr>
|
||||
else if length rst + 2 \<ge> STACK_SIZE
|
||||
then set_error (vm\<lparr>data_stack := drst\<rparr>)
|
||||
else vm\<lparr>data_stack := drst,
|
||||
return_stack := (ip + CELL_BYTES_W) # index # limit # rst\<rparr>
|
||||
| _ \<Rightarrow> set_error vm))"
|
||||
|
||||
lemma qdo_rsp_underflow:
|
||||
assumes "return_stack vm = []"
|
||||
shows "vm_error (forth_qdo_runtime vm)"
|
||||
by (simp add: forth_qdo_runtime_def set_error_def assms)
|
||||
|
||||
lemma qdo_dsp_underflow_nil:
|
||||
assumes "return_stack vm = ip # rst"
|
||||
assumes "data_stack vm = []"
|
||||
shows "vm_error (forth_qdo_runtime vm)"
|
||||
by (simp add: forth_qdo_runtime_def set_error_def assms)
|
||||
|
||||
lemma qdo_dsp_underflow_one:
|
||||
assumes "return_stack vm = ip # rst"
|
||||
assumes "data_stack vm = [x]"
|
||||
shows "vm_error (forth_qdo_runtime vm)"
|
||||
by (simp add: forth_qdo_runtime_def set_error_def assms)
|
||||
|
||||
lemma qdo_empty_skips:
|
||||
assumes "return_stack vm = ip # rst"
|
||||
assumes "data_stack vm = n # n # drst"
|
||||
shows "return_stack (forth_qdo_runtime vm) = (ip + mem_read (memory vm) (unat ip)) # rst"
|
||||
and "data_stack (forth_qdo_runtime vm) = drst"
|
||||
using assms by (simp_all add: forth_qdo_runtime_def)
|
||||
|
||||
lemma qdo_enters:
|
||||
assumes "return_stack vm = ip # rst"
|
||||
assumes "data_stack vm = index # limit # drst"
|
||||
assumes "index \<noteq> limit"
|
||||
assumes "length rst + 2 < STACK_SIZE"
|
||||
shows "return_stack (forth_qdo_runtime vm) = (ip + CELL_BYTES_W) # index # limit # rst"
|
||||
and "data_stack (forth_qdo_runtime vm) = drst"
|
||||
using assms by (simp_all add: forth_qdo_runtime_def)
|
||||
|
||||
(* ── (DO) ( limit index -- ) ──────────────────────────────────────────────
|
||||
C: checks rsp<0 THEN dsp<1; pops index then limit; unconditionally
|
||||
inserts (limit,index) under the current ip (copied, never dereferenced --
|
||||
no early-exit test, unlike (?DO)). Same overflow check as (?DO). *)
|
||||
|
||||
definition forth_do_runtime :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_do_runtime vm =
|
||||
(case return_stack vm of
|
||||
[] \<Rightarrow> set_error vm
|
||||
| ip # rst \<Rightarrow>
|
||||
(case data_stack vm of
|
||||
index # limit # drst \<Rightarrow>
|
||||
if length rst + 2 \<ge> STACK_SIZE
|
||||
then set_error (vm\<lparr>data_stack := drst\<rparr>)
|
||||
else vm\<lparr>data_stack := drst, return_stack := ip # index # limit # rst\<rparr>
|
||||
| _ \<Rightarrow> set_error vm))"
|
||||
|
||||
lemma do_rsp_underflow:
|
||||
assumes "return_stack vm = []"
|
||||
shows "vm_error (forth_do_runtime vm)"
|
||||
by (simp add: forth_do_runtime_def set_error_def assms)
|
||||
|
||||
lemma do_normal:
|
||||
assumes "return_stack vm = ip # rst"
|
||||
assumes "data_stack vm = index # limit # drst"
|
||||
assumes "length rst + 2 < STACK_SIZE"
|
||||
shows "return_stack (forth_do_runtime vm) = ip # index # limit # rst"
|
||||
and "data_stack (forth_do_runtime vm) = drst"
|
||||
using assms by (simp_all add: forth_do_runtime_def)
|
||||
|
||||
lemma do_overflow:
|
||||
assumes "return_stack vm = ip # rst"
|
||||
assumes "data_stack vm = index # limit # drst"
|
||||
assumes "length rst + 2 \<ge> STACK_SIZE"
|
||||
shows "vm_error (forth_do_runtime vm)"
|
||||
using assms by (simp add: forth_do_runtime_def set_error_def)
|
||||
|
||||
(* ── (LOOP) ( -- ) ─────────────────────────────────────────────────────── *)
|
||||
(* C: rsp<2 -> error. idx += 1; back = *ip; continue (signed idx<lim) ->
|
||||
ip += back, keep frame; else drop (limit,index), ip += 1 cell. *)
|
||||
|
||||
definition forth_loop_runtime :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_loop_runtime vm =
|
||||
(case return_stack vm of
|
||||
ip # idx # lim # rst \<Rightarrow>
|
||||
let back = mem_read (memory vm) (unat ip);
|
||||
new_idx = idx + 1
|
||||
in if new_idx <s lim
|
||||
then vm\<lparr>return_stack := (ip + back) # new_idx # lim # rst\<rparr>
|
||||
else vm\<lparr>return_stack := (ip + CELL_BYTES_W) # rst\<rparr>
|
||||
| _ \<Rightarrow> set_error vm)"
|
||||
|
||||
lemma loop_underflow_nil:
|
||||
assumes "return_stack vm = []"
|
||||
shows "vm_error (forth_loop_runtime vm)"
|
||||
by (simp add: forth_loop_runtime_def set_error_def assms)
|
||||
|
||||
lemma loop_underflow_one:
|
||||
assumes "return_stack vm = [ip]"
|
||||
shows "vm_error (forth_loop_runtime vm)"
|
||||
by (simp add: forth_loop_runtime_def set_error_def assms)
|
||||
|
||||
lemma loop_underflow_two:
|
||||
assumes "return_stack vm = [ip, idx]"
|
||||
shows "vm_error (forth_loop_runtime vm)"
|
||||
by (simp add: forth_loop_runtime_def set_error_def assms)
|
||||
|
||||
lemma loop_continues:
|
||||
assumes "return_stack vm = ip # idx # lim # rst"
|
||||
assumes "idx + 1 <s lim"
|
||||
shows "return_stack (forth_loop_runtime vm) =
|
||||
(ip + mem_read (memory vm) (unat ip)) # (idx + 1) # lim # rst"
|
||||
using assms by (simp add: forth_loop_runtime_def)
|
||||
|
||||
lemma loop_exits:
|
||||
assumes "return_stack vm = ip # idx # lim # rst"
|
||||
assumes "\<not> (idx + 1 <s lim)"
|
||||
shows "return_stack (forth_loop_runtime vm) = (ip + CELL_BYTES_W) # rst"
|
||||
using assms by (simp add: forth_loop_runtime_def)
|
||||
|
||||
lemma loop_data_stack_unchanged:
|
||||
"data_stack (forth_loop_runtime vm) = data_stack vm"
|
||||
by (auto simp: forth_loop_runtime_def set_error_def Let_def split: list.split)
|
||||
|
||||
(* ── (+LOOP) ( n -- ) ──────────────────────────────────────────────────── *)
|
||||
(* C: checks dsp<0 THEN rsp<2, BOTH before popping n (unlike ALLOT's
|
||||
pop-then-check -- here an rsp<2 failure leaves the data stack untouched).
|
||||
newv = idx+n; continue test depends on sign of n (ascending vs
|
||||
descending +LOOP). *)
|
||||
|
||||
definition forth_plus_loop_runtime :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_plus_loop_runtime vm =
|
||||
(case data_stack vm of
|
||||
[] \<Rightarrow> set_error vm
|
||||
| n # drst \<Rightarrow>
|
||||
(case return_stack vm of
|
||||
ip # idx # lim # rst \<Rightarrow>
|
||||
let back = mem_read (memory vm) (unat ip);
|
||||
newv = idx + n;
|
||||
cont = if 0 \<le>s n then newv <s lim else lim \<le>s newv
|
||||
in vm\<lparr>data_stack := drst,
|
||||
return_stack := (if cont then (ip + back) # newv # lim # rst
|
||||
else (ip + CELL_BYTES_W) # rst)\<rparr>
|
||||
| _ \<Rightarrow> set_error vm))"
|
||||
|
||||
lemma plus_loop_dsp_underflow:
|
||||
assumes "data_stack vm = []"
|
||||
shows "vm_error (forth_plus_loop_runtime vm)"
|
||||
by (simp add: forth_plus_loop_runtime_def set_error_def assms)
|
||||
|
||||
lemma plus_loop_rsp_underflow_nil:
|
||||
assumes "data_stack vm = n # drst"
|
||||
assumes "return_stack vm = []"
|
||||
shows "vm_error (forth_plus_loop_runtime vm)"
|
||||
and "data_stack (forth_plus_loop_runtime vm) = data_stack vm"
|
||||
using assms by (simp_all add: forth_plus_loop_runtime_def set_error_def)
|
||||
|
||||
lemma plus_loop_rsp_underflow_one:
|
||||
assumes "data_stack vm = n # drst"
|
||||
assumes "return_stack vm = [ip]"
|
||||
shows "vm_error (forth_plus_loop_runtime vm)"
|
||||
and "data_stack (forth_plus_loop_runtime vm) = data_stack vm"
|
||||
using assms by (simp_all add: forth_plus_loop_runtime_def set_error_def)
|
||||
|
||||
lemma plus_loop_rsp_underflow_two:
|
||||
assumes "data_stack vm = n # drst"
|
||||
assumes "return_stack vm = [ip, idx]"
|
||||
shows "vm_error (forth_plus_loop_runtime vm)"
|
||||
and "data_stack (forth_plus_loop_runtime vm) = data_stack vm"
|
||||
using assms by (simp_all add: forth_plus_loop_runtime_def set_error_def)
|
||||
|
||||
lemma plus_loop_ascending_continues:
|
||||
assumes "data_stack vm = n # drst"
|
||||
assumes "return_stack vm = ip # idx # lim # rst"
|
||||
assumes "0 \<le>s n"
|
||||
assumes "idx + n <s lim"
|
||||
shows "return_stack (forth_plus_loop_runtime vm) =
|
||||
(ip + mem_read (memory vm) (unat ip)) # (idx + n) # lim # rst"
|
||||
and "data_stack (forth_plus_loop_runtime vm) = drst"
|
||||
using assms by (simp_all add: forth_plus_loop_runtime_def)
|
||||
|
||||
lemma plus_loop_descending_continues:
|
||||
assumes "data_stack vm = n # drst"
|
||||
assumes "return_stack vm = ip # idx # lim # rst"
|
||||
assumes "\<not> 0 \<le>s n"
|
||||
assumes "lim \<le>s (idx + n)"
|
||||
shows "return_stack (forth_plus_loop_runtime vm) =
|
||||
(ip + mem_read (memory vm) (unat ip)) # (idx + n) # lim # rst"
|
||||
using assms by (simp add: forth_plus_loop_runtime_def)
|
||||
|
||||
(* ── (LEAVE) ( -- ) : force the enclosing loop to exit at next LOOP/+LOOP ── *)
|
||||
(* C: rsp<2 -> error; else index := limit (loop-continue test becomes false
|
||||
at the next (LOOP)/(+LOOP), since idx cannot exceed lim after this). *)
|
||||
|
||||
definition forth_leave_runtime :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_leave_runtime vm =
|
||||
(case return_stack vm of
|
||||
ip # idx # lim # rst \<Rightarrow> vm\<lparr>return_stack := ip # lim # lim # rst\<rparr>
|
||||
| _ \<Rightarrow> set_error vm)"
|
||||
|
||||
lemma leave_runtime_underflow_nil:
|
||||
assumes "return_stack vm = []"
|
||||
shows "vm_error (forth_leave_runtime vm)"
|
||||
by (simp add: forth_leave_runtime_def set_error_def assms)
|
||||
|
||||
lemma leave_runtime_underflow_one:
|
||||
assumes "return_stack vm = [ip]"
|
||||
shows "vm_error (forth_leave_runtime vm)"
|
||||
by (simp add: forth_leave_runtime_def set_error_def assms)
|
||||
|
||||
lemma leave_runtime_underflow_two:
|
||||
assumes "return_stack vm = [ip, idx]"
|
||||
shows "vm_error (forth_leave_runtime vm)"
|
||||
by (simp add: forth_leave_runtime_def set_error_def assms)
|
||||
|
||||
lemma leave_runtime_normal:
|
||||
assumes "return_stack vm = ip # idx # lim # rst"
|
||||
shows "return_stack (forth_leave_runtime vm) = ip # lim # lim # rst"
|
||||
by (simp add: forth_leave_runtime_def assms)
|
||||
|
||||
(* ── UNLOOP ( -- ) : discard the innermost loop frame ─────────────────── *)
|
||||
(* C: rsp<2 -> error; else drop (limit,index), keep ip on top. *)
|
||||
|
||||
definition forth_unloop :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_unloop vm =
|
||||
(case return_stack vm of
|
||||
ip # idx # lim # rst \<Rightarrow> vm\<lparr>return_stack := ip # rst\<rparr>
|
||||
| _ \<Rightarrow> set_error vm)"
|
||||
|
||||
lemma unloop_normal:
|
||||
assumes "return_stack vm = ip # idx # lim # rst"
|
||||
shows "return_stack (forth_unloop vm) = ip # rst"
|
||||
by (simp add: forth_unloop_def assms)
|
||||
|
||||
lemma unloop_data_stack_unchanged:
|
||||
"data_stack (forth_unloop vm) = data_stack vm"
|
||||
by (auto simp: forth_unloop_def set_error_def Let_def split: list.split)
|
||||
|
||||
(* ── I ( -- i ) : innermost loop index ────────────────────────────────── *)
|
||||
|
||||
definition forth_I :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_I vm =
|
||||
(case return_stack vm of
|
||||
ip # idx # lim # rst \<Rightarrow>
|
||||
if ds_full vm then set_error vm else vm\<lparr>data_stack := idx # data_stack vm\<rparr>
|
||||
| _ \<Rightarrow> set_error vm)"
|
||||
|
||||
lemma I_normal:
|
||||
assumes "return_stack vm = ip # idx # lim # rst"
|
||||
assumes "\<not> ds_full vm"
|
||||
shows "data_stack (forth_I vm) = idx # data_stack vm"
|
||||
by (simp add: forth_I_def assms)
|
||||
|
||||
lemma I_outside_loop_nil:
|
||||
assumes "return_stack vm = []"
|
||||
shows "vm_error (forth_I vm)"
|
||||
by (simp add: forth_I_def set_error_def assms)
|
||||
|
||||
lemma I_outside_loop_one:
|
||||
assumes "return_stack vm = [ip]"
|
||||
shows "vm_error (forth_I vm)"
|
||||
by (simp add: forth_I_def set_error_def assms)
|
||||
|
||||
lemma I_outside_loop_two:
|
||||
assumes "return_stack vm = [ip, idx]"
|
||||
shows "vm_error (forth_I vm)"
|
||||
by (simp add: forth_I_def set_error_def assms)
|
||||
|
||||
(* ── J ( -- j ) : next-outer loop index ───────────────────────────────── *)
|
||||
|
||||
definition forth_J :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_J vm =
|
||||
(case return_stack vm of
|
||||
ip # idx # lim # outer_idx # outer_lim # rst \<Rightarrow>
|
||||
if ds_full vm then set_error vm else vm\<lparr>data_stack := outer_idx # data_stack vm\<rparr>
|
||||
| _ \<Rightarrow> set_error vm)"
|
||||
|
||||
lemma J_normal:
|
||||
assumes "return_stack vm = ip # idx # lim # outer_idx # outer_lim # rst"
|
||||
assumes "\<not> ds_full vm"
|
||||
shows "data_stack (forth_J vm) = outer_idx # data_stack vm"
|
||||
by (simp add: forth_J_def assms)
|
||||
|
||||
lemma J_needs_nested_loops_nil:
|
||||
assumes "return_stack vm = []"
|
||||
shows "vm_error (forth_J vm)"
|
||||
by (simp add: forth_J_def set_error_def assms)
|
||||
|
||||
lemma J_needs_nested_loops_one:
|
||||
assumes "return_stack vm = [ip]"
|
||||
shows "vm_error (forth_J vm)"
|
||||
by (simp add: forth_J_def set_error_def assms)
|
||||
|
||||
lemma J_needs_nested_loops_two:
|
||||
assumes "return_stack vm = [ip, idx]"
|
||||
shows "vm_error (forth_J vm)"
|
||||
by (simp add: forth_J_def set_error_def assms)
|
||||
|
||||
lemma J_needs_nested_loops_three:
|
||||
assumes "return_stack vm = [ip, idx, lim]"
|
||||
shows "vm_error (forth_J vm)"
|
||||
by (simp add: forth_J_def set_error_def assms)
|
||||
|
||||
lemma J_needs_nested_loops_four:
|
||||
assumes "return_stack vm = [ip, idx, lim, outer_idx]"
|
||||
shows "vm_error (forth_J vm)"
|
||||
by (simp add: forth_J_def set_error_def assms)
|
||||
|
||||
(* ── EXIT ( -- ) : one-shot return from the current colon definition ────── *)
|
||||
(* C: rsp<0 -> error; else vm->exit_colon = 1. The real interpreter loop
|
||||
checks exit_colon after each word dispatch (per StarForth_Base.thy's
|
||||
vm_state comment on exit_colon) -- this word only sets the flag. *)
|
||||
|
||||
definition forth_exit :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_exit vm =
|
||||
(case return_stack vm of
|
||||
[] \<Rightarrow> set_error vm
|
||||
| _ \<Rightarrow> vm\<lparr>exit_colon := True\<rparr>)"
|
||||
|
||||
lemma exit_underflow:
|
||||
assumes "return_stack vm = []"
|
||||
shows "vm_error (forth_exit vm)"
|
||||
by (simp add: forth_exit_def set_error_def assms)
|
||||
|
||||
lemma exit_sets_flag:
|
||||
assumes "return_stack vm \<noteq> []"
|
||||
shows "exit_colon (forth_exit vm)"
|
||||
using assms by (cases "return_stack vm") (auto simp: forth_exit_def)
|
||||
|
||||
lemma exit_data_stack_unchanged:
|
||||
"data_stack (forth_exit vm) = data_stack vm"
|
||||
by (auto simp: forth_exit_def set_error_def Let_def split: list.split)
|
||||
|
||||
(* ── Compile-time words -- NOT MODELLED, see the headline finding above ──
|
||||
Named sentinels for greppability, matching the SP@/SP! and >BODY/etc.
|
||||
conventions established in StarForth_Dictionary_Words.thy and
|
||||
StarForth_Dictionary_Manipulation_Words.thy. *)
|
||||
|
||||
lemma if_not_modelled: True \<comment> \<open>IF: pushes a CF_IF marker onto the global cf_stack.\<close>
|
||||
by simp
|
||||
lemma else_not_modelled: True \<comment> \<open>ELSE: pops/pushes global cf_stack, patches vm->memory via vm->here.\<close>
|
||||
by simp
|
||||
lemma then_not_modelled: True \<comment> \<open>THEN: pops global cf_stack, patches vm->memory.\<close>
|
||||
by simp
|
||||
lemma begin_not_modelled: True \<comment> \<open>BEGIN: pushes a CF_BEGIN marker onto the global cf_stack.\<close>
|
||||
by simp
|
||||
lemma while_not_modelled: True \<comment> \<open>WHILE: peeks global cf_stack, pushes CF_WHILE.\<close>
|
||||
by simp
|
||||
lemma repeat_not_modelled: True \<comment> \<open>REPEAT: pops global cf_stack twice, patches vm->memory.\<close>
|
||||
by simp
|
||||
lemma again_not_modelled: True \<comment> \<open>AGAIN: pops global cf_stack, patches vm->memory.\<close>
|
||||
by simp
|
||||
lemma until_not_modelled: True \<comment> \<open>UNTIL: pops global cf_stack, patches vm->memory.\<close>
|
||||
by simp
|
||||
lemma qdo_compile_not_modelled: True \<comment> \<open>?DO (compiling half): pushes global cf_stack + leave_mark_stack.\<close>
|
||||
by simp
|
||||
lemma do_compile_not_modelled: True \<comment> \<open>DO (compiling half): pushes global cf_stack + leave_mark_stack.\<close>
|
||||
by simp
|
||||
lemma leave_compile_not_modelled: True \<comment> \<open>LEAVE (compiling half): scans global cf_stack, pushes global leave_addrs.\<close>
|
||||
by simp
|
||||
lemma loop_compile_not_modelled: True \<comment> \<open>LOOP (compiling half): pops global cf_stack/leave_mark_stack, patches vm->memory.\<close>
|
||||
by simp
|
||||
lemma plus_loop_compile_not_modelled: True \<comment> \<open>+LOOP (compiling half): same as LOOP's compiling half.\<close>
|
||||
by simp
|
||||
lemma case_not_modelled: True \<comment> \<open>CASE: pushes global cf_stack + endof_mark_stack.\<close>
|
||||
by simp
|
||||
lemma of_not_modelled: True \<comment> \<open>OF: scans global cf_stack, compiles calls to OVER/=/DROP by dictionary lookup.\<close>
|
||||
by simp
|
||||
lemma endof_not_modelled: True \<comment> \<open>ENDOF: pops global cf_stack, pushes global endof_addrs, patches vm->memory.\<close>
|
||||
by simp
|
||||
lemma endcase_not_modelled: True \<comment> \<open>ENDCASE: pops global cf_stack/endof_mark_stack, patches vm->memory.\<close>
|
||||
by simp
|
||||
|
||||
end
|
||||
Reference in New Issue
Block a user