(* Title: JinjaDCI/BV/BVSpecTypeSafe.thy Author: Cornelia Pusch, Gerwin Klein, Susannah Mansky Copyright 1999 Technische Universitaet Muenchen, 2019-20 UIUC Based on the Jinja theory BV/BVSpecTypeSafe.thy by Cornelia Pusch and Gerwin Klein *) section ‹ BV Type Safety Proof \label{sec:BVSpecTypeSafe} › theory BVSpecTypeSafe imports BVConform StartProg begin 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: › lemmas defs1 = correct_state_def conf_f_def wt_instr_def eff_def norm_eff_def app_def xcpt_app_def lemmas widen_rules [intro] = conf_widen confT_widen confs_widens confTs_widen subsection ‹ Exception Handling › text ‹ For the @{text Invoke} instruction the BV has checked all handlers that guard the current @{text 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). P ⊢ C ≼⇧^{*}D ∧ pc ∈ {f..<t} ∧ pc' = h ∧ d' = d" by (induct xt) (auto simp: relevant_entries_def matches_ex_entry_def is_relevant_entry_def split: if_split_asm) text ‹ For the @{text Invokestatic} instruction the BV has checked all handlers that guard the current @{text pc}. › lemma Invokestatic_handlers: "match_ex_table P C pc xt = Some (pc',d') ⟹ ∃(f,t,D,h,d) ∈ set (relevant_entries P (Invokestatic C⇩_{0}n M) pc xt). P ⊢ C ≼⇧^{*}D ∧ pc ∈ {f..<t} ∧ pc' = h ∧ d' = d" by (induct xt) (auto simp: relevant_entries_def matches_ex_entry_def is_relevant_entry_def split: if_split_asm) text ‹ For the instrs in @{text Called_set} the BV has checked all handlers that guard the current @{text pc}. › lemma Called_set_handlers: "match_ex_table P C pc xt = Some (pc',d') ⟹ i ∈ Called_set ⟹ ∃(f,t,D,h,d) ∈ set (relevant_entries P i pc xt). P ⊢ C ≼⇧^{*}D ∧ pc ∈ {f..<t} ∧ pc' = h ∧ d' = d" by (induct xt) (auto simp: relevant_entries_def matches_ex_entry_def is_relevant_entry_def split: if_split_asm) text ‹ We can prove separately that the recursive search for exception handlers (@{text find_handler}) in the frame stack results in a conforming state (if there was no matching exception handler in the current frame). We require that the exception is a valid heap address, and that the state before the exception occurred conforms. › lemma uncaught_xcpt_correct: assumes wt: "wf_jvm_prog⇘Φ⇙ P" assumes h: "h xcp = Some obj" shows "⋀f. P,Φ ⊢ (None, h, f#frs, sh)√ ⟹ curr_method f ≠ clinit ⟹ P,Φ ⊢ find_handler P xcp h frs sh √" (is "⋀f. ?correct (None, h, f#frs, sh) ⟹ ?prem f ⟹ ?correct (?find frs)") (*<*) proof (induct frs) ― ‹the base case is trivial as it should be› show "?correct (?find [])" by (simp add: correct_state_def) next ― ‹we will need both forms @{text wf_jvm_prog} and @{text wf_prog} later› from wt obtain mb where wf: "wf_prog mb P" by (simp add: wf_jvm_prog_phi_def) ― ‹the assumptions for the cons case:› fix f f' frs' assume cr: "?correct (None, h, f#f'#frs', sh)" assume pr: "?prem f" ― ‹the induction hypothesis:› assume IH: "⋀f. ?correct (None, h, f#frs', sh) ⟹ ?prem f ⟹ ?correct (?find frs')" from cr pr conf_clinit_Cons[where frs="f'#frs'" and f=f] obtain confc: "conf_clinit P sh (f'#frs')" and cr': "?correct (None, h, f'#frs', sh)" by(fastforce simp: correct_state_def) obtain stk loc C M pc ics where [simp]: "f' = (stk,loc,C,M,pc,ics)" by (cases f') from cr' obtain b Ts T mxs mxl⇩_{0}ins xt where meth: "P ⊢ C sees M,b:Ts → T = (mxs,mxl⇩_{0},ins,xt) in C" by (simp add: correct_state_def, blast) hence xt[simp]: "ex_table_of P C M = xt" by simp have cls: "is_class P C" by(rule sees_method_is_class'[OF meth]) from cr' obtain sfs where sfs: "M = clinit ⟹ sh C = Some(sfs,Processing)" by(fastforce simp: defs1 conf_clinit_def) show "?correct (?find (f'#frs'))" proof (cases "match_ex_table P (cname_of h xcp) pc xt") case None with cr' IH[of f'] show ?thesis proof(cases "M=clinit") case True then show ?thesis using xt cr' IH[of f'] None h conf_clinit_Called_Throwing conf_f_Throwing[where h=h and sh=sh, OF _ cls h sfs] by(cases frs', auto simp: correct_state_def image_iff) fastforce qed(auto) next fix pc_d assume "match_ex_table P (cname_of h xcp) pc xt = Some pc_d" then obtain pc' d' where match: "match_ex_table P (cname_of h xcp) pc xt = Some (pc',d')" (is "?match (cname_of h xcp) = _") by (cases pc_d) auto from wt meth cr' [simplified] have wti: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" by (fastforce simp: correct_state_def conf_f_def dest: sees_method_fun elim!: wt_jvm_prog_impl_wt_instr) from cr' obtain ST LT where Φ: "Φ C M ! pc = Some (ST, LT)" by(fastforce dest: sees_method_fun simp: correct_state_def) from cr' Φ meth have conf': "conf_f P h sh (ST, LT) ins f'" by (unfold correct_state_def) (fastforce dest: sees_method_fun) hence loc: "P,h ⊢ loc [:≤⇩_{⊤}] LT" and stk: "P,h ⊢ stk [:≤] ST" by (unfold conf_f_def) auto hence [simp]: "size stk = size ST" by (simp add: list_all2_lengthD) from cr meth pr obtain D n M' where ins: "ins!pc = Invoke n M' ∨ ins!pc = Invokestatic D n M'" (is "_ = ?i ∨ _ = ?i'") by(fastforce dest: sees_method_fun simp: correct_state_def) with match obtain f1 t D where rel: "(f1,t,D,pc',d') ∈ set (relevant_entries P (ins!pc) pc xt)" and D: "P ⊢ cname_of h xcp ≼⇧^{*}D" by(fastforce dest: Invoke_handlers Invokestatic_handlers) from rel have "(pc', Some (Class D # drop (size ST - d') ST, LT)) ∈ set (xcpt_eff (ins!pc) P pc (ST,LT) xt)" (is "(_, Some (?ST',_)) ∈ _") by (force simp: xcpt_eff_def image_def) with wti Φ obtain pc: "pc' < size ins" and "P ⊢ Some (?ST', LT) ≤' Φ C M ! pc'" by (clarsimp simp: defs1) blast then obtain ST' LT' where Φ': "Φ C M ! pc' = Some (ST',LT')" and less: "P ⊢ (?ST', LT) ≤⇩_{i}(ST',LT')" by (auto simp: sup_state_opt_any_Some) let ?f = "(Addr xcp # drop (length stk - d') stk, loc, C, M, pc',No_ics)" have "conf_f P h sh (ST',LT') ins ?f" proof - from wf less loc have "P,h ⊢ loc [:≤⇩_{⊤}] LT'" by simp blast moreover from D h have "P,h ⊢ Addr xcp :≤ Class D" by (simp add: conf_def obj_ty_def case_prod_unfold) with less stk have "P,h ⊢ Addr xcp # drop (length stk - d') stk [:≤] ST'" by (auto intro!: list_all2_dropI) ultimately show ?thesis using pc conf' by(auto simp: conf_f_def) qed with cr' match Φ' meth pc show ?thesis by (unfold correct_state_def) (cases "M=clinit"; fastforce dest: sees_method_fun simp: conf_clinit_def distinct_clinit_def) qed qed (*>*) text ‹ The requirement of lemma @{text uncaught_xcpt_correct} (that the exception is a valid reference on the heap) is always met for welltyped instructions and conformant states: › lemma exec_instr_xcpt_h: "⟦ fst (exec_instr (ins!pc) P h stk vars C M pc ics frs sh) = Some xcp; P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M; P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√ ⟧ ⟹ ∃obj. h xcp = Some obj" (is "⟦ ?xcpt; ?wt; ?correct ⟧ ⟹ ?thesis") (*<*) proof - note [simp] = split_beta note [split] = if_split_asm option.split_asm assume wt: ?wt ?correct hence pre: "preallocated h" by (simp add: correct_state_def hconf_def) assume xcpt: ?xcpt with exec_instr_xcpts have opt: "ins!pc = Throw ∨ xcp ∈ {a. ∃x ∈ sys_xcpts. a = addr_of_sys_xcpt x}" by simp with pre show ?thesis proof (cases "ins!pc") case Throw with xcpt wt pre show ?thesis by (clarsimp iff: list_all2_Cons2 simp: defs1) (auto dest: non_npD simp: is_refT_def elim: preallocatedE) qed (auto elim: preallocatedE) qed (*>*) lemma exec_step_xcpt_h: assumes xcpt: "fst (exec_step P h stk vars C M pc ics frs sh) = Some xcp" and ins: "instrs_of P C M = ins" and wti: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" and correct: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√" shows "∃obj. h xcp = Some obj" proof - from correct have pre: "preallocated h" by(simp add: defs1 hconf_def) { fix C' Cs assume ics[simp]: "ics = Calling C' Cs" with xcpt have "xcp = addr_of_sys_xcpt NoClassDefFoundError" by(cases ics, auto simp: split_beta split: init_state.splits if_split_asm) with pre have ?thesis using preallocated_def by force } moreover { fix Cs a assume [simp]: "ics = Throwing Cs a" with xcpt have eq: "a = xcp" by(cases Cs; simp) from correct have "P,h,sh ⊢⇩_{i}(C,M,pc,ics)" by(auto simp: defs1) with eq have ?thesis by simp } moreover { fix Cs assume ics: "ics = No_ics ∨ ics = Called Cs" with exec_instr_xcpt_h[OF _ wti correct] xcpt ins have ?thesis by(cases Cs, auto) } ultimately show ?thesis by(cases ics, auto) qed lemma conf_sys_xcpt: "⟦preallocated h; C ∈ sys_xcpts⟧ ⟹ P,h ⊢ Addr (addr_of_sys_xcpt C) :≤ Class C" by (auto elim: preallocatedE) lemma match_ex_table_SomeD: "match_ex_table P C pc xt = Some (pc',d') ⟹ ∃(f,t,D,h,d) ∈ set xt. matches_ex_entry P C pc (f,t,D,h,d) ∧ h = pc' ∧ d=d'" by (induct xt) (auto split: if_split_asm) text ‹ Finally we can state that, whenever an exception occurs, the next state always conforms: › lemma xcpt_correct: fixes σ' :: jvm_state assumes wtp: "wf_jvm_prog⇘Φ⇙ P" assumes meth: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩_{0},ins,xt) in C" assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" assumes xp: "fst (exec_step P h stk loc C M pc ics frs sh) = Some xcp" assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" assumes correct: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√" shows "P,Φ ⊢ σ'√" (*<*) proof - from wtp obtain wfmb where wf: "wf_prog wfmb P" by (simp add: wf_jvm_prog_phi_def) from meth have ins[simp]: "instrs_of P C M = ins" by simp have cls: "is_class P C" by(rule sees_method_is_class[OF meth]) from correct obtain sfs where sfs: "M = clinit ⟹ sh C = Some(sfs,Processing)" by(auto simp: correct_state_def conf_clinit_def conf_f_def2) note conf_sys_xcpt [elim!] note xp' = meth s' xp from correct meth obtain ST LT where h_ok: "P ⊢ h √" and sh_ok: "P,h ⊢⇩_{s}sh √" and Φ_pc: "Φ C M ! pc = Some (ST, LT)" and frame: "conf_f P h sh (ST,LT) ins (stk,loc,C,M,pc,ics)" and frames: "conf_fs P h sh Φ C M (size Ts) T frs" and confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)" and vics: "P,h,sh ⊢⇩_{i}(C,M,pc,ics)" by(auto simp: defs1 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 h_ok have preh: "preallocated h" by (simp add: hconf_def) note wtp moreover from exec_step_xcpt_h[OF xp ins wt correct] obtain obj where h: "h xcp = Some obj" by clarify moreover note correct ultimately have fh: "curr_method (stk,loc,C,M,pc,ics) ≠ clinit ⟹ P,Φ ⊢ find_handler P xcp h frs sh √" by (rule uncaught_xcpt_correct) with xp' have "M ≠ clinit ⟹ ∀Cs a. ics ≠ Throwing Cs a ⟹ match_ex_table P (cname_of h xcp) pc xt = None ⟹ ?thesis" (is "?nc ⟹ ?t ⟹ ?m (cname_of h xcp) = _ ⟹ _" is "?nc ⟹ ?t ⟹ ?match = _ ⟹ _") by(cases ics; simp add: split_beta) moreover from correct xp' conf_clinit_Called_Throwing conf_f_Throwing[where h=h and sh=sh, OF _ cls h sfs] have "M = clinit ⟹ ∀Cs a. ics ≠ Throwing Cs a ⟹ match_ex_table P (cname_of h xcp) pc xt = None ⟹ ?thesis" by(cases frs, auto simp: correct_state_def image_iff split_beta) fastforce moreover { fix pc_d assume "?match = Some pc_d" then obtain pc' d' where some_handler: "?match = Some (pc',d')" by (cases pc_d) auto from stk have [simp]: "size stk = size ST" .. 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: defs1) from some_handler obtain f t D where xt: "(f,t,D,pc',d') ∈ set xt" and "matches_ex_entry P (cname_of h xcp) pc (f,t,D,pc',d')" by (auto dest: match_ex_table_SomeD) hence match: "P ⊢ cname_of h xcp ≼⇧^{*}D" "pc ∈ {f..<t}" by (auto simp: matches_ex_entry_def) { fix C' Cs assume ics: "ics = Calling C' Cs ∨ ics = Called (C'#Cs)" let ?stk' = "Addr xcp # drop (length stk - d') stk" let ?f = "(?stk', loc, C, M, pc', No_ics)" from some_handler xp' ics have σ': "σ' = (None, h, ?f#frs, sh)" by (cases ics; simp add: split_beta) from xp ics have "xcp = addr_of_sys_xcpt NoClassDefFoundError" by(cases ics, auto simp: split_beta split: init_state.splits if_split_asm) with match preh have conf: "P,h ⊢ Addr xcp :≤ Class D" by fastforce from correct ics obtain C1 where "Called_context P C1 (ins!pc)" by(fastforce simp: correct_state_def conf_f_def2) then have "ins!pc ∈ Called_set" by(rule Called_context_Called_set) with xt match have "(f,t,D,pc',d') ∈ set (relevant_entries P (ins!pc) pc xt)" by(auto simp: relevant_entries_def is_relevant_entry_def) with eff 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')" by (fastforce simp: xcpt_eff_def sup_state_opt_any_Some) with conf loc stk conf_f_def2 frame ics have "conf_f P h sh (ST',LT') ins ?f" by (auto simp: defs1 intro: list_all2_dropI) with meth h_ok frames Φ_pc' σ' sh_ok confc ics have ?thesis by (unfold correct_state_def) (auto dest: sees_method_fun conf_clinit_diff' sees_method_is_class; fastforce) } moreover { assume ics: "ics = No_ics ∨ ics = Called []" let ?stk' = "Addr xcp # drop (length stk - d') stk" let ?f = "(?stk', loc, C, M, pc', No_ics)" from some_handler xp' ics have σ': "σ' = (None, h, ?f#frs, sh)" by (cases ics; simp add: split_beta) from xp ics obtain "(f,t,D,pc',d') ∈ set (relevant_entries P (ins!pc) pc xt)" and conf: "P,h ⊢ Addr xcp :≤ Class D" proof (cases "ins!pc") case Return with xp ics have False by(cases ics; cases frs, auto simp: split_beta split: if_split_asm) then show ?thesis by simp next case New with xp match have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')" by (simp add: is_relevant_entry_def) moreover from xp wt correct obtain obj where xcp: "h xcp = Some obj" by (blast dest: exec_step_xcpt_h[OF _ ins]) ultimately show ?thesis using xt match by (auto simp: relevant_entries_def conf_def case_prod_unfold intro: that) next case Getfield with xp ics have xcp: "xcp = addr_of_sys_xcpt NullPointer ∨ xcp = addr_of_sys_xcpt NoSuchFieldError ∨ xcp = addr_of_sys_xcpt IncompatibleClassChangeError" by (cases ics; simp add: split_beta split: if_split_asm staticb.splits) with Getfield match preh have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')" by (fastforce simp: is_relevant_entry_def) with match preh xt xcp show ?thesis by(fastforce simp: relevant_entries_def intro: that) next case Getstatic with xp match have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')" by (simp add: is_relevant_entry_def) moreover from xp wt correct obtain obj where xcp: "h xcp = Some obj" by (blast dest: exec_step_xcpt_h[OF _ ins]) ultimately show ?thesis using xt match by (auto simp: relevant_entries_def conf_def case_prod_unfold intro: that) next case Putfield with xp ics have xcp: "xcp = addr_of_sys_xcpt NullPointer ∨ xcp = addr_of_sys_xcpt NoSuchFieldError ∨ xcp = addr_of_sys_xcpt IncompatibleClassChangeError" by (cases ics; simp add: split_beta split: if_split_asm staticb.splits) with Putfield match preh have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')" by (fastforce simp: is_relevant_entry_def) with match preh xt xcp show ?thesis by (fastforce simp: relevant_entries_def intro: that) next case Putstatic with xp match have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')" by (simp add: is_relevant_entry_def) moreover from xp wt correct obtain obj where xcp: "h xcp = Some obj" by (blast dest: exec_step_xcpt_h[OF _ ins]) ultimately show ?thesis using xt match by (auto simp: relevant_entries_def conf_def case_prod_unfold intro: that) next case Checkcast with xp ics have [simp]: "xcp = addr_of_sys_xcpt ClassCast" by (cases ics; simp add: split_beta split: if_split_asm) with Checkcast match preh have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')" by (simp add: is_relevant_entry_def) with match preh xt show ?thesis by (fastforce simp: relevant_entries_def intro: that) next case Invoke with xp match have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')" by (simp add: is_relevant_entry_def) moreover from xp wt correct obtain obj where xcp: "h xcp = Some obj" by (blast dest: exec_step_xcpt_h[OF _ ins]) ultimately show ?thesis using xt match by (auto simp: relevant_entries_def conf_def case_prod_unfold intro: that) next case Invokestatic with xp match have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')" by (simp add: is_relevant_entry_def) moreover from xp wt correct obtain obj where xcp: "h xcp = Some obj" by (blast dest: exec_step_xcpt_h[OF _ ins]) ultimately show ?thesis using xt match by (auto simp: relevant_entries_def conf_def case_prod_unfold intro: that) next case Throw with xp match preh have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')" by (simp add: is_relevant_entry_def) moreover from xp wt correct obtain obj where xcp: "h xcp = Some obj" by (blast dest: exec_step_xcpt_h[OF _ ins]) ultimately show ?thesis using xt match by (auto simp: relevant_entries_def conf_def case_prod_unfold intro: that) qed(cases ics, (auto)[5])+ with eff 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')" by (fastforce simp: xcpt_eff_def sup_state_opt_any_Some) with conf loc stk conf_f_def2 frame ics have "conf_f P h sh (ST',LT') ins ?f" by (auto simp: defs1 intro: list_all2_dropI) with meth h_ok frames Φ_pc' σ' sh_ok confc ics have ?thesis by (unfold correct_state_def) (auto dest: sees_method_fun conf_clinit_diff'; fastforce) } ultimately have "∀Cs a. ics ≠ Throwing Cs a ⟹ ?thesis" by(cases ics; metis list.exhaust) } moreover { fix Cs a assume "ics = Throwing Cs a" with xp' have ics: "ics = Throwing [] xcp" by(cases Cs; clarsimp) let ?frs = "(stk,loc,C,M,pc,No_ics)#frs" have eT: "exec_step P h stk loc C M pc (Throwing [] xcp) frs sh = (Some xcp, h, ?frs, sh)" by auto with xp' ics have σ'_fh: "σ' = find_handler P xcp h ?frs sh" by simp from meth have [simp]: "xt = ex_table_of P C M" by simp let ?match = "match_ex_table P (cname_of h xcp) pc xt" { assume clinit: "M = clinit" and None: "?match = None" note asms = clinit None have "P,Φ |- find_handler P xcp h ?frs sh [ok]" proof(cases frs) case Nil with h_ok sh_ok asms show "P,Φ |- find_handler P xcp h ?frs sh [ok]" by(simp add: correct_state_def) next case [simp]: (Cons f' frs') obtain stk' loc' C' M' pc' ics' where [simp]: "f' = (stk',loc',C',M',pc',ics')" by(cases f') have cls: "is_class P C" by(rule sees_method_is_class[OF meth]) have shC: "sh C = Some(sfs,Processing)" by(rule sfs[OF clinit]) from correct obtain b Ts T mxs' mxl⇩_{0}' ins' xt' ST' LT' where meth': "P ⊢ C' sees M', b : Ts→T = (mxs', mxl⇩_{0}', ins', xt') in C'" and Φ_pc': "Φ C' M' ! pc' = ⌊(ST', LT')⌋" and frame': "conf_f P h sh (ST',LT') ins' (stk', loc', C', M', pc', ics')" and frames': "conf_fs P h sh Φ C' M' (length Ts) T frs'" and confc': "conf_clinit P sh ((stk',loc',C',M',pc',ics')#frs')" by(auto dest: conf_clinit_Cons simp: correct_state_def) from meth' have ins'[simp]: "instrs_of P C' M' = ins'" and [simp]: "xt' = ex_table_of P C' M'" by simp+ let ?f' = "case ics' of Called Cs' ⇒ (stk',loc',C',M',pc',Throwing (C#Cs') xcp) | _ ⇒ (stk',loc',C',M',pc',ics')" from asms confc have confc_T: "conf_clinit P sh (?f'#frs')" by(cases ics', auto simp: conf_clinit_def distinct_clinit_def) from asms conf_f_Throwing[where h=h and sh=sh, OF _ cls h shC] frame' have frame_T: "conf_f P h sh (ST', LT') ins' ?f'" by(cases ics'; simp) with h_ok sh_ok meth' Φ_pc' confc_T frames' have "P,Φ |- (None, h, ?f'#frs', sh) [ok]" by(cases ics') (fastforce simp: correct_state_def)+ with asms show ?thesis by(cases ics'; simp) qed } moreover { assume asms: "M ≠ clinit" "?match = None" from asms uncaught_xcpt_correct[OF wtp h correct] have "P,Φ |- find_handler P xcp h frs sh [ok]" by simp with asms have "P,Φ |- find_handler P xcp h ?frs sh [ok]" by auto } moreover { fix pc_d assume some_handler: "?match = ⌊pc_d⌋" (is "?match = ⌊pc_d⌋") then obtain pc1 d1 where sh': "?match = Some(pc1,d1)" by(cases pc_d, simp) let ?stk' = "Addr xcp # drop (length stk - d1) stk" let ?f = "(?stk', loc, C, M, pc1, No_ics)" from stk have [simp]: "size stk = size ST" .. from wt Φ_pc have eff: "∀(pc1, s')∈set (xcpt_eff (ins!pc) P pc (ST,LT) xt). pc1 < size ins ∧ P ⊢ s' ≤' Φ C M!pc1" by (auto simp: defs1) from match_ex_table_SomeD[OF sh'] obtain f t D where xt: "(f,t,D,pc1,d1) ∈ set xt" and "matches_ex_entry P (cname_of h xcp) pc (f,t,D,pc1,d1)" by auto hence match: "P ⊢ cname_of h xcp ≼⇧^{*}D" "pc ∈ {f..<t}" by (auto simp: matches_ex_entry_def) from ics vics obtain C1 where "Called_context P C1 (ins ! pc)" by auto then have "ins!pc ∈ Called_set" by(rule Called_context_Called_set) with match xt xp ics obtain res: "(f,t,D,pc1,d1) ∈ set (relevant_entries P (ins!pc) pc xt)" by(auto simp: relevant_entries_def is_relevant_entry_def) with h match xt xp ics have conf: "P,h ⊢ Addr xcp :≤ Class D" by (auto simp: relevant_entries_def conf_def case_prod_unfold) with eff res obtain ST1 LT1 where Φ_pc1: "Φ C M ! pc1 = Some (ST1, LT1)" and pc1: "pc1 < size ins" and less1: "P ⊢ (Class D # drop (size ST - d1) ST, LT) ≤⇩_{i}(ST1, LT1)" by (fastforce simp: xcpt_eff_def sup_state_opt_any_Some) with conf loc stk conf_f_def2 frame ics have frame1: "conf_f P h sh (ST1,LT1) ins ?f" by (auto simp: defs1 intro: list_all2_dropI) from Φ_pc1 h_ok sh_ok meth frame1 frames conf_clinit_diff'[OF confc] have "P,Φ |- (None, h, ?f # frs, sh) [ok]" by(fastforce simp: correct_state_def) with sh' have "P,Φ |- find_handler P xcp h ?frs sh [ok]" by auto } ultimately have cr': "P,Φ |- find_handler P xcp h ?frs sh [ok]" by(cases "?match") blast+ with σ'_fh have ?thesis by simp } ultimately show ?thesis by (cases "?match") blast+ qed (*>*) (**********Non-exception Single-step correctness*************************) declare defs1 [simp] subsection ‹ Initialization procedure steps › text ‹ In this section we prove that, for states that result in a step of the initialization procedure rather than an instruction execution, the state after execution of the step still conforms. › lemma Calling_correct: fixes σ' :: jvm_state assumes wtprog: "wf_jvm_prog⇘Φ⇙ P" assumes mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩_{0},ins,xt) in C" assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" assumes cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√" assumes xc: "fst (exec_step P h stk loc C M pc ics frs sh) = None" assumes ics: "ics = Calling C' Cs" shows "P,Φ ⊢ σ'√" proof - from wtprog obtain wfmb where wf: "wf_prog wfmb P" by (simp add: wf_jvm_prog_phi_def) from mC cf obtain ST LT where h_ok: "P ⊢ h √" and sh_ok: "P,h ⊢⇩_{s}sh √" 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 frame: "conf_f P h sh (ST, LT) ins (stk,loc,C,M,pc,ics)" and fs: "conf_fs P h sh Φ C M (size Ts) T frs" and confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)" and vics: "P,h,sh ⊢⇩_{i}(C,M,pc,ics)" by (fastforce dest: sees_method_fun) with ics have confc⇩_{0}: "conf_clinit P sh ((stk,loc,C,M,pc,Calling C' Cs)#frs)" by simp from vics ics have cls': "is_class P C'" by auto { assume None: "sh C' = None" let ?sh = "sh(C' ↦ (sblank P C', Prepared))" obtain FDTs where flds: "P ⊢ C' has_fields FDTs" using wf_Fields_Ex[OF wf cls'] by clarsimp from shconf_upd_obj[where C=C', OF sh_ok soconf_sblank[OF flds]] have sh_ok': "P,h ⊢⇩_{s}?sh √" by simp from None have "∀sfs. sh C' ≠ Some(sfs,Processing)" by simp with conf_clinit_nProc_dist[OF confc] have dist': "distinct (C' # clinit_classes ((stk, loc, C, M, pc, ics) # frs))" by simp then have dist'': "distinct (C' # clinit_classes frs)" by simp have confc': "conf_clinit P ?sh ((stk, loc, C, M, pc, ics) # frs)" by(rule conf_clinit_shupd[OF confc dist']) have fs': "conf_fs P h ?sh Φ C M (size Ts) T frs" by(rule conf_fs_shupd[OF fs dist'']) from vics ics have vics': "P,h,?sh ⊢⇩_{i}(C, M, pc, ics)" by auto from s' ics None have "σ' = (None, h, (stk, loc, C, M, pc, ics)#frs, ?sh)" by auto with mC h_ok sh_ok' Φ stk loc pc fs' confc vics' confc' frame None have ?thesis by fastforce } moreover { fix a assume "sh C' = Some a" then obtain sfs i where shC'[simp]: "sh C' = Some(sfs,i)" by(cases a, simp) from confc ics have last: "∃sobj. sh (last(C'#Cs)) = Some sobj" by(fastforce simp: conf_clinit_def) let "?f" = "λics'. (stk, loc, C, M, pc, ics'::init_call_status)" { assume i: "i = Done ∨ i = Processing" let ?ics = "Called Cs" from last vics ics have vics': "P,h,sh ⊢⇩_{i}(C, M, pc, ?ics)" by auto from confc ics have confc': "conf_clinit P sh (?f ?ics#frs)" by(cases "M=clinit"; clarsimp simp: conf_clinit_def distinct_clinit_def) from i s' ics have "σ' = (None, h, ?f ?ics#frs, sh)" by auto with mC h_ok sh_ok Φ stk loc pc fs confc' vics' frame ics have ?thesis by fastforce } moreover { assume i[simp]: "i = Error" let ?a = "addr_of_sys_xcpt NoClassDefFoundError" let ?ics = "Throwing Cs ?a" from h_ok have preh: "preallocated h" by (simp add: hconf_def) then obtain obj where ha: "h ?a = Some obj" by(clarsimp simp: preallocated_def sys_xcpts_def) with vics ics have vics': "P,h,sh ⊢⇩_{i}(C, M, pc, ?ics)" by auto from confc ics have confc'': "conf_clinit P sh (?f ?ics#frs)" by(cases "M=clinit"; clarsimp simp: conf_clinit_def distinct_clinit_def) from s' ics have σ': "σ' = (None, h, ?f ?ics#frs, sh)" by auto from mC h_ok sh_ok Φ stk loc pc fs confc'' vics σ' ics ha have ?thesis by fastforce } moreover { assume i[simp]: "i = Prepared" let ?sh = "sh(C' ↦ (sfs,Processing))" let ?D = "fst(the(class P C'))" let ?ics = "if C' = Object then Called (C'#Cs) else Calling ?D (C'#Cs)" from shconf_upd_obj[where C=C', OF sh_ok shconfD[OF sh_ok shC']] have sh_ok': "P,h ⊢⇩_{s}?sh √" by simp from cls' have "C' ≠ Object ⟹ P ⊢ C' ≼⇧^{*}?D" by(auto simp: is_class_def intro!: subcls1I) with is_class_supclass[OF wf _ cls'] have D: "C' ≠ Object ⟹ is_class P ?D" by simp from i have "∀sfs. sh C' ≠ Some(sfs,Processing)" by simp with conf_clinit_nProc_dist[OF confc⇩_{0}] have dist': "distinct (C' # clinit_classes ((stk, loc, C, M, pc, Calling C' Cs) # frs))" by fast then have dist'': "distinct (C' # clinit_classes frs)" by simp from conf_clinit_shupd_Calling[OF confc⇩_{0}dist' cls'] conf_clinit_shupd_Called[OF confc⇩_{0}dist' cls'] have confc': "conf_clinit P ?sh (?f ?ics#frs)" by clarsimp with last ics have "∃sobj. ?sh (last(C'#Cs)) = Some sobj" by(auto simp: conf_clinit_def fun_upd_apply) with D vics ics have vics': "P,h,?sh ⊢⇩_{i}(C, M, pc, ?ics)" by auto have fs': "conf_fs P h ?sh Φ C M (size Ts) T frs" by(rule conf_fs_shupd[OF fs dist'']) from frame vics' have frame': "conf_f P h ?sh (ST, LT) ins (?f ?ics)" by simp from i s' ics have "σ' = (None, h, ?f ?ics#frs, ?sh)" by(auto simp: if_split_asm) with mC h_ok sh_ok' Φ stk loc pc fs' confc' frame' ics have ?thesis by fastforce } ultimately have ?thesis by(cases i, auto) } ultimately show ?thesis by(cases "sh C'", auto) qed lemma Throwing_correct: fixes σ' :: jvm_state assumes wtprog: "wf_jvm_prog⇘Φ⇙ P" assumes mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩_{0},ins,xt) in C" assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" assumes cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√" assumes xc: "fst (exec_step P h stk loc C M pc ics frs sh) = None" assumes ics: "ics = Throwing (C'#Cs) a" shows "P,Φ ⊢ σ'√" proof - from wtprog obtain wfmb where wf: "wf_prog wfmb P" by (simp add: wf_jvm_prog_phi_def) from mC cf obtain ST LT where h_ok: "P ⊢ h √" and sh_ok: "P,h ⊢⇩_{s}sh √" 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 frame: "conf_f P h sh (ST, LT) ins (stk,loc,C,M,pc,ics)" and fs: "conf_fs P h sh Φ C M (size Ts) T frs" and confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)" and vics: "P,h,sh ⊢⇩_{i}(C,M,pc,ics)" by (fastforce dest: sees_method_fun) with ics have confc⇩_{0}: "conf_clinit P sh ((stk,loc,C,M,pc,Throwing (C'#Cs) a)#frs)" by simp from frame ics mC have cc: "∃C1. Called_context P C1 (ins ! pc)" by(clarsimp simp: conf_f_def2) from frame ics obtain obj where ha: "h a = Some obj" by(auto simp: conf_f_def2) from confc ics obtain sfs i where shC': "sh C' = Some(sfs,i)" by(clarsimp simp: conf_clinit_def) then have sfs: "P,h,C' ⊢⇩_{s}sfs √" by(rule shconfD[OF sh_ok]) from s' ics have σ': "σ' = (None, h, (stk,loc,C,M,pc,Throwing Cs a)#frs, sh(C' ↦ (fst(the(sh C')), Error)))" (is "σ' = (None, h, ?f'#frs, ?sh')") by simp from confc ics have dist: "distinct (C' # clinit_classes (?f' # frs))" by (simp add: conf_clinit_def distinct_clinit_def) then have dist': "distinct (C' # clinit_classes frs)" by simp from conf_clinit_Throwing confc ics have confc': "conf_clinit P sh (?f' # frs)" by simp from shconf_upd_obj[OF sh_ok sfs] shC' have "P,h ⊢⇩_{s}?sh' √" by simp moreover have "conf_fs P h ?sh' Φ C M (length Ts) T frs" by(rule conf_fs_shupd[OF fs dist']) moreover have "conf_clinit P ?sh' (?f' # frs)" by(rule conf_clinit_shupd[OF confc' dist]) moreover note σ' h_ok mC Φ pc stk loc ha cc ultimately show "P,Φ ⊢ σ' √" by fastforce qed lemma Called_correct: fixes σ' :: jvm_state assumes wtprog: "wf_jvm_prog⇘Φ⇙ P" assumes mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩_{0},ins,xt) in C" assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" assumes cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√" assumes xc: "fst (exec_step P h stk loc C M pc ics frs sh) = None" assumes ics[simp]: "ics = Called (C'#Cs)" shows "P,Φ ⊢ σ'√" proof - from wtprog obtain wfmb where wf: "wf_prog wfmb P" by (simp add: wf_jvm_prog_phi_def) from mC cf obtain ST LT where h_ok: "P ⊢ h √" and sh_ok: "P,h ⊢⇩_{s}sh √" 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 frame: "conf_f P h sh (ST, LT) ins (stk,loc,C,M,pc,ics)" and fs: "conf_fs P h sh Φ C M (size Ts) T frs" and confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)" and vics: "P,h,sh ⊢⇩_{i}(C,M,pc,ics)" by (fastforce dest: sees_method_fun) then have confc⇩_{0}: "conf_clinit P sh ((stk,loc,C,M,pc,Called (C'#Cs))#frs)" by simp from frame mC obtain C1 sobj where ss: "Called_context P C1 (ins ! pc)" and shC1: "sh C1 = Some sobj" by(clarsimp simp: conf_f_def2) from confc wf_sees_clinit[OF wf] obtain mxs' mxl' ins' xt' where clinit: "P ⊢ C' sees clinit,Static: [] → Void=(mxs',mxl',ins',xt') in C'" by(fastforce simp: conf_clinit_def is_class_def) let ?loc' = "replicate mxl' undefined" from s' clinit have σ': "σ' = (None, h, ([],?loc',C',clinit,0,No_ics)#(stk,loc,C,M,pc,Called Cs)#frs, sh)" (is "σ' = (None, h, ?if#?f'#frs, sh)") by simp with wtprog clinit obtain start: "wt_start P C' Static [] mxl' (Φ C' clinit)" and ins': "ins' ≠ []" by (auto dest: wt_jvm_prog_impl_wt_start) then obtain LT⇩_{0}where LT⇩_{0}: "Φ C' clinit ! 0 = Some ([], LT⇩_{0})" by (clarsimp simp: wt_start_def defs1 sup_state_opt_any_Some split: staticb.splits) moreover have "conf_f P h sh ([], LT⇩_{0}) ins' ?if" proof - let ?LT = "replicate mxl' Err" 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 moreover from conf_clinit_Called confc clinit have "conf_clinit P sh (?if # ?f' # frs)" by simp moreover note σ' h_ok sh_ok mC Φ pc stk loc clinit ss shC1 fs ultimately show "P,Φ ⊢ σ' √" by fastforce qed subsection ‹ Single Instructions › text ‹ In this section we prove for each single (welltyped) instruction that the state after execution of the instruction still conforms. Since we have already handled exceptions above, we can now assume that no exception occurs in this step. For instructions that may call the initialization procedure, we cover the calling and non-calling cases separately. › lemma Invoke_correct: fixes σ' :: jvm_state assumes wtprog: "wf_jvm_prog⇘Φ⇙ P" assumes meth_C: "P ⊢ C sees M,b: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 σ': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" assumes approx: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√" assumes no_xcp: "fst (exec_step P h stk loc C M pc ics frs sh) = None" shows "P,Φ ⊢ σ'√" (*<*) proof - from meth_C approx ins have [simp]: "ics = No_ics" by(cases ics, auto) 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: "P⊢ h√" and Φ_pc: "Φ C M!pc = Some (ST,LT)" and frame: "conf_f P h sh (ST,LT) ins (stk,loc,C,M,pc,ics)" and frames: "conf_fs P h sh Φ C M (size Ts) T frs" and confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)" by (fastforce dest: sees_method_fun) from ins wti Φ_pc have n: "n < size ST" by simp { assume "stk!n = Null" with ins no_xcp meth_C have False by (simp add: split_beta) hence ?thesis .. } moreover { 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 ins no_xcp meth_C have False by (simp add: split_beta) hence ?thesis .. } moreover { assume NT: "ST!n ≠ NT" and Null: "stk!n ≠ Null" from NT ins wti Φ_pc obtain D D' b Ts T m ST' LT' where D: "ST!n = Class D" and pc': "pc+1 < size ins" and m_D: "P ⊢ D sees M',b: Ts→T = m in D'" and Ts: "P ⊢ rev (take n ST) [≤] Ts" and Φ': "Φ C M ! (pc+1) = Some (ST', LT')" and LT': "P ⊢ LT [≤⇩_{⊤}] LT'" and ST': "P ⊢ (T # drop (n+1) ST) [≤] ST'" and b[simp]: "b = NonStatic" by (clarsimp simp: sup_state_opt_any_Some) from frame obtain stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩_{⊤}] LT" by simp from n stk D have "P,h ⊢ stk!n :≤ Class D" by (auto simp: list_all2_conv_all_nth) with Null obtain a C' fs where Addr: "stk!n = Addr a" and obj: "h a = Some (C',fs)" and C'subD: "P ⊢ C' ≼⇧^{*}D" by (fastforce dest!: conf_ClassD) with wfprog m_D no_xcp obtain Ts' T' D'' mxs' mxl' ins' xt' where m_C': "P ⊢ C' sees M',NonStatic: Ts'→T' = (mxs',mxl',ins',xt') in D''" and T': "P ⊢ T' ≤ T" and Ts': "P ⊢ Ts [≤] Ts'" by (auto dest: sees_method_mono) with wf_NonStatic_nclinit wtprog have nclinit: "M' ≠ clinit" by(simp add: wf_jvm_prog_phi_def) have D''subD': "P ⊢ D'' ≼⇧^{*}D'" by(rule sees_method_decl_mono[OF C'subD m_D m_C']) let ?loc' = "Addr a # rev (take n stk) @ replicate mxl' undefined" let ?f' = "([], ?loc', D'', M', 0, No_ics)" let ?f = "(stk, loc, C, M, pc, ics)" from Addr obj m_C' ins σ' meth_C no_xcp have s': "σ' = (None, h, ?f' # ?f # frs, sh)" by simp from Ts n have [simp]: "size Ts = 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',NonStatic:Ts'→T'=(mxs',mxl',ins',xt') in D''" by (fast dest: sees_method_idemp) moreover with wtprog obtain start: "wt_start P D'' NonStatic 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: wt_start_def defs1 sup_state_opt_any_Some split: staticb.splits) moreover have "conf_f P h sh ([], 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 [:≤⇩_{⊤}] replicate mxl' Err" by simp also from m_C' have "P ⊢ C' ≼⇧^{*}D''" by (rule sees_method_decl_above) with obj have "P,h ⊢ Addr a :≤ Class D''" by (simp add: conf_def) 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' nclinit by simp qed moreover have "conf_clinit P sh (?f'#?f#frs)" using conf_clinit_Invoke[OF confc nclinit] by simp ultimately have ?thesis using s' Φ_pc approx meth_C m_D T' ins D nclinit D''subD' by(fastforce dest: sees_method_fun [of _ C]) } ultimately show ?thesis by blast qed (*>*) lemma Invokestatic_nInit_correct: fixes σ' :: jvm_state assumes wtprog: "wf_jvm_prog⇘Φ⇙ P" assumes meth_C: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩_{0},ins,xt) in C" assumes ins: "ins ! pc = Invokestatic D M' n" and nclinit: "M' ≠ clinit" assumes wti: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" assumes σ': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" assumes approx: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√" assumes no_xcp: "fst (exec_step P h stk loc C M pc ics frs sh) = None" assumes cs: "ics = Called [] ∨ (ics = No_ics ∧ (∃sfs. sh (fst(method P D M')) = Some(sfs, Done)))" shows "P,Φ ⊢ σ'√" (*<*) 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: "P⊢ h√" and Φ_pc: "Φ C M!pc = Some (ST,LT)" and frame: "conf_f P h sh (ST,LT) ins (stk,loc,C,M,pc,ics)" and frames: "conf_fs P h sh Φ C M (size Ts) T frs" and confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)" by (fastforce dest: sees_method_fun) from ins wti Φ_pc have n: "n ≤ size ST" by simp from ins wti Φ_pc obtain D' b Ts T mxs' mxl' ins' xt' ST' LT' where pc': "pc+1 < size ins" and m_D: "P ⊢ D sees M',b: Ts→T = (mxs',mxl',ins',xt') in D'" and Ts: "P ⊢ rev (take n ST) [≤] Ts" and Φ': "Φ C M ! (pc+1) = Some (ST', LT')" and LT': "P ⊢ LT [≤⇩_{⊤}] LT'" and ST': "P ⊢ (T # drop n ST) [≤] ST'" and b[simp]: "b = Static" by (clarsimp simp: sup_state_opt_any_Some) from frame obtain stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩_{⊤}] LT" by simp let ?loc' = "rev (take n stk) @ replicate mxl' undefined" let ?f' = "([], ?loc', D', M', 0, No_ics)" let ?f = "(stk, loc, C, M, pc, No_ics)" from m_D ins σ' meth_C no_xcp cs have s': "σ' = (None, h, ?f' # ?f # frs, sh)" by auto from Ts n have [simp]: "size Ts = n" by (auto dest: list_all2_lengthD) from m_D wfprog b obtain mD': "P ⊢ D' sees M',Static:Ts→T=(mxs',mxl',ins',xt') in D'" by (fast dest: sees_method_idemp) moreover with wtprog obtain start: "wt_start P D' Static 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: wt_start_def defs1 sup_state_opt_any_Some split: staticb.splits) moreover have "conf_f P h sh ([], LT⇩_{0}) ins' ?f'" proof - let ?LT = "(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 finally have "P,h ⊢ rev (take n stk) [:≤⇩_{⊤}] map OK Ts" by simp also have "P,h ⊢ replicate mxl' undefined [:≤⇩_{⊤}] replicate mxl' Err" by simp also from m_D have "P ⊢ D ≼⇧^{*}D'" by (rule sees_method_decl_above) 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 moreover have "conf_clinit P sh (?f'#?f#frs)" by(rule conf_clinit_Invoke[OF confc nclinit]) ultimately show ?thesis using s' Φ_pc approx meth_C m_D ins nclinit by (fastforce dest: sees_method_fun [of _ C]) qed (*>*) lemma Invokestatic_Init_correct: fixes σ' :: jvm_state assumes wtprog: "wf_jvm_prog⇘Φ⇙ P" assumes meth_C: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩_{0},ins,xt) in C" assumes ins: "ins ! pc = Invokestatic D M' n" and nclinit: "M' ≠ clinit" assumes wti: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" assumes σ': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,No_ics)#frs, sh)" assumes approx: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,No_ics)#frs, sh)√" assumes no_xcp: "fst (exec_step P h stk loc C M pc No_ics frs sh) = None" assumes nDone: "∀sfs. sh (fst(method P D M')) ≠ Some(sfs, Done)" shows "P,Φ ⊢ σ'√" (*<*) 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: "P⊢ h√" 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 frames: "conf_fs P h sh Φ C M (size Ts) T frs" and confc: "conf_clinit P sh ((stk,loc,C,M,pc,No_ics)#frs)" and pc: "pc < size ins" by (fastforce dest: sees_method_fun) from ins wti Φ_pc obtain D' b Ts T mxs' mxl' ins' xt' where m_D: "P ⊢ D sees M',b: Ts→T = (mxs',mxl',ins',xt') in D'" and b[simp]: "b = Static" by clarsimp let ?f = "(stk, loc, C, M, pc, Calling D' [])" from m_D ins σ' meth_C no_xcp nDone have s': "σ' = (None, h, ?f # frs, sh)" by(auto split: init_state.splits) have cls: "is_class P D'" by(rule sees_method_is_class'[OF m_D]) from confc have confc': "conf_clinit P sh (?f#frs)" by(auto simp: conf_clinit_def distinct_clinit_def split: if_split_asm) with s' Φ_pc approx meth_C m_D ins nclinit stk loc pc cls frames show ?thesis by(fastforce dest: sees_method_fun [of _ C]) qed (*>*) declare list_all2_Cons2 [iff] lemma Return_correct: fixes σ' :: jvm_state assumes wt_prog: "wf_jvm_prog⇘Φ⇙ P" assumes meth: "P ⊢ C sees M,b: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 s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" assumes correct: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√" shows "P,Φ ⊢ σ'√" (*<*) proof - from meth correct ins have [simp]: "ics = No_ics" by(cases ics, auto) from wt_prog obtain wfmb where wf: "wf_prog wfmb P" by (simp add: wf_jvm_prog_phi_def) from meth ins s' have "frs = [] ⟹ ?thesis" by (simp add: correct_state_def) moreover { fix f frs' assume frs': "frs = f#frs'" then obtain stk' loc' C' M' pc' ics' where f: "f = (stk',loc',C',M',pc',ics')" by (cases f) from correct meth obtain ST LT where h_ok: "P ⊢ h √" and sh_ok: "P,h ⊢⇩_{s}sh √" and Φ_pc: "Φ C M ! pc = Some (ST, LT)" and frame: "conf_f P h sh (ST, LT) ins (stk,loc,C,M,pc,ics)" and frames: "conf_fs P h sh Φ C M (size Ts) T frs" and confc: "conf_clinit P sh frs" by (auto dest: sees_method_fun conf_clinit_Cons simp: correct_state_def) 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: conf_f_def) from f frs' frames meth obtain ST' LT' b' Ts'' T'' mxs' mxl⇩_{0}' ins' xt' where Φ': "Φ C' M' ! pc' = Some (ST', LT')" and meth_C': "P ⊢ C' sees M',b':Ts''→T''=(mxs',mxl⇩_{0}',ins',xt') in C'" and frame': "conf_f P h sh (ST',LT') ins' f" and conf_fs: "conf_fs P h sh Φ C' M' (size Ts'') T'' frs'" by clarsimp 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) { assume b[simp]: "b = NonStatic" from wf_NonStatic_nclinit[OF wf] meth have nclinit[simp]: "M ≠ clinit" by simp from f frs' meth ins s' have σ': "σ' = (None,h,(hd stk#(drop (1+size Ts) stk'),loc',C',M',pc'+1,ics')#frs',sh)" (is "σ' = (None,h,?f'#frs',sh)") by simp from f frs' confc conf_clinit_diff have confc'': "conf_clinit P sh (?f'#frs')" by blast with Φ' meth_C' f frs' frames meth obtain D Ts' T' m D' where ins': "ins' ! pc' = Invoke M (size Ts)" and D: "ST' ! (size Ts) = Class D" and meth_D: "P ⊢ D sees M,b: Ts'→T' = m in D'" and T': "P ⊢ T ≤ T'" and CsubD': "P ⊢ C ≼⇧^{*}D'" by(auto dest: sees_method_fun sees_method_fun[OF sees_method_idemp]) from wt_prog meth_C' pc' have "P,T'',mxs',size ins',xt' ⊢ ins'!pc',pc' :: Φ C' M'" by (rule wt_jvm_prog_impl_wt_instr) with ins' Φ' D meth_D obtain 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'" by (clarsimp simp: sup_state_opt_any_Some) from hd_stk T' have hd_stk': "P,h ⊢ hd stk :≤ T'" .. have frame'': "conf_f P h sh (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' moreover from f frs' frames (* ics' = No_ics *) have "P,h,sh ⊢⇩_{i}(C', M', Suc pc', ics')" by auto ultimately show ?thesis by (simp add: conf_f_def) qed with σ' frs' f meth h_ok sh_ok hd_stk Φ_suc frames confc'' meth_C' Φ' have ?thesis by(fastforce dest: sees_method_fun [of _ C']) } moreover { assume b[simp]: "b = Static" and nclinit[simp]: "M ≠ clinit" from f frs' meth ins s' have σ': "σ' = (None,h,(hd stk#(drop (size Ts) stk'),loc',C',M',pc'+1,ics')#frs',sh)" (is "σ' = (None,h,?f'#frs',sh)") by simp from f frs' confc conf_clinit_diff have confc'': "conf_clinit P sh (?f'#frs')" by blast with Φ' meth_C' f frs' frames meth obtain D Ts' T' m where ins': "ins' ! pc' = Invokestatic D M (size Ts)" and meth_D: "P ⊢ D sees M,b: Ts'→T' = m in C" and T': "P ⊢ T ≤ T'" by(auto dest: sees_method_fun sees_method_mono2[OF _ wf sees_method_idemp]) from wt_prog meth_C' pc' have "P,T'',mxs',size ins',xt' ⊢ ins'!pc',pc' :: Φ C' M'" by (rule wt_jvm_prog_impl_wt_instr) with ins' Φ' meth_D obtain ST'' LT'' where Φ_suc: "Φ C' M' ! Suc pc' = Some (ST'', LT'')" and less: "P ⊢ (T' # drop (size Ts) ST', LT') ≤⇩_{i}(ST'', LT'')" and suc_pc': "Suc pc' < size ins'" by (clarsimp simp: sup_state_opt_any_Some) from hd_stk T' have hd_stk': "P,h ⊢ hd stk :≤ T'" .. have frame'': "conf_f P h sh (ST'',LT'') ins' ?f'" proof - from stk' have "P,h ⊢ drop (size Ts) stk' [:≤] drop (size Ts) ST'" .. moreover with hd_stk' less have "P,h ⊢ hd stk # drop (size Ts) stk' [:≤] ST''" by auto moreover from wf loc' less have "P,h ⊢ loc' [:≤⇩_{⊤}] LT''" by auto moreover note suc_pc' moreover from f frs' frames (* ics' = No_ics *) have "P,h,sh ⊢⇩_{i}(C', M', Suc pc', ics')" by auto ultimately show ?thesis by (simp add: conf_f_def) qed with σ' frs' f meth h_ok sh_ok hd_stk Φ_suc frames confc'' meth_C' Φ' have ?thesis by(fastforce dest: sees_method_fun [of _ C']) } moreover { assume b[simp]: "b = Static" and clinit[simp]: "M = clinit" from frs' meth ins s' have σ': "σ' = (None,h,frs,sh(C↦(fst(the(sh C)), Done)))" (is "σ' = (None,h,frs,?sh)") by simp from correct have dist': "distinct (C # clinit_classes frs)" by(simp add: conf_clinit_def distinct_clinit_def) from f frs' correct have confc1: "conf_clinit P sh ((stk, loc, C, clinit, pc, No_ics) # (stk',loc',C',M',pc',ics') # frs')" by simp then have ics_dist: "distinct (C # ics_classes ics')" by(simp add: conf_clinit_def distinct_clinit_def) from conf_clinit_Cons_Cons[OF confc1] have dist'': "distinct (C # clinit_classes frs')" by(simp add: conf_clinit_def distinct_clinit_def) from correct shconf_upd_obj[OF sh_ok _ [OF shconfD[OF sh_ok]]] have sh'_ok: "P,h ⊢⇩_{s}?sh √" by(clarsimp simp: conf_clinit_def) have frame'': "conf_f P h ?sh (ST',LT') ins' f" proof - note stk' loc' pc' f valid_ics_shupd[OF _ ics_dist] moreover from f frs' frames have "P,h,sh ⊢⇩_{i}(C', M', pc', ics')" by auto ultimately show ?thesis by (simp add: conf_f_def2) qed have conf_fs': "conf_fs P h ?sh Φ C' M' (length Ts'') T'' frs'" by(rule conf_fs_shupd[OF conf_fs dist'']) have confc'': "conf_clinit P ?sh frs" by(rule conf_clinit_shupd[OF confc dist']) from σ' f frs' h_ok sh'_ok conf_fs' frame'' Φ' stk' loc' pc' meth_C' confc'' have ?thesis by(fastforce dest: sees_method_fun) } ultimately have ?thesis by (cases b) blast+ } ultimately show ?thesis by (cases frs) blast+ qed (*>*) declare sup_state_opt_any_Some [iff] declare not_Err_eq [iff] lemma Load_correct: assumes "wf_prog wt P" and mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩_{0},ins,xt) in C" and i: "ins!pc = Load idx" and "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" and "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" and cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√" shows "P,Φ |- σ' [ok]" (*<*) proof - have "ics = No_ics" using mC i cf by(cases ics) auto then show ?thesis using assms(1,3-6) sees_method_fun[OF mC] by(fastforce elim!: confTs_confT_sup conf_clinit_diff) qed (*>*) declare [[simproc del: list_to_set_comprehension]] lemma Store_correct: assumes "wf_prog wt P" and mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩_{0},ins,xt) in C" and i: "ins!pc = Store idx" and "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" and "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" and cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√" shows "P,Φ |- σ' [ok]" (*<*) proof - have "ics = No_ics" using mC i cf by(cases ics) auto then show ?thesis using assms(1,3-6) sees_method_fun[OF mC] by clarsimp (blast intro!: list_all2_update_cong conf_clinit_diff) qed (*>*) lemma Push_correct: assumes "wf_prog wt P" and mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩_{0},ins,xt) in C" and i: "ins!pc = Push v" and "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" and "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" and cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√" shows "P,Φ |- σ' [ok]" (*<*) proof - have "ics = No_ics" using mC i cf by(cases ics) auto then show ?thesis using assms(1,3-6) sees_method_fun[OF mC] by clarsimp (blast dest: typeof_lit_conf conf_clinit_diff) qed lemma Cast_conf2: "⟦ wf_prog ok P; P,h ⊢ v :≤ T; is_refT T; cast_ok P C h v; P ⊢ Class C ≤ T'; is_class P C⟧ ⟹ P,h ⊢ v :≤ T'" (*<*) proof - assume "wf_prog ok P" and "P,h ⊢ v :≤ T" and "is_refT T" and "cast_ok P C h v" and wid: "P ⊢ Class C ≤ T'" and "is_class P C" then show "P,h ⊢ v :≤ T'" using Class_widen[OF wid] by(cases v) (auto simp: cast_ok_def is_refT_def conf_def obj_ty_def intro: rtrancl_trans) qed (*>*) lemma Checkcast_correct: assumes "wf_jvm_prog⇘Φ⇙ P" and mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩_{0},ins,xt) in C" and i: "ins!pc = Checkcast D" and "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" and "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" and cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√" and "fst (exec_step P h stk loc C M pc ics frs sh) = None" shows "P,Φ |- σ' [ok]" (*<*) proof - have "ics = No_ics" using mC i cf by(cases ics) auto then show ?thesis using assms by (clarsimp simp: wf_jvm_prog_phi_def split: if_split_asm) (blast intro: Cast_conf2 dest: sees_method_fun conf_clinit_diff) qed (*>*) declare split_paired_All [simp del] lemmas widens_Cons [iff] = list_all2_Cons1 [of "widen P"] for P lemma Getfield_correct: fixes σ' :: jvm_state assumes wf: "wf_prog wt P" assumes mC: "P ⊢ C sees M,b: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 s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" assumes cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√" assumes xc: "fst (exec_step P h stk loc C M pc ics frs sh) = None" shows "P,Φ ⊢ σ'√" (*<*) proof - from mC cf i have [simp]: "ics = No_ics" by(cases ics, auto) from mC cf obtain ST LT where "h√": "P ⊢ h √" and "sh√": "P,h ⊢⇩_{s}sh √" 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 sh Φ C M (size Ts)