Theory TF_JVM
section ‹The Typing Framework for the JVM \label{sec:JVM}›
theory TF_JVM
imports "../DFA/Typing_Framework_err" EffectMono BVSpec
begin
definition exec :: "jvm_prog ⇒ nat ⇒ ty ⇒ ex_table ⇒ instr list ⇒ ty⇩i' err step_type"
where
"exec G maxs rT et bs ≡
err_step (size bs) (λpc. app (bs!pc) G maxs rT pc (size bs) et)
(λpc. eff (bs!pc) G pc et)"
locale JVM_sl =
fixes P :: jvm_prog and mxs and mxl⇩0 and n
fixes Ts :: "ty list" and "is" and xt and T⇩r
fixes mxl and A and r and f and app and eff and step
defines [simp]: "mxl ≡ 1+size Ts+mxl⇩0"
defines [simp]: "A ≡ states P mxs mxl"
defines [simp]: "r ≡ JVM_SemiType.le P mxs mxl"
defines [simp]: "f ≡ JVM_SemiType.sup P mxs mxl"
defines [simp]: "app ≡ λpc. Effect.app (is!pc) P mxs T⇩r pc (size is) xt"
defines [simp]: "eff ≡ λpc. Effect.eff (is!pc) P pc xt"
defines [simp]: "step ≡ err_step (size is) app eff"
defines [simp]: "n ≡ size is"
locale start_context = JVM_sl +
fixes p and C
assumes wf: "wf_prog p P"
assumes C: "is_class P C"
assumes Ts: "set Ts ⊆ types P"
fixes first :: ty⇩i' and start
defines [simp]:
"first ≡ Some ([],OK (Class C) # map OK Ts @ replicate mxl⇩0 Err)"
defines [simp]:
"start ≡ OK first # replicate (size is - 1) (OK None)"
subsection ‹Connecting JVM and Framework›
lemma (in start_context) semi: "semilat (A, r, f)"
apply (insert semilat_JVM[OF wf])
apply (unfold A_def r_def f_def JVM_SemiType.le_def JVM_SemiType.sup_def states_def)
apply auto
done
lemma (in JVM_sl) step_def_exec: "step ≡ exec P mxs T⇩r xt is"
by (simp add: exec_def)
lemma special_ex_swap_lemma [iff]:
"(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
by blast
lemma ex_in_nlists [iff]:
"(∃n. ST ∈ nlists n A ∧ n ≤ mxs) = (set ST ⊆ A ∧ size ST ≤ mxs)"
by (unfold nlists_def) auto
lemma singleton_nlists:
"(∃n. [Class C] ∈ nlists n (types P) ∧ n ≤ mxs) = (is_class P C ∧ 0 < mxs)"
by auto
lemma set_drop_subset:
"set xs ⊆ A ⟹ set (drop n xs) ⊆ A"
by (auto dest: in_set_dropD)
lemma Suc_minus_minus_le:
"n < mxs ⟹ Suc (n - (n - b)) ≤ mxs"
by arith
lemma in_nlistsE:
"⟦ xs ∈ nlists n A; ⟦size xs = n; set xs ⊆ A⟧ ⟹ P ⟧ ⟹ P"
by (unfold nlists_def) blast
declare is_relevant_entry_def [simp]
declare set_drop_subset [simp]
theorem (in start_context) exec_pres_type:
"pres_type step (size is) A"
apply (insert wf)
apply simp
apply (unfold JVM_states_unfold)
apply (rule pres_type_lift)
apply clarify
apply (rename_tac s pc pc' s')
apply (case_tac s)
apply simp
apply (drule effNone)
apply simp
apply (simp add: Effect.app_def xcpt_app_def Effect.eff_def
xcpt_eff_def norm_eff_def relevant_entries_def)
apply (case_tac "is!pc")
apply clarsimp
apply (frule nlistsE_nth_in, assumption)
apply fastforce
apply fastforce
apply (fastforce simp add: typeof_lit_is_type)
apply clarsimp apply fastforce
apply clarsimp apply (fastforce dest: sees_field_is_type)
apply clarsimp apply fastforce
apply clarsimp apply fastforce
defer
apply fastforce
apply fastforce
apply fastforce
apply fastforce
apply fastforce
apply fastforce
apply clarsimp apply fastforce
apply (clarsimp split!: if_splits)
apply fastforce
apply (erule disjE)
prefer 2
apply fastforce
apply clarsimp
apply (rule conjI)
apply (drule (1) sees_wf_mdecl)
apply (clarsimp simp add: wf_mdecl_def)
apply arith
done
declare is_relevant_entry_def [simp del]
declare set_drop_subset [simp del]
lemma lesubstep_type_simple:
"xs [⊑⇘Product.le (=) r⇙] ys ⟹ set xs {⊑⇘r⇙} set ys"
apply (unfold lesubstep_type_def)
apply clarify
apply (simp add: set_conv_nth)
apply clarify
apply (drule le_listD, assumption)
apply (clarsimp simp add: lesub_def Product.le_def)
apply (rule exI)
apply (rule conjI)
apply (rule exI)
apply (rule conjI)
apply (rule sym)
apply assumption
apply assumption
apply assumption
done
declare is_relevant_entry_def [simp del]
lemma conjI2: "⟦ A; A ⟹ B ⟧ ⟹ A ∧ B" by blast
lemma (in JVM_sl) eff_mono:
"⟦wf_prog p P; pc < length is; s ⊑⇘sup_state_opt P⇙ t; app pc t⟧
⟹ set (eff pc s) {⊑⇘sup_state_opt P⇙} set (eff pc t)"
apply simp
apply (unfold Effect.eff_def)
apply (cases t)
apply (simp add: lesub_def)
apply (rename_tac a)
apply (cases s)
apply simp
apply (rename_tac b)
apply simp
apply (rule lesubstep_union)
prefer 2
apply (rule lesubstep_type_simple)
apply (simp add: xcpt_eff_def)
apply (rule le_listI)
apply (simp add: split_beta)
apply (simp add: split_beta)
apply (simp add: lesub_def fun_of_def)
apply (case_tac a)
apply (case_tac b)
apply simp
apply (subgoal_tac "size ab = size aa")
prefer 2
apply (clarsimp simp add: list_all2_lengthD)
apply simp
apply (clarsimp simp add: norm_eff_def lesubstep_type_def lesub_def iff del: sup_state_conv)
apply (rule exI)
apply (rule conjI2)
apply (rule imageI)
apply (clarsimp simp add: Effect.app_def iff del: sup_state_conv)
apply (drule (2) succs_mono)
apply blast
apply simp
apply (erule eff⇩i_mono)
apply simp
apply assumption
apply clarsimp
apply clarsimp
done
lemma (in JVM_sl) bounded_step: "bounded step (size is)"
apply simp
apply (unfold bounded_def err_step_def Effect.app_def Effect.eff_def)
apply (auto simp add: error_def map_snd_def split: err.splits option.splits)
done
theorem (in JVM_sl) step_mono:
"wf_prog wf_mb P ⟹ mono r step (size is) A"
apply (simp add: JVM_le_Err_conv)
apply (insert bounded_step)
apply (unfold JVM_states_unfold)
apply (rule mono_lift)
apply blast
apply (unfold app_mono_def lesub_def)
apply clarsimp
apply (erule (2) app_mono)
apply simp
apply clarify
apply (drule eff_mono)
apply (auto simp add: lesub_def)
done
lemma (in start_context) first_in_A [iff]: "OK first ∈ A"
using Ts C by (force intro!: nlists_appendI simp add: JVM_states_unfold)
lemma (in JVM_sl) wt_method_def2:
"wt_method P C' Ts T⇩r mxs mxl⇩0 is xt τs =
(is ≠ [] ∧
size τs = size is ∧
OK ` set τs ⊆ states P mxs mxl ∧
wt_start P C' Ts mxl⇩0 τs ∧
wt_app_eff (sup_state_opt P) app eff τs)"
apply (unfold wt_method_def wt_app_eff_def wt_instr_def lesub_def check_types_def)
apply auto
done
end