Theory BVConform

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

The invariant for the type safety proof.
*)

header {* \isaheader{BV Type Safety Invariant} *}

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


consts
  confT :: "'c prog => heap => val => ty err => bool" 
           ("_,_ |- _ :<=T _" [51,51,51,51] 50)

syntax (xsymbols)
  confT :: "'c prog => heap => val => ty err => bool" 
           ("_,_ \<turnstile> _ :≤\<top> _" [51,51,51,51] 50)

defs confT_def:
  "P,h \<turnstile> v :≤\<top> E ≡ case E of Err => True | OK T => P,h \<turnstile> v :≤ T"

syntax
  confTs :: "'c prog => heap => val list => tyl => bool" 
            ("_,_ |- _ [:<=T] _" [51,51,51,51] 50)

abbreviation (xsymbols)
  confTs :: "'c prog => heap => val list => tyl => bool"
           ("_,_ \<turnstile> _ [:≤\<top>] _" [51,51,51,51] 50) where
  "P,h \<turnstile> vs [:≤\<top>] Ts ≡ list_all2 (confT P h) vs Ts"

constdefs
  conf_f  :: "jvm_prog => heap => tyi => bytecode => frame => bool"
  "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)


consts
 conf_fs :: "[jvm_prog,heap,tyP,mname,nat,ty,frame list] => bool"
primrec
"conf_fs P h Φ M0 n0 T0 [] = True"

"conf_fs P h Φ M0 n0 T0 (f#frs) =
  (let (stk,loc,C,M,pc) = f in
  (∃ST LT Ts T mxs mxl0 is xt.
    Φ C M ! pc = Some (ST,LT) ∧ 
    (P \<turnstile> C sees M:Ts -> T = (mxs,mxl0,is,xt) in C) ∧
    (∃D Ts' T' m D'.  
       is!pc = (Invoke M0 n0) ∧ ST!n0 = Class D ∧
       P \<turnstile> D sees M0:Ts' -> T' = m in D' ∧ P \<turnstile> T0 ≤ T') ∧
    conf_f P h (ST, LT) is f ∧ conf_fs P h Φ M (size Ts) T frs))"

primrec conf_xcp :: "jvm_prog => heap => addr option => instr => bool" where
  "conf_xcp P h None i = True"
| "conf_xcp P h ⌊a⌋ i = (∃D fs. h a = ⌊Obj D fs⌋ ∧ P \<turnstile> D \<preceq>* Throwable ∧ (∀D'. P \<turnstile> D \<preceq>* D' --> is_relevant_class i P D'))"

constdefs
 correct_state :: "[jvm_prog,tyP,jvm_state] => bool"
                  ("_,_ |- _ [ok]"  [61,0,0] 61)
"correct_state P Φ ≡ λ(xp,h,frs).
        case frs of
             [] => True
             | (f#fs) => P\<turnstile> h\<surd> ∧ 
             (let (stk,loc,C,M,pc) = f
              in ∃Ts T mxs mxl0 is xt τ.
                    (P \<turnstile> C sees M:Ts->T = (mxs,mxl0,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) )"

syntax (xsymbols)
 correct_state :: "[jvm_prog,tyP,jvm_state] => bool"
                  ("_,_ \<turnstile> _ \<surd>"  [61,0,0] 61)

lemma oconf_blank [intro, simp]:
    "[|is_class P C; wf_prog wt P|] ==> P,h \<turnstile> blank P C \<surd>"
  by (fastsimp simp add: blank_def has_fields_b_fields oconf_init_fields
               dest: wf_Fields_Ex)

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", standard]

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_f_hext:
  "[| conf_f P h Φ M f; hext 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:
  "!!M n Tr. 
  [| conf_fs P h Φ M n Tr frs; h \<unlhd> h' |] ==> conf_fs P h' Φ M n Tr 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