src/HOL/MicroJava/BV/Correct.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 55524 f41ef840f09d
child 58886 8a6cac7c7247
permissions -rw-r--r--
eliminated spurious semicolons;
     1 (*  Title:      HOL/MicroJava/BV/Correct.thy
     2     Author:     Cornelia Pusch, Gerwin Klein
     3     Copyright   1999 Technische Universitaet Muenchen
     4 *)
     5 
     6 header {* \isaheader{BV Type Safety Invariant} *}
     7 
     8 theory Correct
     9 imports BVSpec "../JVM/JVMExec"
    10 begin
    11 
    12 definition approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool" where
    13   "approx_val G h v any == case any of Err \<Rightarrow> True | OK T \<Rightarrow> G,h\<turnstile>v::\<preceq>T"
    14 
    15 definition approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \<Rightarrow> bool" where
    16   "approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
    17 
    18 definition approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \<Rightarrow> bool" where
    19   "approx_stk G hp stk ST == approx_loc G hp stk (map OK ST)"
    20 
    21 definition correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool" where
    22   "correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
    23                          approx_stk G hp stk ST  \<and> approx_loc G hp loc LT \<and> 
    24                          pc < length ins \<and> length loc=length(snd sig)+maxl+1"
    25 
    26 primrec correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \<Rightarrow> bool" where
    27   "correct_frames G hp phi rT0 sig0 [] = True"
    28 | "correct_frames G hp phi rT0 sig0 (f#frs) =
    29     (let (stk,loc,C,sig,pc) = f in
    30     (\<exists>ST LT rT maxs maxl ins et.
    31       phi C sig ! pc = Some (ST,LT) \<and> is_class G C \<and> 
    32       method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) \<and>
    33     (\<exists>C' mn pTs. ins!pc = (Invoke C' mn pTs) \<and> 
    34            (mn,pTs) = sig0 \<and> 
    35            (\<exists>apTs D ST' LT'.
    36            (phi C sig)!pc = Some ((rev apTs) @ (Class D) # ST', LT') \<and>
    37            length apTs = length pTs \<and>
    38            (\<exists>D' rT' maxs' maxl' ins' et'.
    39              method (G,D) sig0 = Some(D',rT',(maxs',maxl',ins',et')) \<and>
    40              G \<turnstile> rT0 \<preceq> rT') \<and>
    41      correct_frame G hp (ST, LT) maxl ins f \<and> 
    42      correct_frames G hp phi rT sig frs))))"
    43 
    44 definition correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
    45                   ("_,_ |-JVM _ [ok]"  [51,51] 50) where
    46 "correct_state G phi == \<lambda>(xp,hp,frs).
    47    case xp of
    48      None \<Rightarrow> (case frs of
    49              [] \<Rightarrow> True
    50              | (f#fs) \<Rightarrow> G\<turnstile>h hp\<surd> \<and> preallocated hp \<and> 
    51       (let (stk,loc,C,sig,pc) = f
    52              in
    53                          \<exists>rT maxs maxl ins et s.
    54                          is_class G C \<and>
    55                          method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) \<and>
    56                          phi C sig ! pc = Some s \<and>
    57        correct_frame G hp s maxl ins f \<and> 
    58              correct_frames G hp phi rT sig fs))
    59    | Some x \<Rightarrow> frs = []" 
    60 
    61 
    62 notation (xsymbols)
    63  correct_state  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
    64 
    65 
    66 lemma sup_ty_opt_OK:
    67   "(G \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')"
    68   by (cases X) auto
    69 
    70 
    71 section {* approx-val *}
    72 
    73 lemma approx_val_Err [simp,intro!]:
    74   "approx_val G hp x Err"
    75   by (simp add: approx_val_def)
    76 
    77 lemma approx_val_OK [iff]: 
    78   "approx_val G hp x (OK T) = (G,hp \<turnstile> x ::\<preceq> T)"
    79   by (simp add: approx_val_def)
    80 
    81 lemma approx_val_Null [simp,intro!]:
    82   "approx_val G hp Null (OK (RefT x))"
    83   by (auto simp add: approx_val_def)
    84 
    85 lemma approx_val_sup_heap:
    86   "\<lbrakk> approx_val G hp v T; hp \<le>| hp' \<rbrakk> \<Longrightarrow> approx_val G hp' v T"
    87   by (cases T) (blast intro: conf_hext)+
    88 
    89 lemma approx_val_heap_update:
    90   "\<lbrakk> hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk> 
    91   \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T"
    92   by (cases v) (auto simp add: obj_ty_def conf_def)
    93 
    94 lemma approx_val_widen:
    95   "\<lbrakk> approx_val G hp v T; G \<turnstile> T <=o T'; wf_prog wt G \<rbrakk>
    96   \<Longrightarrow> approx_val G hp v T'"
    97   by (cases T') (auto simp add: sup_ty_opt_OK intro: conf_widen)
    98 
    99 section {* approx-loc *}
   100 
   101 lemma approx_loc_Nil [simp,intro!]:
   102   "approx_loc G hp [] []"
   103   by (simp add: approx_loc_def)
   104 
   105 lemma approx_loc_Cons [iff]:
   106   "approx_loc G hp (l#ls) (L#LT) = 
   107   (approx_val G hp l L \<and> approx_loc G hp ls LT)"
   108 by (simp add: approx_loc_def)
   109 
   110 lemma approx_loc_nth:
   111   "\<lbrakk> approx_loc G hp loc LT; n < length LT \<rbrakk>
   112   \<Longrightarrow> approx_val G hp (loc!n) (LT!n)"
   113   by (simp add: approx_loc_def list_all2_conv_all_nth)
   114 
   115 lemma approx_loc_imp_approx_val_sup:
   116   "\<lbrakk>approx_loc G hp loc LT; n < length LT; LT ! n = OK T; G \<turnstile> T \<preceq> T'; wf_prog wt G\<rbrakk> 
   117   \<Longrightarrow> G,hp \<turnstile> (loc!n) ::\<preceq> T'"
   118   apply (drule approx_loc_nth, assumption) 
   119   apply simp
   120   apply (erule conf_widen, assumption+)
   121   done
   122 
   123 lemma approx_loc_conv_all_nth:
   124   "approx_loc G hp loc LT = 
   125   (length loc = length LT \<and> (\<forall>n < length loc. approx_val G hp (loc!n) (LT!n)))"
   126   by (simp add: approx_loc_def list_all2_conv_all_nth)
   127 
   128 lemma approx_loc_sup_heap:
   129   "\<lbrakk> approx_loc G hp loc LT; hp \<le>| hp' \<rbrakk>
   130   \<Longrightarrow> approx_loc G hp' loc LT"
   131   apply (clarsimp simp add: approx_loc_conv_all_nth)
   132   apply (blast intro: approx_val_sup_heap)
   133   done
   134 
   135 lemma approx_loc_widen:
   136   "\<lbrakk> approx_loc G hp loc LT; G \<turnstile> LT <=l LT'; wf_prog wt G \<rbrakk>
   137   \<Longrightarrow> approx_loc G hp loc LT'"
   138 apply (unfold Listn.le_def lesub_def sup_loc_def)
   139 apply (simp (no_asm_use) only: list_all2_conv_all_nth approx_loc_conv_all_nth)
   140 apply (simp (no_asm_simp))
   141 apply clarify
   142 apply (erule allE, erule impE) 
   143  apply simp
   144 apply (erule approx_val_widen)
   145  apply simp
   146 apply assumption
   147 done
   148 
   149 lemma loc_widen_Err [dest]:
   150   "\<And>XT. G \<turnstile> replicate n Err <=l XT \<Longrightarrow> XT = replicate n Err"
   151   by (induct n) auto
   152   
   153 lemma approx_loc_Err [iff]:
   154   "approx_loc G hp (replicate n v) (replicate n Err)"
   155   by (induct n) auto
   156 
   157 lemma approx_loc_subst:
   158   "\<lbrakk> approx_loc G hp loc LT; approx_val G hp x X \<rbrakk>
   159   \<Longrightarrow> approx_loc G hp (loc[idx:=x]) (LT[idx:=X])"
   160 apply (unfold approx_loc_def list_all2_iff)
   161 apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
   162 done
   163 
   164 lemma approx_loc_append:
   165   "length l1=length L1 \<Longrightarrow>
   166   approx_loc G hp (l1@l2) (L1@L2) = 
   167   (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
   168   apply (unfold approx_loc_def list_all2_iff)
   169   apply (simp cong: conj_cong)
   170   apply blast
   171   done
   172 
   173 section {* approx-stk *}
   174 
   175 lemma approx_stk_rev_lem:
   176   "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
   177   apply (unfold approx_stk_def approx_loc_def)
   178   apply (simp add: rev_map [THEN sym])
   179   done
   180 
   181 lemma approx_stk_rev:
   182   "approx_stk G hp (rev s) t = approx_stk G hp s (rev t)"
   183   by (auto intro: subst [OF approx_stk_rev_lem])
   184 
   185 lemma approx_stk_sup_heap:
   186   "\<lbrakk> approx_stk G hp stk ST; hp \<le>| hp' \<rbrakk> \<Longrightarrow> approx_stk G hp' stk ST"
   187   by (auto intro: approx_loc_sup_heap simp add: approx_stk_def)
   188 
   189 lemma approx_stk_widen:
   190   "\<lbrakk> approx_stk G hp stk ST; G \<turnstile> map OK ST <=l map OK ST'; wf_prog wt G \<rbrakk>
   191   \<Longrightarrow> approx_stk G hp stk ST'" 
   192   by (auto elim: approx_loc_widen simp add: approx_stk_def)
   193 
   194 lemma approx_stk_Nil [iff]:
   195   "approx_stk G hp [] []"
   196   by (simp add: approx_stk_def)
   197 
   198 lemma approx_stk_Cons [iff]:
   199   "approx_stk G hp (x#stk) (S#ST) = 
   200   (approx_val G hp x (OK S) \<and> approx_stk G hp stk ST)"
   201   by (simp add: approx_stk_def)
   202 
   203 lemma approx_stk_Cons_lemma [iff]:
   204   "approx_stk G hp stk (S#ST') = 
   205   (\<exists>s stk'. stk = s#stk' \<and> approx_val G hp s (OK S) \<and> approx_stk G hp stk' ST')"
   206   by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def)
   207 
   208 lemma approx_stk_append:
   209   "approx_stk G hp stk (S@S') \<Longrightarrow>
   210   (\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length S' \<and> 
   211             approx_stk G hp s S \<and> approx_stk G hp stk' S')"
   212   by (simp add: list_all2_append2 approx_stk_def approx_loc_def)
   213 
   214 lemma approx_stk_all_widen:
   215   "\<lbrakk> approx_stk G hp stk ST; \<forall>(x, y) \<in> set (zip ST ST'). G \<turnstile> x \<preceq> y; length ST = length ST'; wf_prog wt G \<rbrakk> 
   216   \<Longrightarrow> approx_stk G hp stk ST'"
   217 apply (unfold approx_stk_def)
   218 apply (clarsimp simp add: approx_loc_conv_all_nth all_set_conv_all_nth)
   219 apply (erule allE, erule impE, assumption)
   220 apply (erule allE, erule impE, assumption)
   221 apply (erule conf_widen, assumption+)
   222 done
   223 
   224 section {* oconf *}
   225 
   226 lemma oconf_field_update:
   227   "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
   228   \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
   229   by (simp add: oconf_def lconf_def)
   230 
   231 lemma oconf_newref:
   232   "\<lbrakk>hp oref = None; G,hp \<turnstile> obj \<surd>; G,hp \<turnstile> obj' \<surd>\<rbrakk> \<Longrightarrow> G,hp(oref\<mapsto>obj') \<turnstile> obj \<surd>"
   233   apply (unfold oconf_def lconf_def)
   234   apply simp
   235   apply (blast intro: conf_hext hext_new)
   236   done
   237 
   238 lemma oconf_heap_update:
   239   "\<lbrakk> hp a = Some obj'; obj_ty obj' = obj_ty obj''; G,hp\<turnstile>obj\<surd> \<rbrakk>
   240   \<Longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
   241   apply (unfold oconf_def lconf_def)
   242   apply (fastforce intro: approx_val_heap_update)
   243   done
   244 
   245 section {* hconf *}
   246 
   247 lemma hconf_newref:
   248   "\<lbrakk> hp oref = None; G\<turnstile>h hp\<surd>; G,hp\<turnstile>obj\<surd> \<rbrakk> \<Longrightarrow> G\<turnstile>h hp(oref\<mapsto>obj)\<surd>"
   249   apply (simp add: hconf_def)
   250   apply (fast intro: oconf_newref)
   251   done
   252 
   253 lemma hconf_field_update:
   254   "\<lbrakk> map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs); 
   255      G,hp\<turnstile>v::\<preceq>T; G\<turnstile>h hp\<surd> \<rbrakk> 
   256   \<Longrightarrow> G\<turnstile>h hp(a \<mapsto> (oT, fs(X\<mapsto>v)))\<surd>"
   257   apply (simp add: hconf_def)
   258   apply (fastforce intro: oconf_heap_update oconf_field_update 
   259                   simp add: obj_ty_def)
   260   done
   261 
   262 section {* preallocated *}
   263 
   264 lemma preallocated_field_update:
   265   "\<lbrakk> map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs); 
   266      G\<turnstile>h hp\<surd>; preallocated hp \<rbrakk> 
   267   \<Longrightarrow> preallocated (hp(a \<mapsto> (oT, fs(X\<mapsto>v))))"
   268   apply (unfold preallocated_def)
   269   apply (rule allI)
   270   apply (erule_tac x=x in allE)
   271   apply simp
   272   apply (rule ccontr)  
   273   apply (unfold hconf_def)
   274   apply (erule allE, erule allE, erule impE, assumption)
   275   apply (unfold oconf_def lconf_def)
   276   apply (simp del: split_paired_All)
   277   done  
   278 
   279 
   280 lemma 
   281   assumes none: "hp oref = None" and alloc: "preallocated hp"
   282   shows preallocated_newref: "preallocated (hp(oref\<mapsto>obj))"
   283 proof (cases oref)
   284   case (XcptRef x) 
   285   with none alloc have False by (auto elim: preallocatedE [of _ x])
   286   thus ?thesis ..
   287 next
   288   case (Loc l)
   289   with alloc show ?thesis by (simp add: preallocated_def)
   290 qed
   291   
   292 section {* correct-frames *}
   293 
   294 lemmas [simp del] = fun_upd_apply
   295 
   296 lemma correct_frames_field_update [rule_format]:
   297   "\<forall>rT C sig. 
   298   correct_frames G hp phi rT sig frs \<longrightarrow> 
   299   hp a = Some (C,fs) \<longrightarrow> 
   300   map_of (fields (G, C)) fl = Some fd \<longrightarrow> 
   301   G,hp\<turnstile>v::\<preceq>fd 
   302   \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs"
   303 apply (induct frs)
   304  apply simp
   305 apply clarify
   306 apply (simp (no_asm_use))
   307 apply clarify
   308 apply (unfold correct_frame_def)
   309 apply (simp (no_asm_use))
   310 apply clarify
   311 apply (intro exI conjI)
   312     apply assumption+
   313    apply (erule approx_stk_sup_heap)
   314    apply (erule hext_upd_obj)
   315   apply (erule approx_loc_sup_heap)
   316   apply (erule hext_upd_obj)
   317  apply assumption+
   318 apply blast
   319 done
   320 
   321 lemma correct_frames_newref [rule_format]:
   322   "\<forall>rT C sig. 
   323   hp x = None \<longrightarrow> 
   324   correct_frames G hp phi rT sig frs \<longrightarrow>
   325   correct_frames G (hp(x \<mapsto> obj)) phi rT sig frs"
   326 apply (induct frs)
   327  apply simp
   328 apply clarify
   329 apply (simp (no_asm_use))
   330 apply clarify
   331 apply (unfold correct_frame_def)
   332 apply (simp (no_asm_use))
   333 apply clarify
   334 apply (intro exI conjI)
   335     apply assumption+
   336    apply (erule approx_stk_sup_heap)
   337    apply (erule hext_new)
   338   apply (erule approx_loc_sup_heap)
   339   apply (erule hext_new)
   340  apply assumption+
   341 apply blast
   342 done
   343 
   344 end