(* Title: HOL/MicroJava/BV/BVNoTypeError.thy Author: Gerwin Klein *) section {* Welltyped Programs produce no Type Errors *} theory BVNoTypeError imports "../JVM/JVMDefensive" BVSpecTypeSafe begin text {* Some simple lemmas about the type testing functions of the defensive JVM: *} lemma typeof_NoneD [simp,dest]: "typeof (λv. None) v = Some x ==> ¬isAddr v" by (cases v) auto lemma isRef_def2: "isRef v = (v = Null ∨ (∃loc. v = Addr loc))" by (cases v) (auto simp add: isRef_def) lemma app'Store[simp]: "app' (Store idx, G, pc, maxs, rT, (ST,LT)) = (∃T ST'. ST = T#ST' ∧ idx < length LT)" by (cases ST) auto lemma app'GetField[simp]: "app' (Getfield F C, G, pc, maxs, rT, (ST,LT)) = (∃oT vT ST'. ST = oT#ST' ∧ is_class G C ∧ field (G,C) F = Some (C,vT) ∧ G \<turnstile> oT \<preceq> Class C)" by (cases ST) auto lemma app'PutField[simp]: "app' (Putfield F C, G, pc, maxs, rT, (ST,LT)) = (∃vT vT' oT ST'. ST = vT#oT#ST' ∧ is_class G C ∧ field (G,C) F = Some (C, vT') ∧ G \<turnstile> oT \<preceq> Class C ∧ G \<turnstile> vT \<preceq> vT')" apply rule defer apply clarsimp apply (cases ST) apply simp apply (cases "tl ST") apply auto done lemma app'Checkcast[simp]: "app' (Checkcast C, G, pc, maxs, rT, (ST,LT)) = (∃rT ST'. ST = RefT rT#ST' ∧ is_class G C)" apply rule defer apply clarsimp apply (cases ST) apply simp apply (cases "hd ST") defer apply simp apply simp done lemma app'Pop[simp]: "app' (Pop, G, pc, maxs, rT, (ST,LT)) = (∃T ST'. ST = T#ST')" by (cases ST) auto lemma app'Dup[simp]: "app' (Dup, G, pc, maxs, rT, (ST,LT)) = (∃T ST'. ST = T#ST' ∧ length ST < maxs)" by (cases ST) auto lemma app'Dup_x1[simp]: "app' (Dup_x1, G, pc, maxs, rT, (ST,LT)) = (∃T1 T2 ST'. ST = T1#T2#ST' ∧ length ST < maxs)" by (cases ST, simp, cases "tl ST", auto) lemma app'Dup_x2[simp]: "app' (Dup_x2, G, pc, maxs, rT, (ST,LT)) = (∃T1 T2 T3 ST'. ST = T1#T2#T3#ST' ∧ length ST < maxs)" by (cases ST, simp, cases "tl ST", simp, cases "tl (tl ST)", auto) lemma app'Swap[simp]: "app' (Swap, G, pc, maxs, rT, (ST,LT)) = (∃T1 T2 ST'. ST = T1#T2#ST')" by (cases ST, simp, cases "tl ST", auto) lemma app'IAdd[simp]: "app' (IAdd, G, pc, maxs, rT, (ST,LT)) = (∃ST'. ST = PrimT Integer#PrimT Integer#ST')" apply (cases ST) apply simp apply simp apply (case_tac a) apply auto apply (rename_tac prim_ty, case_tac prim_ty) apply auto apply (rename_tac prim_ty, case_tac prim_ty) apply auto apply (case_tac list) apply auto apply (case_tac a) apply auto apply (rename_tac prim_ty, case_tac prim_ty) apply auto done lemma app'Ifcmpeq[simp]: "app' (Ifcmpeq b, G, pc, maxs, rT, (ST,LT)) = (∃T1 T2 ST'. ST = T1#T2#ST' ∧ 0 ≤ b + int pc ∧ ((∃p. T1 = PrimT p ∧ T1 = T2) ∨ (∃r r'. T1 = RefT r ∧ T2 = RefT r')))" apply auto apply (cases ST) apply simp apply (cases "tl ST") apply (case_tac a) apply auto done lemma app'Return[simp]: "app' (Return, G, pc, maxs, rT, (ST,LT)) = (∃T ST'. ST = T#ST'∧ G \<turnstile> T \<preceq> rT)" by (cases ST) auto lemma app'Throw[simp]: "app' (Throw, G, pc, maxs, rT, (ST,LT)) = (∃ST' r. ST = RefT r#ST')" apply (cases ST) apply simp apply (cases "hd ST") apply auto done lemma app'Invoke[simp]: "app' (Invoke C mn fpTs, G, pc, maxs, rT, ST, LT) = (∃apTs X ST' mD' rT' b'. ST = (rev apTs) @ X # ST' ∧ length apTs = length fpTs ∧ is_class G C ∧ (∀(aT,fT)∈set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) ∧ method (G,C) (mn,fpTs) = Some (mD', rT', b') ∧ G \<turnstile> X \<preceq> Class C)" (is "?app ST LT = ?P ST LT") proof assume "?P ST LT" thus "?app ST LT" by (auto simp add: list_all2_iff) next assume app: "?app ST LT" hence l: "length fpTs < length ST" by simp obtain xs ys where xs: "ST = xs @ ys" "length xs = length fpTs" proof - have "ST = take (length fpTs) ST @ drop (length fpTs) ST" by simp moreover from l have "length (take (length fpTs) ST) = length fpTs" by simp ultimately show ?thesis .. qed obtain apTs where "ST = (rev apTs) @ ys" and "length apTs = length fpTs" proof - from xs(1) have "ST = rev (rev xs) @ ys" by simp then show thesis by (rule that) (simp add: xs(2)) qed moreover from l xs obtain X ST' where "ys = X#ST'" by (auto simp add: neq_Nil_conv) ultimately have "ST = (rev apTs) @ X # ST'" "length apTs = length fpTs" by auto with app show "?P ST LT" apply (clarsimp simp add: list_all2_iff) apply (intro exI conjI) apply auto done qed lemma approx_loc_len [simp]: "approx_loc G hp loc LT ==> length loc = length LT" by (simp add: approx_loc_def list_all2_iff) lemma approx_stk_len [simp]: "approx_stk G hp stk ST ==> length stk = length ST" by (simp add: approx_stk_def) lemma isRefI [intro, simp]: "G,hp \<turnstile> v ::\<preceq> RefT T ==> isRef v" apply (drule conf_RefTD) apply (auto simp add: isRef_def) done lemma isIntgI [intro, simp]: "G,hp \<turnstile> v ::\<preceq> PrimT Integer ==> isIntg v" apply (unfold conf_def) apply auto apply (erule widen.cases) apply auto apply (cases v) apply auto done lemma list_all2_approx: "list_all2 (approx_val G hp) s (map OK S) = list_all2 (conf G hp) s S" apply (induct S arbitrary: s) apply (auto simp add: list_all2_Cons2 approx_val_def) done lemma list_all2_conf_widen: "wf_prog mb G ==> list_all2 (conf G hp) a b ==> list_all2 (λx y. G \<turnstile> x \<preceq> y) b c ==> list_all2 (conf G hp) a c" apply (rule list_all2_trans) defer apply assumption apply assumption apply (drule conf_widen, assumption+) done text {* The main theorem: welltyped programs do not produce type errors if they are started in a conformant state. *} theorem no_type_error: assumes welltyped: "wt_jvm_prog G Phi" and conforms: "G,Phi \<turnstile>JVM s \<surd>" shows "exec_d G (Normal s) ≠ TypeError" proof - from welltyped obtain mb where wf: "wf_prog mb G" by (fast dest: wt_jvm_progD) obtain xcp hp frs where s [simp]: "s = (xcp, hp, frs)" by (cases s) from conforms have "xcp ≠ None ∨ frs = [] ==> check G s" by (unfold correct_state_def check_def) auto moreover { assume "¬(xcp ≠ None ∨ frs = [])" then obtain stk loc C sig pc frs' where xcp [simp]: "xcp = None" and frs [simp]: "frs = (stk,loc,C,sig,pc)#frs'" by (clarsimp simp add: neq_Nil_conv) from conforms obtain ST LT rT maxs maxl ins et where hconf: "G \<turnstile>h hp \<surd>" and "class": "is_class G C" and meth: "method (G, C) sig = Some (C, rT, maxs, maxl, ins, et)" and phi: "Phi C sig ! pc = Some (ST,LT)" and frame: "correct_frame G hp (ST,LT) maxl ins (stk,loc,C,sig,pc)" and frames: "correct_frames G hp Phi rT sig frs'" by (auto simp add: correct_state_def) from frame obtain stk: "approx_stk G hp stk ST" and loc: "approx_loc G hp loc LT" and pc: "pc < length ins" and len: "length loc = length (snd sig) + maxl + 1" by (auto simp add: correct_frame_def) note approx_val_def [simp] from welltyped meth conforms have "wt_instr (ins!pc) G rT (Phi C sig) maxs (length ins) et pc" by simp (rule wt_jvm_prog_impl_wt_instr_cor) then obtain app': "app (ins!pc) G maxs rT pc et (Phi C sig!pc) " and eff: "∀(pc', s')∈set (eff (ins ! pc) G pc et (Phi C sig ! pc)). pc' < length ins" by (simp add: wt_instr_def phi) blast from eff have pc': "∀pc' ∈ set (succs (ins!pc) pc). pc' < length ins" by (simp add: eff_def) blast from app' phi have app: "xcpt_app (ins!pc) G pc et ∧ app' (ins!pc, G, pc, maxs, rT, (ST,LT))" by (clarsimp simp add: app_def) with eff stk loc pc' have "check_instr (ins!pc) G hp stk loc C sig pc maxs frs'" proof (cases "ins!pc") case (Getfield F C) with app stk loc phi obtain v vT stk' where "class": "is_class G C" and field: "field (G, C) F = Some (C, vT)" and stk: "stk = v # stk'" and conf: "G,hp \<turnstile> v ::\<preceq> Class C" apply clarsimp apply (blast dest: conf_widen [OF wf]) done from conf have isRef: "isRef v" .. moreover { assume "v ≠ Null" with conf field isRef wf have "∃D vs. hp (the_Addr v) = Some (D,vs) ∧ G \<turnstile> D \<preceq>C C" by (auto dest!: non_np_objD) } ultimately show ?thesis using Getfield field "class" stk hconf wf apply clarsimp apply (fastforce dest!: hconfD widen_cfs_fields oconf_objD) done next case (Putfield F C) with app stk loc phi obtain v ref vT stk' where "class": "is_class G C" and field: "field (G, C) F = Some (C, vT)" and stk: "stk = v # ref # stk'" and confv: "G,hp \<turnstile> v ::\<preceq> vT" and confr: "G,hp \<turnstile> ref ::\<preceq> Class C" apply clarsimp apply (blast dest: conf_widen [OF wf]) done from confr have isRef: "isRef ref" .. moreover { assume "ref ≠ Null" with confr field isRef wf have "∃D vs. hp (the_Addr ref) = Some (D,vs) ∧ G \<turnstile> D \<preceq>C C" by (auto dest: non_np_objD) } ultimately show ?thesis using Putfield field "class" stk confv by clarsimp next case (Invoke C mn ps) with app obtain apTs X ST' where ST: "ST = rev apTs @ X # ST'" and ps: "length apTs = length ps" and w: "∀(x, y)∈set (zip apTs ps). G \<turnstile> x \<preceq> y" and C: "G \<turnstile> X \<preceq> Class C" and mth: "method (G, C) (mn, ps) ≠ None" by (simp del: app'.simps) blast from ST stk obtain aps x stk' where stk': "stk = aps @ x # stk'" and aps: "approx_stk G hp aps (rev apTs)" and x: "G,hp \<turnstile> x ::\<preceq> X" and l: "length aps = length apTs" by (auto dest!: approx_stk_append) from stk' l ps have [simp]: "stk!length ps = x" by (simp add: nth_append) from stk' l ps have [simp]: "take (length ps) stk = aps" by simp from w ps have widen: "list_all2 (λx y. G \<turnstile> x \<preceq> y) apTs ps" by (simp add: list_all2_iff) from stk' l ps have "length ps < length stk" by simp moreover from wf x C have x: "G,hp \<turnstile> x ::\<preceq> Class C" by (rule conf_widen) hence "isRef x" by simp moreover { assume "x ≠ Null" with x obtain D fs where hp: "hp (the_Addr x) = Some (D,fs)" and D: "G \<turnstile> D \<preceq>C C" by - (drule non_npD, assumption, clarsimp) hence "hp (the_Addr x) ≠ None" (is ?P1) by simp moreover from wf mth hp D have "method (G, cname_of hp x) (mn, ps) ≠ None" (is ?P2) by (auto dest: subcls_widen_methd) moreover from aps have "list_all2 (conf G hp) aps (rev apTs)" by (simp add: list_all2_approx approx_stk_def approx_loc_def) hence "list_all2 (conf G hp) (rev aps) (rev (rev apTs))" by (simp only: list_all2_rev) hence "list_all2 (conf G hp) (rev aps) apTs" by simp with wf widen have "list_all2 (conf G hp) (rev aps) ps" (is ?P3) by - (rule list_all2_conf_widen) ultimately have "?P1 ∧ ?P2 ∧ ?P3" by blast } moreover note Invoke ultimately show ?thesis by simp next case Return with stk app phi meth frames show ?thesis apply clarsimp apply (drule conf_widen [OF wf], assumption) apply (clarsimp simp add: neq_Nil_conv isRef_def2) done qed auto hence "check G s" by (simp add: check_def meth pc) } ultimately have "check G s" by blast thus "exec_d G (Normal s) ≠ 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: "wt_jvm_prog G Phi ==> G,Phi \<turnstile>JVM s \<surd> ==> G \<turnstile> s \<midarrow>jvm-> t ==> G \<turnstile> (Normal s) \<midarrow>jvmd-> (Normal t)" apply (unfold exec_all_def) apply (erule rtrancl_induct) apply (simp add: exec_all_d_def) apply simp apply (fold exec_all_def) apply (frule BV_correct, assumption+) apply (drule no_type_error, assumption, drule no_type_error_commutes, simp) apply (simp add: exec_all_d_def) apply (rule rtrancl_trans, assumption) apply blast done lemma neq_TypeError_eq [simp]: "s ≠ TypeError = (∃s'. s = Normal s')" by (cases s, auto) theorem no_type_errors: "wt_jvm_prog G Phi ==> G,Phi \<turnstile>JVM s \<surd> ==> G \<turnstile> (Normal s) \<midarrow>jvmd-> t ==> t ≠ TypeError" apply (unfold exec_all_d_def) apply (erule rtrancl_induct) apply simp apply (fold exec_all_d_def) apply (auto dest: defensive_imp_aggressive BV_correct no_type_error) done corollary no_type_errors_initial: fixes G ("Γ") and Phi ("Φ") assumes wt: "wt_jvm_prog Γ Φ" assumes is_class: "is_class Γ C" and "method": "method (Γ,C) (m,[]) = Some (C, b)" and m: "m ≠ init" defines start: "s ≡ start_state Γ C m" assumes s: "Γ \<turnstile> (Normal s) \<midarrow>jvmd-> t" shows "t ≠ TypeError" proof - from wt is_class "method" have "Γ,Φ \<turnstile>JVM s \<surd>" unfolding start by (rule BV_correct_initial) from wt this s show ?thesis by (rule no_type_errors) 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 G ("Γ") and Phi ("Φ") assumes wt: "wt_jvm_prog Γ Φ" and *: "Γ,Φ \<turnstile>JVM s \<surd>" shows "Γ \<turnstile> (Normal s) \<midarrow>jvmd-> (Normal t) = Γ \<turnstile> s \<midarrow>jvm-> t" apply rule apply (erule defensive_imp_aggressive, rule welltyped_aggressive_imp_defensive) apply (rule wt) apply (rule *) apply assumption done corollary welltyped_initial_commutes: fixes G ("Γ") and Phi ("Φ") assumes wt: "wt_jvm_prog Γ Φ" assumes is_class: "is_class Γ C" and "method": "method (Γ,C) (m,[]) = Some (C, b)" and m: "m ≠ init" defines start: "s ≡ start_state Γ C m" shows "Γ \<turnstile> (Normal s) \<midarrow>jvmd-> (Normal t) = Γ \<turnstile> s \<midarrow>jvm-> t" proof - from wt is_class "method" have "Γ,Φ \<turnstile>JVM s \<surd>" unfolding start by (rule BV_correct_initial) with wt show ?thesis by (rule welltyped_commutes) qed end