Quelle  BVConform.thy

(*  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 :≤_\<top> 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 [:≤_\<top>] 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₀ (New C') = (C₀=C')" |
"Called_context P C₀ (Getstatic C F D) = ((C₀=D) ∧ (∃t. P ⊨ C has F,Static:t in D))" |
"Called_context P C₀ (Putstatic C F D) = ((C₀=D) ∧ (∃t. P ⊨ C has F,Static:t in D))" |
"Called_context P C₀ (Invokestatic C M n)
   = (∃Ts T m D. (C₀=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 [:≤_\<top>] 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 [:≤_\<top>] LT ∧ pc < size is ∧ P,h,sh ⊨_i (C,M,pc,ics)"
  by (simp add: conf_f_def)

primrec conf_fs :: "[jvm_prog,heap,sheap,ty_P,cname,mname,nat,ty,frame list] ==> bool"
where
  "conf_fs P h sh Φ C₀ M₀ n₀ T₀ [] = True"
| "conf_fs P h sh Φ C₀ M₀ n₀ T₀ (f#frs) =
  (let (stk,loc,C,M,pc,ics) = f in
  (∃ST LT b Ts T mxs mxl₀ is xt.
    Φ C M ! pc = Some (ST,LT) ∧
    (P ⊨ C sees M,b:Ts → T = (mxs,mxl₀,is,xt) in C) ∧
    ((∃D Ts' T' m D'. M₀ ≠ clinit ∧ ics = No_ics ∧
       is!pc = Invoke M₀ n₀ ∧ ST!n₀ = Class D ∧
       P ⊨ D sees M₀,NonStatic:Ts' → T' = m in D' ∧ P ⊨ C₀ ⪯^* D' ∧ P ⊨ T₀ ≤ T') ∨
     (∃D Ts' T' m. M₀ ≠ clinit ∧ ics = No_ics ∧
       is!pc = Invokestatic D M₀ n₀ ∧
       P ⊨ D sees M₀,Static:Ts' → T' = m in C₀ ∧ P ⊨ T₀ ≤ T') ∨
     (M₀ = 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₀ is xt τ.
                    (P ⊨ C sees M,b:Ts→T = (mxs,mxl₀,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 :≤_\<top> Err" 
  by (simp add: confT_def)

lemma confT_OK [iff]:  "P,h ⊨ x :≤_\<top> OK T = (P,h ⊨ x :≤ T)"
  by (simp add: confT_def)

lemma confT_cases:
  "P,h ⊨ x :≤_\<top> X = (X = Err ∨ (∃T. X = OK T ∧ P,h ⊨ x :≤ T))"
  by (cases X) auto

lemma confT_hext [intro?, trans]:
  "[ P,h ⊨ x :≤_\<top> T; h ⊴ h' ] ==> P,h' ⊨ x :≤_\<top> T"
  by (cases T) (blast intro: conf_hext)+

lemma confT_widen [intro?, trans]:
  "[ P,h ⊨ x :≤_\<top> T; P ⊨ T ≤_\<top> T' ] ==> P,h ⊨ x :≤_\<top> 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 [:≤_\<top>] 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 [:≤_\<top>] LT ==> h ⊴ h' ==> P,h' ⊨ loc [:≤_\<top>] LT"
  by (fast elim: list_all2_mono confT_hext)    

lemma confTs_widen [intro?, trans]:
  "P,h ⊨ loc [:≤_\<top>] LT ==> P ⊨ LT [≤_\<top>] LT' ==> P,h ⊨ loc [:≤_\<top>] LT'"
  by (rule list_all2_trans, rule confT_widen)

lemma confTs_map [iff]:
  "∧vs. (P,h ⊨ vs [:≤_\<top>] 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 [≤_\<top>] LT) = (LT = replicate n Err)"
  by (induct n) (auto simp: list_all2_Cons1)
    
lemma confTs_Err [iff]:
  "P,h ⊨ replicate n v [:≤_\<top>] 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 [:≤_\<top>] 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₀ M n T frs"
 and dist: "distinct (C#clinit_classes frs)"
shows "conf_fs P h (sh(C ↦ (sfs, i))) Φ C₀ M n T frs"
using assms proof(induct frs arbitrary: C₀ 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₀ ins xt where
    ty: "Φ C' M' ! pc' = Some (ST,LT)" and
    meth: "P ⊨ C' sees M',b:Ts → T1 = (mxs,mxl₀,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₀ M n T frs"
 and shC: "sh C = Some(sfs,i)"
shows "conf_fs P h (sh(C ↦ (sfs', i))) Φ C₀ M n T frs"
using assms proof(induct frs arbitrary: C₀ 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₀ ins xt where
    ty: "Φ C' M' ! pc' = Some (ST,LT)" and
    meth: "P ⊨ C' sees M',b:Ts → T1 = (mxs,mxl₀,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)"
 by(simp add: conf_clinit_def distinct_clinit_def)

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

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

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)"
   by(simp add: correct_state_def)
  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₀ ins xt ST LT where
         meth: "P ⊨ C' sees M',b:Ts→T = (mxs,mxl₀,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)
  qed(simp add: correct_state_def)
qed(simp add: 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