Theory BVExec
section ‹ Kildall for the JVM \label{sec:JVM} ›
theory BVExec
imports Jinja.Abstract_BV TF_JVM Jinja.Typing_Framework_2
begin
definition kiljvm :: "jvm_prog ⇒ nat ⇒ nat ⇒ ty ⇒
instr list ⇒ ex_table ⇒ ty⇩i' err list ⇒ ty⇩i' err list"
where
"kiljvm P mxs mxl T⇩r is xt ≡
kildall (JVM_SemiType.le P mxs mxl) (JVM_SemiType.sup P mxs mxl)
(exec P mxs T⇩r xt is)"
definition wt_kildall :: "jvm_prog ⇒ cname ⇒ staticb ⇒ ty list ⇒ ty ⇒ nat ⇒ nat ⇒
instr list ⇒ ex_table ⇒ bool"
where
"wt_kildall P C' b Ts T⇩r mxs mxl⇩0 is xt ≡ (b = Static ∨ b = NonStatic) ∧
0 < size is ∧
(let first = Some ([],(case b of Static ⇒ [] | NonStatic ⇒ [OK (Class C')])
@(map OK Ts)@(replicate mxl⇩0 Err));
start = (OK first)#(replicate (size is - 1) (OK None));
result = kiljvm P mxs
((case b of Static ⇒ 0 | NonStatic ⇒ 1)+size Ts+mxl⇩0)
T⇩r is xt start
in ∀n < size is. result!n ≠ Err)"
definition wf_jvm_prog⇩k :: "jvm_prog ⇒ bool"
where
"wf_jvm_prog⇩k P ≡
wf_prog (λP C' (M,b,Ts,T⇩r,(mxs,mxl⇩0,is,xt)). wt_kildall P C' b Ts T⇩r mxs mxl⇩0 is xt) P"
context start_context
begin
lemma Cons_less_Conss3 [simp]:
"x#xs [⊏⇘r⇙] y#ys = (x ⊏⇘r⇙ y ∧ xs [⊑⇘r⇙] ys ∨ x = y ∧ xs [⊏⇘r⇙] ys)"
apply (unfold lesssub_def )
apply auto
apply (insert sup_state_opt_err)
apply (unfold lesssub_def lesub_def sup_state_opt_def sup_state_def sup_ty_opt_def)
apply (simp only: JVM_le_unfold )
apply fastforce
done
lemma acc_le_listI3 [intro!]:
" acc r ⟹ acc (Listn.le r)"
apply (unfold acc_def)
apply (subgoal_tac
"wf(UN n. {(ys,xs). size xs = n ∧ size ys = n ∧ xs <_(Listn.le r) ys})")
apply (erule wf_subset)
apply (blast intro: lesssub_lengthD)
apply (rule wf_UN)
prefer 2
apply (rename_tac m n)
apply (case_tac "m=n")
apply simp
apply (fast intro!: equals0I dest: not_sym)
apply (rename_tac n)
apply (induct_tac n)
apply (simp add: lesssub_def cong: conj_cong)
apply (rename_tac k)
apply (simp add: wf_eq_minimal del: r_def f_def step_def A_def)
apply (simp (no_asm) add: length_Suc_conv cong: conj_cong del: r_def f_def step_def A_def)
apply clarify
apply (rename_tac M m)
apply (case_tac "∃x xs. size xs = k ∧ x#xs ∈ M")
prefer 2
apply (erule thin_rl)
apply (erule thin_rl)
apply blast
apply (erule_tac x = "{a. ∃xs. size xs = k ∧ a#xs:M}" in allE)
apply (erule impE)
apply blast
apply (thin_tac "∃x xs. P x xs" for P)
apply clarify
apply (rename_tac maxA xs)
apply (erule_tac x = "{ys. size ys = size xs ∧ maxA#ys ∈ M}" in allE)
apply (erule impE)
apply blast
apply clarify
apply (thin_tac "m ∈ M")
apply (thin_tac "maxA#xs ∈ M")
apply (rule bexI)
prefer 2
apply assumption
apply clarify
apply (simp del: r_def f_def step_def A_def)
apply blast
done
lemma wf_jvm: " wf {(ss', ss). ss [⊏⇘r⇙] ss'}"
apply (insert acc_le_listI3 acc_JVM [OF wf])
by (simp add: acc_def r_def)
lemma iter_properties_bv[rule_format]:
shows "⟦ ∀p∈w0. p < n; ss0 ∈ nlists n A; ∀p<n. p ∉ w0 ⟶ stable r step ss0 p ⟧ ⟹
iter f step ss0 w0 = (ss',w') ⟶
ss' ∈ nlists n A ∧ stables r step ss' ∧ ss0 [⊑⇩r] ss' ∧
(∀ts∈nlists n A. ss0 [⊑⇩r] ts ∧ stables r step ts ⟶ ss' [⊑⇩r] ts)"
(is "PROP ?P")
proof -
show "PROP ?P"
apply (insert semi bounded_step exec_pres_type step_mono[OF wf])
apply (unfold iter_def stables_def)
apply (rule_tac P = "λ(ss,w).
ss ∈ nlists n A ∧ (∀p<n. p ∉ w ⟶ stable r step ss p) ∧ ss0 [⊑⇩r] ss ∧
(∀ts∈nlists n A. ss0 [⊑⇩r] ts ∧ stables r step ts ⟶ ss [⊑⇩r] ts) ∧
(∀p∈w. p < n)" and
r = "{(ss',ss) . ss [⊏⇩r] ss'} <*lex*> finite_psubset"
in while_rule)
apply (simp add:stables_def semilat_Def del: n_def A_def r_def f_def step_def)
apply (blast intro:le_list_refl')
apply(simp add: stables_def split_paired_all del: A_def r_def f_def step_def n_def)
apply(rename_tac ss w)
apply(subgoal_tac "(SOME p. p ∈ w) ∈ w")
prefer 2 apply (fast intro: someI)
apply(subgoal_tac "∀(q,t) ∈ set (step (SOME p. p ∈ w) (ss ! (SOME p. p ∈ w))). q < length ss ∧ t ∈ A")
prefer 2
apply clarify
apply (rule conjI)
apply(clarsimp, blast dest!: boundedD)
apply (subgoal_tac "(SOME p. p ∈ w) < n")
apply (subgoal_tac "(ss ! (SOME p. p ∈ w)) ∈ A")
apply (fastforce simp only:n_def dest:pres_typeD )
apply simp
apply simp
apply (subst decomp_propa)
apply blast
apply (simp del:A_def r_def f_def step_def n_def)
apply (rule conjI)
apply (rule Semilat.merges_preserves_type[OF Semilat.intro, OF semi])
apply blast
apply clarify
apply (rule conjI)
apply(clarsimp, blast dest!: boundedD)
apply (erule pres_typeD)
prefer 3
apply assumption
apply (erule nlistsE_nth_in)
apply blast
apply (simp only:n_def)
apply (rule conjI)
apply clarify
apply (subgoal_tac "ss ∈ nlists (length is) A" "∀p∈w. p < (length is) " "∀p<(length is). p ∉ w ⟶ stable r step ss p "
"p < length is")
apply (blast intro!: Semilat.stable_pres_lemma[OF Semilat.intro, OF semi])
apply (simp only:n_def)
apply (simp only:n_def)
apply (simp only:n_def)
apply (simp only:n_def)
apply (rule conjI)
apply (subgoal_tac "ss ∈ nlists (length is) A"
"∀(q,t)∈set (step (SOME p. p ∈ w) (ss ! (SOME p. p ∈ w))). q < length is ∧ t ∈ A"
"ss [⊑⇘r⇙] merges f (step (SOME p. p ∈ w) (ss ! (SOME p. p ∈ w))) ss" "ss0∈ nlists (size is) A"
"merges f (step (SOME p. p ∈ w) (ss ! (SOME p. p ∈ w))) ss ∈ nlists (size is) A"
"ss ∈nlists (size is) A" "order r A" "ss0 [⊑⇘r⇙] ss ")
apply (blast dest: le_list_trans)
apply simp
apply (simp only:semilat_Def)
apply (simp only:n_def)
apply (fastforce simp only: n_def dest:Semilat.merges_preserves_type[OF Semilat.intro, OF semi] )
apply (simp only:n_def)
apply (blast intro:Semilat.merges_incr[OF Semilat.intro, OF semi])
apply (subgoal_tac "length ss = n")
apply (simp only:n_def)
apply (subgoal_tac "ss ∈nlists n A")
defer
apply simp
apply (simp only:n_def)
prefer 5
apply (simp only:nlistsE_length n_def)
apply(rule conjI)
apply (clarsimp simp del: A_def r_def f_def step_def)
apply (blast intro!: Semilat.merges_bounded_lemma[OF Semilat.intro, OF semi])
apply (subgoal_tac "bounded step n")
apply (blast dest!: boundedD)
apply (simp only:n_def)
apply(clarsimp simp add: stables_def split_paired_all)
apply (rule wf_lex_prod)
apply (simp only:wf_jvm)
apply (rule wf_finite_psubset)
apply(simp add: stables_def split_paired_all del: A_def r_def f_def step_def)
apply(rename_tac ss w)
apply(subgoal_tac "(SOME p. p ∈ w) ∈ w")
prefer 2 apply (fast intro: someI)
apply(subgoal_tac "∀(q,t) ∈ set (step (SOME p. p ∈ w) (ss ! (SOME p. p ∈ w))). q < length ss ∧ t ∈ A")
prefer 2
apply clarify
apply (rule conjI)
apply(clarsimp, blast dest!: boundedD)
apply (erule pres_typeD)
prefer 3
apply assumption
apply (erule nlistsE_nth_in)
apply blast
apply blast
apply (subst decomp_propa)
apply blast
apply clarify
apply (simp del: nlistsE_length A_def r_def f_def step_def
add: lex_prod_def finite_psubset_def
bounded_nat_set_is_finite)
apply (rule termination_lemma)
apply (insert Semilat.intro)
apply assumption+
defer
apply assumption
defer
apply clarsimp
done
qed
lemma kildall_properties_bv:
shows "⟦ ss0 ∈ nlists n A ⟧ ⟹
kildall r f step ss0 ∈ nlists n A ∧
stables r step (kildall r f step ss0) ∧
ss0 [⊑⇩r] kildall r f step ss0 ∧
(∀ts∈nlists n A. ss0 [⊑⇩r] ts ∧ stables r step ts ⟶
kildall r f step ss0 [⊑⇩r] ts)"
(is "PROP ?P")
proof -
show "PROP ?P"
apply (unfold kildall_def)
apply(case_tac "iter f step ss0 (unstables r step ss0)")
apply (simp del:r_def f_def n_def step_def A_def)
apply (rule iter_properties_bv)
apply (simp_all add: unstables_def stable_def)
done
qed
end
theorem (in start_context) is_bcv_kiljvm:
"is_bcv r Err step (size is) A (kiljvm P mxs mxl T⇩r is xt)"
apply (insert wf)
apply (unfold kiljvm_def)
apply (fold r_def f_def step_def_exec n_def)
apply(unfold is_bcv_def wt_step_def)
apply(insert semi kildall_properties_bv)
apply(simp only:stables_def)
apply clarify
apply(subgoal_tac "kildall r f step τs⇩0 ∈ nlists n A")
prefer 2
apply (fastforce intro: kildall_properties_bv)
apply (rule iffI)
apply (rule_tac x = "kildall r f step τs⇩0" in bexI)
apply (rule conjI)
apply (fastforce intro: kildall_properties_bv)
apply (force intro: kildall_properties_bv)
apply simp
apply clarify
apply(subgoal_tac "kildall r f step τs⇩0!pa <=_r τs!pa")
defer
apply (blast intro!: le_listD less_lengthI)
apply (subgoal_tac "τs!pa ≠ Err")
defer
apply simp
apply (rule ccontr)
apply (simp only:top_def r_def JVM_le_unfold)
apply fastforce
done
lemma subset_replicate [intro?]: "set (replicate n x) ⊆ {x}"
by (induct n) auto
lemma in_set_replicate:
assumes "x ∈ set (replicate n y)"
shows "x = y"
proof -
note assms
also have "set (replicate n y) ⊆ {y}" ..
finally show ?thesis by simp
qed
lemma (in start_context) start_in_A [intro?]:
"0 < size is ⟹ start ∈ nlists (size is) A"
using Ts C
proof(cases b)
qed (force simp: JVM_states_unfold intro!: nlistsI nlists_appendI
dest!: in_set_replicate)+
theorem (in start_context) wt_kil_correct:
assumes wtk: "wt_kildall P C b Ts T⇩r mxs mxl⇩0 is xt"
shows "∃τs. wt_method P C b Ts T⇩r mxs mxl⇩0 is xt τs"
proof -
from wtk obtain res where
result: "res = kiljvm P mxs mxl T⇩r is xt start" and
success: "∀n < size is. res!n ≠ Err" and
instrs: "0 < size is" and
stab: "b = Static ∨ b = NonStatic"
by (unfold wt_kildall_def) simp
have bcv: "is_bcv r Err step (size is) A (kiljvm P mxs mxl T⇩r is xt)"
by (rule is_bcv_kiljvm)
from instrs have "start ∈ nlists (size is) A" ..
with bcv success result have
"∃ts∈nlists (size is) A. start [⊑⇩r] ts ∧ wt_step r Err step ts"
by (unfold is_bcv_def) blast
then obtain τs' where
in_A: "τs' ∈ nlists (size is) A" and
s: "start [⊑⇩r] τs'" and
w: "wt_step r Err step τs'"
by blast
hence wt_err_step: "wt_err_step (sup_state_opt P) step τs'"
by (simp add: wt_err_step_def JVM_le_Err_conv)
from in_A have l: "size τs' = size is" by simp
moreover {
from in_A have "check_types P mxs mxl τs'" by (simp add: check_types_def)
also from w have "∀x ∈ set τs'. x ≠ Err"
by (auto simp add: wt_step_def all_set_conv_all_nth)
hence [symmetric]: "map OK (map ok_val τs') = τs'"
by (auto intro!: map_idI simp add: wt_step_def)
finally have "check_types P mxs mxl (map OK (map ok_val τs'))" .
}
moreover {
from s have "start!0 ⊑⇩r τs'!0" by (rule le_listD) simp
moreover
from instrs w l
have "τs'!0 ≠ Err" by (unfold wt_step_def) simp
then obtain τs0 where "τs'!0 = OK τs0" by auto
ultimately
have "wt_start P C b Ts mxl⇩0 (map ok_val τs')" using l instrs
by (unfold wt_start_def)
(cases b; simp add: lesub_def JVM_le_Err_conv Err.le_def)
}
moreover
from in_A have "set τs' ⊆ A" by simp
with wt_err_step bounded_step
have "wt_app_eff (sup_state_opt P) app eff (map ok_val τs')"
by (auto intro: wt_err_imp_wt_app_eff simp add: l)
ultimately
have "wt_method P C b Ts T⇩r mxs mxl⇩0 is xt (map ok_val τs')"
using instrs stab by (simp add: wt_method_def2 check_types_def del: map_map)
thus ?thesis by blast
qed
theorem (in start_context) wt_kil_complete:
assumes wtm: "wt_method P C b Ts T⇩r mxs mxl⇩0 is xt τs"
shows "wt_kildall P C b Ts T⇩r mxs mxl⇩0 is xt"
proof -
from wtm obtain
instrs: "0 < size is" and
length: "length τs = length is" and
ck_type: "check_types P mxs mxl (map OK τs)" and
wt_start: "wt_start P C b Ts mxl⇩0 τs" and
app_eff: "wt_app_eff (sup_state_opt P) app eff τs" and
stab: "b = Static ∨ b = NonStatic"
by (simp add: wt_method_def2 check_types_def )
from ck_type
have in_A: "set (map OK τs) ⊆ A"
by (simp add: check_types_def)
with app_eff in_A bounded_step
have "wt_err_step (sup_state_opt P) (err_step (size τs) app eff) (map OK τs)"
by - (erule wt_app_eff_imp_wt_err,
auto simp add: exec_def length states_def)
hence wt_err: "wt_err_step (sup_state_opt P) step (map OK τs)"
by (simp add: length)
have is_bcv: "is_bcv r Err step (size is) A (kiljvm P mxs mxl T⇩r is xt)"
by (rule is_bcv_kiljvm)
moreover from instrs have "start ∈ nlists (size is) A" ..
moreover
let ?τs = "map OK τs"
have less_τs: "start [⊑⇩r] ?τs"
proof (rule le_listI)
from length instrs
show "length start = length (map OK τs)" by simp
next
fix n
from wt_start have "P ⊢ ok_val (start!0) ≤' τs!0"
by (cases b; simp add: wt_start_def)
moreover from instrs length have "0 < length τs" by simp
ultimately have "start!0 ⊑⇩r ?τs!0"
by (simp add: JVM_le_Err_conv lesub_def)
moreover {
fix n'
have "OK None ⊑⇩r ?τs!n"
by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def
split: err.splits)
hence "⟦n = Suc n'; n < size start⟧ ⟹ start!n ⊑⇩r ?τs!n" by simp
}
ultimately
show "n < size start ⟹ start!n ⊑⇩r ?τs!n" by (cases n, blast+)
qed
moreover
from ck_type length
have "?τs ∈ nlists (size is) A"
by (auto intro!: nlistsI simp add: check_types_def)
moreover
from wt_err have "wt_step r Err step ?τs"
by (simp add: wt_err_step_def JVM_le_Err_conv)
ultimately
have "∀p. p < size is ⟶ kiljvm P mxs mxl T⇩r is xt start ! p ≠ Err"
by (unfold is_bcv_def) blast
with instrs
show "wt_kildall P C b Ts T⇩r mxs mxl⇩0 is xt"
using start_context_intro_auxi[OF staticb] using stab by (unfold wt_kildall_def) simp
qed
theorem jvm_kildall_correct:
"wf_jvm_prog⇩k P = wf_jvm_prog P"
proof -
let ?Φ = "λC M. let (C,b,Ts,T⇩r,(mxs,mxl⇩0,is,xt)) = method P C M in
SOME τs. wt_method P C b Ts T⇩r mxs mxl⇩0 is xt τs"
let ?A = "λP C' (M, b, Ts, T⇩r, mxs, mxl⇩0, is, xt). wt_kildall P C' b Ts T⇩r mxs mxl⇩0 is xt"
let ?B⇩Φ = "λΦ. (λP C (M,b,Ts,T⇩r,(mxs,mxl⇩0,is,xt)).
wt_method P C b Ts T⇩r mxs mxl⇩0 is xt (Φ C M))"
show ?thesis proof(rule iffI)
assume wt: "wf_jvm_prog⇩k P"
then have wt': "wf_prog ?A P" by(simp add: wf_jvm_prog⇩k_def)
moreover {
fix wf_md C M b Ts Ca T m bd
assume ass1: "wf_prog wf_md P" and sees: "P ⊢ Ca sees M, b : Ts→T = m in Ca" and
ass2: "set Ts ⊆ types P" and ass3: "bd = (M, b, Ts, T, m)" and
ass4: "?A P Ca bd"
from ass3 ass4 have stab: "b = Static ∨ b = NonStatic" by (simp add:wt_kildall_def)
from ass1 sees ass2 ass3 ass4 have "(?B⇩Φ ?Φ) P Ca bd" using sees_method_is_class[OF sees]
by (auto dest!: start_context.wt_kil_correct[OF start_context_intro_auxi[OF stab]]
intro: someI)
}
ultimately have "wf_prog (?B⇩Φ ?Φ) P" by(rule wf_prog_lift)
then have "wf_jvm_prog⇘?Φ⇙ P" by (simp add: wf_jvm_prog_phi_def)
thus "wf_jvm_prog P" by (unfold wf_jvm_prog_def) fast
next
assume wt: "wf_jvm_prog P"
then obtain Φ where "wf_prog (?B⇩Φ Φ) P" by(clarsimp simp: wf_jvm_prog_def wf_jvm_prog_phi_def)
moreover {
fix wf_md C M b Ts Ca T m bd
assume ass1: "wf_prog wf_md P" and sees: "P ⊢ Ca sees M, b : Ts→T = m in Ca" and
ass2: "set Ts ⊆ types P" and ass3: "bd = (M, b, Ts, T, m)" and
ass4: "(?B⇩Φ Φ) P Ca bd"
from ass3 ass4 have stab: "b = Static ∨ b = NonStatic" by (simp add:wt_method_def)
from ass1 sees ass2 ass3 ass4 have "?A P Ca bd" using sees_method_is_class[OF sees] using JVM_sl.staticb
by (auto intro!: start_context.wt_kil_complete start_context_intro_auxi[OF stab])
}
ultimately have "wf_prog ?A P" by(rule wf_prog_lift)
thus "wf_jvm_prog⇩k P" by (simp add: wf_jvm_prog⇩k_def)
qed
qed
end