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