header {* \isaheader{BV Type Safety Invariant} *}
theory BVConform
imports BVSpec "../JVM/JVMExec" "../Common/Conform"
begin
definition confT :: "'c prog => heap => val => ty err => bool"
("_,_ |- _ :<=T _" [51,51,51,51] 50)
where
"P,h |- v :<=T E ≡ case E of Err => True | OK T => P,h \<turnstile> v :≤ T"
notation (xsymbols)
confT ("_,_ \<turnstile> _ :≤⇩\<top> _" [51,51,51,51] 50)
abbreviation
confTs :: "'c prog => heap => val list => ty⇣l => bool"
("_,_ |- _ [:<=T] _" [51,51,51,51] 50) where
"P,h |- vs [:<=T] Ts ≡ list_all2 (confT P h) vs Ts"
notation (xsymbols)
confTs ("_,_ \<turnstile> _ [:≤⇩\<top>] _" [51,51,51,51] 50)
definition conf_f :: "jvm_prog => heap => ty⇣i => bytecode => frame => bool"
where
"conf_f P h ≡ λ(ST,LT) is (stk,loc,C,M,pc).
P,h \<turnstile> stk [:≤] ST ∧ P,h \<turnstile> loc [:≤⇩\<top>] LT ∧ pc < size is"
lemma conf_f_def2:
"conf_f P h (ST,LT) is (stk,loc,C,M,pc) ≡
P,h \<turnstile> stk [:≤] ST ∧ P,h \<turnstile> loc [:≤⇩\<top>] LT ∧ pc < size is"
by (simp add: conf_f_def)
primrec conf_fs :: "[jvm_prog,heap,ty⇣P,mname,nat,ty,frame list] => bool"
where
"conf_fs P h Φ M⇣0 n⇣0 T⇣0 [] = True"
| "conf_fs P h Φ M⇣0 n⇣0 T⇣0 (f#frs) =
(let (stk,loc,C,M,pc) = f in
(∃ST LT Ts T mxs mxl⇣0 is xt.
Φ C M ! pc = Some (ST,LT) ∧
(P \<turnstile> C sees M:Ts -> T = (mxs,mxl⇣0,is,xt) in C) ∧
(∃D Ts' T' m D'.
is!pc = (Invoke M⇣0 n⇣0) ∧ ST!n⇣0 = Class D ∧
P \<turnstile> D sees M⇣0:Ts' -> T' = m in D' ∧ P \<turnstile> T⇣0 ≤ T') ∧
conf_f P h (ST, LT) is f ∧ conf_fs P h Φ M (size Ts) T frs))"
definition correct_state :: "[jvm_prog,ty⇣P,jvm_state] => bool"
("_,_ |- _ [ok]" [61,0,0] 61)
where
"correct_state P Φ ≡ λ(xp,h,frs).
case xp of
None => (case frs of
[] => True
| (f#fs) => P\<turnstile> h\<surd> ∧
(let (stk,loc,C,M,pc) = f
in ∃Ts T mxs mxl⇣0 is xt τ.
(P \<turnstile> C sees M:Ts->T = (mxs,mxl⇣0,is,xt) in C) ∧
Φ C M ! pc = Some τ ∧
conf_f P h τ is f ∧ conf_fs P h Φ M (size Ts) T fs))
| Some x => frs = []"
notation (xsymbols)
correct_state ("_,_ \<turnstile> _ \<surd>" [61,0,0] 61)
section {* Values and @{text "\<top>"} *}
lemma confT_Err [iff]: "P,h \<turnstile> x :≤⇩\<top> Err"
by (simp add: confT_def)
lemma confT_OK [iff]: "P,h \<turnstile> x :≤⇩\<top> OK T = (P,h \<turnstile> x :≤ T)"
by (simp add: confT_def)
lemma confT_cases:
"P,h \<turnstile> x :≤⇩\<top> X = (X = Err ∨ (∃T. X = OK T ∧ P,h \<turnstile> x :≤ T))"
by (cases X) auto
lemma confT_hext [intro?, trans]:
"[| P,h \<turnstile> x :≤⇩\<top> T; h \<unlhd> h' |] ==> P,h' \<turnstile> x :≤⇩\<top> T"
by (cases T) (blast intro: conf_hext)+
lemma confT_widen [intro?, trans]:
"[| P,h \<turnstile> x :≤⇩\<top> T; P \<turnstile> T ≤⇩\<top> T' |] ==> P,h \<turnstile> x :≤⇩\<top> T'"
by (cases T', auto intro: conf_widen)
section {* Stack and Registers *}
lemmas confTs_Cons1 [iff] = list_all2_Cons1 [of "confT P h"] for P h
lemma confTs_confT_sup:
"[| P,h \<turnstile> loc [:≤⇩\<top>] LT; n < size LT; LT!n = OK T; P \<turnstile> T ≤ T' |]
==> P,h \<turnstile> (loc!n) :≤ T'"
apply (frule list_all2_lengthD)
apply (drule list_all2_nthD, simp)
apply simp
apply (erule conf_widen, assumption+)
done
lemma confTs_hext [intro?]:
"P,h \<turnstile> loc [:≤⇩\<top>] LT ==> h \<unlhd> h' ==> P,h' \<turnstile> loc [:≤⇩\<top>] LT"
by (fast elim: list_all2_mono confT_hext)
lemma confTs_widen [intro?, trans]:
"P,h \<turnstile> loc [:≤⇩\<top>] LT ==> P \<turnstile> LT [≤⇩\<top>] LT' ==> P,h \<turnstile> loc [:≤⇩\<top>] LT'"
by (rule list_all2_trans, rule confT_widen)
lemma confTs_map [iff]:
"!!vs. (P,h \<turnstile> vs [:≤⇩\<top>] map OK Ts) = (P,h \<turnstile> vs [:≤] Ts)"
by (induct Ts) (auto simp add: list_all2_Cons2)
lemma reg_widen_Err [iff]:
"!!LT. (P \<turnstile> replicate n Err [≤⇩\<top>] LT) = (LT = replicate n Err)"
by (induct n) (auto simp add: list_all2_Cons1)
lemma confTs_Err [iff]:
"P,h \<turnstile> replicate n v [:≤⇩\<top>] replicate n Err"
by (induct n) auto
section {* correct-frames *}
lemmas [simp del] = fun_upd_apply
lemma conf_fs_hext:
"!!M n T⇣r.
[| conf_fs P h Φ M n T⇣r frs; h \<unlhd> h' |] ==> conf_fs P h' Φ M n T⇣r frs"
apply (induct frs)
apply simp
apply clarify
apply (simp (no_asm_use))
apply clarify
apply (unfold conf_f_def)
apply (simp (no_asm_use))
apply clarify
apply (fast elim!: confs_hext confTs_hext)
done
end