Theory TF_JVM
section ‹ The Typing Framework for the JVM \label{sec:JVM} ›
theory TF_JVM
imports Jinja.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 b and 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 ≡ (case b of Static ⇒ 0 | NonStatic ⇒ 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"
assumes staticb: "b = Static ∨ b = NonStatic"
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 ([],(case b of Static ⇒ [] | NonStatic ⇒ [OK (Class C)]) @ map OK Ts @ replicate mxl⇩0 Err)"
defines [simp]:
"start ≡ (OK first) # replicate (size is - 1) (OK None)"
thm start_context.intro
lemma start_context_intro_auxi:
fixes P b Ts p C
assumes "b = Static ∨ b = NonStatic "
and "wf_prog p P"
and "is_class P C"
and "set Ts ⊆ types P"
shows " start_context P b Ts p C"
using start_context.intro[OF JVM_sl.intro] start_context_axioms_def assms by auto
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_list [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"
proof -
let ?n = "size is" and ?app = app and ?step = eff
let ?mxl = "(case b of Static ⇒ 0 | NonStatic ⇒ 1) + length Ts + mxl⇩0"
let ?A = "opt((Union {nlists n (types P) |n. n <= mxs}) ×
nlists ?mxl (err(types P)))"
have "pres_type (err_step ?n ?app ?step) ?n (err ?A)"
proof(rule pres_type_lift)
have "⋀s pc pc' s'. s∈?A ⟹ pc < ?n ⟹ ?app pc s
⟹ (pc', s')∈set (?step pc s) ⟹ s' ∈ ?A"
proof -
fix s pc pc' s'
assume asms: "s∈?A" "pc < ?n" "?app pc s" "(pc', s')∈set (?step pc s)"
show "s' ∈ ?A"
proof(cases s)
case None
then show ?thesis using asms by (fastforce dest: effNone)
next
case (Some ab)
then show ?thesis using asms proof(cases "is!pc")
case Load
then show ?thesis using asms
by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def
xcpt_eff_def norm_eff_def
dest: nlistsE_nth_in)
next
case Push
then show ?thesis using asms Some
by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def
xcpt_eff_def norm_eff_def typeof_lit_is_type)
next
case Getfield
then show ?thesis using asms wf
by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def
xcpt_eff_def norm_eff_def
dest: sees_field_is_type)
next
case Getstatic
then show ?thesis using asms wf
by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def
xcpt_eff_def norm_eff_def
dest: sees_field_is_type)
next
case (Invoke M n)
obtain a b where [simp]: "s = ⌊(a,b)⌋" using Some asms(1) by blast
show ?thesis
proof(cases "a!n = NT")
case True
then show ?thesis using Invoke asms wf
by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def
xcpt_eff_def norm_eff_def)
next
case False
have "(pc', s') ∈ set (norm_eff (Invoke M n) P pc (a, b)) ∨
(pc', s') ∈ set (xcpt_eff (Invoke M n) P pc (a, b) xt)"
using Invoke asms(4) by (simp add: Effect.eff_def)
then show ?thesis proof(rule disjE)
assume "(pc', s') ∈ set (xcpt_eff (Invoke M n) P pc (a, b) xt)"
then show ?thesis using Invoke asms(1-3)
by (fastforce simp: Effect.app_def xcpt_app_def xcpt_eff_def)
next
assume norm: "(pc', s') ∈ set (norm_eff (Invoke M n) P pc (a, b))"
also have "Suc (length a - Suc n) ≤ mxs" using Invoke asms(1,3)
by (simp add: Effect.app_def xcpt_app_def) arith
ultimately show ?thesis using False Invoke asms(1-3) wf
by (auto simp: Effect.app_def xcpt_app_def norm_eff_def wf_mdecl_def
dest!: sees_wf_mdecl)
qed
qed
next
case (Invokestatic C M n)
obtain a b where [simp]: "s = ⌊(a,b)⌋" using Some asms(1) by blast
have "(pc', s') ∈ set (norm_eff (Invokestatic C M n) P pc (a, b)) ∨
(pc', s') ∈ set (xcpt_eff (Invokestatic C M n) P pc (a, b) xt)"
using Invokestatic asms(4) by (simp add: Effect.eff_def)
then show ?thesis proof(rule disjE)
assume "(pc', s') ∈ set (xcpt_eff (Invokestatic C M n) P pc (a, b) xt)"
then show ?thesis using Invokestatic asms(1-3)
by (fastforce simp: Effect.app_def xcpt_app_def xcpt_eff_def)
next
assume norm: "(pc', s') ∈ set (norm_eff (Invokestatic C M n) P pc (a, b))"
also have "Suc (length a - Suc n) ≤ mxs" using Invokestatic asms(1,3)
by (simp add: Effect.app_def xcpt_app_def) arith
ultimately show ?thesis using Invokestatic asms(1-3) wf
by (auto simp: Effect.app_def xcpt_app_def norm_eff_def wf_mdecl_def
dest!: sees_wf_mdecl)
qed
qed (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def
xcpt_eff_def norm_eff_def)+
qed
qed
then show "∀s∈?A. ∀p. p < ?n ⟶ ?app p s ⟶ (∀(q, s')∈set (?step p s). s' ∈ ?A)"
by clarsimp
qed
then show ?thesis by (simp add: JVM_states_unfold)
qed
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"
proof -
assume assm: "xs [⊑⇘Product.le (=) r⇙] ys"
have "⋀a b i y. (a, b) = xs ! i ⟹ i < length xs
⟹ ∃τ'. (∃i. (a, τ') = ys ! i ∧ i < length xs) ∧ b ⊑⇘r⇙ τ'"
proof -
fix a b i assume ith: "(a, b) = xs ! i" and len: "i < length xs"
obtain τ where "ys ! i = (a, τ) ∧ r b τ"
using le_listD[OF assm len] ith
by (clarsimp simp: lesub_def Product.le_def)
then have "(a, τ) = ys ! i ∧ b ⊑⇘r⇙ τ"
by (clarsimp simp: lesub_def)
with len show "∃τ'. (∃i. (a, τ') = ys ! i ∧ i < length xs) ∧ b ⊑⇘r⇙ τ'"
by fastforce
qed
then show "set xs {⊑⇘r⇙} set ys" using assm
by (clarsimp simp: lesubstep_type_def set_conv_nth)
qed
declare is_relevant_entry_def [simp del]
lemma conjI2: "⟦ A; A ⟹ B ⟧ ⟹ A ∧ B" by blast
lemma (in JVM_sl) eff_mono:
assumes wf: "wf_prog p P" and "pc < length is" and
lesub: "s ⊑⇘sup_state_opt P⇙ t" and app: "app pc t"
shows "set (eff pc s) {⊑⇘sup_state_opt P⇙} set (eff pc t)"
proof(cases t)
case None then show ?thesis using lesub
by (simp add: Effect.eff_def lesub_def)
next
case tSome: (Some a)
show ?thesis proof(cases s)
case None then show ?thesis using lesub
by (simp add: Effect.eff_def lesub_def)
next
case (Some b)
let ?norm = "λx. norm_eff (is ! pc) P pc x"
let ?xcpt = "λx. xcpt_eff (is ! pc) P pc x xt"
let ?r = "Product.le (=) (sup_state_opt P)"
let ?τ' = "⌊eff⇩i (is ! pc, P, a)⌋"
{
fix x assume xb: "x ∈ set (succs (is ! pc) b pc)"
then have appi: "app⇩i (is ! pc, P, pc, mxs, T⇩r, a)" and
bia: "P ⊢ b ≤⇩i a" and appa: "app pc ⌊a⌋"
using lesub app tSome Some by (auto simp add: lesub_def Effect.app_def)
have xa: "x ∈ set (succs (is ! pc) a pc)"
using xb succs_mono[OF wf appi bia] by auto
then have "(x, ?τ') ∈ (λpc'. (pc', ?τ')) ` set (succs (is ! pc) a pc)"
by (rule imageI)
moreover have "P ⊢ ⌊eff⇩i (is ! pc, P, b)⌋ ≤' ?τ'"
using xb xa eff⇩i_mono[OF wf bia] appa by fastforce
ultimately have "∃τ'. (x, τ') ∈ (λpc'. (pc', ⌊eff⇩i (is ! pc, P, a)⌋)) ` set (succs (is ! pc) a pc) ∧
P ⊢ ⌊eff⇩i (is ! pc, P, b)⌋ ≤' τ'" by blast
}
then have norm: "set (?norm b) {⊑⇘sup_state_opt P⇙} set (?norm a)"
using tSome Some by (clarsimp simp: norm_eff_def lesubstep_type_def lesub_def)
obtain a1 b1 a2 b2 where a: "a = (a1, b1)" and b: "b = (a2, b2)"
using tSome Some by fastforce
then have a12: "size a2 = size a1" using lesub tSome Some
by (clarsimp simp: lesub_def list_all2_lengthD)
have "length (?xcpt b) = length (?xcpt a)"
by (simp add: xcpt_eff_def split_beta)
moreover have "⋀n. n < length (?xcpt b) ⟹ (?xcpt b) ! n ⊑⇘?r⇙ (?xcpt a) ! n"
using lesub tSome Some a b a12
by (simp add: xcpt_eff_def split_beta fun_of_def) (simp add: lesub_def)
ultimately have "?xcpt b [⊑⇘?r⇙] ?xcpt a"
by(rule le_listI)
then have "set (?xcpt b) {⊑⇘sup_state_opt P⇙} set (?xcpt a)"
by (rule lesubstep_type_simple)
moreover note norm
ultimately have
"set (?norm b) ∪ set (?xcpt b) {⊑⇘sup_state_opt P⇙} set (?norm a) ∪ set (?xcpt a)"
by(intro lesubstep_union)
then show ?thesis using tSome Some by(simp add: Effect.eff_def)
qed
qed
lemma (in JVM_sl) bounded_step: "bounded step (size is)"
by (auto simp: bounded_def err_step_def Effect.app_def Effect.eff_def
error_def map_snd_def
split: err.splits option.splits)
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 (subgoal_tac "b = Static ∨ b = NonStatic")
apply (fastforce split:if_splits)
apply (simp only:staticb)
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 (cases b; force intro!: nlists_appendI simp add: JVM_states_unfold)
lemma (in JVM_sl) wt_method_def2:
"wt_method P C' b Ts T⇩r mxs mxl⇩0 is xt τs =
(is ≠ [] ∧
(b = Static ∨ b = NonStatic) ∧
size τs = size is ∧
OK ` set τs ⊆ states P mxs mxl ∧
wt_start P C' b Ts mxl⇩0 τs ∧
wt_app_eff (sup_state_opt P) app eff τs)"
using staticb
by (unfold wt_method_def wt_app_eff_def wt_instr_def lesub_def
check_types_def) auto
end