Theory Correct

(*  Title:      HOL/MicroJava/BV/Correct.thy
    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

section ‹BV Type Safety Invariant›

theory Correct
imports BVSpec "../JVM/JVMExec"
begin

definition approx_val :: "[jvm_prog,aheap,val,ty err] ⇒ bool" where
  "approx_val G h v any == case any of Err ⇒ True | OK T ⇒ G,h⊢v::≼T"

definition approx_loc :: "[jvm_prog,aheap,val list,locvars_type] ⇒ bool" where
  "approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"

definition approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] ⇒ bool" where
  "approx_stk G hp stk ST == approx_loc G hp stk (map OK ST)"

definition correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] ⇒ frame ⇒ bool" where
  "correct_frame G hp == λ(ST,LT) maxl ins (stk,loc,C,sig,pc).
                         approx_stk G hp stk ST  ∧ approx_loc G hp loc LT ∧ 
                         pc < length ins ∧ length loc=length(snd sig)+maxl+1"

primrec correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] ⇒ bool" where
  "correct_frames G hp phi rT0 sig0 [] = True"
| "correct_frames G hp phi rT0 sig0 (f#frs) =
    (let (stk,loc,C,sig,pc) = f in
    (∃ST LT rT maxs maxl ins et.
      phi C sig ! pc = Some (ST,LT) ∧ is_class G C ∧ 
      method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) ∧
    (∃C' mn pTs. ins!pc = (Invoke C' mn pTs) ∧ 
           (mn,pTs) = sig0 ∧ 
           (∃apTs D ST' LT'.
           (phi C sig)!pc = Some ((rev apTs) @ (Class D) # ST', LT') ∧
           length apTs = length pTs ∧
           (∃D' rT' maxs' maxl' ins' et'.
             method (G,D) sig0 = Some(D',rT',(maxs',maxl',ins',et')) ∧
             G ⊢ rT0 ≼ rT') ∧
     correct_frame G hp (ST, LT) maxl ins f ∧ 
     correct_frames G hp phi rT sig frs))))"

definition correct_state :: "[jvm_prog,prog_type,jvm_state] ⇒ bool"
                  ("_,_ ⊢JVM _ √"  [51,51] 50) where
"correct_state G phi == λ(xp,hp,frs).
   case xp of
     None ⇒ (case frs of
             [] ⇒ True
             | (f#fs) ⇒ G⊢h hp√ ∧ preallocated hp ∧ 
      (let (stk,loc,C,sig,pc) = f
             in
                         ∃rT maxs maxl ins et s.
                         is_class G C ∧
                         method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) ∧
                         phi C sig ! pc = Some s ∧
       correct_frame G hp s maxl ins f ∧ 
             correct_frames G hp phi rT sig fs))
   | Some x ⇒ frs = []" 


lemma sup_ty_opt_OK:
  "(G ⊢ X <=o (OK T')) = (∃T. X = OK T ∧ G ⊢ T ≼ T')"
  by (cases X) auto


subsection ‹approx-val›

lemma approx_val_Err [simp,intro!]:
  "approx_val G hp x Err"
  by (simp add: approx_val_def)

lemma approx_val_OK [iff]: 
  "approx_val G hp x (OK T) = (G,hp ⊢ x ::≼ T)"
  by (simp add: approx_val_def)

lemma approx_val_Null [simp,intro!]:
  "approx_val G hp Null (OK (RefT x))"
  by (auto simp add: approx_val_def)

lemma approx_val_sup_heap:
  "⟦ approx_val G hp v T; hp ≤| hp' ⟧ ⟹ approx_val G hp' v T"
  by (cases T) (blast intro: conf_hext)+

lemma approx_val_heap_update:
  "⟦ hp a = Some obj'; G,hp⊢ v::≼T; obj_ty obj = obj_ty obj'⟧ 
  ⟹ G,hp(a↦obj)⊢ v::≼T"
  by (cases v) (auto simp add: obj_ty_def conf_def)

lemma approx_val_widen:
  "⟦ approx_val G hp v T; G ⊢ T <=o T'; wf_prog wt G ⟧
  ⟹ approx_val G hp v T'"
  by (cases T') (auto simp add: sup_ty_opt_OK intro: conf_widen)

subsection ‹approx-loc›

lemma approx_loc_Nil [simp,intro!]:
  "approx_loc G hp [] []"
  by (simp add: approx_loc_def)

lemma approx_loc_Cons [iff]:
  "approx_loc G hp (l#ls) (L#LT) = 
  (approx_val G hp l L ∧ approx_loc G hp ls LT)"
by (simp add: approx_loc_def)

lemma approx_loc_nth:
  "⟦ approx_loc G hp loc LT; n < length LT ⟧
  ⟹ approx_val G hp (loc!n) (LT!n)"
  by (simp add: approx_loc_def list_all2_conv_all_nth)

lemma approx_loc_imp_approx_val_sup:
  "⟦approx_loc G hp loc LT; n < length LT; LT ! n = OK T; G ⊢ T ≼ T'; wf_prog wt G⟧ 
  ⟹ G,hp ⊢ (loc!n) ::≼ T'"
  apply (drule approx_loc_nth, assumption) 
  apply simp
  apply (erule conf_widen, assumption+)
  done

lemma approx_loc_conv_all_nth:
  "approx_loc G hp loc LT = 
  (length loc = length LT ∧ (∀n < length loc. approx_val G hp (loc!n) (LT!n)))"
  by (simp add: approx_loc_def list_all2_conv_all_nth)

lemma approx_loc_sup_heap:
  "⟦ approx_loc G hp loc LT; hp ≤| hp' ⟧
  ⟹ approx_loc G hp' loc LT"
  apply (clarsimp simp add: approx_loc_conv_all_nth)
  apply (blast intro: approx_val_sup_heap)
  done

lemma approx_loc_widen:
  "⟦ approx_loc G hp loc LT; G ⊢ LT <=l LT'; wf_prog wt G ⟧
  ⟹ approx_loc G hp loc LT'"
apply (unfold Listn.le_def lesub_def sup_loc_def)
apply (simp (no_asm_use) only: list_all2_conv_all_nth approx_loc_conv_all_nth)
apply (simp (no_asm_simp))
apply clarify
apply (erule allE, erule impE) 
 apply simp
apply (erule approx_val_widen)
 apply simp
apply assumption
done

lemma loc_widen_Err [dest]:
  "⋀XT. G ⊢ replicate n Err <=l XT ⟹ XT = replicate n Err"
  by (induct n) auto
  
lemma approx_loc_Err [iff]:
  "approx_loc G hp (replicate n v) (replicate n Err)"
  by (induct n) auto

lemma approx_loc_subst:
  "⟦ approx_loc G hp loc LT; approx_val G hp x X ⟧
  ⟹ approx_loc G hp (loc[idx:=x]) (LT[idx:=X])"
apply (unfold approx_loc_def list_all2_iff)
apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
done

lemma approx_loc_append:
  "length l1=length L1 ⟹
  approx_loc G hp (l1@l2) (L1@L2) = 
  (approx_loc G hp l1 L1 ∧ approx_loc G hp l2 L2)"
  apply (unfold approx_loc_def list_all2_iff)
  apply (simp cong: conj_cong)
  apply blast
  done

subsection ‹approx-stk›

lemma approx_stk_rev_lem:
  "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
  apply (unfold approx_stk_def approx_loc_def)
  apply (simp add: rev_map [symmetric])
  done

lemma approx_stk_rev:
  "approx_stk G hp (rev s) t = approx_stk G hp s (rev t)"
  by (auto intro: subst [OF approx_stk_rev_lem])

lemma approx_stk_sup_heap:
  "⟦ approx_stk G hp stk ST; hp ≤| hp' ⟧ ⟹ approx_stk G hp' stk ST"
  by (auto intro: approx_loc_sup_heap simp add: approx_stk_def)

lemma approx_stk_widen:
  "⟦ approx_stk G hp stk ST; G ⊢ map OK ST <=l map OK ST'; wf_prog wt G ⟧
  ⟹ approx_stk G hp stk ST'" 
  by (auto elim: approx_loc_widen simp add: approx_stk_def)

lemma approx_stk_Nil [iff]:
  "approx_stk G hp [] []"
  by (simp add: approx_stk_def)

lemma approx_stk_Cons [iff]:
  "approx_stk G hp (x#stk) (S#ST) = 
  (approx_val G hp x (OK S) ∧ approx_stk G hp stk ST)"
  by (simp add: approx_stk_def)

lemma approx_stk_Cons_lemma [iff]:
  "approx_stk G hp stk (S#ST') = 
  (∃s stk'. stk = s#stk' ∧ approx_val G hp s (OK S) ∧ approx_stk G hp stk' ST')"
  by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def)

lemma approx_stk_append:
  "approx_stk G hp stk (S@S') ⟹
  (∃s stk'. stk = s@stk' ∧ length s = length S ∧ length stk' = length S' ∧ 
            approx_stk G hp s S ∧ approx_stk G hp stk' S')"
  by (simp add: list_all2_append2 approx_stk_def approx_loc_def)

lemma approx_stk_all_widen:
  "⟦ approx_stk G hp stk ST; ∀(x, y) ∈ set (zip ST ST'). G ⊢ x ≼ y; length ST = length ST'; wf_prog wt G ⟧ 
  ⟹ approx_stk G hp stk ST'"
apply (unfold approx_stk_def)
apply (clarsimp simp add: approx_loc_conv_all_nth all_set_conv_all_nth)
apply (erule allE, erule impE, assumption)
apply (erule allE, erule impE, assumption)
apply (erule conf_widen, assumption+)
done

subsection ‹oconf›

lemma oconf_field_update:
  "⟦map_of (fields (G, oT)) FD = Some T; G,hp⊢v::≼T; G,hp⊢(oT,fs)√ ⟧
  ⟹ G,hp⊢(oT, fs(FD↦v))√"
  by (simp add: oconf_def lconf_def)

lemma oconf_newref:
  "⟦hp oref = None; G,hp ⊢ obj √; G,hp ⊢ obj' √⟧ ⟹ G,hp(oref↦obj') ⊢ obj √"
  apply (unfold oconf_def lconf_def)
  apply simp
  apply (blast intro: conf_hext hext_new)
  done

lemma oconf_heap_update:
  "⟦ hp a = Some obj'; obj_ty obj' = obj_ty obj''; G,hp⊢obj√ ⟧
  ⟹ G,hp(a↦obj'')⊢obj√"
  apply (unfold oconf_def lconf_def)
  apply (fastforce intro: approx_val_heap_update)
  done

subsection ‹hconf›

lemma hconf_newref:
  "⟦ hp oref = None; G⊢h hp√; G,hp⊢obj√ ⟧ ⟹ G⊢h hp(oref↦obj)√"
  apply (simp add: hconf_def)
  apply (fast intro: oconf_newref)
  done

lemma hconf_field_update:
  "⟦ map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs); 
     G,hp⊢v::≼T; G⊢h hp√ ⟧ 
  ⟹ G⊢h hp(a ↦ (oT, fs(X↦v)))√"
  apply (simp add: hconf_def)
  apply (fastforce intro: oconf_heap_update oconf_field_update 
                  simp add: obj_ty_def)
  done

subsection ‹preallocated›

lemma preallocated_field_update:
  "⟦ map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs); 
     G⊢h hp√; preallocated hp ⟧ 
  ⟹ preallocated (hp(a ↦ (oT, fs(X↦v))))"
  apply (unfold preallocated_def)
  apply (rule allI)
  apply (erule_tac x=x in allE)
  apply simp
  apply (rule ccontr)  
  apply (unfold hconf_def)
  apply (erule allE, erule allE, erule impE, assumption)
  apply (unfold oconf_def lconf_def)
  apply (simp del: split_paired_All)
  done  


lemma 
  assumes none: "hp oref = None" and alloc: "preallocated hp"
  shows preallocated_newref: "preallocated (hp(oref↦obj))"
proof (cases oref)
  case (XcptRef x) 
  with none alloc have False by (auto elim: preallocatedE [of _ x])
  thus ?thesis ..
next
  case (Loc l)
  with alloc show ?thesis by (simp add: preallocated_def)
qed
  
subsection ‹correct-frames›

lemmas [simp del] = fun_upd_apply

lemma correct_frames_field_update [rule_format]:
  "∀rT C sig. 
  correct_frames G hp phi rT sig frs ⟶ 
  hp a = Some (C,fs) ⟶ 
  map_of (fields (G, C)) fl = Some fd ⟶ 
  G,hp⊢v::≼fd 
  ⟶ correct_frames G (hp(a ↦ (C, fs(fl↦v)))) phi rT sig frs"
apply (induct frs)
 apply simp
apply clarify
apply (simp (no_asm_use))
apply clarify
apply (unfold correct_frame_def)
apply (simp (no_asm_use))
apply clarify
apply (intro exI conjI)
    apply assumption+
   apply (erule approx_stk_sup_heap)
   apply (erule hext_upd_obj)
  apply (erule approx_loc_sup_heap)
  apply (erule hext_upd_obj)
 apply assumption+
apply blast
done

lemma correct_frames_newref [rule_format]:
  "∀rT C sig. 
  hp x = None ⟶ 
  correct_frames G hp phi rT sig frs ⟶
  correct_frames G (hp(x ↦ obj)) phi rT sig frs"
apply (induct frs)
 apply simp
apply clarify
apply (simp (no_asm_use))
apply clarify
apply (unfold correct_frame_def)
apply (simp (no_asm_use))
apply clarify
apply (intro exI conjI)
    apply assumption+
   apply (erule approx_stk_sup_heap)
   apply (erule hext_new)
  apply (erule approx_loc_sup_heap)
  apply (erule hext_new)
 apply assumption+
apply blast
done

end