Up to index of Isabelle/HOL/MicroJava
theory BVNoTypeError(* Title: HOL/MicroJava/BV/BVNoTypeErrors.thy ID: $Id: BVNoTypeError.thy,v 1.8 2005/06/17 14:13:08 haftmann Exp $ Author: Gerwin Klein *) header {* \isaheader{Welltyped Programs produce no Type Errors} *} theory BVNoTypeError imports 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 (case_tac prim_ty) apply auto apply (case_tac prim_ty) apply auto apply (case_tac list) apply auto apply (case_tac a) apply auto apply (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, 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: min_def list_all2_def) 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 add: min_def) ultimately show ?thesis .. qed obtain apTs where "ST = (rev apTs) @ ys" and "length apTs = length fpTs" proof - have "ST = rev (rev xs) @ ys" by simp with xs show ?thesis by - (rule that, assumption, simp) 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_def min_def) apply ((rule exI)+, (rule 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_def) 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.elims) apply auto apply (cases v) apply auto done lemma list_all2_approx: "!!s. list_all2 (approx_val G hp) s (map OK S) = list_all2 (conf G hp) s S" apply (induct 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) fast 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 (fastsimp intro: wf_prog_ws_prog 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∈set (zip apTs ps). x ∈ widen G" 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_def) 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, blast) 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 -jvm-> t ==> G \<turnstile> (Normal s) -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) -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_jvm_prog Γ Φ" assumes "is_class Γ C" "method (Γ,C) (m,[]) = Some (C, b)" "m ≠ init" defines start: "s ≡ start_state Γ C m" assumes "Γ \<turnstile> (Normal s) -jvmd-> t" shows "t ≠ TypeError" proof - have "Γ,Φ \<turnstile>JVM s \<surd>" by (unfold start, rule BV_correct_initial) thus ?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_jvm_prog Γ Φ" and "Γ,Φ \<turnstile>JVM s \<surd>" shows "Γ \<turnstile> (Normal s) -jvmd-> (Normal t) = Γ \<turnstile> s -jvm-> t" by rule (erule defensive_imp_aggressive,rule welltyped_aggressive_imp_defensive) corollary welltyped_initial_commutes: fixes G ("Γ") and Phi ("Φ") assumes "wt_jvm_prog Γ Φ" assumes "is_class Γ C" "method (Γ,C) (m,[]) = Some (C, b)" "m ≠ init" defines start: "s ≡ start_state Γ C m" shows "Γ \<turnstile> (Normal s) -jvmd-> (Normal t) = Γ \<turnstile> s -jvm-> t" proof - have "Γ,Φ \<turnstile>JVM s \<surd>" by (unfold start, rule BV_correct_initial) thus ?thesis by - (rule welltyped_commutes) qed end
lemma typeof_NoneD:
typeof empty v = Some x ==> ¬ isAddr v
lemma isRef_def2:
isRef v = (v = Null ∨ (∃loc. v = Addr loc))
lemma app'Store:
app' (Store idx, G, pc, maxs, rT, ST, LT) = (∃T ST'. ST = T # ST' ∧ idx < length LT)
lemma app'GetField:
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 |- oT <= Class C)
lemma app'PutField:
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 |- oT <= Class C ∧ G |- vT <= vT')
lemma app'Checkcast:
app' (Checkcast C, G, pc, maxs, rT, ST, LT) = (∃rT ST'. ST = RefT rT # ST' ∧ is_class G C)
lemma app'Pop:
app' (Pop, G, pc, maxs, rT, ST, LT) = (∃T ST'. ST = T # ST')
lemma app'Dup:
app' (Dup, G, pc, maxs, rT, ST, LT) = (∃T ST'. ST = T # ST' ∧ length ST < maxs)
lemma app'Dup_x1:
app' (Dup_x1, G, pc, maxs, rT, ST, LT) = (∃T1 T2 ST'. ST = T1 # T2 # ST' ∧ length ST < maxs)
lemma app'Dup_x2:
app' (Dup_x2, G, pc, maxs, rT, ST, LT) = (∃T1 T2 T3 ST'. ST = T1 # T2 # T3 # ST' ∧ length ST < maxs)
lemma app'Swap:
app' (Swap, G, pc, maxs, rT, ST, LT) = (∃T1 T2 ST'. ST = T1 # T2 # ST')
lemma app'IAdd:
app' (IAdd, G, pc, maxs, rT, ST, LT) = (∃ST'. ST = PrimT Integer # PrimT Integer # ST')
lemma app'Ifcmpeq:
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')))
lemma app'Return:
app' (Return, G, pc, maxs, rT, ST, LT) = (∃T ST'. ST = T # ST' ∧ G |- T <= rT)
lemma app'Throw:
app' (Throw, G, pc, maxs, rT, ST, LT) = (∃ST' r. ST = RefT r # ST')
lemma app'Invoke:
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 |- aT <= fT) ∧ method (G, C) (mn, fpTs) = Some (mD', rT', b') ∧ G |- X <= Class C)
lemma approx_loc_len:
approx_loc G hp loc LT ==> length loc = length LT
lemma approx_stk_len:
approx_stk G hp stk ST ==> length stk = length ST
lemma isRefI:
G,hp |- v ::<= RefT T ==> isRef v
lemma isIntgI:
G,hp |- v ::<= PrimT Integer ==> isIntg v
lemma list_all2_approx:
list_all2 (approx_val G hp) s (map OK S) = list_all2 (conf G hp) s S
lemma list_all2_conf_widen:
[| wf_prog mb G; list_all2 (conf G hp) a b; list_all2 (%x y. G |- x <= y) b c |] ==> list_all2 (conf G hp) a c
theorem no_type_error:
[| wt_jvm_prog G Phi; G,Phi |-JVM s [ok] |] ==> exec_d G (Normal s) ≠ TypeError
theorem welltyped_aggressive_imp_defensive:
[| wt_jvm_prog G Phi; G,Phi |-JVM s [ok]; G |- s -jvm-> t |] ==> G |- Normal s -jvmd-> Normal t
lemma neq_TypeError_eq:
(s ≠ TypeError) = (∃s'. s = Normal s')
theorem no_type_errors:
[| wt_jvm_prog G Phi; G,Phi |-JVM s [ok]; G |- Normal s -jvmd-> t |] ==> t ≠ TypeError
corollary no_type_errors_initial:
[| wt_jvm_prog G Phi; is_class G C; method (G, C) (m, []) = Some (C, b); m ≠ init; G |- Normal (start_state G C m) -jvmd-> t |] ==> t ≠ TypeError
corollary welltyped_commutes:
[| wt_jvm_prog G Phi; G,Phi |-JVM s [ok] |] ==> G |- Normal s -jvmd-> Normal t = G |- s -jvm-> t
corollary welltyped_initial_commutes:
[| wt_jvm_prog G Phi; is_class G C; method (G, C) (m, []) = Some (C, b); m ≠ init |] ==> G |- Normal (start_state G C m) -jvmd-> Normal t = G |- start_state G C m -jvm-> t