(* Title: JinjaThreads/BV/BVSpecTypeSafe.thy Author: Cornelia Pusch, Gerwin Klein, Andreas Lochbihler *) section ‹BV Type Safety Proof \label{sec:BVSpecTypeSafe}› theory BVSpecTypeSafe imports BVConform "../Common/ExternalCallWF" begin declare listE_length [simp del] text ‹ This theory contains proof that the specification of the bytecode verifier only admits type safe programs. › subsection ‹Preliminaries› text ‹ Simp and intro setup for the type safety proof: › context JVM_heap_conf_base begin lemmas widen_rules [intro] = conf_widen confT_widen confs_widens confTs_widen end subsection ‹Exception Handling› text ‹ For the ‹Invoke› instruction the BV has checked all handlers that guard the current ‹pc›. › lemma Invoke_handlers: "match_ex_table P C pc xt = Some (pc',d') ⟹ ∃(f,t,D,h,d) ∈ set (relevant_entries P (Invoke n M) pc xt). (case D of None ⇒ True | Some D' ⇒ P ⊢ C ≼⇧^{*}D') ∧ pc ∈ {f..<t} ∧ pc' = h ∧ d' = d" by (induct xt) (auto simp add: relevant_entries_def matches_ex_entry_def is_relevant_entry_def split: if_split_asm) lemma match_is_relevant: assumes rv: "⋀D'. P ⊢ D ≼⇧^{*}D' ⟹ is_relevant_class (ins ! i) P D'" assumes match: "match_ex_table P D pc xt = Some (pc',d')" shows "∃(f,t,D',h,d) ∈ set (relevant_entries P (ins ! i) pc xt). (case D' of None ⇒ True | Some D'' ⇒ P ⊢ D ≼⇧^{*}D'') ∧ pc ∈ {f..<t} ∧ pc' = h ∧ d' = d" using rv match by(fastforce simp add: relevant_entries_def is_relevant_entry_def matches_ex_entry_def dest: match_ex_table_SomeD) context JVM_heap_conf_base begin lemma exception_step_conform: fixes σ' :: "('addr, 'heap) jvm_state" assumes wtp: "wf_jvm_prog⇘Φ⇙ P" assumes correct: "Φ ⊢ t:(⌊xcp⌋, h, fr # frs) √" shows "Φ ⊢ t:exception_step P xcp h fr frs √" proof - obtain stk loc C M pc where fr: "fr = (stk, loc, C, M, pc)" by(cases fr) from correct obtain Ts T mxs mxl⇩_{0}ins xt where meth: "P ⊢ C sees M:Ts → T = ⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C" by (simp add: correct_state_def fr) blast from correct meth fr obtain D where hxcp: "typeof_addr h xcp = ⌊Class_type D⌋" and DsubThrowable: "P ⊢ D ≼⇧^{*}Throwable" and rv: "⋀D'. P ⊢ D ≼⇧^{*}D' ⟹ is_relevant_class (instrs_of P C M ! pc) P D'" by(fastforce simp add: correct_state_def dest: sees_method_fun) from meth have [simp]: "ex_table_of P C M = xt" by simp from correct have tconf: "P,h ⊢ t √t" by(simp add: correct_state_def) show ?thesis proof(cases "match_ex_table P D pc xt") case None with correct fr meth hxcp show ?thesis by(fastforce simp add: correct_state_def cname_of_def split: list.split) next case (Some pc_d) then obtain pc' d' where pcd: "pc_d = (pc', d')" and match: "match_ex_table P D pc xt = Some (pc',d')" by (cases pc_d) auto from match_is_relevant[OF rv match] meth obtain f t D' where rv: "(f, t, D', pc', d') ∈ set (relevant_entries P (ins ! pc) pc xt)" and DsubD': "(case D' of None ⇒ True | Some D'' ⇒ P ⊢ D ≼⇧^{*}D'')" and pc: "pc ∈ {f..<t}" by(auto) from correct meth obtain ST LT where h_ok: "hconf h" and Φ_pc: "Φ C M ! pc = Some (ST, LT)" and frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and frames: "conf_fs P h Φ M (size Ts) T frs" and preh: "preallocated h" unfolding correct_state_def fr by(auto dest: sees_method_fun) from frame obtain stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩_{⊤}] LT" and pc: "pc < size ins" by (unfold conf_f_def) auto from stk have [simp]: "size stk = size ST" .. from wtp meth correct fr have wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" by (auto simp add: correct_state_def conf_f_def dest: sees_method_fun elim!: wt_jvm_prog_impl_wt_instr) from wt Φ_pc have eff: "∀(pc', s')∈set (xcpt_eff (ins!pc) P pc (ST,LT) xt). pc' < size ins ∧ P ⊢ s' ≤' Φ C M!pc'" by (auto simp add: defs1) let ?stk' = "Addr xcp # drop (length stk - d') stk" let ?f = "(?stk', loc, C, M, pc')" have conf: "P,h ⊢ Addr xcp :≤ Class (case D' of None ⇒ Throwable | Some D'' ⇒ D'')" using DsubD' hxcp DsubThrowable by(auto simp add: conf_def) obtain ST' LT' where Φ_pc': "Φ C M ! pc' = Some (ST', LT')" and pc': "pc' < size ins" and less: "P ⊢ (Class D # drop (size ST - d') ST, LT) ≤⇩_{i}(ST', LT')" proof(cases D') case Some thus ?thesis using eff rv DsubD' conf that by(fastforce simp add: xcpt_eff_def sup_state_opt_any_Some intro: widen_trans[OF widen_subcls]) next case None with that eff rv conf DsubThrowable show ?thesis by(fastforce simp add: xcpt_eff_def sup_state_opt_any_Some intro: widen_trans[OF widen_subcls]) qed with conf loc stk hxcp have "conf_f P h (ST',LT') ins ?f" by (auto simp add: defs1 conf_def intro: list_all2_dropI) with meth h_ok frames Φ_pc' fr match hxcp tconf preh show ?thesis unfolding correct_state_def by(fastforce dest: sees_method_fun simp add: cname_of_def) qed qed end subsection ‹Single Instructions› text ‹ In this subsection we prove for each single (welltyped) instruction that the state after execution of the instruction still conforms. Since we have already handled raised exceptions above, we can now assume that no exception has been raised in this step. › context JVM_conf_read begin declare defs1 [simp] lemma Invoke_correct: fixes σ' :: "('addr, 'heap) jvm_state" assumes wtprog: "wf_jvm_prog⇘Φ⇙ P" assumes meth_C: "P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C" assumes ins: "ins ! pc = Invoke M' n" assumes wti: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" assumes approx: "Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√" assumes exec: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs" shows "Φ ⊢ t:σ √" proof - note split_paired_Ex [simp del] from wtprog obtain wfmb where wfprog: "wf_prog wfmb P" by (simp add: wf_jvm_prog_phi_def) from ins meth_C approx obtain ST LT where heap_ok: "hconf h" and tconf: "P,h ⊢ t √t" and Φ_pc: "Φ C M!pc = Some (ST,LT)" and frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and frames: "conf_fs P h Φ M (size Ts) T frs" and preh: "preallocated h" by (fastforce dest: sees_method_fun) from ins wti Φ_pc have n: "n < size ST" by simp show ?thesis proof(cases "stk!n = Null") case True with ins heap_ok Φ_pc frame frames exec meth_C tconf preh show ?thesis by(fastforce elim: wf_preallocatedE[OF wfprog, where C=NullPointer]) next case False note Null = this have NT: "ST!n ≠ NT" proof assume "ST!n = NT" moreover from frame have "P,h ⊢ stk [:≤] ST" by simp with n have "P,h ⊢ stk!n :≤ ST!n" by (simp add: list_all2_conv_all_nth) ultimately have "stk!n = Null" by simp with Null show False by contradiction qed from frame obtain stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩_{⊤}] LT" by simp from NT ins wti Φ_pc have pc': "pc+1 < size ins" by simp from NT ins wti Φ_pc obtain ST' LT' where pc': "pc+1 < size ins" and Φ': "Φ C M ! (pc+1) = Some (ST', LT')" and LT': "P ⊢ LT [≤⇩_{⊤}] LT'" by(auto simp add: neq_Nil_conv sup_state_opt_any_Some split: if_split_asm) with NT ins wti Φ_pc obtain D D' TTs TT m where D: "class_type_of' (ST!n) = ⌊D⌋" and m_D: "P ⊢ D sees M': TTs→TT = m in D'" and Ts: "P ⊢ rev (take n ST) [≤] TTs" and ST': "P ⊢ (TT # drop (n+1) ST) [≤] ST'" by(auto) from n stk D have "P,h ⊢ stk!n :≤ ST ! n" by (auto simp add: list_all2_conv_all_nth) from ‹P,h ⊢ stk!n :≤ ST ! n› Null D obtain U a where Addr: "stk!n = Addr a" and obj: "typeof_addr h a = Some U" and UsubSTn: "P ⊢ ty_of_htype U ≤ ST ! n" by(cases "stk ! n")(auto simp add: conf_def widen_Class) from D UsubSTn obtain C' where C': "class_type_of' (ty_of_htype U) = ⌊C'⌋" and C'subD: "P ⊢ C' ≼⇧^{*}D" by(rule widen_is_class_type_of) simp with wfprog m_D obtain Ts' T' D'' meth' where m_C': "P ⊢ C' sees M': Ts'→T' = meth' in D''" and T': "P ⊢ T' ≤ TT" and Ts': "P ⊢ TTs [≤] Ts'" by (auto dest: sees_method_mono) from Ts n have [simp]: "size TTs = n" by (auto dest: list_all2_lengthD simp: min_def) with Ts' have [simp]: "size Ts' = n" by (auto dest: list_all2_lengthD) from m_C' wfprog obtain mD'': "P ⊢ D'' sees M':Ts'→T'=meth' in D''" by (fast dest: sees_method_idemp) { fix mxs' mxl' ins' xt' assume [simp]: "meth' = ⌊(mxs', mxl', ins', xt')⌋" let ?loc' = "Addr a # rev (take n stk) @ replicate mxl' undefined_value" let ?f' = "([], ?loc', D'', M', 0)" let ?f = "(stk, loc, C, M, pc)" from Addr obj m_C' ins meth_C exec C' False have s': "σ = (None, h, ?f' # ?f # frs)" by(auto split: if_split_asm) moreover from wtprog mD'' obtain start: "wt_start P D'' Ts' mxl' (Φ D'' M')" and ins': "ins' ≠ []" by (auto dest: wt_jvm_prog_impl_wt_start) then obtain LT⇩_{0}where LT⇩_{0}: "Φ D'' M' ! 0 = Some ([], LT⇩_{0})" by (clarsimp simp add: wt_start_def defs1 sup_state_opt_any_Some) moreover have "conf_f P h ([], LT⇩_{0}) ins' ?f'" proof - let ?LT = "OK (Class D'') # (map OK Ts') @ (replicate mxl' Err)" from stk have "P,h ⊢ take n stk [:≤] take n ST" .. hence "P,h ⊢ rev (take n stk) [:≤] rev (take n ST)" by simp also note Ts also note Ts' finally have "P,h ⊢ rev (take n stk) [:≤⇩_{⊤}] map OK Ts'" by simp also have "P,h ⊢ replicate mxl' undefined_value [:≤⇩_{⊤}] replicate mxl' Err" by simp also from m_C' have "P ⊢ C' ≼⇧^{*}D''" by (rule sees_method_decl_above) from obj heap_ok have "is_htype P U" by (rule typeof_addr_is_type) with C' have "P ⊢ ty_of_htype U ≤ Class C'" by(cases U)(simp_all add: widen_array_object) with ‹P ⊢ C' ≼⇧^{*}D''› obj C' have "P,h ⊢ Addr a :≤ Class D''" by (auto simp add: conf_def intro: widen_trans) ultimately have "P,h ⊢ ?loc' [:≤⇩_{⊤}] ?LT" by simp also from start LT⇩_{0}have "P ⊢ … [≤⇩_{⊤}] LT⇩_{0}" by (simp add: wt_start_def) finally have "P,h ⊢ ?loc' [:≤⇩_{⊤}] LT⇩_{0}" . thus ?thesis using ins' by simp qed ultimately have ?thesis using s' Φ_pc approx meth_C m_D T' ins D tconf C' mD'' by (fastforce dest: sees_method_fun [of _ C]) } moreover { assume [simp]: "meth' = Native" with wfprog m_C' have "D''∙M'(Ts') :: T'" by(simp add: sees_wf_native) with C' m_C' have nec: "is_native P U M'" by(auto intro: is_native.intros) from ins n Addr obj exec m_C' C' obtain va h' tas' where va: "(tas', va, h') ∈ red_external_aggr P t a M' (rev (take n stk)) h" and σ: "σ = extRet2JVM n h' stk loc C M pc frs va" by(auto) from va nec obj have hext: "h ⊴ h'" by(auto intro: red_external_aggr_hext) with frames have frames': "conf_fs P h' Φ M (length Ts) T frs" by(rule conf_fs_hext) from preh hext have preh': "preallocated h'" by(rule preallocated_hext) from va nec obj tconf have tconf': "P,h' ⊢ t √t" by(auto dest: red_external_aggr_preserves_tconf) from hext obj have obj': "typeof_addr h' a = ⌊U⌋" by(rule typeof_addr_hext_mono) from stk have "P,h ⊢ take n stk [:≤] take n ST" by(rule list_all2_takeI) then obtain Us where "map typeof⇘h⇙ (take n stk) = map Some Us" "P ⊢ Us [≤] take n ST" by(auto simp add: confs_conv_map) hence Us: "map typeof⇘h⇙ (rev (take n stk)) = map Some (rev Us)" "P ⊢ rev Us [≤] rev (take n ST)" by- (simp only: rev_map[symmetric], simp) from ‹P ⊢ rev Us [≤] rev (take n ST)› Ts Ts' have "P ⊢ rev Us [≤] Ts'" by(blast intro: widens_trans) with obj ‹map typeof⇘h⇙ (rev (take n stk)) = map Some (rev Us)› C' m_C' have wtext': "P,h ⊢ a∙M'(rev (take n stk)) : T'" by(simp add: external_WT'.intros) from va have va': "P,t ⊢ ⟨a∙M'(rev (take n stk)),h⟩ -tas'→ext ⟨va,h'⟩" by(unfold WT_red_external_list_conv[OF wfprog wtext' tconf]) with heap_ok wtext' tconf wfprog have heap_ok': "hconf h'" by(auto dest: external_call_hconf) have ?thesis proof(cases va) case (RetExc a') from frame hext have "conf_f P h' (ST, LT) ins (stk, loc, C, M, pc)" by(rule conf_f_hext) with σ tconf' heap_ok' meth_C Φ_pc frames' RetExc red_external_conf_extRet[OF wfprog va' wtext' heap_ok preh tconf] ins preh' show ?thesis by(fastforce simp add: conf_def widen_Class) next case RetStaySame from frame hext have "conf_f P h' (ST, LT) ins (stk, loc, C, M, pc)" by(rule conf_f_hext) with σ heap_ok' meth_C Φ_pc RetStaySame frames' tconf' preh' show ?thesis by fastforce next case (RetVal v) with σ have σ: "σ = (None, h', (v # drop (n+1) stk, loc, C, M, pc+1) # frs)" by simp from heap_ok wtext' va' RetVal preh tconf have "P,h' ⊢ v :≤ T'" by(auto dest: red_external_conf_extRet[OF wfprog]) from stk have "P,h ⊢ drop (n + 1) stk [:≤] drop (n+1) ST" by(rule list_all2_dropI) hence "P,h' ⊢ drop (n + 1) stk [:≤] drop (n+1) ST" using hext by(rule confs_hext) with ‹P,h' ⊢ v :≤ T'› have "P,h' ⊢ v # drop (n + 1) stk [:≤] T' # drop (n+1) ST" by(auto simp add: conf_def intro: widen_trans) also with NT ins wti Φ_pc Φ' nec False D m_D T' have "P ⊢ (T' # drop (n + 1) ST) [≤] ST'" by(auto dest: sees_method_fun intro: widen_trans) also from loc hext have "P,h' ⊢ loc [:≤⇩_{⊤}] LT" by(rule confTs_hext) hence "P,h' ⊢ loc [:≤⇩_{⊤}] LT'" using LT' by(rule confTs_widen) ultimately show ?thesis using ‹hconf h'› σ meth_C Φ' pc' frames' tconf' preh' by fastforce qed } ultimately show ?thesis by(cases meth') auto qed qed declare list_all2_Cons2 [iff] lemma Return_correct: assumes wt_prog: "wf_jvm_prog⇘Φ⇙ P" assumes meth: "P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C" assumes ins: "ins ! pc = Return" assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" assumes correct: "Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√" assumes s': "(tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs)" shows "Φ ⊢ t:σ'√" proof - from wt_prog obtain wfmb where wf: "wf_prog wfmb P" by (simp add: wf_jvm_prog_phi_def) from meth ins s' correct have "frs = [] ⟹ ?thesis" by (simp add: correct_state_def) moreover { fix f frs' assume frs': "frs = f#frs'" moreover obtain stk' loc' C' M' pc' where f: "f = (stk',loc',C',M',pc')" by (cases f) moreover note meth ins s' ultimately have σ': "σ' = (None,h,(hd stk#(drop (1+size Ts) stk'),loc',C',M',pc'+1)#frs')" (is "σ' = (None,h,?f'#frs')") by simp from correct meth obtain ST LT where h_ok: "hconf h" and tconf: "P,h ⊢ t √t" and Φ_pc: "Φ C M ! pc = Some (ST, LT)" and frame: "conf_f P h (ST, LT) ins (stk,loc,C,M,pc)" and frames: "conf_fs P h Φ M (size Ts) T frs" and preh: "preallocated h" by (auto dest: sees_method_fun) from Φ_pc ins wt obtain U ST⇩_{0}where "ST = U # ST⇩_{0}" "P ⊢ U ≤ T" by (simp add: wt_instr_def app_def) blast with wf frame have hd_stk: "P,h ⊢ hd stk :≤ T" by (auto simp add: conf_f_def) from f frs' frames obtain ST' LT' Ts'' T'' mxs' mxl⇩_{0}' ins' xt' Ts' T' where Φ': "Φ C' M' ! pc' = Some (ST', LT')" and meth_C': "P ⊢ C' sees M':Ts''→T''=⌊(mxs',mxl⇩_{0}',ins',xt')⌋ in C'" and ins': "ins' ! pc' = Invoke M (size Ts)" and D: "∃D m D'. class_type_of' (ST' ! (size Ts)) = Some D ∧ P ⊢ D sees M: Ts'→T' = m in D'" and T': "P ⊢ T ≤ T'" and frame': "conf_f P h (ST',LT') ins' f" and conf_fs: "conf_fs P h Φ M' (size Ts'') T'' frs'" by clarsimp blast from f frame' obtain stk': "P,h ⊢ stk' [:≤] ST'" and loc': "P,h ⊢ loc' [:≤⇩_{⊤}] LT'" and pc': "pc' < size ins'" by (simp add: conf_f_def) from wt_prog meth_C' pc' have wti: "P,T'',mxs',size ins',xt' ⊢ ins'!pc',pc' :: Φ C' M'" by (rule wt_jvm_prog_impl_wt_instr) obtain aTs ST'' LT'' where Φ_suc: "Φ C' M' ! Suc pc' = Some (ST'', LT'')" and less: "P ⊢ (T' # drop (size Ts+1) ST', LT') ≤⇩_{i}(ST'', LT'')" and suc_pc': "Suc pc' < size ins'" using ins' Φ' D T' wti by(fastforce simp add: sup_state_opt_any_Some split: if_split_asm) from hd_stk T' have hd_stk': "P,h ⊢ hd stk :≤ T'" .. have frame'': "conf_f P h (ST'',LT'') ins' ?f'" proof - from stk' have "P,h ⊢ drop (1+size Ts) stk' [:≤] drop (1+size Ts) ST'" .. moreover with hd_stk' less have "P,h ⊢ hd stk # drop (1+size Ts) stk' [:≤] ST''" by auto moreover from wf loc' less have "P,h ⊢ loc' [:≤⇩_{⊤}] LT''" by auto moreover note suc_pc' ultimately show ?thesis by (simp add: conf_f_def) qed with σ' frs' f meth h_ok hd_stk Φ_suc frames meth_C' Φ' tconf preh have ?thesis by (fastforce dest: sees_method_fun [of _ C']) } ultimately show ?thesis by (cases frs) blast+ qed declare sup_state_opt_any_Some [iff] declare not_Err_eq [iff] lemma Load_correct: "⟦ wf_prog wt P; P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C; ins!pc = Load idx; P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M; Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√ ; (tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧ ⟹ Φ ⊢ t:σ' √" by (fastforce dest: sees_method_fun [of _ C] elim!: confTs_confT_sup) declare [[simproc del: list_to_set_comprehension]] lemma Store_correct: "⟦ wf_prog wt P; P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C; ins!pc = Store idx; P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M; Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√; (tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧ ⟹ Φ ⊢ t:σ'√" apply clarsimp apply (drule (1) sees_method_fun) apply clarsimp apply (blast intro!: list_all2_update_cong) done lemma Push_correct: "⟦ wf_prog wt P; P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C; ins!pc = Push v; P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M; Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√; (tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧ ⟹ Φ ⊢ t:σ'√" apply clarsimp apply (drule (1) sees_method_fun) apply clarsimp apply (blast dest: typeof_lit_conf) done declare [[simproc add: list_to_set_comprehension]] lemma Checkcast_correct: "⟦ wf_jvm_prog⇘Φ⇙ P; P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C; ins!pc = Checkcast D; P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M; Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√; (tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs ⟧ ⟹ Φ ⊢ t:σ √" using wf_preallocatedD[of "λP C (M, Ts, T⇩_{r}, mxs, mxl⇩_{0}, is, xt). wt_method P C Ts T⇩_{r}mxs mxl⇩_{0}is xt (Φ C M)" P h ClassCast] apply (clarsimp simp add: wf_jvm_prog_phi_def split: if_split_asm) apply(drule (1) sees_method_fun) apply(fastforce simp add: conf_def intro: widen_trans) apply (drule (1) sees_method_fun) apply(fastforce simp add: conf_def intro: widen_trans) done lemma Instanceof_correct: "⟦ wf_jvm_prog⇘Φ⇙ P; P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C; ins!pc = Instanceof Ty; P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M; Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√; (tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs ⟧ ⟹ Φ ⊢ t:σ √" apply (clarsimp simp add: wf_jvm_prog_phi_def split: if_split_asm) apply (drule (1) sees_method_fun) apply fastforce done declare split_paired_All [simp del] end lemma widens_Cons [iff]: "P ⊢ (T # Ts) [≤] Us = (∃z zs. Us = z # zs ∧ P ⊢ T ≤ z ∧ P ⊢ Ts [≤] zs)" by(rule list_all2_Cons1) context heap_conf_base begin end context JVM_conf_read begin lemma Getfield_correct: assumes wf: "wf_prog wt P" assumes mC: "P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C" assumes i: "ins!pc = Getfield F D" assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" assumes cf: "Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√" assumes xc: "(tas, σ') ∈ exec_instr (ins!pc) P t h stk loc C M pc frs" shows "Φ ⊢ t:σ'√" proof - from mC cf obtain ST LT where "h√": "hconf h" and tconf: "P,h ⊢ t √t" and Φ: "Φ C M ! pc = Some (ST,LT)" and stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩_{⊤}] LT" and pc: "pc < size ins" and fs: "conf_fs P h Φ M (size Ts) T frs" and preh: "preallocated h" by (fastforce dest: sees_method_fun) from i Φ wt obtain oT ST'' vT ST' LT' vT' fm where oT: "P ⊢ oT ≤ Class D" and ST: "ST = oT # ST''" and F: "P ⊢ D sees F:vT (fm) in D" and pc': "pc+1 < size ins" and Φ': "Φ C M ! (pc+1) = Some (vT'#ST', LT')" and ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩_{⊤}] LT'" and vT': "P ⊢ vT ≤ vT'" by fastforce from stk ST obtain ref stk' where stk': "stk = ref#stk'" and ref: "P,h ⊢ ref :≤ oT" and ST'': "P,h ⊢ stk' [:≤] ST''" by auto show ?thesis proof(cases "ref = Null") case True with tconf "h√" i xc stk' mC fs Φ ST'' ref ST loc pc' wf_preallocatedD[OF wf, of h NullPointer] preh show ?thesis by(fastforce) next case False from ref oT have "P,h ⊢ ref :≤ Class D" .. with False obtain a U' D' where a: "ref = Addr a" and h: "typeof_addr h a = Some U'" and U': "D' = class_type_of U'" and D': "P ⊢ D' ≼⇧^{*}D" by (blast dest: non_npD2) { fix v assume read: "heap_read h a (CField D F) v" from D' F have has_field: "P ⊢ D' has F:vT (fm) in D" by (blast intro: has_field_mono has_visible_field) with h have "P,h ⊢ a@CField D F : vT" unfolding U' .. with read have v: "P,h ⊢ v :≤ vT" using "h√" by(rule heap_read_conf) from ST'' ST' have "P,h ⊢ stk' [:≤] ST'" .. moreover from v vT' have "P,h ⊢ v :≤ vT'" by blast moreover from loc LT' have "P,h ⊢ loc [:≤⇩_{⊤}] LT'" .. moreover note "h√" mC Φ' pc' v fs tconf preh ultimately have "Φ ⊢ t:(None, h, (v#stk',loc,C,M,pc+1)#frs) √" by fastforce } with a h i mC stk' xc show ?thesis by auto qed qed lemma Putfield_correct: assumes wf: "wf_prog wt P" assumes mC: "P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C" assumes i: "ins!pc = Putfield F D" assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" assumes cf: "Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√" assumes xc: "(tas, σ') ∈ exec_instr (ins!pc) P t h stk loc C M pc frs" shows "Φ ⊢ t:σ' √" proof - from mC cf obtain ST LT where "h√": "hconf h" and tconf: "P,h ⊢ t √t" and Φ: "Φ C M ! pc = Some (ST,LT)" and stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩_{⊤}] LT" and pc: "pc < size ins" and fs: "conf_fs P h Φ M (size Ts) T frs" and preh: "preallocated h" by (fastforce dest: sees_method_fun) from i Φ wt obtain vT vT' oT ST'' ST' LT' fm where ST: "ST = vT # oT # ST''" and field: "P ⊢ D sees F:vT' (fm) in D" and oT: "P ⊢ oT ≤ Class D" and vT: "P ⊢ vT ≤ vT'" and pc': "pc+1 < size ins" and Φ': "Φ C M!(pc+1) = Some (ST',LT')" and ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩_{⊤}] LT'" by clarsimp from stk ST obtain v ref stk' where stk': "stk = v#ref#stk'" and v: "P,h ⊢ v :≤ vT" and ref: "P,h ⊢ ref :≤ oT" and ST'': "P,h ⊢ stk' [:≤] ST''" by auto show ?thesis proof(cases "ref = Null") case True with tconf "h√" i xc stk' mC fs Φ ST'' ref ST loc pc' v wf_preallocatedD[OF wf, of h NullPointer] preh show ?thesis by(fastforce) next case False from ref oT have "P,h ⊢ ref :≤ Class D" .. with False obtain a U' D' where a: "ref = Addr a" and h: "typeof_addr h a = Some U'" and U': "D' = class_type_of U'" and D': "P ⊢ D' ≼⇧^{*}D" by (blast dest: non_npD2) from v vT have vT': "P,h ⊢ v :≤ vT'" .. from field D' have has_field: "P ⊢ D' has F:vT' (fm) in D" by (blast intro: has_field_mono has_visible_field) with h have al: "P,h ⊢ a@CField D F : vT'" unfolding U' .. let ?f' = "(stk',loc,C,M,pc+1)" { fix h' assume "write": "heap_write h a (CField D F) v h'" hence hext: "h ⊴ h'" by(rule hext_heap_write) with preh have "preallocated h'" by(rule preallocated_hext) moreover from "write" "h√" al vT' have "hconf h'" by(rule hconf_heap_write_mono) moreover from ST'' ST' have "P,h ⊢ stk' [:≤] ST'" .. from this hext have "P,h' ⊢ stk' [:≤] ST'" by (rule confs_hext) moreover from loc LT' have "P,h ⊢ loc [:≤⇩_{⊤}] LT'" .. from this hext have "P,h' ⊢ loc [:≤⇩_{⊤}] LT'" by (rule confTs_hext) moreover from fs hext have "conf_fs P h' Φ M (size Ts) T frs" by (rule conf_fs_hext) moreover note mC Φ' pc' moreover from tconf hext have "P,h' ⊢ t √t" by(rule tconf_hext_mono) ultimately have "Φ ⊢ t:(None, h', ?f'#frs) √" by fastforce } with a h i mC stk' xc show ?thesis by(auto simp del: correct_state_def) qed qed lemma CAS_correct: assumes wf: "wf_prog wt P" assumes mC: "P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C" assumes i: "ins!pc = CAS F D" assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" assumes cf: "Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√" assumes xc: "(tas, σ') ∈ exec_instr (ins!pc) P t h stk loc C M pc frs" shows "Φ ⊢ t:σ' √" proof - from mC cf obtain ST LT where "h√": "hconf h" and tconf: "P,h ⊢ t √t" and Φ: "Φ C M ! pc = Some (ST,LT)" and stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩_{⊤}] LT" and pc: "pc < size ins" and fs: "conf_fs P h Φ M (size Ts) T frs" and preh: "preallocated h" by (fastforce dest: sees_method_fun) from i Φ wt obtain T1 T2 T3 T' ST'' ST' LT' fm where ST: "ST = T3 # T2 # T1 # ST''" and field: "P ⊢ D sees F:T' (fm) in D" and oT: "P ⊢ T1 ≤ Class D" and T2: "P ⊢ T2 ≤ T'" and T3: "P ⊢ T3 ≤ T'" and pc': "pc+1 < size ins" and Φ': "Φ C M!(pc+1) = Some (Boolean # ST',LT')" and ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩_{⊤}] LT'" by clarsimp from stk ST obtain v'' v' v stk' where stk': "stk = v''#v'#v#stk'" and v: "P,h ⊢ v :≤ T1" and v': "P,h ⊢ v' :≤ T2" and v'': "P,h ⊢ v'' :≤ T3" and ST'': "P,h ⊢ stk' [:≤] ST''" by auto show ?thesis proof(cases "v = Null") case True with tconf "h√" i xc stk' mC fs Φ ST'' v ST loc pc' v' v'' wf_preallocatedD[OF wf, of h NullPointer] preh show ?thesis by(fastforce) next case False from v oT have "P,h ⊢ v :≤ Class D" .. with False obtain a U' D' where a: "v = Addr a" and h: "typeof_addr h a = Some U'" and U': "D' = class_type_of U'" and D': "P ⊢ D' ≼⇧^{*}D" by (blast dest: non_npD2) from v' T2 have vT': "P,h ⊢ v' :≤ T'" .. from v'' T3 have vT'': "P,h ⊢ v'' :≤ T'" .. from field D' have has_field: "P ⊢ D' has F:T' (fm) in D" by (blast intro: has_field_mono has_visible_field) with h have al: "P,h ⊢ a@CField D F : T'" unfolding U' .. from ST'' ST' have stk'': "P,h ⊢ stk' [:≤] ST'" .. from loc LT' have loc': "P,h ⊢ loc [:≤⇩_{⊤}] LT'" .. { fix h' assume "write": "heap_write h a (CField D F) v'' h'" hence hext: "h ⊴ h'" by(rule hext_heap_write) with preh have "preallocated h'" by(rule preallocated_hext) moreover from "write" "h√" al vT'' have "hconf h'" by(rule hconf_heap_write_mono) moreover from stk'' hext have "P,h' ⊢ stk' [:≤] ST'" by (rule confs_hext) moreover from loc' hext have "P,h' ⊢ loc [:≤⇩_{⊤}] LT'" by (rule confTs_hext) moreover from fs hext have "conf_fs P h' Φ M (size Ts) T frs" by (rule conf_fs_hext) moreover note mC Φ' pc' moreover let ?f' = "(Bool True # stk',loc,C,M,pc+1)" from tconf hext have "P,h' ⊢ t √t" by(rule tconf_hext_mono) ultimately have "Φ ⊢ t:(None, h', ?f'#frs) √" by fastforce } moreover { let ?f' = "(Bool False # stk',loc,C,M,pc+1)" have "Φ ⊢ t:(None, h, ?f'#frs) √" using tconf "h√" preh mC Φ' stk'' loc' pc' fs by fastforce } ultimately show ?thesis using a h i mC stk' xc by(auto simp del: correct_state_def) qed qed lemma New_correct: assumes wf: "wf_prog wt P" assumes meth: "P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C" assumes ins: "ins!pc = New X" assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" assumes conf: "Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√" assumes no_x: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs" shows "Φ ⊢ t:σ √" proof - from ins conf meth obtain ST LT where heap_ok: "hconf h" and tconf: "P,h ⊢ t √t" and Φ_pc: "Φ C M!pc = Some (ST,LT)" and frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and frames: "conf_fs P h Φ M (size Ts) T frs" and preh: "preallocated h" by (auto dest: sees_method_fun) from Φ_pc ins wt obtain ST' LT' where is_class_X: "is_class P X" and mxs: "size ST < mxs" and suc_pc: "pc+1 < size ins" and Φ_suc: "Φ C M!(pc+1) = Some (ST', LT')" and less: "P ⊢ (Class X # ST, LT) ≤⇩_{i}(ST', LT')" by auto show ?thesis proof(cases "allocate h (Class_type X) = {}") case True with frame frames tconf suc_pc no_x ins meth Φ_pc wf_preallocatedD[OF wf, of h OutOfMemory] preh is_class_X heap_ok show ?thesis by(fastforce intro: tconf_hext_mono confs_hext confTs_hext conf_fs_hext) next case False with ins meth no_x obtain h' oref where new: "(h', oref) ∈ allocate h (Class_type X)" and σ': "σ = (None, h', (Addr oref#stk,loc,C,M,pc+1)#frs)" (is "σ = (None, h', ?f # frs)") by auto from new have hext: "h ⊴ h'" by(rule hext_allocate) with preh have preh': "preallocated h'" by(rule preallocated_hext) from new heap_ok is_class_X have heap_ok': "hconf h'" by(auto intro: hconf_allocate_mono) with new is_class_X have h': "typeof_addr h' oref = ⌊Class_type X⌋" by(auto dest: allocate_SomeD) note heap_ok' σ' moreover from frame less suc_pc wf h' hext have "conf_f P h' (ST', LT') ins ?f" apply (clarsimp simp add: fun_upd_apply conf_def split_beta) apply (auto intro: confs_hext confTs_hext) done moreover from frames hext have "conf_fs P h' Φ M (size Ts) T frs" by (rule conf_fs_hext) moreover from tconf hext have "P,h' ⊢ t √t" by(rule tconf_hext_mono) ultimately show ?thesis using meth Φ_suc preh' by fastforce qed qed lemma Goto_correct: "⟦ wf_prog wt P; P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C; ins ! pc = Goto branch; P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M; Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√; (tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧ ⟹ Φ ⊢ t:σ' √" apply clarsimp apply (drule (1) sees_method_fun) apply fastforce done declare [[simproc del: list_to_set_comprehension]] lemma IfFalse_correct: "⟦ wf_prog wt P; P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C; ins ! pc = IfFalse branch; P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M; Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√; (tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧ ⟹ Φ ⊢ t:σ'√" apply clarsimp apply (drule (1) sees_method_fun) apply fastforce done declare [[simproc add: list_to_set_comprehension]] lemma BinOp_correct: "⟦ wf_prog wt P; P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C; ins ! pc = BinOpInstr bop; P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M; Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√; (tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧ ⟹ Φ ⊢ t:σ'√" apply clarsimp apply (drule (1) sees_method_fun) apply(clarsimp simp add: conf_def) apply(drule (2) WTrt_binop_widen_mono) apply clarsimp apply(frule (2) binop_progress) apply(clarsimp split: sum.split_asm) apply(frule (5) binop_type) apply(fastforce intro: widen_trans simp add: conf_def) apply(frule (5) binop_type) apply(clarsimp simp add: conf_def) apply(clarsimp simp add: widen_Class) apply(fastforce intro: widen_trans dest: binop_relevant_class simp add: cname_of_def conf_def) done lemma Pop_correct: "⟦ wf_prog wt P; P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C; ins ! pc = Pop; P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M; Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√; (tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧ ⟹ Φ ⊢ t:σ'√" apply clarsimp apply (drule (1) sees_method_fun) apply fastforce done lemma Dup_correct: "⟦ wf_prog wt P; P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C; ins ! pc = Dup; P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M; Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√; (tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧ ⟹ Φ ⊢ t:σ'√" apply clarsimp apply (drule (1) sees_method_fun) apply fastforce done lemma Swap_correct: "⟦ wf_prog wt P; P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C; ins ! pc = Swap; P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M; Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√; (tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧ ⟹ Φ ⊢ t:σ'√" apply clarsimp apply (drule (1) sees_method_fun) apply fastforce done declare [[simproc del: list_to_set_comprehension]] lemma Throw_correct: "⟦ wf_prog wt P; P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C; ins ! pc = ThrowExc; P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M; Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√; (tas, σ') ∈ exec_instr (ins!pc) P t h stk loc C M pc frs ⟧ ⟹ Φ ⊢ t:σ'√" using wf_preallocatedD[of wt P h NullPointer] apply(clarsimp) apply(drule (1) sees_method_fun) apply(auto) apply fastforce apply fastforce apply(drule (1) non_npD) apply fastforce+ done declare [[simproc add: list_to_set_comprehension]] lemma NewArray_correct: assumes wf: "wf_prog wt P" assumes meth: "P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C" assumes ins: "ins!pc = NewArray X" assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" assumes conf: "Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√" assumes no_x: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs" shows "Φ ⊢ t:σ √" proof - from ins conf meth obtain ST LT where heap_ok: "hconf h" and tconf: "P,h ⊢ t √t" and Φ_pc: "Φ C M!pc = Some (ST,LT)" and stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩_{⊤}] LT" and pc: "pc < size ins" and frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and frames: "conf_fs P h Φ M (size Ts) T frs" and preh: "preallocated h" by (auto dest: sees_method_fun) from ins Φ_pc wt obtain ST'' X' ST' LT' where ST: "ST = Integer # ST''" and pc': "pc+1 < size ins" and Φ': "Φ C M ! (pc+1) = Some (X'#ST', LT')" and ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩_{⊤}] LT'" and XX': "P ⊢ X⌊⌉ ≤ X'" and suc_pc: "pc+1 < size ins" and is_type_X: "is_type P (X⌊⌉)" by(fastforce dest: Array_widen) from stk ST obtain si stk' where si: "stk = Intg si # stk'" by(auto simp add: conf_def) show ?thesis proof(cases "si <s 0 ∨ allocate h (Array_type X (nat (sint si))) = {}") case True with frame frames tconf heap_ok suc_pc no_x ins meth Φ_pc si preh wf_preallocatedD[OF wf, of h OutOfMemory] wf_preallocatedD[OF wf, of h NegativeArraySize] show ?thesis by(fastforce intro: tconf_hext_mono confs_hext confTs_hext conf_fs_hext split: if_split_asm)+ next case False with ins meth si no_x obtain h' oref where new: "(h', oref) ∈ allocate h (Array_type X (nat (sint si)))" and σ': "σ = (None, h', (Addr oref#tl stk,loc,C,M,pc+1)#frs)" (is "σ = (None, h', ?f # frs)") by(auto split: if_split_asm) from new have hext: "h ⊴ h'" by(rule hext_allocate) with preh have preh': "preallocated h'" by(rule preallocated_hext) from new heap_ok is_type_X have heap_ok': "hconf h'" by(auto intro: hconf_allocate_mono) from False have si': "0 <=s si" by auto with new is_type_X have h': "typeof_addr h' oref = ⌊Array_type X (nat (sint si))⌋" by(auto dest: allocate_SomeD) note σ' heap_ok' moreover from frame ST' ST LT' suc_pc wf XX' h' hext have "conf_f P h' (X' # ST', LT') ins ?f" by(clarsimp simp add: fun_upd_apply conf_def split_beta)(auto intro: confs_hext confTs_hext) moreover from frames hext have "conf_fs P h' Φ M (size Ts) T frs" by (rule conf_fs_hext) moreover from tconf hext have "P,h' ⊢ t √t" by(rule tconf_hext_mono) ultimately show ?thesis using meth Φ' preh' by fastforce qed qed lemma ALoad_correct: assumes wf: "wf_prog wt P" assumes meth: "P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C" assumes ins: "ins!pc = ALoad" assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" assumes conf: "Φ ⊢ t: (None, h, (stk,loc,C,M,pc)#frs)√" assumes no_x: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs" shows "Φ ⊢ t:σ √" proof - from ins conf meth obtain ST LT where heap_ok: "hconf h" and tconf: "P,h ⊢ t √t" and Φ_pc: "Φ C M!pc = Some (ST,LT)" and stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩_{⊤}] LT" and pc: "pc < size ins" and frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and frames: "conf_fs P h Φ M (size Ts) T frs" and preh: "preallocated h" by (auto dest: sees_method_fun) from ins wt Φ_pc have lST: "length ST > 1" by(auto) show ?thesis proof(cases "hd (tl stk) = Null") case True with ins no_x heap_ok tconf Φ_pc stk loc frame frames meth wf_preallocatedD[OF wf, of h NullPointer] preh show ?thesis by(fastforce) next case False note stkNN = this have STNN: "hd (tl ST) ≠ NT" proof assume "hd (tl ST) = NT" moreover from frame have "P,h ⊢ stk [:≤] ST" by simp with lST have "P,h ⊢ hd (tl stk) :≤ hd (tl ST)" by (cases ST, auto, case_tac list, auto) ultimately have "hd (tl stk) = Null" by simp with stkNN show False by contradiction qed with stkNN ins Φ_pc wt obtain ST'' X X' ST' LT' where ST: "ST = Integer # X⌊⌉ # ST''" and pc': "pc+1 < size ins" and Φ': "Φ C M ! (pc+1) = Some (X'#ST', LT')" and ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩_{⊤}] LT'" and XX': "P ⊢ X ≤ X'" and suc_pc: "pc+1 < size ins" by(fastforce) from stk ST obtain ref idx stk' where stk': "stk = idx#ref#stk'" and idx: "P,h ⊢ idx :≤ Integer" and ref: "P,h ⊢ ref :≤ X⌊⌉" and ST'': "P,h ⊢ stk' [:≤] ST''" by auto from stkNN stk' have "ref ≠ Null" by(simp) with ref obtain a Xel n where a: "ref = Addr a" and ha: "typeof_addr h a = ⌊Array_type Xel n⌋" and Xel: "P ⊢ Xel ≤ X" by(cases ref)(fastforce simp add: conf_def widen_Array)+ from idx obtain idxI where idxI: "idx = Intg idxI" by(auto simp add: conf_def) show ?thesis proof(cases "0 <=s idxI ∧ sint idxI < int n") case True hence si': "0 <=s idxI" "sint idxI < int n" by auto hence "nat (sint idxI) < n" by (simp add: word_sle_eq nat_less_iff) with ha have al: "P,h ⊢ a@ACell (nat (sint idxI)) : Xel" .. { fix v assume read: "heap_read h a (ACell (nat (sint idxI))) v" hence v: "P,h ⊢ v :≤ Xel" using al heap_ok by(rule heap_read_conf) let ?f = "(v # stk', loc, C, M, pc + 1)" from frame ST' ST LT' suc_pc wf XX' Xel idxI si' v ST'' have "conf_f P h (X' # ST', LT') ins ?f" by(auto intro: widen_trans simp add: conf_def) hence "Φ ⊢ t:(None, h, ?f # frs) √" using meth Φ' heap_ok Φ_pc frames tconf preh by fastforce } with ins meth si' stk' a ha no_x idxI idx show ?thesis by(auto simp del: correct_state_def split: if_split_asm) next case False with stk' idxI ins no_x heap_ok tconf meth a ha Xel Φ_pc frame frames wf_preallocatedD[OF wf, of h ArrayIndexOutOfBounds] show ?thesis by (fastforce simp: preh split: if_split_asm simp del: Listn.lesub_list_impl_same_size) qed qed qed lemma AStore_correct: assumes wf: "wf_prog wt P" assumes meth: "P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C" assumes ins: "ins!pc = AStore" assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" assumes conf: "Φ ⊢ t: (None, h, (stk,loc,C,M,pc)#frs)√" assumes no_x: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs" shows "Φ ⊢ t: σ √" proof - from ins conf meth obtain ST LT where heap_ok: "hconf h" and tconf: "P,h ⊢ t √t" and Φ_pc: "Φ C M!pc = Some (ST,LT)" and stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩_{⊤}] LT" and pc: "pc < size ins" and frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and frames: "conf_fs P h Φ M (size Ts) T frs" and preh: "preallocated h" by (auto dest: sees_method_fun) from ins wt Φ_pc have lST: "length ST > 2" by(auto) show ?thesis proof(cases "hd (tl (tl stk)) = Null") case True with ins no_x heap_ok tconf Φ_pc stk loc frame frames meth wf_preallocatedD[OF wf, of h NullPointer] preh show ?thesis by(fastforce) next case False note stkNN = this have STNN: "hd (tl (tl ST)) ≠ NT" proof assume "hd (tl (tl ST)) = NT" moreover from frame have "P,h ⊢ stk [:≤] ST" by simp with lST have "P,h ⊢ hd (tl (tl stk)) :≤ hd (tl (tl ST))" by (cases ST, auto, case_tac list, auto, case_tac lista, auto) ultimately have "hd (tl (tl stk)) = Null" by simp with stkNN show False by contradiction qed with ins stkNN Φ_pc wt obtain ST'' Y X ST' LT' where ST: "ST = Y # Integer # X⌊⌉ # ST''" and pc': "pc+1 < size ins" and Φ': "Φ C M ! (pc+1) = Some (ST', LT')" and ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩_{⊤}] LT'" and suc_pc: "pc+1 < size ins" by(fastforce) from stk ST obtain ref e idx stk' where stk': "stk = e#idx#ref#stk'" and idx: "P,h ⊢ idx :≤ Integer" and ref: "P,h ⊢ ref :≤ X⌊⌉" and e: "P,h ⊢ e :≤ Y" and ST'': "P,h ⊢ stk' [:≤] ST''" by auto from stkNN stk' have "ref ≠ Null" by(simp) with ref obtain a Xel n where a: "ref = Addr a" and ha: "typeof_addr h a = ⌊Array_type Xel n⌋" and Xel: "P ⊢ Xel ≤ X" by(cases ref)(fastforce simp add: conf_def widen_Array)+ from idx obtain idxI where idxI: "idx = Intg idxI" by(auto simp add: conf_def) show ?thesis proof(cases "0 <=s idxI ∧ sint idxI < int n") case True hence si': "0 <=s idxI" "sint idxI < int n" by simp_all from e obtain Te where Te: "typeof⇘h⇙ e = ⌊Te⌋" "P ⊢ Te ≤ Y" by(auto simp add: conf_def) show ?thesis proof(cases "P ⊢ Te ≤ Xel") case True with Te have eXel: "P,h ⊢ e :≤ Xel" by(auto simp add: conf_def intro: widen_trans) { fix h' assume "write": "heap_write h a (ACell (nat (sint idxI))) e h'" hence hext: "h ⊴ h'" by(rule hext_heap_write) with preh have preh': "preallocated h'" by(rule preallocated_hext) let ?f = "(stk', loc, C, M, pc + 1)" from si' have "nat (sint idxI) < n" by (simp add: word_sle_eq nat_less_iff) with ha have "P,h ⊢ a@ACell (nat (sint idxI)) : Xel" .. with "write" heap_ok have heap_ok': "hconf h'" using eXel by(rule hconf_heap_write_mono) moreover from ST stk stk' ST' have "P,h ⊢ stk' [:≤] ST'" by auto with hext have stk'': "P,h' ⊢ stk' [:≤] ST'" by- (rule confs_hext) moreover from loc LT' have "P,h ⊢ loc [:≤⇩_{⊤}] LT'" .. with hext have "P,h' ⊢ loc [:≤⇩_{⊤}] LT'" by - (rule confTs_hext) moreover with frame ST' ST LT' suc_pc wf Xel idxI si' stk'' have "conf_f P h' (ST', LT') ins ?f" by(clarsimp) with frames hext have "conf_fs P h' Φ M (size Ts) T frs" by- (rule conf_fs_hext) moreover from tconf hext have "P,h' ⊢ t √t" by(rule tconf_hext_mono) ultimately have "Φ ⊢ t:(None, h', ?f # frs) √" using meth Φ' Φ_pc suc_pc preh' by(fastforce) } with True si' ins meth stk' a ha no_x idxI idx Te show ?thesis by(auto split: if_split_asm simp del: correct_state_def intro: widen_trans) next case False with stk' idxI ins no_x heap_ok tconf meth a ha Xel Te Φ_pc frame frames si' wf_preallocatedD[OF wf, of h ArrayStore] show ?thesis by (fastforce split: if_splits list.splits simp: preh simp del: Listn.lesub_list_impl_same_size) qed next case False with stk' idxI ins no_x heap_ok tconf meth a ha Xel Φ_pc frame frames preh wf_preallocatedD[OF wf, of h ArrayIndexOutOfBounds] show ?thesis by(fastforce split: if_split_asm) qed qed qed lemma ALength_correct: assumes wf: "wf_prog wt P" assumes meth: "P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C" assumes ins: "ins!pc = ALength" assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" assumes conf: "Φ ⊢ t: (None, h, (stk,loc,C,M,pc)#frs)√" assumes no_x: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs" shows "Φ ⊢ t: σ √" proof - from ins conf meth obtain ST LT where heap_ok: "hconf h" and tconf: "P,h ⊢ t √t" and Φ_pc: "Φ C M!pc = Some (ST,LT)" and stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩_{⊤}] LT" and pc: "pc < size ins" and frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and frames: "conf_fs P h Φ M (size Ts) T frs" and preh: "preallocated h" by (auto dest: sees_method_fun) from ins wt Φ_pc have lST: "length ST > 0" by(auto) show ?thesis proof(cases "hd stk = Null") case True with ins no_x heap_ok tconf Φ_pc stk loc frame frames meth wf_preallocatedD[OF wf, of h NullPointer] preh show ?thesis by(fastforce) next case False note stkNN = this have STNN: "hd ST ≠ NT" proof assume "hd ST = NT" moreover from frame have "P,h ⊢ stk [:≤] ST" by simp with lST have "P,h ⊢ hd stk :≤ hd ST" by (cases ST, auto) ultimately have "hd stk = Null" by simp with stkNN show False by contradiction qed with stkNN ins Φ_pc wt obtain ST'' X ST' LT' where ST: "ST = (X⌊⌉) # ST''" and pc': "pc+1 < size ins" and Φ': "Φ C M ! (pc+1) = Some (ST', LT')" and ST': "P ⊢ (Integer # ST'') [≤] ST'" and LT': "P ⊢ LT [≤⇩_{⊤}] LT'" and suc_pc: "pc+1 < size ins" by(fastforce) from stk ST obtain ref stk' where stk': "stk = ref#stk'" and ref: "P,h ⊢ ref :≤ X⌊⌉" and ST'': "P,h ⊢ stk' [:≤] ST''" by auto from stkNN stk' have "ref ≠ Null" by(simp) with ref obtain a Xel n where a: "ref = Addr a" and ha: "typeof_addr h a = ⌊Array_type Xel n⌋" and Xel: "P ⊢ Xel ≤ X" by(cases ref)(fastforce simp add: conf_def widen_Array)+ from ins meth stk' a ha no_x have σ': "σ = (None, h, (Intg (word_of_int (int n)) # stk', loc, C, M, pc + 1) # frs)" (is "σ = (None, h, ?f # frs)") by(auto) moreover from ST stk stk' ST' have "P,h ⊢ Intg si # stk' [:≤] ST'" by(auto) with frame ST' ST LT' suc_pc wf have "conf_f P h (ST', LT') ins ?f" by(fastforce intro: widen_trans) ultimately show ?thesis using meth Φ' heap_ok Φ_pc frames tconf preh by fastforce qed qed lemma MEnter_correct: assumes wf: "wf_prog wt P" assumes meth: "P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C" assumes ins: "ins!pc = MEnter" assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" assumes conf: "Φ ⊢ t: (None, h, (stk,loc,C,M,pc)#frs)√" assumes no_x: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs" shows "Φ ⊢ t: σ √" proof - from ins conf meth obtain ST LT where heap_ok: "hconf h" and tconf: "P,h ⊢ t √t" and Φ_pc: "Φ C M!pc = Some (ST,LT)" and stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩_{⊤}] LT" and pc: "pc < size ins" and frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and frames: "conf_fs P h Φ M (size Ts) T frs" and preh: "preallocated h" by (auto dest: sees_method_fun) from ins wt Φ_pc have lST: "length ST > 0" by(auto) show ?thesis proof(cases "hd stk = Null") case True with ins no_x heap_ok tconf Φ_pc stk loc frame frames meth wf_preallocatedD[OF wf, of h NullPointer] preh show ?thesis by(fastforce) next case False note stkNN = this have STNN: "hd ST ≠ NT" proof assume "hd ST = NT" moreover from frame have "P,h ⊢ stk [:≤] ST" by simp with lST have "P,h ⊢ hd stk :≤ hd ST" by (cases ST, auto) ultimately have "hd stk = Null" by simp with stkNN show False by contradiction qed with stkNN ins Φ_pc wt obtain ST'' X ST' LT' where ST: "ST = X # ST''" and refT: "is_refT X" and pc': "pc+1 < size ins" and Φ': "Φ C M ! (pc+1) = Some (ST', LT')" and ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩_{⊤}] LT'" and suc_pc: "pc+1 < size ins" by(fastforce) from stk ST obtain ref stk' where stk': "stk = ref#stk'" and ref: "P,h ⊢ ref :≤ X" by auto from stkNN stk' have "ref ≠ Null" by(simp) moreover from loc LT' have "P,h ⊢ loc [:≤⇩_{⊤}] LT'" .. moreover from ST stk stk' ST' have "P,h ⊢ stk' [:≤] ST'" by(auto) ultimately show ?thesis using meth Φ' heap_ok Φ_pc suc_pc frames loc LT' no_x ins stk' ST' tconf preh by(fastforce) qed qed lemma MExit_correct: assumes wf: "wf_prog wt P" assumes meth: "P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C" assumes ins: "ins!pc = MExit" assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" assumes conf: "Φ ⊢ t: (None, h, (stk,loc,C,M,pc)#frs)√" assumes no_x: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs" shows "Φ ⊢ t: σ √" proof - from ins conf meth obtain ST LT where heap_ok: "hconf h" and tconf: "P,h ⊢ t √t" and Φ_pc: "Φ C M!pc = Some (ST,LT)" and stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩_{⊤}] LT" and pc: "pc < size ins" and frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and frames: "conf_fs P h Φ M (size Ts) T frs" and preh: "preallocated h" by (auto dest: sees_method_fun) from ins wt Φ_pc have lST: "length ST > 0" by(auto) show ?thesis proof(cases "hd stk = Null") case True with ins no_x heap_ok tconf Φ_pc stk loc frame frames meth wf_preallocatedD[OF wf, of h NullPointer] preh show ?thesis by(fastforce) next case False note stkNN = this have STNN: "hd ST ≠ NT" proof assume "hd ST = NT" moreover from frame have "P,h ⊢ stk [:≤] ST" by simp with lST have "P,h ⊢ hd stk :≤ hd ST" by (cases ST, auto) ultimately have "hd stk = Null" by simp with stkNN show False by contradiction qed with stkNN ins Φ_pc wt obtain ST'' X ST' LT' where ST: "ST = X # ST''" and refT: "is_refT X" and pc': "pc+1 < size ins" and Φ': "Φ C M ! (pc+1) = Some (ST', LT')" and ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩_{⊤}] LT'" and suc_pc: "pc+1 < size ins" by(fastforce) from stk ST obtain ref stk' where stk': "stk = ref#stk'" and ref: "P,h ⊢ ref :≤ X" by auto from stkNN stk' have "ref ≠ Null" by(simp) moreover from loc LT' have "P,h ⊢ loc [:≤⇩_{⊤}] LT'" .. moreover from ST stk stk' ST' have "P,h ⊢ stk' [:≤] ST'" by(auto) ultimately show ?thesis using meth Φ' heap_ok Φ_pc suc_pc frames loc LT' no_x ins stk' ST' tconf frame preh wf_preallocatedD[OF wf, of h IllegalMonitorState] by(fastforce) qed qed text ‹ The next theorem collects the results of the sections above, i.e.~exception handling and the execution step for each instruction. It states type safety for single step execution: in welltyped programs, a conforming state is transformed into another conforming state when one instruction is executed. › theorem instr_correct: "⟦ wf_jvm_prog⇘Φ⇙ P; P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩_{0},ins,xt)⌋ in C; (tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs); Φ ⊢ t: (None, h, (stk,loc,C,M,pc)#frs)√ ⟧ ⟹ Φ ⊢ t: σ'√" apply (subgoal_tac "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M") prefer 2 apply (erule wt_jvm_prog_impl_wt_instr, assumption) apply clarsimp apply (drule (1) sees_method_fun) apply simp apply(unfold exec.simps Let_def set_map) apply (frule wt_jvm_progD, erule exE) apply (cases "ins ! pc") apply (rule Load_correct, assumption+, fastforce) apply (rule Store_correct, assumption+, fastforce) apply (rule Push_correct, assumption+, fastforce) apply (rule New_correct, assumption+, fastforce) apply (rule NewArray_correct, assumption+, fastforce) apply (rule ALoad_correct, assumption+, fastforce) apply (rule AStore_correct, assumption+, fastforce) apply (rule ALength_correct, assumption+, fastforce) apply (rule Getfield_correct, assumption+, fastforce) apply (rule Putfield_correct, assumption+, fastforce) apply (rule CAS_correct, assumption+, fastforce) apply (rule Checkcast_correct, assumption+, fastforce) apply (rule Instanceof_correct, assumption+, fastforce) apply (rule Invoke_correct, assumption+, fastforce) apply (rule Return_correct, assumption+, fastforce simp add: split_beta) apply (rule Pop_correct, assumption+, fastforce) apply (rule Dup_correct, assumption+, fastforce) apply (rule Swap_correct, assumption+, fastforce) apply (rule BinOp_correct, assumption+, fastforce) apply (rule Goto_correct, assumption+, fastforce) apply (rule IfFalse_correct, assumption+, fastforce) apply (rule Throw_correct, assumption+, fastforce) apply (rule MEnter_correct, assumption+, fastforce) apply (rule MExit_correct, assumption+, fastforce) done declare defs1 [simp del] end subsection ‹Main› lemma (in JVM_conf_read) BV_correct_1 [rule_format]: "⋀σ. ⟦ wf_jvm_prog⇘Φ⇙ P; Φ ⊢ t: σ√⟧ ⟹ P,t ⊢ σ -tas-jvm→ σ' ⟶ Φ