header {* 
  \isaheader{Extended Jinja Virtual Machine} 
*}

theory JBC_Semantics = Form:


(* changes the preprocessor for the simplifier, such that internally
   generated lemmas are augmented with proof objects *)
setup {* [Simplifier.change_simpset_of op setmksimps (setmp proofs 2 (mksimps mksimps_pairs))] *} 


section {* States and Program Syntax *}

record env =
cs::"heap list"
lv::"var \<Rightarrow> val option"

types
jbc_state = "pos \<times> jvm_state \<times> env"

types
jbc_prog = "jvm_prog \<times> (pos ~~> expr)"

subsection {* Auxiliary functions *}
constdefs 
incA::"pos \<Rightarrow> pos"
"incA \<equiv> \<lambda>(C,M,n). (C,M,n+1)"

constdefs
cmd::"jbc_prog \<Rightarrow> pos \<Rightarrow> instr option"
"cmd \<equiv> \<lambda>(P,A) (C,M,pc). case class P C of None \<Rightarrow> None
| Some c \<Rightarrow> (case (map_of (snd (snd c)) M)
             of None \<Rightarrow> None
             | Some m \<Rightarrow> (let is=fst (snd (snd (snd (snd m))))
                          in (if pc < length is then Some (is!pc) else None)))"
                       
consts
domMC::"(cname \<times> mname \<times> jvm_method) \<Rightarrow> pos list"

recdef domMC "measure (\<lambda>x.0)"
"domMC (C,M,(mxs,mxl,bd,et)) = map (\<lambda>n. (C,M,n)) (upt 0  (length bd))"

consts
domCC::"jvm_method cdecl \<Rightarrow> pos list"

recdef domCC "measure (\<lambda>(C,cd). length (snd (snd cd)))"
"domCC (C,(C',fs,[])) = []"
"domCC (C,(C',fs,(M,Ts,T,m)#ms)) = domMC (C,M,m) @ (domCC (C,(C',fs,ms)))"

constdefs
domC::"jbc_prog \<Rightarrow> pos list"
"domC \<Pi> \<equiv> concat (map domCC (fst \<Pi>))"

constdefs
anF::"jbc_prog \<Rightarrow> pos \<Rightarrow> expr option"
"anF \<equiv> \<lambda>(P,An) p. An ? p"

consts
hasAn::"jbc_prog \<Rightarrow> pos \<Rightarrow> bool"
defs hasAn_def [simp]:
"hasAn \<Pi> p \<equiv> (case anF \<Pi> p of None \<Rightarrow> False | Some a \<Rightarrow> True)"

constdefs aF::"jbc_prog \<Rightarrow> pos \<Rightarrow> expr"
"aF \<Pi> p \<equiv> (case anF \<Pi> p of None \<Rightarrow> TT | Some A \<Rightarrow> A)"

constdefs
domA :: "jbc_prog \<Rightarrow> pos list"
"domA \<equiv> (\<lambda> \<Pi>.[p\<in> domC \<Pi>. hasAn \<Pi> p])"

consts
invokes::"instr option \<times> pos \<Rightarrow> bool"

recdef invokes "{}"
--"invokes (ins,(C,M,p)) checks whether ins calls method M."
"invokes (Some (Invoke Mn n),(C,M,pc)) = (Mn=M)"
"invokes (instr,p) = False"

constdefs
callers::"jbc_prog \<Rightarrow> pos \<Rightarrow> pos list"
"callers \<Pi> p \<equiv> [cp \<in> (domC \<Pi>). invokes ((cmd \<Pi> cp),p)]"

constdefs classnames ::"jvm_prog \<Rightarrow> cname list"
"classnames P \<equiv> map fst P"

constdefs has_method::"jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> bool"
"has_method P C M \<equiv> (C,M) mem (methodnames P)"

subsection {* Operational Semantics *}

constdefs
 Start :: cname
 "Start \<equiv> ''Start''"
 main ::mname
 "main \<equiv> ''main''"

constdefs ipc::"jbc_prog \<Rightarrow> pos"
"ipc P \<equiv> (Start,main,0)"

section {* Transition Relation *}

consts
effS::"jbc_prog \<Rightarrow> (jbc_state \<times> jbc_state) set"


--{* Note: In case of an uncaught exception this semantics halts, 
     whereas the JVM Semantics halts and empties the framestack. *}
inductive "effS \<Pi>"
intros

expt:
"\<lbrakk> P = fst \<Pi>; p = (C,M,pc); i = instrs_of P C M ! pc;
   \<sigma> = (None,h,(stk,loc,p)#frs);
   has_method P C M;
   exec_instr i P h stk loc C M pc frs = (Some xa,h',bla);
   find_handler P xa h ((stk,loc,p)#frs) = \<sigma>'; 
   \<sigma>' = (None,h,([Addr xa],loc',p')#frs');
   e' = e\<lparr>cs:=drop (length frs - length frs') (cs e)\<rparr>  
 \<rbrakk> \<Longrightarrow> ((p,\<sigma>,e),(p',\<sigma>',e')) \<in> effS \<Pi>"


nrml:
"\<lbrakk> P = fst \<Pi>; p = (C,M,pc); i = instrs_of P C M ! pc;
   \<sigma> = (None,h,(stk,loc,p)#frs);
   has_method P C M;
   exec_instr i P h stk loc C M pc frs = (None,h',fr'#frs');
   \<sigma>' = (None,h',fr' # frs');
   p' = snd (snd fr');
   e' = e\<lparr>cs:=if \<exists>M n. i = Invoke M n then h#(cs e)
        else if i = Return then tl (cs e) else cs e\<rparr> 
\<rbrakk> \<Longrightarrow> ((p,\<sigma>,e),(p',\<sigma>',e')) \<in> effS \<Pi>"


constdefs
initS ::"jbc_prog \<Rightarrow> jbc_state set"
"initS \<Pi> \<equiv> { (p,\<sigma>,e) . p = ipc \<Pi> \<and> \<sigma> = start_state (fst \<Pi>) (fst (ipc \<Pi>)) (fst (snd (ipc \<Pi>))) \<and> cs e = [] }"


consts Reachables::"jbc_prog \<Rightarrow> jbc_state set"

inductive "Reachables \<Pi>"
intros
init: "\<lbrakk> s \<in> initS \<Pi>  \<rbrakk> \<Longrightarrow> s \<in> Reachables \<Pi>"
step: "\<lbrakk> s \<in> Reachables \<Pi>; (s,s') \<in> effS \<Pi> \<rbrakk> 
        \<Longrightarrow> s' \<in> Reachables \<Pi>"

section {* Auxiliary Lemmas *}

lemma sees_field_class:
"P \<turnstile> Cl sees F:T in Cl' \<Longrightarrow> is_class P Cl"
(*<*)
apply (simp add: is_class_def)
apply (drule has_visible_field)
apply (simp only: has_field_def)
apply (erule conjE  | erule exE)+
apply (erule Fields.elims)
apply fastsimp
apply fastsimp
done
(*>*)


lemma domCC_split:
"domCC (C,(S,fs,ms@ms')) = domCC (C,(S,fs,ms)) @ domCC (C,(S,fs,ms'))"
(*<*)
apply (induct ms)
apply (simp add: split_paired_all domCC.simps)+
done
(*>*)


lemma cmd_domC:
"\<And>p \<Pi> instr.  cmd \<Pi> p = Some instr \<Longrightarrow> p\<in> set (domC \<Pi>)"
(*<*)
apply (simp add: domC_def cmd_def domCC.simps split_def split_paired_all fst_conv snd_conv split add: split_if_asm)
apply (rule_tac x="(a,ac,ad,ba)" in bexI)
apply (drule map_of_SomeD)
apply (simp add: domCC.simps in_set_conv_decomp)
apply (erule exE)+
apply (simp add: domCC_split)
apply (subgoal_tac "(upt 0 (length ai)) = (upt 0 b)@(upt b (length ai))")
 prefer 2
 apply (subgoal_tac "\<exists>c. length ai = b + c")
  prefer 2
  apply (rule_tac x="length ai - b" in exI)
  apply arith
 apply (erule exE)
 apply simp
 apply (rule upt_add_eq_append)
 apply simp
apply (simp add: upt_conv_Cons)
apply (rule_tac x="domCC (a, ac, ad, ys) @
                    map (\<lambda>n. (a, aa, n)) (upt 0 b)" in exI)
apply fastsimp
apply (rule map_of_SomeD)
apply (simp add: class_def)
done
(*>*)


lemma domC_cmd:
"p\<notin> set (domC \<Pi>) \<Longrightarrow>  cmd \<Pi> p = None"
(*<*)
apply (rule classical)
apply simp
apply (erule exE)
apply (drule cmd_domC)
apply simp
done 
(*>*)


lemma domCC_split_parts:
"(C,M,pc) \<in> set (domCC (C',S,Fs,Ms)) \<Longrightarrow> 
\<exists> Ms' Ms'' Ts T mxs mxl is et. Ms = Ms' @ (M,Ts,T,(mxs,mxl,is,et)) # Ms'' 
\<and> (C,M,pc) \<in> set (domMC (C',M,mxs,mxl,is,et))"
(*<*)
apply (induct Ms)
apply simp

apply (simp add: split_paired_all domCC.simps)
apply (erule disjE)

apply (erule imageE)
apply (rule_tac x="[]" in exI)
apply (rule_tac x="Ms" in exI)
apply fastsimp

apply simp
apply (erule exE | erule conjE)+
apply (rule_tac x="(a,aa,ab,ac,ad,ae,b)#Ms'" in exI)
apply fastsimp
done
(*>*)


lemma domCC_map:
"domCC (C,C',fs,ms) = concat (map (\<lambda> (M,Ts,T,m). domMC (C,M,m)) ms)"
(*<*)
apply (induct ms)
apply simp
apply (simp add: split_paired_all)
done
(*>*)


lemma domMC_props:
"\<And> m. (C,M,pc) \<in> set (domMC (C',M',m)) \<Longrightarrow> C = C' \<and> M = M' \<and> pc < length (fst (snd (snd m)))"
(*<*)
apply (subgoal_tac "\<exists> mxs mxr is et. m = (mxs,mxr,is,et)")
 prefer 2
 apply (simp add: split_paired_all)
apply (erule exE)+
apply (simp only: domMC.simps)
apply (simp add: set_map)
apply (erule imageE)
apply simp
done
(*>*)


lemma domA_simp:
"domA = (\<lambda>\<Pi>. [pc\<in>domC \<Pi>. anF \<Pi> pc \<noteq> None])"
(*<*)
apply (rule ext)
apply (simp add: domA_def)
done
(*>*)


lemma effS_Reachables:
"s \<in> Reachables \<Pi> = (\<exists> s0. s0 \<in> initS \<Pi> \<and> (s0,s) \<in> (effS \<Pi>)\<^sup>*)"
(*<*)
apply (rule iffI)
-- {* if *}
apply (erule Reachables.induct)
apply (rule_tac x="s" in exI)
apply simp

apply (erule exE | erule conjE)+
apply (rule_tac x="s0" in exI)
apply (rule conjI)
apply assumption

apply (rule_tac b="s" in rtrancl_into_rtrancl)
apply assumption
apply assumption

--{* only if *}
apply (erule exE | erule conjE)+
apply (erule rev_mp)
apply (erule  rtrancl.induct)
apply (rule impI)
apply (rule Reachables.init)
apply assumption

apply (rule impI)
apply (rule Reachables.step)
apply simp

apply simp
done
(*>*)

lemma check_inv:
assumes wt:"wf_jvm_prog\<^isub>k P"
assumes initial:"\<sigma> = start_state P C M \<and> (P \<turnstile> C sees M:[]\<rightarrow>T = m in C)"
assumes reachable:"P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'"
shows "check P \<sigma>'"
(*<*)
proof -
 from wt have wf_P:"\<exists> \<Phi>. wf_jvm_prog\<^sub>\<Phi>  P " by (simp add: jvm_kildall_correct wf_jvm_prog_def)
 from initial reachable show ?thesis proof -
  from wf_P obtain \<Phi> where wf_P': "wf_jvm_prog\<^sub>\<Phi>  P" ..
  from this have state_ok: "P,\<Phi> \<turnstile> \<sigma>' \<surd>" proof (rule typesafe)
   from initial show "P \<turnstile> C sees M: []\<rightarrow>T = m in C" ..
   from initial reachable show "P \<turnstile> start_state P C M -jvm\<rightarrow> \<sigma>'" by simp
  qed
 from wf_P' this have "exec_d P \<sigma>' \<noteq> TypeError" proof (rule no_type_error) qed
 from this show "check P \<sigma>'" apply (simp add: exec_d_def split add: split_if_asm) done qed
qed
(*>*)

end