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  tyl  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  tyi  '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,tyP,mname,nat,ty,'addr frame list]  bool"
where
  "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  C sees M:Ts  T = (mxs,mxl0,is,xt) in C) 
    (Ts' T' D m D'.  
       is!pc = (Invoke M0 n0)  class_type_of' (ST!n0) = D  P  D sees M0:Ts'  T' = m in D'  P  T0  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 :: "[tyP,'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 mxl0 is xt τ.
                    (P  C sees M:TsT = (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) ))"

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 Tr frs; h  h'   conf_fs P h' Φ M n Tr frs"
apply (induct frs arbitrary: M n Tr)
 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:TsT = 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