# Theory BVConform

```(*  Title:      JinjaThreads/BV/BVConform.thy
Author:     Cornelia Pusch, Gerwin Klein, Andreas Lochbihler

The invariant for the type safety proof.
*)

section ‹BV Type Safety Invariant›

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

context JVM_heap_base begin

definition confT :: "'c prog ⇒ 'heap ⇒ 'addr 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 ⇒ 'addr 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 :: "'addr jvm_prog ⇒ 'heap ⇒ ty⇩i ⇒ 'addr bytecode ⇒ 'addr 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"

primrec conf_fs :: "['addr jvm_prog,'heap,ty⇩P,mname,nat,ty,'addr 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) ∧
(∃Ts' T' D m D'.
is!pc = (Invoke M⇩0 n⇩0) ∧ class_type_of' (ST!n⇩0) = ⌊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))"

primrec conf_xcp :: "'addr jvm_prog ⇒ 'heap ⇒ 'addr option ⇒ 'addr instr ⇒ bool" where
"conf_xcp P h None i = True"
| "conf_xcp P h ⌊a⌋   i = (∃D. typeof_addr h a = ⌊Class_type D⌋ ∧ P ⊢ D ≼⇧* Throwable ∧
(∀D'. P ⊢ D ≼⇧* D' ⟶ is_relevant_class i P D'))"

end

context JVM_heap_conf_base begin

definition correct_state :: "[ty⇩P,'thread_id,('addr, 'heap) jvm_state] ⇒ bool"
where
"correct_state Φ t ≡ λ(xp,h,frs).
P,h ⊢ t √t ∧ hconf h ∧ preallocated h ∧
(case frs of
[] ⇒ True
| (f#fs) ⇒
(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 ∧
conf_xcp P h xp (is ! pc) ))"

notation
correct_state  ("_ ⊢ _:_ √"  [61,0,0] 61)

notation (ASCII)
correct_state  ("_ |- _:_ [ok]"  [61,0,0] 61)

end

context JVM_heap_base begin

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"
by (simp add: conf_f_def)

subsection ‹Values and ‹⊤››

lemma confT_Err [iff]: "P,h ⊢ x :≤⇩⊤ Err"
by (simp add: confT_def)

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

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

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

end

context JVM_heap begin

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

end

subsection ‹Stack and Registers›

context JVM_heap_base begin

lemma confTs_Cons1 [iff]:
"P,h ⊢ x # xs [:≤⇩⊤] Ts = (∃z zs. Ts = z # zs ∧ P,h ⊢ x :≤⇩⊤ z ∧ list_all2 (confT P h) xs zs)"
by(rule list_all2_Cons1)

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_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]:
"(P,h ⊢ vs [:≤⇩⊤] map OK Ts) = (P,h ⊢ vs [:≤] Ts)"
by (induct Ts arbitrary: vs) (auto simp add: list_all2_Cons2)

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

declare reg_widen_Err [iff]

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

end

context JVM_heap begin

lemma confTs_hext [intro?]:
"P,h ⊢ loc [:≤⇩⊤] LT ⟹ h ⊴ h' ⟹ P,h' ⊢ loc [:≤⇩⊤] LT"
by (fast elim: list_all2_mono confT_hext)

subsection ‹correct-frames›

declare fun_upd_apply[simp del]

lemma conf_f_hext:
"⟦ conf_f P h Φ M f; h ⊴ h' ⟧ ⟹ conf_f P h' Φ M f"
by(cases f, cases Φ, auto simp add: conf_f_def intro: confs_hext confTs_hext)

lemma conf_fs_hext:
"⟦ conf_fs P h Φ M n T⇩r frs; h ⊴ h' ⟧ ⟹ conf_fs P h' Φ M n T⇩r frs"
apply (induct frs arbitrary: M n T⇩r)
apply simp
apply clarify
apply (simp (no_asm_use))
apply clarify
apply (unfold conf_f_def)
apply (simp (no_asm_use) split: if_split_asm)
apply (fast elim!: confs_hext confTs_hext)+
done

declare fun_upd_apply[simp]

lemma conf_xcp_hext:
"⟦ conf_xcp P h xcp i; h ⊴ h' ⟧ ⟹ conf_xcp P h' xcp i"
by(cases xcp)(auto elim: typeof_addr_hext_mono)

end

context JVM_heap_conf_base begin

lemmas defs1 = correct_state_def conf_f_def wt_instr_def eff_def norm_eff_def app_def xcpt_app_def

lemma correct_state_impl_Some_method:
"Φ ⊢ t: (None, h, (stk,loc,C,M,pc)#frs)√
⟹ ∃m Ts T. P ⊢ C sees M:Ts→T = ⌊m⌋ in C"
by(fastforce simp add: defs1)

end

context JVM_heap_conf_base' begin

lemma correct_state_hext_mono:
"⟦ Φ ⊢ t: (xcp, h, frs) √; h ⊴ h'; hconf h' ⟧ ⟹ Φ ⊢ t: (xcp, h', frs) √"
unfolding correct_state_def
by(fastforce elim: tconf_hext_mono preallocated_hext conf_f_hext conf_fs_hext conf_xcp_hext split: list.split)

end

end
```