# Theory BVConform

```(*  Title:      JinjaDCI/BV/BVConform.thy

Author:     Cornelia Pusch, Gerwin Klein, Susannah Mansky
Copyright   1999 Technische Universitaet Muenchen, 2019-20 UIUC

Based on the Jinja theory BV/BVConform.thy by Cornelia Pusch and Gerwin Klein

The invariant for the type safety proof.
*)

section ‹ BV Type Safety Invariant ›

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

subsection ‹ @{text "correct_state"} definitions ›

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)

fun Called_context :: "jvm_prog ⇒ cname ⇒ instr ⇒ bool" where
"Called_context P C⇩0 (New C') = (C⇩0=C')" |
"Called_context P C⇩0 (Getstatic C F D) =  ((C⇩0=D) ∧ (∃t. P ⊢ C has F,Static:t in D))" |
"Called_context P C⇩0 (Putstatic C F D) = ((C⇩0=D) ∧ (∃t. P ⊢ C has F,Static:t in D))" |
"Called_context P C⇩0 (Invokestatic C M n)
= (∃Ts T m D. (C⇩0=D) ∧ P ⊢ C sees M,Static:Ts → T = m in D)" |
"Called_context P _ _ = False"

abbreviation Called_set :: "instr set" where
"Called_set ≡ {i. ∃C. i = New C} ∪ {i. ∃C M n. i = Invokestatic C M n}
∪ {i. ∃C F D. i = Getstatic C F D} ∪ {i. ∃C F D. i = Putstatic C F D}"

lemma Called_context_Called_set:
"Called_context P D i ⟹ i ∈ Called_set" by(cases i, auto)

fun valid_ics :: "jvm_prog ⇒ heap ⇒ sheap ⇒ cname × mname × pc × init_call_status ⇒ bool"
("_,_,_ ⊢⇩i _" [51,51,51,51] 50) where
"valid_ics P h sh (C,M,pc,Calling C' Cs)
= (let ins = instrs_of P C M in Called_context P (last (C'#Cs)) (ins!pc)
∧ is_class P C')" |
"valid_ics P h sh (C,M,pc,Throwing Cs a)
=(let ins = instrs_of P C M in ∃C1. Called_context P C1 (ins!pc)
∧ (∃obj. h a = Some obj))" |
"valid_ics P h sh (C,M,pc,Called Cs)
= (let ins = instrs_of P C M
in ∃C1 sobj. Called_context P C1 (ins!pc) ∧ sh C1 = Some sobj)" |
"valid_ics P _ _ _ = True"

definition conf_f  :: "jvm_prog ⇒ heap ⇒ sheap ⇒ ty⇩i ⇒ bytecode ⇒ frame ⇒ bool"
where
"conf_f P h sh ≡ λ(ST,LT) is (stk,loc,C,M,pc,ics).
P,h ⊢ stk [:≤] ST ∧ P,h ⊢ loc [:≤⇩⊤] LT ∧ pc < size is ∧ P,h,sh ⊢⇩i (C,M,pc,ics)"

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

primrec conf_fs :: "[jvm_prog,heap,sheap,ty⇩P,cname,mname,nat,ty,frame list] ⇒ bool"
where
"conf_fs P h sh Φ C⇩0 M⇩0 n⇩0 T⇩0 [] = True"
| "conf_fs P h sh Φ C⇩0 M⇩0 n⇩0 T⇩0 (f#frs) =
(let (stk,loc,C,M,pc,ics) = f in
(∃ST LT b Ts T mxs mxl⇩0 is xt.
Φ C M ! pc = Some (ST,LT) ∧
(P ⊢ C sees M,b:Ts → T = (mxs,mxl⇩0,is,xt) in C) ∧
((∃D Ts' T' m D'. M⇩0 ≠ clinit ∧ ics = No_ics ∧
is!pc = Invoke M⇩0 n⇩0 ∧ ST!n⇩0 = Class D ∧
P ⊢ D sees M⇩0,NonStatic:Ts' → T' = m in D' ∧ P ⊢ C⇩0 ≼⇧* D' ∧ P ⊢ T⇩0 ≤ T') ∨
(∃D Ts' T' m. M⇩0 ≠ clinit ∧ ics = No_ics ∧
is!pc = Invokestatic D M⇩0 n⇩0 ∧
P ⊢ D sees M⇩0,Static:Ts' → T' = m in C⇩0 ∧ P ⊢ T⇩0 ≤ T') ∨
(M⇩0 = clinit ∧ (∃Cs. ics = Called Cs))) ∧
conf_f P h sh (ST, LT) is f ∧ conf_fs P h sh Φ C M (size Ts) T frs))"

fun ics_classes :: "init_call_status ⇒ cname list" where
"ics_classes (Calling C Cs) = Cs" |
"ics_classes (Throwing Cs a) = Cs" |
"ics_classes (Called Cs) = Cs" |
"ics_classes _ = []"

fun frame_clinit_classes :: "frame ⇒ cname list" where
"frame_clinit_classes (stk,loc,C,M,pc,ics) = (if M=clinit then [C] else []) @ ics_classes ics"

abbreviation clinit_classes :: "frame list ⇒ cname list" where
"clinit_classes frs ≡ concat (map frame_clinit_classes frs)"

definition distinct_clinit :: "frame list ⇒ bool" where
"distinct_clinit frs ≡ distinct (clinit_classes frs)"

definition conf_clinit :: "jvm_prog ⇒ sheap ⇒ frame list ⇒ bool" where
"conf_clinit P sh frs
≡ distinct_clinit frs ∧
(∀C ∈ set(clinit_classes frs). is_class P C ∧ (∃sfs. sh C = Some(sfs, Processing)))"

(*************************)

definition correct_state :: "[jvm_prog,ty⇩P,jvm_state] ⇒ bool"  ("_,_ ⊢ _ √"  [61,0,0] 61)
where
"correct_state P Φ ≡ λ(xp,h,frs,sh).
case xp of
None ⇒ (case frs of
[] ⇒ True
| (f#fs) ⇒ P⊢ h√ ∧ P,h⊢⇩s sh√ ∧ conf_clinit P sh frs ∧
(let (stk,loc,C,M,pc,ics) = f
in ∃b Ts T mxs mxl⇩0 is xt τ.
(P ⊢ C sees M,b:Ts→T = (mxs,mxl⇩0,is,xt) in C) ∧
Φ C M ! pc = Some τ ∧
conf_f P h sh τ is f ∧ conf_fs P h sh Φ C M (size Ts) T fs))
| Some x ⇒ frs = []"

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

subsection ‹ Values and @{text "⊤"} ›

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:
assumes confTs: "P,h ⊢ loc [:≤⇩⊤] LT" and n: "n < size LT" and
LTn: "LT!n = OK T" and subtype: "P ⊢ T ≤ T'"
shows "P,h ⊢ (loc!n) :≤ T'"
(*<*)
proof -
have len: "n < length loc" using list_all2_lengthD[OF confTs] n
by simp
show ?thesis
using list_all2_nthD[OF confTs len] conf_widen[OF _ subtype] LTn
by simp
qed
(*>*)

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: list_all2_Cons2)

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

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

subsection ‹ valid @{text "init_call_status"} ›

lemma valid_ics_shupd:
assumes "P,h,sh ⊢⇩i (C, M, pc, ics)" and "distinct (C'#ics_classes ics)"
shows "P,h,sh(C' ↦ (sfs, i')) ⊢⇩i (C, M, pc, ics)"
using assms by(cases ics; clarsimp simp: fun_upd_apply) fastforce

subsection ‹ correct-frame ›

lemma conf_f_Throwing:
assumes "conf_f P h sh (ST, LT) is (stk, loc, C, M, pc, Called Cs)"
and "is_class P C'" and "h xcp = Some obj" and "sh C' = Some(sfs,Processing)"
shows "conf_f P h sh (ST, LT) is (stk, loc, C, M, pc, Throwing (C' # Cs) xcp)"
using assms by(auto simp: conf_f_def2)

lemma conf_f_shupd:
assumes "conf_f P h sh (ST,LT) ins f"
and "i = Processing
∨ (distinct (C#ics_classes (ics_of f)) ∧ (curr_method f = clinit ⟶ C ≠ curr_class f))"
shows "conf_f P h (sh(C ↦ (sfs, i))) (ST,LT) ins f"
using assms
by(cases f, cases "ics_of f"; clarsimp simp: conf_f_def2 fun_upd_apply) fastforce+

lemma conf_f_shupd':
assumes "conf_f P h sh (ST,LT) ins f"
and "sh C = Some(sfs,i)"
shows "conf_f P h (sh(C ↦ (sfs', i))) (ST,LT) ins f"
using assms
by(cases f, cases "ics_of f"; clarsimp simp: conf_f_def2 fun_upd_apply) fastforce+

subsection ‹ correct-frames ›

lemmas [simp del] = fun_upd_apply

lemma conf_fs_hext:
"⋀C M n T⇩r.
⟦ conf_fs P h sh Φ C M n T⇩r frs; h ⊴ h' ⟧ ⟹ conf_fs P h' sh Φ C M n T⇩r frs"
(*<*)
proof(induct frs)
case (Cons fr frs)
obtain stk ls C M pc ics where fr: "fr = (stk, ls, C, M, pc, ics)" by(cases fr) simp
moreover obtain ST LT where Φ: "Φ C M ! pc = ⌊(ST, LT)⌋" and
ST: "P,h ⊢ stk [:≤] ST" and LT: "P,h ⊢ ls [:≤⇩⊤] LT"
using Cons.prems(1) fr by(auto simp: conf_f_def)
ultimately show ?case using Cons confs_hext[OF ST Cons(3)] confTs_hext[OF LT Cons(3)]
by (fastforce simp: conf_f_def)
qed simp
(*>*)

lemma conf_fs_shupd:
assumes "conf_fs P h sh Φ C⇩0 M n T frs"
and dist: "distinct (C#clinit_classes frs)"
shows "conf_fs P h (sh(C ↦ (sfs, i))) Φ C⇩0 M n T frs"
using assms proof(induct frs arbitrary: C⇩0 C M n T)
case (Cons f' frs')
then obtain stk' loc' C' M' pc' ics' where f': "f' = (stk',loc',C',M',pc',ics')" by(cases f')
with assms Cons obtain ST LT b Ts T1 mxs mxl⇩0 ins xt where
ty: "Φ C' M' ! pc' = Some (ST,LT)" and
meth: "P ⊢ C' sees M',b:Ts → T1 = (mxs,mxl⇩0,ins,xt) in C'" and
conf: "conf_f P h sh (ST, LT) ins f'" and
confs: "conf_fs P h sh Φ C' M' (size Ts) T1 frs'" by clarsimp

from f' Cons.prems(2) have
"distinct (C#ics_classes (ics_of f')) ∧ (curr_method f' = clinit ⟶ C ≠ curr_class f')"
by fastforce
with conf_f_shupd[where C=C, OF conf] have
conf': "conf_f P h (sh(C ↦ (sfs, i))) (ST, LT) ins f'" by simp

from Cons.prems(2) have dist': "distinct (C # clinit_classes frs')"
by(auto simp: distinct_length_2_or_more)
from Cons.hyps[OF confs dist'] have
confs': "conf_fs P h (sh(C ↦ (sfs, i))) Φ C' M' (length Ts) T1 frs'" by simp

from conf' confs' ty meth f' Cons.prems show ?case by(fastforce dest: sees_method_fun)
qed(simp)

lemma conf_fs_shupd':
assumes "conf_fs P h sh Φ C⇩0 M n T frs"
and shC: "sh C = Some(sfs,i)"
shows "conf_fs P h (sh(C ↦ (sfs', i))) Φ C⇩0 M n T frs"
using assms proof(induct frs arbitrary: C⇩0 C M n T sfs i sfs')
case (Cons f' frs')
then obtain stk' loc' C' M' pc' ics' where f': "f' = (stk',loc',C',M',pc',ics')" by(cases f')
with assms Cons obtain ST LT b Ts T1 mxs mxl⇩0 ins xt where
ty: "Φ C' M' ! pc' = Some (ST,LT)" and
meth: "P ⊢ C' sees M',b:Ts → T1 = (mxs,mxl⇩0,ins,xt) in C'" and
conf: "conf_f P h sh (ST, LT) ins f'" and
confs: "conf_fs P h sh Φ C' M' (size Ts) T1 frs'" and
shC': "sh C = Some(sfs,i)" by clarsimp

have conf': "conf_f P h (sh(C ↦ (sfs', i))) (ST, LT) ins f'" by(rule conf_f_shupd'[OF conf shC'])

from Cons.hyps[OF confs shC'] have
confs': "conf_fs P h (sh(C ↦ (sfs', i))) Φ C' M' (length Ts) T1 frs'" by simp

from conf' confs' ty meth f' Cons.prems show ?case by(fastforce dest: sees_method_fun)
qed(simp)

subsection ‹ correctness wrt @{term clinit} use ›

lemma conf_clinit_Cons:
assumes "conf_clinit P sh (f#frs)"
shows "conf_clinit P sh frs"
proof -
from assms have dist: "distinct_clinit (f#frs)"
by(cases "curr_method f = clinit", auto simp: conf_clinit_def)
then have dist': "distinct_clinit frs" by(simp add: distinct_clinit_def)

with assms show ?thesis by(cases frs; fastforce simp: conf_clinit_def)
qed

lemma conf_clinit_Cons_Cons:
"conf_clinit P sh (f'#f#frs) ⟹ conf_clinit P sh (f'#frs)"
by(auto simp: conf_clinit_def distinct_clinit_def)

lemma conf_clinit_diff:
assumes "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)"
shows "conf_clinit P sh ((stk',loc',C,M,pc',ics)#frs)"
using assms by(cases "M = clinit", simp_all add: conf_clinit_def distinct_clinit_def)

lemma conf_clinit_diff':
assumes "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)"
shows "conf_clinit P sh ((stk',loc',C,M,pc',No_ics)#frs)"
using assms by(cases "M = clinit", simp_all add: conf_clinit_def distinct_clinit_def)

lemma conf_clinit_Called_Throwing:
"conf_clinit P sh ((stk', loc', C', clinit, pc', ics') # (stk, loc, C, M, pc, Called Cs) # fs)
⟹ conf_clinit P sh ((stk, loc, C, M, pc, Throwing (C' # Cs) xcp) # fs)"

lemma conf_clinit_Throwing:
"conf_clinit P sh ((stk, loc, C, M, pc, Throwing (C'#Cs) xcp) # fs)
⟹ conf_clinit P sh ((stk, loc, C, M, pc, Throwing Cs xcp) # fs)"

lemma conf_clinit_Called:
"⟦ conf_clinit P sh ((stk, loc, C, M, pc, Called (C'#Cs)) # frs);
P ⊢ C' sees clinit,Static: [] → Void=(mxs',mxl',ins',xt') in C' ⟧
⟹ conf_clinit P sh (create_init_frame P C' # (stk, loc, C, M, pc, Called Cs) # frs)"

lemma conf_clinit_Cons_nclinit:
assumes "conf_clinit P sh frs" and nclinit: "M ≠ clinit"
shows "conf_clinit P sh ((stk, loc, C, M, pc, No_ics) # frs)"
proof -
from nclinit
have "clinit_classes ((stk, loc, C, M, pc, No_ics) # frs) = clinit_classes frs" by simp
with assms show ?thesis by(simp add: conf_clinit_def distinct_clinit_def)
qed

lemma conf_clinit_Invoke:
assumes "conf_clinit P sh ((stk, loc, C, M, pc, ics) # frs)" and "M' ≠ clinit"
shows "conf_clinit P sh ((stk', loc', C', M', pc', No_ics) # (stk, loc, C, M, pc, No_ics) # frs)"
using assms conf_clinit_Cons_nclinit conf_clinit_diff' by auto

lemma conf_clinit_nProc_dist:
assumes "conf_clinit P sh frs"
and "∀sfs. sh C ≠ Some(sfs,Processing)"
shows "distinct (C # clinit_classes frs)"
using assms by(auto simp: conf_clinit_def distinct_clinit_def)

lemma conf_clinit_shupd:
assumes "conf_clinit P sh frs"
and dist: "distinct (C#clinit_classes frs)"
shows "conf_clinit P (sh(C ↦ (sfs, i))) frs"
using assms by(simp add: conf_clinit_def fun_upd_apply)

lemma conf_clinit_shupd':
assumes "conf_clinit P sh frs"
and "sh C = Some(sfs,i)"
shows "conf_clinit P (sh(C ↦ (sfs', i))) frs"
using assms by(fastforce simp: conf_clinit_def fun_upd_apply)

lemma conf_clinit_shupd_Called:
assumes "conf_clinit P sh ((stk,loc,C,M,pc,Calling C' Cs)#frs)"
and dist: "distinct (C'#clinit_classes ((stk,loc,C,M,pc,Calling C' Cs)#frs))"
and cls: "is_class P C'"
shows "conf_clinit P (sh(C' ↦ (sfs, Processing))) ((stk,loc,C,M,pc,Called (C'#Cs))#frs)"
using assms by(clarsimp simp: conf_clinit_def fun_upd_apply distinct_clinit_def)

lemma conf_clinit_shupd_Calling:
assumes "conf_clinit P sh ((stk,loc,C,M,pc,Calling C' Cs)#frs)"
and dist: "distinct (C'#clinit_classes ((stk,loc,C,M,pc,Calling C' Cs)#frs))"
and cls: "is_class P C'"
shows "conf_clinit P (sh(C' ↦ (sfs, Processing)))
((stk,loc,C,M,pc,Calling (fst(the(class P C'))) (C'#Cs))#frs)"
using assms by(clarsimp simp: conf_clinit_def fun_upd_apply distinct_clinit_def)

subsection ‹ correct state ›

lemma correct_state_Cons:
assumes cr: "P,Φ |- (xp,h,f#frs,sh) [ok]"
shows "P,Φ |- (xp,h,frs,sh) [ok]"
proof -
from cr have dist: "conf_clinit P sh (f#frs)"
then have "conf_clinit P sh frs" by(rule conf_clinit_Cons)

with cr show ?thesis by(cases frs; fastforce simp: correct_state_def)
qed

lemma correct_state_shupd:
assumes cs: "P,Φ |- (xp,h,frs,sh) [ok]" and shC: "sh C = Some(sfs,i)"
and dist: "distinct (C#clinit_classes frs)"
shows "P,Φ |- (xp,h,frs,sh(C ↦ (sfs, i'))) [ok]"
using assms
proof(cases xp)
case None with assms show ?thesis
proof(cases frs)
case (Cons f' frs')
let ?sh = "sh(C ↦ (sfs, i'))"

obtain stk' loc' C' M' pc' ics' where f': "f' = (stk',loc',C',M',pc',ics')" by(cases f')
with cs Cons None obtain b Ts T mxs mxl⇩0 ins xt ST LT where
meth: "P ⊢ C' sees M',b:Ts→T = (mxs,mxl⇩0,ins,xt) in C'"
and ty: "Φ C' M' ! pc' = Some (ST,LT)" and conf: "conf_f P h sh (ST,LT) ins f'"
and confs: "conf_fs P h sh Φ C' M' (size Ts) T frs'"
and confc: "conf_clinit P sh frs"
and h_ok: "P⊢ h√" and sh_ok: "P,h ⊢⇩s sh √"
by(auto simp: correct_state_def)

from Cons dist have dist': "distinct (C#clinit_classes frs')"
by(auto simp: distinct_length_2_or_more)

from shconf_upd_obj[OF sh_ok shconfD[OF sh_ok shC]] have sh_ok': "P,h ⊢⇩s ?sh √"
by simp

from conf f' valid_ics_shupd Cons dist have conf': "conf_f P h ?sh (ST,LT) ins f'"
by(auto simp: conf_f_def2 fun_upd_apply)
have confs': "conf_fs P h ?sh Φ C' M' (size Ts) T frs'" by(rule conf_fs_shupd[OF confs dist'])

have confc': "conf_clinit P ?sh frs" by(rule conf_clinit_shupd[OF confc dist])

with h_ok sh_ok' meth ty conf' confs' f' Cons None show ?thesis
by(fastforce simp: correct_state_def)

lemma correct_state_Throwing_ex:
assumes correct: "P,Φ ⊢ (xp,h,(stk,loc,C,M,pc,ics)#frs,sh)√"
shows "⋀Cs a. ics = Throwing Cs a ⟹ ∃obj. h a = Some obj"
using correct by(clarsimp simp: correct_state_def conf_f_def)

end
```