# Theory BVConform

```(*  Title:      HOL/MicroJava/BV/Correct.thy

Author:     Cornelia Pusch, Gerwin Klein

The invariant for the type safety proof.
*)

section ‹BV Type Safety Invariant›

theory BVConform
imports BVSpec "../JVM/JVMExec" "../Common/Conform"
begin

definition confT :: "'c prog ⇒ heap ⇒ val ⇒ ty err ⇒ bool"
("_,_ ⊢ _ :≤⇩⊤ _" [51,51,51,51] 50)
where
"P,h ⊢ v :≤⇩⊤ E ≡ case E of Err ⇒ True | OK T ⇒ P,h ⊢ v :≤ T"

notation (ASCII)
confT  ("_,_ |- _ :<=T _" [51,51,51,51] 50)

abbreviation
confTs :: "'c prog ⇒ heap ⇒ val list ⇒ ty⇩l ⇒ bool"
("_,_ ⊢ _ [:≤⇩⊤] _" [51,51,51,51] 50) where
"P,h ⊢ vs [:≤⇩⊤] Ts ≡ list_all2 (confT P h) vs Ts"

notation (ASCII)
confTs  ("_,_ |- _ [:<=T] _" [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 ⊢ stk [:≤] ST ∧ P,h ⊢ loc [:≤⇩⊤] LT ∧ pc < size is"

lemma conf_f_def2:
"conf_f P h (ST,LT) is (stk,loc,C,M,pc) ≡
P,h ⊢ stk [:≤] ST ∧ P,h ⊢ loc [:≤⇩⊤] LT ∧ pc < size is"

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 ⊢ 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 ⊢ D sees M⇩0:Ts' → T' = m in D' ∧ P ⊢ 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"  ("_,_ ⊢ _ √"  [61,0,0] 61)
where
"correct_state P Φ ≡ λ(xp,h,frs).
case xp of
None ⇒ (case frs of
[] ⇒ True
| (f#fs) ⇒ P⊢ h√ ∧
(let (stk,loc,C,M,pc) = f
in ∃Ts T mxs mxl⇩0 is xt τ.
(P ⊢ 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
correct_state  ("_,_ |- _ [ok]"  [61,0,0] 61)

subsection ‹Values and ‹⊤››

lemma confT_Err [iff]: "P,h ⊢ x :≤⇩⊤ Err"

lemma confT_OK [iff]:  "P,h ⊢ x :≤⇩⊤ OK T = (P,h ⊢ x :≤ T)"

lemma confT_cases:
"P,h ⊢ x :≤⇩⊤ X = (X = Err ∨ (∃T. X = OK T ∧ P,h ⊢ x :≤ T))"
by (cases X) auto

lemma confT_hext [intro?, trans]:
"⟦ P,h ⊢ x :≤⇩⊤ T; h ⊴ h' ⟧ ⟹ P,h' ⊢ x :≤⇩⊤ T"
by (cases T) (blast intro: conf_hext)+

lemma confT_widen [intro?, trans]:
"⟦ P,h ⊢ x :≤⇩⊤ T; P ⊢ T ≤⇩⊤ T' ⟧ ⟹ P,h ⊢ x :≤⇩⊤ T'"
by (cases T', auto intro: conf_widen)

subsection ‹Stack and Registers›

lemmas confTs_Cons1 [iff] = list_all2_Cons1 [of "confT P h"] for P h

lemma confTs_confT_sup:
"⟦ P,h ⊢ loc [:≤⇩⊤] LT; n < size LT; LT!n = OK T; P ⊢ T ≤ T' ⟧
⟹ P,h ⊢ (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 ⊢ loc [:≤⇩⊤] LT ⟹ h ⊴ h' ⟹ P,h' ⊢ loc [:≤⇩⊤] LT"
by (fast elim: list_all2_mono confT_hext)

lemma confTs_widen [intro?, trans]:
"P,h ⊢ loc [:≤⇩⊤] LT ⟹ P ⊢ LT [≤⇩⊤] LT' ⟹ P,h ⊢ loc [:≤⇩⊤] LT'"
by (rule list_all2_trans, rule confT_widen)

lemma confTs_map [iff]:
"⋀vs. (P,h ⊢ vs [:≤⇩⊤] map OK Ts) = (P,h ⊢ vs [:≤] Ts)"
by (induct Ts) (auto simp add: list_all2_Cons2)

lemma reg_widen_Err [iff]:
"⋀LT. (P ⊢ replicate n Err [≤⇩⊤] LT) = (LT = replicate n Err)"
by (induct n) (auto simp add: list_all2_Cons1)

lemma confTs_Err [iff]:
"P,h ⊢ replicate n v [:≤⇩⊤] replicate n Err"
by (induct n) auto

subsection ‹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 ⊴ 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
```