header {* \isaheader{LBV for the JVM}\label{sec:JVM} *}
theory LBVJVM
imports "../DFA/Abstract_BV" TF_JVM
begin
type_synonym prog_cert = "cname => mname => ty⇣i' err list"
definition check_cert :: "jvm_prog => nat => nat => nat => ty⇣i' err list => bool"
where
"check_cert P mxs mxl n cert ≡ check_types P mxs mxl cert ∧ size cert = n+1 ∧
(∀i<n. cert!i ≠ Err) ∧ cert!n = OK None"
definition lbvjvm :: "jvm_prog => nat => nat => ty => ex_table =>
ty⇣i' err list => instr list => ty⇣i' err => ty⇣i' err"
where
"lbvjvm P mxs maxr T⇣r et cert bs ≡
wtl_inst_list bs cert (JVM_SemiType.sup P mxs maxr) (JVM_SemiType.le P mxs maxr) Err (OK None) (exec P mxs T⇣r et bs) 0"
definition wt_lbv :: "jvm_prog => cname => ty list => ty => nat => nat =>
ex_table => ty⇣i' err list => instr list => bool"
where
"wt_lbv P C Ts T⇣r mxs mxl⇣0 et cert ins ≡
check_cert P mxs (1+size Ts+mxl⇣0) (size ins) cert ∧
0 < size ins ∧
(let start = Some ([],(OK (Class C))#((map OK Ts))@(replicate mxl⇣0 Err));
result = lbvjvm P mxs (1+size Ts+mxl⇣0) T⇣r et cert ins (OK start)
in result ≠ Err)"
definition wt_jvm_prog_lbv :: "jvm_prog => prog_cert => bool"
where
"wt_jvm_prog_lbv P cert ≡
wf_prog (λP C (mn,Ts,T⇣r,(mxs,mxl⇣0,b,et)). wt_lbv P C Ts T⇣r mxs mxl⇣0 et (cert C mn) b) P"
definition mk_cert :: "jvm_prog => nat => ty => ex_table => instr list
=> ty⇣m => ty⇣i' err list"
where
"mk_cert P mxs T⇣r et bs phi ≡ make_cert (exec P mxs T⇣r et bs) (map OK phi) (OK None)"
definition prg_cert :: "jvm_prog => ty⇣P => prog_cert"
where
"prg_cert P phi C mn ≡ let (C,Ts,T⇣r,(mxs,mxl⇣0,ins,et)) = method P C mn
in mk_cert P mxs T⇣r et ins (phi C mn)"
lemma check_certD [intro?]:
"check_cert P mxs mxl n cert ==> cert_ok cert n Err (OK None) (states P mxs mxl)"
by (unfold cert_ok_def check_cert_def check_types_def) auto
lemma (in start_context) wt_lbv_wt_step:
assumes lbv: "wt_lbv P C Ts T⇣r mxs mxl⇣0 xt cert is"
shows "∃τs ∈ list (size is) A. wt_step r Err step τs ∧ OK first \<sqsubseteq>⇩r τs!0"
proof -
from wf have "semilat (JVM_SemiType.sl P mxs mxl)" ..
hence "semilat (A, r, f)" by (simp add: sl_def2)
moreover have "top r Err" by (simp add: JVM_le_Err_conv)
moreover have "Err ∈ A" by (simp add: JVM_states_unfold)
moreover have "bottom r (OK None)"
by (simp add: JVM_le_Err_conv bottom_def lesub_def Err.le_def split: err.split)
moreover have "OK None ∈ A" by (simp add: JVM_states_unfold)
moreover note bounded_step
moreover from lbv have "cert_ok cert (size is) Err (OK None) A"
by (unfold wt_lbv_def) (auto dest: check_certD)
moreover note exec_pres_type
moreover
from lbv
have "wtl_inst_list is cert f r Err (OK None) step 0 (OK first) ≠ Err"
by (simp add: wt_lbv_def lbvjvm_def step_def_exec [symmetric])
moreover note first_in_A
moreover from lbv have "0 < size is" by (simp add: wt_lbv_def)
ultimately show ?thesis by (rule lbvs.wtl_sound_strong [OF lbvs.intro, OF lbv.intro lbvs_axioms.intro, OF Semilat.intro lbv_axioms.intro])
qed
lemma (in start_context) wt_lbv_wt_method:
assumes lbv: "wt_lbv P C Ts T⇣r mxs mxl⇣0 xt cert is"
shows "∃τs. wt_method P C Ts T⇣r mxs mxl⇣0 is xt τs"
proof -
from lbv have l: "is ≠ []" by (simp add: wt_lbv_def)
moreover
from wf lbv C Ts obtain τs where
list: "τs ∈ list (size is) A" and
step: "wt_step r Err step τs" and
start: "OK first \<sqsubseteq>⇩r τs!0"
by (blast dest: wt_lbv_wt_step)
from list have [simp]: "size τs = size is" by simp
have "size (map ok_val τs) = size is" by simp
moreover from l have 0: "0 < size τs" by simp
with step obtain τs0 where "τs!0 = OK τs0"
by (unfold wt_step_def) blast
with start 0 have "wt_start P C Ts mxl⇣0 (map ok_val τs)"
by (simp add: wt_start_def JVM_le_Err_conv lesub_def Err.le_def)
moreover {
from list have "check_types P mxs mxl τs" by (simp add: check_types_def)
also from step have "∀x ∈ set τs. x ≠ Err"
by (auto simp add: all_set_conv_all_nth wt_step_def)
hence [symmetric]: "map OK (map ok_val τs) = τs"
by (auto intro!: map_idI)
finally have "check_types P mxs mxl (map OK (map ok_val τs))" .
}
moreover {
note bounded_step
moreover from list have "set τs ⊆ A" by simp
moreover from step have "wt_err_step (sup_state_opt P) step τs"
by (simp add: wt_err_step_def JVM_le_Err_conv)
ultimately 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: exec_def states_def)
}
ultimately have "wt_method P C Ts T⇣r mxs mxl⇣0 is xt (map ok_val τs)"
by (simp add: wt_method_def2 check_types_def del: map_map)
thus ?thesis ..
qed
lemma (in start_context) wt_method_wt_lbv:
assumes wt: "wt_method P C Ts T⇣r mxs mxl⇣0 is xt τs"
defines [simp]: "cert ≡ mk_cert P mxs T⇣r xt is τs"
shows "wt_lbv P C Ts T⇣r mxs mxl⇣0 xt cert is"
proof -
let ?τs = "map OK τs"
let ?cert = "make_cert step ?τs (OK None)"
from wt obtain
0: "0 < size is" and
size: "size is = size ?τs" and
ck_types: "check_types P mxs mxl ?τs" and
wt_start: "wt_start P C Ts mxl⇣0 τs" and
app_eff: "wt_app_eff (sup_state_opt P) app eff τs"
by (force simp add: wt_method_def2 check_types_def)
from wf have "semilat (JVM_SemiType.sl P mxs mxl)" ..
hence "semilat (A, r, f)" by (simp add: sl_def2)
moreover have "top r Err" by (simp add: JVM_le_Err_conv)
moreover have "Err ∈ A" by (simp add: JVM_states_unfold)
moreover have "bottom r (OK None)"
by (simp add: JVM_le_Err_conv bottom_def lesub_def Err.le_def split: err.split)
moreover have "OK None ∈ A" by (simp add: JVM_states_unfold)
moreover from wf have "mono r step (size is) A" by (rule step_mono)
hence "mono r step (size ?τs) A" by (simp add: size)
moreover from exec_pres_type
have "pres_type step (size ?τs) A" by (simp add: size)
moreover
from ck_types have τs_in_A: "set ?τs ⊆ A" by (simp add: check_types_def)
hence "∀pc. pc < size ?τs --> ?τs!pc ∈ A ∧ ?τs!pc ≠ Err" by auto
moreover from bounded_step
have "bounded step (size ?τs)" by (simp add: size)
moreover have "OK None ≠ Err" by simp
moreover from bounded_step size τs_in_A app_eff
have "wt_err_step (sup_state_opt P) step ?τs"
by (auto intro: wt_app_eff_imp_wt_err simp add: exec_def states_def)
hence "wt_step r Err step ?τs"
by (simp add: wt_err_step_def JVM_le_Err_conv)
moreover
from 0 size have "0 < size τs" by auto
hence "?τs!0 = OK (τs!0)" by simp
with wt_start have "OK first \<sqsubseteq>⇩r ?τs!0"
by (clarsimp simp add: wt_start_def lesub_def Err.le_def JVM_le_Err_conv)
moreover note first_in_A
moreover have "OK first ≠ Err" by simp
moreover note size
ultimately
have "wtl_inst_list is ?cert f r Err (OK None) step 0 (OK first) ≠ Err"
by (rule lbvc.wtl_complete [OF lbvc.intro, OF lbv.intro lbvc_axioms.intro, OF Semilat.intro lbv_axioms.intro])
moreover from 0 size have "τs ≠ []" by auto
moreover from ck_types have "check_types P mxs mxl ?cert"
by (auto simp add: make_cert_def check_types_def JVM_states_unfold)
moreover note 0 size
ultimately show ?thesis
by (simp add: wt_lbv_def lbvjvm_def mk_cert_def step_def_exec [symmetric]
check_cert_def make_cert_def nth_append)
qed
theorem jvm_lbv_correct:
"wt_jvm_prog_lbv P Cert ==> wf_jvm_prog P"
proof -
let ?Φ = "λC mn. let (C,Ts,T⇣r,(mxs,mxl⇣0,is,xt)) = method P C mn in
SOME τs. wt_method P C Ts T⇣r mxs mxl⇣0 is xt τs"
assume wt: "wt_jvm_prog_lbv P Cert"
hence "wf_jvm_prog⇘?Φ⇙ P"
apply (unfold wf_jvm_prog_phi_def wt_jvm_prog_lbv_def)
apply (erule wf_prog_lift)
apply (auto dest!: start_context.wt_lbv_wt_method [OF start_context.intro]
intro: someI)
apply (erule sees_method_is_class)
done
thus ?thesis by (unfold wf_jvm_prog_def) blast
qed
theorem jvm_lbv_complete:
assumes wt: "wf_jvm_prog⇘Φ⇙ P"
shows "wt_jvm_prog_lbv P (prg_cert P Φ)"
using wt
apply (unfold wf_jvm_prog_phi_def wt_jvm_prog_lbv_def)
apply (erule wf_prog_lift)
apply (auto simp add: prg_cert_def
intro!: start_context.wt_method_wt_lbv start_context.intro)
apply (erule sees_method_is_class)
done
end