Theory BVNoTypeError

theory BVNoTypeError
imports JVMDefensive BVSpecTypeSafe
(*  Title:      HOL/MicroJava/BV/BVNoTypeError.thy
Author: Gerwin Klein
*)


header {* \isaheader{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 (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)
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_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
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_def)
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_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.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) 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) (rule that)

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_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 \<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