Up to index of Isabelle/HOL/SafeImp
theory SVMSemantics(* Title: Safe Virtual Machine Semantics
Author: Ricardo Pe~na
Copyright: March 2008, Universidad Complutense de Madrid
*)
header {* Semantics of the SVM instructions *}
theory SVMSemantics
imports SVMState HaskellLib
begin
text{*
\begin{itemize}
\item 'execSVMInst' executes a single SafeImp instruction in a state and
gives another state.
\item 'execSVM' executes the next SafeImp instruction in a
SVM program.
\item 'execOp' operates two basic values with an operator.
\end{itemize}
*}
consts
execSVMInst :: "[SafeInstr,ConstructorTableFun,Heap,Region,PC,Stack]
=> (SVMState,SVMState) Either"
consts
item2Stack :: "Region => Stack => Item => StackObject"
item2Val :: "Stack => Item => Val"
text{* Auxiliary functions for BUILDENV and BUILDCLS *}
fun stackOffset :: "Stack => nat => StackObject" (infix "!+" 110 ) where
"(so # S) !+ 0 = so"
| "(Val v # S) !+ n = S !+ (n - 1)"
| "(Reg r # S) !+ n = S !+ (n - 1)"
| "(Cont c # S) !+ n = S !+ (n - 2)"
primrec
"item2Stack k S (ItemConst v) = Val v"
"item2Stack k S (ItemVar off) = S !+off"
"item2Stack k S ItemRegSelf = Reg k"
primrec
"item2Val S (ItemConst v) = v"
"item2Val S (ItemVar off) = (case S !+ off of Val v => v)"
-- "We use fun here for full pattern matching"
constdefs
execSVM :: "SafeImpProg => SVMState => (SVMState,SVMState) Either"
"execSVM prog state == (
case prog of ((code,cnt),q,ct,st) =>
case state of (h,k0,(l,i),S) =>
let codef = map_of code
in execSVMInst (fst(the (codef l))!i) (map_of ct) h k0 (l,i) S)"
consts
execSVM_N :: "SafeImpProg => SVMState => nat => SVMState"
primrec
"execSVM_N prog s 0 = s "
"execSVM_N prog s (Suc n) = (case execSVM prog s of
Right s' => execSVM_N prog s' n)"
text{* Function {\sl execSVMInst} executes a single SVM instruction. If it
is POPCONT and there is no continuation in the stack, it returns the
current state with the constructor Left. Otherwise, it returns the next
state with the constructor Right. *}
primrec
"execSVMInst DECREGION ct h k0 pc S = Right (h \<down> k0,k0,incrPC pc,S)"
"execSVMInst POPCONT ct h k0 pc S = (case S of
Val v#[] => Left (h,k0,pc,S)
| Val v#Cont (k0,l)#S' => Right (h,k0,(l,0),Val v#S'))"
"execSVMInst (PUSHCONT p)ct h k0 pc S = Right (h,snd h,incrPC pc,Cont (k0,p)#S)"
"execSVMInst COPY ct h k0 pc S = (case S of
Val (Loc b)#Reg j#S' =>
if j ≤ snd h then
let pair = copy h j b in
case pair of (h',b') =>
Right (h',k0,incrPC pc,Val (Loc b')#S')
else Left (h,k0,pc,S))"
"execSVMInst REUSE ct h k0 pc S = (case S of
Val (Loc b)#S' =>
case h of (hm,k) =>
let cell = the (hm b);
b' = getFresh hm in
Right ((hm(b:=None)(b'\<mapsto> cell),k),
k0,incrPC pc,Val (Loc b')#S'))"
"execSVMInst (CALL p) ct h k0 pc S = (case h of
(hm,k) => Right ((hm,k+1),k0,(p,0),S))"
"execSVMInst (PRIMOP oper) ct h k0 pc S = (case S of
Val (IntT i)#Val (IntT i')#S' =>
let v = execOp oper (IntT i) (IntT i') in
Right (h,k0,incrPC pc,Val v#S'))"
"execSVMInst (MATCH l ps) ct h k0 pc S = (case S!+l of Val (Loc b) =>
case (fst h) b of
Some (j,C,vs) =>
case ct C of
Some (_,r,_) =>
Right (h,k0,(ps!r,0),(map Val vs) @ S))"
"execSVMInst (MATCHD l ps) ct h k0 pc S = (case S!+l of Val (Loc b) =>
case (fst h) b of
Some (j,C,vs) =>
case ct C of
Some (_,r,_) =>
let h' = ((fst h)(b:= None), snd h) in
Right (h',k0,(ps!r,0),(map Val vs) @ S))"
"execSVMInst (MATCHN l v m ps) ct h k0 pc S = (case S!+l of
Val (IntT i) =>
let r = (nat i)- v;
p = if r ≥ 0 ∧ r ≤ m - 1
then ps!r
else ps!m
in Right (h,k0,(p,0),S)
| Val (BoolT b) =>
let p = if ¬ b then ps!0 else ps!1
in Right (h,k0,(p,0),S))"
"execSVMInst (BUILDENV is) ct h k0 pc S =
(let bs = map (item2Stack (snd h) S) is
in Right (h,k0,incrPC pc,bs @ S))"
"execSVMInst (BUILDCLS C is i) ct h k0 pc S =
(case item2Stack (snd h) S i of
Reg j =>
case h of
(hm,k) =>
if j ≤ snd h then
let vs = map (item2Val S) is;
b = getFresh hm;
h' = (hm (b \<mapsto> (j,C,vs)),k)
in Right (h',k0,incrPC pc,Val (Loc b)#S)
else Left (h,k0,pc,S))"
"execSVMInst (SLIDE m n) ct h k0 pc S = Right (h,k0,incrPC pc,take m S @ drop (m+n) S)"
text{* We convert function {\sl execSVM} into a reflexive transitive
relation. Also, we define an inductive relation {\sl execSVMBalanced}
giving us the list of all the states reachable from an initial one so that
the stack does not decrease more than a given amount n. The list is given
in reverse order.*}
constdefs
execSVMAll :: "[SafeImpProg,SVMState,SVMState] => bool"
("_\<turnstile> _ -svm-> _" [61,61,61]60)
"P \<turnstile> s -svm-> s' ≡ (s,s') ∈ {(s,t) . execSVM P s = Right t}^*"
fun
diffStack :: "SVMState => SVMState => nat => int"
where
"diffStack (h',k0',pc',S') (h,k0,pc,S) m = (
let n = length S;
n' = length S'
in int m + (int n' - int n))"
fun instrSVM :: "SafeImpProg => SVMState => SafeInstr"
where
"instrSVM ((code,cnt),q,ct,st) (h,k0,(l,i),S) = fst(the (map_of code l))!i"
inductive
execSVMBalanced :: "[SafeImpProg,SVMState,nat list,SVMState list,nat list] => bool"
("_\<turnstile>_ , _ -svm-> _ , _" [61,61,61,61,61]60)
where
init: "P \<turnstile> s, n#ns -svm-> [s], n#ns"
| step: "[| P \<turnstile> s, n#ns -svm-> s'#ss, m#ms;
execSVM P s' = Right s'';
m' = nat (diffStack s'' s' m);
m' ≥ 0;
ms' = (if pushcont (instrSVM P s') then 0#m#ms
else if popcont (instrSVM P s') ∧ ms=m''#ms'' then (Suc m'')#ms''
else m'#ms)|]
==>
P \<turnstile> s, n#ns -svm-> s''#s'#ss, ms'"
lemma popcont_neq_pushcont:
"popcont (instrSVM P s) ==> ¬pushcont (instrSVM P s)"
by (case_tac "instrSVM P s",simp_all)
lemma execSVMBalanced_n_step_aux [rule_format]:
" P \<turnstile> s'', n''#ns'' -svm-> sss , n'''#ns''' --> (∀ s''' ss'' ss. sss = s'''#ss'' -->
P \<turnstile> s', n'#ns' -svm-> s'' # ss', n''#ns'' -->
ss = ss'' @ ss' -->
P \<turnstile> s', n'#ns' -svm-> s'''# ss, n'''#ns''')"
apply (rule impI)
apply (erule execSVMBalanced.induct) apply simp
apply (rule allI)+
apply (erule_tac x="s'a" in allE)
apply (erule_tac x="ss" in allE)
apply (erule_tac x="ss @ ss'" in allE)
apply (rule impI)+
apply simp
apply (elim conjE)
apply (rule conjI) apply (rule impI) apply (rule conjI) apply (rule impI)
apply simp
apply (erule conjE) apply (frule popcont_neq_pushcont) apply simp
apply (rule impI)
apply simp
apply (drule_tac t="ss''" in sym) apply simp
apply (rule execSVMBalanced.step) apply simp apply simp apply simp apply simp apply simp
apply (rule conjI) apply simp apply simp
apply (rule impI) apply (rule conjI) apply (rule impI)
apply simp
apply (drule_tac t="ss''" in sym) apply simp
apply (rule execSVMBalanced.step) apply simp apply simp apply simp apply simp apply simp
apply (rule impI)
apply simp
apply (drule_tac t="ss''" in sym) apply simp
apply (rule execSVMBalanced.step) apply simp apply simp apply simp apply simp
apply (split split_if_asm) apply simp apply simp
apply (rule impI) apply (elim conjE)
apply (rule conjI) apply simp apply auto
done
lemma execSVMBalanced_n_step:
"[|P \<turnstile> s', n'#ns' -svm-> s'' # ss', n''#ns'';
P \<turnstile> s'', n''#ns'' -svm-> s'''# ss'', n'''#ns''';
ss = ss'' @ ss'|]
==> P \<turnstile> s', n'#ns' -svm-> s'''# ss, n'''#ns'''"
apply (rule execSVMBalanced_n_step_aux)
apply simp_all
done
end
lemma popcont_neq_pushcont:
popcont (instrSVM P s) ==> ¬ pushcont (instrSVM P s)
lemma execSVMBalanced_n_step_aux:
[| P\<turnstile>s'' , n'' # ns'' -svm-> sss , n''' # ns'''; sss = s''' # ss'';
P\<turnstile>s' , n' # ns' -svm-> s'' # ss' , n'' # ns''; ss = ss'' @ ss' |]
==> P\<turnstile>s' , n' # ns' -svm-> s''' # ss , n''' # ns'''
lemma execSVMBalanced_n_step:
[| P\<turnstile>s' , n' # ns' -svm-> s'' # ss' , n'' # ns'';
P\<turnstile>s'' , n'' # ns'' -svm-> s''' # ss'' , n''' # ns''';
ss = ss'' @ ss' |]
==> P\<turnstile>s' , n' # ns' -svm-> s''' # ss , n''' # ns'''