(* Title: JinjaDCI/BV/BVNoTypeErrors.thy Author: Gerwin Klein, Susannah Mansky Copyright GPL Based on the Jinja theory BV/BVNoTypeErrors.thy by Gerwin Klein *) section ‹ Welltyped Programs produce no Type Errors › theory BVNoTypeError imports "../JVM/JVMDefensive" BVSpecTypeSafe begin lemma has_methodI: "P ⊢ C sees M,b:Ts→T = m in D ⟹ P ⊢ C has M,b" by (unfold has_method_def) blast text ‹ Some simple lemmas about the type testing functions of the defensive JVM: › lemma typeof_NoneD [simp,dest]: "typeof v = Some x ⟹ ¬is_Addr v" by (cases v) auto lemma is_Ref_def2: "is_Ref v = (v = Null ∨ (∃a. v = Addr a))" by (cases v) (auto simp add: is_Ref_def) lemma [iff]: "is_Ref Null" by (simp add: is_Ref_def2) lemma is_RefI [intro, simp]: "P,h ⊢ v :≤ T ⟹ is_refT T ⟹ is_Ref v" (*<*) proof(cases T) qed (auto simp add: is_refT_def is_Ref_def dest: conf_ClassD) (*>*) lemma is_IntgI [intro, simp]: "P,h ⊢ v :≤ Integer ⟹ is_Intg v" (*<*)by (unfold conf_def) auto(*>*) lemma is_BoolI [intro, simp]: "P,h ⊢ v :≤ Boolean ⟹ is_Bool v" (*<*)by (unfold conf_def) auto(*>*) declare defs1 [simp del] lemma wt_jvm_prog_states_NonStatic: assumes wf: "wf_jvm_prog⇘Φ⇙ P" and mC: "P ⊢ C sees M,NonStatic: Ts→T = (mxs, mxl, ins, et) in C" and Φ: "Φ C M ! pc = τ" and pc: "pc < size ins" shows "OK τ ∈ states P mxs (1+size Ts+mxl)" (*<*) proof - let ?wf_md = "(λP C (M, b, Ts, T⇩_{r}, mxs, mxl⇩_{0}, is, xt). wt_method P C b Ts T⇩_{r}mxs mxl⇩_{0}is xt (Φ C M))" have wfmd: "wf_prog ?wf_md P" using wf by (unfold wf_jvm_prog_phi_def) assumption show ?thesis using sees_wf_mdecl[OF wfmd mC] Φ pc by (simp add: wf_mdecl_def wt_method_def check_types_def) (blast intro: nth_in) qed (*>*) lemma wt_jvm_prog_states_Static: assumes wf: "wf_jvm_prog⇘Φ⇙ P" and mC: "P ⊢ C sees M,Static: Ts→T = (mxs, mxl, ins, et) in C" and Φ: "Φ C M ! pc = τ" and pc: "pc < size ins" shows "OK τ ∈ states P mxs (size Ts+mxl)" (*<*) proof - let ?wf_md = "(λP C (M, b, Ts, T⇩_{r}, mxs, mxl⇩_{0}, is, xt). wt_method P C b Ts T⇩_{r}mxs mxl⇩_{0}is xt (Φ C M))" have wfmd: "wf_prog ?wf_md P" using wf by (unfold wf_jvm_prog_phi_def) assumption show ?thesis using sees_wf_mdecl[OF wfmd mC] Φ pc by (simp add: wf_mdecl_def wt_method_def check_types_def) (blast intro: nth_in) qed (*>*) text ‹ The main theorem: welltyped programs do not produce type errors if they are started in a conformant state. › theorem no_type_error: fixes σ :: jvm_state assumes welltyped: "wf_jvm_prog⇘Φ⇙ P" and conforms: "P,Φ ⊢ σ √" shows "exec_d P σ ≠ TypeError" (*<*) proof - from welltyped obtain mb where wf: "wf_prog mb P" by (fast dest: wt_jvm_progD) obtain xcp h frs sh where s [simp]: "σ = (xcp, h, frs, sh)" by (cases σ) from conforms have "xcp ≠ None ∨ frs = [] ⟹ check P σ" by (unfold correct_state_def check_def) auto moreover { assume "¬(xcp ≠ None ∨ frs = [])" then obtain stk reg C M pc ics frs' where xcp [simp]: "xcp = None" and frs [simp]: "frs = (stk,reg,C,M,pc,ics)#frs'" by (clarsimp simp add: neq_Nil_conv) from conforms obtain ST LT b Ts T mxs mxl ins xt where hconf: "P ⊢ h √" and shconf: "P,h ⊢⇩_{s}sh √" and meth: "P ⊢ C sees M,b:Ts→T = (mxs, mxl, ins, xt) in C" and Φ: "Φ C M ! pc = Some (ST,LT)" and frame: "conf_f P h sh (ST,LT) ins (stk,reg,C,M,pc,ics)" and frames: "conf_fs P h sh Φ C M (size Ts) T frs'" by (fastforce simp add: correct_state_def dest: sees_method_fun) from frame obtain stk: "P,h ⊢ stk [:≤] ST" and reg: "P,h ⊢ reg [:≤⇩_{⊤}] LT" and pc: "pc < size ins" by (simp add: conf_f_def) from welltyped meth Φ pc have "OK (Some (ST, LT)) ∈ states P mxs (1+size Ts+mxl) ∨ OK (Some (ST, LT)) ∈ states P mxs (size Ts+mxl)" by (cases b, auto dest: wt_jvm_prog_states_NonStatic wt_jvm_prog_states_Static) hence "size ST ≤ mxs" by (auto simp add: JVM_states_unfold) with stk have mxs: "size stk ≤ mxs" by (auto dest: list_all2_lengthD) from welltyped meth pc have "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" by (rule wt_jvm_prog_impl_wt_instr) hence app⇩_{0}: "app (ins!pc) P mxs T pc (size ins) xt (Φ C M!pc) " by (simp add: wt_instr_def) with Φ have eff: "∀(pc',s')∈set (eff (ins ! pc) P pc xt (Φ C M ! pc)). pc' < size ins" by (unfold app_def) simp from app⇩_{0}Φ have app: "xcpt_app (ins!pc) P pc mxs xt (ST,LT) ∧ app⇩_{i}(ins!pc, P, pc, mxs, T, (ST,LT))" by (clarsimp simp add: app_def) with eff stk reg have "check_instr (ins!pc) P h stk reg C M pc frs' sh" proof (cases "ins!pc") case (Getfield F C) with app stk reg Φ obtain v vT stk' where field: "P ⊢ C sees F,NonStatic:vT in C" and stk: "stk = v # stk'" and conf: "P,h ⊢ v :≤ Class C" by auto from conf have is_Ref: "is_Ref v" by auto moreover { assume "v ≠ Null" with conf field is_Ref wf have "∃D vs. h (the_Addr v) = Some (D,vs) ∧ P ⊢ D ≼⇧^{*}C" by (auto dest!: non_npD) } ultimately show ?thesis using Getfield field stk has_field_mono[OF has_visible_field[OF field]] hconfD[OF hconf] by (unfold oconf_def has_field_def) (fastforce dest: has_fields_fun) next case (Getstatic C F D) with app stk reg Φ obtain vT where field: "P ⊢ C sees F,Static:vT in D" by auto then show ?thesis using Getstatic stk has_field_idemp[OF has_visible_field[OF field]] shconfD[OF shconf] by (unfold soconf_def has_field_def) (fastforce dest: has_fields_fun) next case (Putfield F C) with app stk reg Φ obtain v ref vT stk' where field: "P ⊢ C sees F,NonStatic:vT in C" and stk: "stk = v # ref # stk'" and confv: "P,h ⊢ v :≤ vT" and confr: "P,h ⊢ ref :≤ Class C" by fastforce from confr have is_Ref: "is_Ref ref" by simp moreover { assume "ref ≠ Null" with confr field is_Ref wf have "∃D vs. h (the_Addr ref) = Some (D,vs) ∧ P ⊢ D ≼⇧^{*}C" by (auto dest: non_npD) } ultimately show ?thesis using Putfield field stk confv by fastforce next case (Invoke M' n) with app have n: "n < size ST" by simp from stk have [simp]: "size stk = size ST" by (rule list_all2_lengthD) { assume "stk!n = Null" with n Invoke have ?thesis by simp } moreover { assume "ST!n = NT" with n stk have "stk!n = Null" by (auto simp: list_all2_conv_all_nth) with n Invoke have ?thesis by simp } moreover { assume Null: "stk!n ≠ Null" and NT: "ST!n ≠ NT" from NT app Invoke obtain D D' Ts T m where D: "ST!n = Class D" and M': "P ⊢ D sees M',NonStatic: Ts→T = m in D'" and Ts: "P ⊢ rev (take n ST) [≤] Ts" by auto from D stk n have "P,h ⊢ stk!n :≤ Class D" by (auto simp: list_all2_conv_all_nth) with Null obtain a C' fs where [simp]: "stk!n = Addr a" "h a = Some (C',fs)" and "P ⊢ C' ≼⇧^{*}D" by (fastforce dest!: conf_ClassD) with M' wf obtain m' Ts' T' D'' where C': "P ⊢ C' sees M',NonStatic: Ts'→T' = m' in D''" and Ts': "P ⊢ Ts [≤] Ts'" by (auto dest!: sees_method_mono) from stk have "P,h ⊢ take n stk [:≤] take n ST" .. hence "P,h ⊢ rev (take n stk) [:≤] rev (take n ST)" .. also note Ts also note Ts' finally have "P,h ⊢ rev (take n stk) [:≤] Ts'" . with Invoke Null n C' have ?thesis by (auto simp add: is_Ref_def2 has_methodI) } ultimately show ?thesis by blast next case (Invokestatic C M' n) with app have n: "n ≤ size ST" by simp from stk have [simp]: "size stk = size ST" by (rule list_all2_lengthD) from app Invokestatic obtain D Ts T m where M': "P ⊢ C sees M',Static: Ts→T = m in D" and Ts: "P ⊢ rev (take n ST) [≤] Ts" by auto from stk have "P,h ⊢ take n stk [:≤] take n ST" .. hence "P,h ⊢ rev (take n stk) [:≤] rev (take n ST)" .. also note Ts finally have "P,h ⊢ rev (take n stk) [:≤] Ts" . with Invokestatic n M' show ?thesis by (auto simp add: is_Ref_def2 has_methodI) next case Return show ?thesis proof(cases "M = clinit") case True have "is_class P C" by(rule sees_method_is_class[OF meth]) with wf_sees_clinit[OF wf] obtain m where "P ⊢ C sees clinit,Static: [] → Void = m in C" by(fastforce simp: is_class_def) with stk app Φ meth frames True Return show ?thesis by (auto simp add: has_methodI) next case False with stk app Φ meth frames Return show ?thesis by (auto intro: has_methodI) qed qed (auto simp add: list_all2_lengthD) hence "check P σ" using meth pc mxs by (auto simp: check_def intro: has_methodI) } ultimately have "check P σ" by blast thus "exec_d P σ ≠ TypeError" .. qed (*>*) text ‹ The theorem above tells us that, in welltyped programs, the defensive machine reaches the same result as the aggressive one (after arbitrarily many steps). › theorem welltyped_aggressive_imp_defensive: "wf_jvm_prog⇘Φ⇙ P ⟹ P,Φ ⊢ σ √ ⟹ P ⊢ σ -jvm→ σ' ⟹ P ⊢ (Normal σ) -jvmd→ (Normal σ')" (*<*) proof - assume wf: "wf_jvm_prog⇘Φ⇙ P" and cf: "P,Φ ⊢ σ √" and exec: "P ⊢ σ -jvm→ σ'" then have "(σ, σ') ∈ {(σ, σ'). exec (P, σ) = ⌊σ'⌋}⇧^{*}" by(simp only: exec_all_def) then show ?thesis proof(induct rule: rtrancl_induct) case base then show ?case by (simp add: exec_all_d_def1) next case (step y z) then have σy: "P ⊢ σ -jvm→ y" by (simp only: exec_all_def [symmetric]) have exec_d: "exec_d P y = Normal ⌊z⌋" using step no_type_error_commutes[OF no_type_error[OF wf BV_correct[OF wf σy cf]]] by (simp add: exec_all_d_def1) show ?case using step.hyps(3) exec_1_d_NormalI[OF exec_d] by (simp add: exec_all_d_def1) qed qed (*>*) text ‹ As corollary we get that the aggressive and the defensive machine are equivalent for welltyped programs (if started in a conformant state or in the canonical start state) › corollary welltyped_commutes: fixes σ :: jvm_state assumes wf: "wf_jvm_prog⇘Φ⇙ P" and conforms: "P,Φ ⊢ σ √" shows "P ⊢ (Normal σ) -jvmd→ (Normal σ') = P ⊢ σ -jvm→ σ'" proof(rule iffI) assume "P ⊢ Normal σ -jvmd→ Normal σ'" then show "P ⊢ σ -jvm→ σ'" by (rule defensive_imp_aggressive) next assume "P ⊢ σ -jvm→ σ'" then show "P ⊢ Normal σ -jvmd→ Normal σ'" by (rule welltyped_aggressive_imp_defensive [OF wf conforms]) qed corollary welltyped_initial_commutes: assumes wf: "wf_jvm_prog P" assumes nstart: "¬ is_class P Start" assumes meth: "P ⊢ C sees M,Static:[]→Void = b in C" assumes nclinit: "M ≠ clinit" assumes Obj_start_m: "(⋀b' Ts' T' m' D'. P ⊢ Object sees start_m, b' : Ts'→T' = m' in D' ⟹ b' = Static ∧ Ts' = [] ∧ T' = Void)" defines start: "σ ≡ start_state P" shows "start_prog P C M ⊢ (Normal σ) -jvmd→ (Normal σ') = start_prog P C M ⊢ σ -jvm→ σ'" proof - from wf obtain Φ where wf': "wf_jvm_prog⇘Φ⇙ P" by (auto simp: wf_jvm_prog_def) let ?Φ = "Φ_start Φ" from start_prog_wf_jvm_prog_phi[where Φ'="?Φ", OF wf' nstart meth nclinit Φ_start Obj_start_m] have "wf_jvm_prog⇘?Φ⇙(start_prog P C M)" by simp moreover from wf' nstart meth nclinit Φ_start(2) have "start_prog P C M,?Φ ⊢ σ √" unfolding start by (rule BV_correct_initial) ultimately show ?thesis by (rule welltyped_commutes) qed lemma not_TypeError_eq [iff]: "x ≠ TypeError = (∃t. x = Normal t)" by (cases x) auto locale cnf = fixes P and Φ and σ assumes wf: "wf_jvm_prog⇘Φ⇙ P" assumes cnf: "correct_state P Φ σ" theorem (in cnf) no_type_errors: "P ⊢ (Normal σ) -jvmd→ σ' ⟹ σ' ≠ TypeError" proof - assume "P ⊢ (Normal σ) -jvmd→ σ'" then have "(Normal σ, σ') ∈ (exec_1_d P)⇧^{*}" by (unfold exec_all_d_def1) simp then show ?thesis proof(induct rule: rtrancl_induct) case (step y z) then obtain y⇩_{n}where [simp]: "y = Normal y⇩_{n}" by clarsimp have nσy: "P ⊢ Normal σ -jvmd→ Normal y⇩_{n}" using step.hyps(1) by (fold exec_all_d_def1) simp have σy: "P ⊢ σ -jvm→ y⇩_{n}" using defensive_imp_aggressive[OF nσy] by simp show ?case using step no_type_error[OF wf BV_correct[OF wf σy cnf]] by (auto simp add: exec_1_d_eq) qed simp qed locale start = fixes P and C and M and σ and T and b and P⇩_{0}assumes wf: "wf_jvm_prog P" assumes nstart: "¬ is_class P Start" assumes sees: "P ⊢ C sees M,Static:[]→Void = b in C" assumes nclinit: "M ≠ clinit" assumes Obj_start_m: "(⋀b' Ts' T' m' D'. P ⊢ Object sees start_m, b' : Ts'→T' = m' in D' ⟹ b' = Static ∧ Ts' = [] ∧ T' = Void)" defines "σ ≡ Normal (start_state P)" defines [simp]: "P⇩_{0}≡ start_prog P C M" corollary (in start) bv_no_type_error: shows "P⇩_{0}⊢ σ -jvmd→ σ' ⟹ σ' ≠ TypeError" proof - from wf obtain Φ where wf': "wf_jvm_prog⇘Φ⇙ P" by (auto simp: wf_jvm_prog_def) let ?Φ = "Φ_start Φ" from start_prog_wf_jvm_prog_phi[where Φ'="?Φ", OF wf' nstart sees nclinit Φ_start Obj_start_m] have "wf_jvm_prog⇘?Φ⇙P⇩_{0}" by simp moreover from BV_correct_initial[where Φ'="?Φ", OF wf' nstart sees nclinit Φ_start(2)] have "correct_state P⇩_{0}?Φ (start_state P)" by simp ultimately have "cnf P⇩_{0}?Φ (start_state P)" by (rule cnf.intro) moreover assume "P⇩_{0}⊢ σ -jvmd→ σ'" ultimately show ?thesis by (unfold σ_def) (rule cnf.no_type_errors) qed end