src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 23467 d1b97708d5eb
child 27680 5a557a5afc48
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/MicroJava/BV/BVSpecTypeSafe.thy
     2     ID:         $Id$
     3     Author:     Cornelia Pusch, Gerwin Klein
     4     Copyright   1999 Technische Universitaet Muenchen
     5 *)
     6 
     7 header {* \isaheader{BV Type Safety Proof}\label{sec:BVSpecTypeSafe} *}
     8 
     9 theory BVSpecTypeSafe imports Correct begin
    10 
    11 text {*
    12   This theory contains proof that the specification of the bytecode
    13   verifier only admits type safe programs.  
    14 *}
    15 
    16 section {* Preliminaries *}
    17 
    18 text {*
    19   Simp and intro setup for the type safety proof:
    20 *}
    21 lemmas defs1 = sup_state_conv correct_state_def correct_frame_def 
    22                wt_instr_def eff_def norm_eff_def 
    23 
    24 lemmas widen_rules[intro] = approx_val_widen approx_loc_widen approx_stk_widen
    25 
    26 lemmas [simp del] = split_paired_All
    27 
    28 
    29 text {*
    30   If we have a welltyped program and a conforming state, we
    31   can directly infer that the current instruction is well typed:
    32 *}
    33 lemma wt_jvm_prog_impl_wt_instr_cor:
    34   "\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
    35       G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
    36   \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
    37 apply (unfold correct_state_def Let_def correct_frame_def)
    38 apply simp
    39 apply (blast intro: wt_jvm_prog_impl_wt_instr)
    40 done
    41 
    42 
    43 section {* Exception Handling *}
    44 
    45 text {*
    46   Exceptions don't touch anything except the stack:
    47 *}
    48 lemma exec_instr_xcpt:
    49   "(fst (exec_instr i G hp stk vars Cl sig pc frs) = Some xcp)
    50   = (\<exists>stk'. exec_instr i G hp stk vars Cl sig pc frs = 
    51             (Some xcp, hp, (stk', vars, Cl, sig, pc)#frs))"
    52   by (cases i, auto simp add: split_beta split: split_if_asm)
    53 
    54 
    55 text {*
    56   Relates @{text match_any} from the Bytecode Verifier with 
    57   @{text match_exception_table} from the operational semantics:
    58 *}
    59 lemma in_match_any:
    60   "match_exception_table G xcpt pc et = Some pc' \<Longrightarrow> 
    61   \<exists>C. C \<in> set (match_any G pc et) \<and> G \<turnstile> xcpt \<preceq>C C \<and> 
    62       match_exception_table G C pc et = Some pc'"
    63   (is "PROP ?P et" is "?match et \<Longrightarrow> ?match_any et")
    64 proof (induct et)  
    65   show "PROP ?P []" 
    66     by simp
    67 
    68   fix e es
    69   assume IH: "PROP ?P es"
    70   assume match: "?match (e#es)"
    71 
    72   obtain start_pc end_pc handler_pc catch_type where
    73     e [simp]: "e = (start_pc, end_pc, handler_pc, catch_type)"
    74     by (cases e) 
    75 
    76   from IH match
    77   show "?match_any (e#es)" 
    78   proof (cases "match_exception_entry G xcpt pc e")
    79     case False
    80     with match
    81     have "match_exception_table G xcpt pc es = Some pc'" by simp
    82     with IH
    83     obtain C where
    84       set: "C \<in> set (match_any G pc es)" and
    85       C:   "G \<turnstile> xcpt \<preceq>C C" and
    86       m:   "match_exception_table G C pc es = Some pc'" by blast
    87 
    88     from set
    89     have "C \<in> set (match_any G pc (e#es))" by simp
    90     moreover
    91     from False C
    92     have "\<not> match_exception_entry G C pc e"
    93       by - (erule contrapos_nn, 
    94             auto simp add: match_exception_entry_def)
    95     with m
    96     have "match_exception_table G C pc (e#es) = Some pc'" by simp
    97     moreover note C
    98     ultimately
    99     show ?thesis by blast
   100   next
   101     case True with match
   102     have "match_exception_entry G catch_type pc e"
   103       by (simp add: match_exception_entry_def)
   104     moreover
   105     from True match
   106     obtain 
   107       "start_pc \<le> pc" 
   108       "pc < end_pc" 
   109       "G \<turnstile> xcpt \<preceq>C catch_type" 
   110       "handler_pc = pc'" 
   111       by (simp add: match_exception_entry_def)
   112     ultimately
   113     show ?thesis by auto
   114   qed
   115 qed
   116 
   117 lemma match_et_imp_match:
   118   "match_exception_table G (Xcpt X) pc et = Some handler
   119   \<Longrightarrow> match G X pc et = [Xcpt X]"
   120   apply (simp add: match_some_entry)
   121   apply (induct et)
   122   apply (auto split: split_if_asm)
   123   done
   124 
   125 text {*
   126   We can prove separately that the recursive search for exception
   127   handlers (@{text find_handler}) in the frame stack results in 
   128   a conforming state (if there was no matching exception handler 
   129   in the current frame). We require that the exception is a valid
   130   heap address, and that the state before the exception occured
   131   conforms. 
   132 *}
   133 lemma uncaught_xcpt_correct:
   134   "\<And>f. \<lbrakk> wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T;
   135       G,phi \<turnstile>JVM (None, hp, f#frs)\<surd> \<rbrakk>
   136   \<Longrightarrow> G,phi \<turnstile>JVM (find_handler G (Some xcp) hp frs)\<surd>" 
   137   (is "\<And>f. \<lbrakk> ?wt; ?adr; ?hp; ?correct (None, hp, f#frs) \<rbrakk> \<Longrightarrow> ?correct (?find frs)")
   138 proof (induct frs) 
   139   -- "the base case is trivial, as it should be"
   140   show "?correct (?find [])" by (simp add: correct_state_def)
   141 
   142   -- "we will need both forms @{text wt_jvm_prog} and @{text wf_prog} later"
   143   assume wt: ?wt 
   144   then obtain mb where wf: "wf_prog mb G" by (simp add: wt_jvm_prog_def)
   145 
   146   -- "these two don't change in the induction:"
   147   assume adr: ?adr
   148   assume hp: ?hp
   149   
   150   -- "the assumption for the cons case:"
   151   fix f f' frs' 
   152   assume cr: "?correct (None, hp, f#f'#frs')" 
   153 
   154   -- "the induction hypothesis as produced by Isabelle, immediatly simplified
   155     with the fixed assumptions above"
   156   assume "\<And>f. \<lbrakk> ?wt; ?adr; ?hp; ?correct (None, hp, f#frs') \<rbrakk> \<Longrightarrow> ?correct (?find frs')"  
   157   with wt adr hp 
   158   have IH: "\<And>f. ?correct (None, hp, f#frs') \<Longrightarrow> ?correct (?find frs')" by blast
   159 
   160   from cr
   161   have cr': "?correct (None, hp, f'#frs')" by (auto simp add: correct_state_def)
   162     
   163   obtain stk loc C sig pc where f' [simp]: "f' = (stk,loc,C,sig,pc)"
   164     by (cases f') 
   165 
   166   from cr 
   167   obtain rT maxs maxl ins et where
   168     meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
   169     by (simp add: correct_state_def, blast)
   170 
   171   hence [simp]: "ex_table_of (snd (snd (the (method (G, C) sig)))) = et"
   172     by simp
   173 
   174   show "?correct (?find (f'#frs'))" 
   175   proof (cases "match_exception_table G (cname_of hp xcp) pc et")
   176     case None
   177     with cr' IH 
   178     show ?thesis by simp
   179   next
   180     fix handler_pc 
   181     assume match: "match_exception_table G (cname_of hp xcp) pc et = Some handler_pc"
   182     (is "?match (cname_of hp xcp) = _")
   183 
   184     from wt meth cr' [simplified]
   185     have wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc" 
   186       by (rule wt_jvm_prog_impl_wt_instr_cor)
   187 
   188     from cr meth
   189     obtain C' mn pts ST LT where
   190       ins: "ins!pc = Invoke C' mn pts" (is "_ = ?i") and
   191       phi: "phi C sig ! pc = Some (ST, LT)"
   192       by (simp add: correct_state_def) blast    
   193 
   194     from match
   195     obtain D where
   196       in_any: "D \<in> set (match_any G pc et)" and
   197       D:      "G \<turnstile> cname_of hp xcp \<preceq>C D" and
   198       match': "?match D = Some handler_pc"
   199       by (blast dest: in_match_any)
   200 
   201     from ins wti phi have 
   202       "\<forall>D\<in>set (match_any G pc et). the (?match D) < length ins \<and> 
   203       G \<turnstile> Some ([Class D], LT) <=' phi C sig!the (?match D)"
   204       by (simp add: wt_instr_def eff_def xcpt_eff_def)      
   205     with in_any match' obtain
   206       pc: "handler_pc < length ins" 
   207       "G \<turnstile> Some ([Class D], LT) <=' phi C sig ! handler_pc"
   208       by auto
   209     then obtain ST' LT' where
   210       phi': "phi C sig ! handler_pc = Some (ST',LT')" and
   211       less: "G \<turnstile> ([Class D], LT) <=s (ST',LT')"
   212       by auto    
   213     
   214     from cr' phi meth f'
   215     have "correct_frame G hp (ST, LT) maxl ins f'"
   216       by (unfold correct_state_def) auto
   217     then obtain
   218      len: "length loc = 1+length (snd sig)+maxl" and
   219      loc: "approx_loc G hp loc LT"
   220       by (unfold correct_frame_def) auto
   221 
   222     let ?f = "([xcp], loc, C, sig, handler_pc)"
   223     have "correct_frame G hp (ST', LT') maxl ins ?f" 
   224     proof -
   225       from wf less loc
   226       have "approx_loc G hp loc LT'" by (simp add: sup_state_conv) blast
   227       moreover
   228       from D adr hp
   229       have "G,hp \<turnstile> xcp ::\<preceq> Class D" by (simp add: conf_def obj_ty_def)
   230       with wf less loc
   231       have "approx_stk G hp [xcp] ST'"
   232         by (auto simp add: sup_state_conv approx_stk_def approx_val_def 
   233                  elim: conf_widen split: Err.split)
   234       moreover
   235       note len pc
   236       ultimately
   237       show ?thesis by (simp add: correct_frame_def)
   238     qed
   239 
   240     with cr' match phi' meth  
   241     show ?thesis by (unfold correct_state_def) auto
   242   qed
   243 qed
   244 
   245 declare raise_if_def [simp]
   246 text {*
   247   The requirement of lemma @{text uncaught_xcpt_correct} (that
   248   the exception is a valid reference on the heap) is always met
   249   for welltyped instructions and conformant states:
   250 *}
   251 lemma exec_instr_xcpt_hp:
   252   "\<lbrakk>  fst (exec_instr (ins!pc) G hp stk vars Cl sig pc frs) = Some xcp;
   253        wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
   254        G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
   255   \<Longrightarrow> \<exists>adr T. xcp = Addr adr \<and> hp adr = Some T" 
   256   (is "\<lbrakk> ?xcpt; ?wt; ?correct \<rbrakk> \<Longrightarrow> ?thesis")
   257 proof -
   258   note [simp] = split_beta raise_system_xcpt_def
   259   note [split] = split_if_asm option.split_asm 
   260   
   261   assume wt: ?wt ?correct
   262   hence pre: "preallocated hp" by (simp add: correct_state_def)
   263 
   264   assume xcpt: ?xcpt with pre show ?thesis 
   265   proof (cases "ins!pc")
   266     case New with xcpt pre
   267     show ?thesis by (auto dest: new_Addr_OutOfMemory dest!: preallocatedD) 
   268   next
   269     case Throw with xcpt wt
   270     show ?thesis
   271       by (auto simp add: wt_instr_def correct_state_def correct_frame_def 
   272                dest: non_npD dest!: preallocatedD)
   273   qed (auto dest!: preallocatedD)
   274 qed
   275 
   276 
   277 lemma cname_of_xcp [intro]:
   278   "\<lbrakk>preallocated hp; xcp = Addr (XcptRef x)\<rbrakk> \<Longrightarrow> cname_of hp xcp = Xcpt x"
   279   by (auto elim: preallocatedE [of hp x])
   280 
   281 
   282 text {*
   283   Finally we can state that, whenever an exception occurs, the
   284   resulting next state always conforms:
   285 *}
   286 lemma xcpt_correct:
   287   "\<lbrakk> wt_jvm_prog G phi;
   288       method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   289       wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   290       fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = Some xcp; 
   291       Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
   292       G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   293   \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   294 proof -
   295   assume wtp: "wt_jvm_prog G phi"
   296   assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
   297   assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
   298   assume xp: "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = Some xcp"
   299   assume s': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
   300   assume correct: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
   301 
   302   from wtp obtain wfmb where wf: "wf_prog wfmb G" by (simp add: wt_jvm_prog_def)
   303 
   304   note xp' = meth s' xp
   305 
   306   note wtp
   307   moreover
   308   from xp wt correct
   309   obtain adr T where
   310     adr: "xcp = Addr adr" "hp adr = Some T"
   311     by (blast dest: exec_instr_xcpt_hp)
   312   moreover
   313   note correct
   314   ultimately
   315   have "G,phi \<turnstile>JVM find_handler G (Some xcp) hp frs \<surd>" by (rule uncaught_xcpt_correct)
   316   with xp'
   317   have "match_exception_table G (cname_of hp xcp) pc et = None \<Longrightarrow> ?thesis" 
   318     (is "?m (cname_of hp xcp) = _ \<Longrightarrow> _" is "?match = _ \<Longrightarrow> _")
   319     by (clarsimp simp add: exec_instr_xcpt split_beta)
   320   moreover
   321   { fix handler
   322     assume some_handler: "?match = Some handler"
   323     
   324     from correct meth
   325     obtain ST LT where
   326       hp_ok:  "G \<turnstile>h hp \<surd>" and
   327       prehp:  "preallocated hp" and
   328       "class":  "is_class G C" and
   329       phi_pc: "phi C sig ! pc = Some (ST, LT)" and
   330       frame:  "correct_frame G hp (ST, LT) maxl ins (stk, loc, C, sig, pc)" and
   331       frames: "correct_frames G hp phi rT sig frs"
   332       by (unfold correct_state_def) auto
   333 
   334     from frame obtain 
   335       stk: "approx_stk G hp stk ST" and
   336       loc: "approx_loc G hp loc LT" and
   337       pc:  "pc < length ins" and
   338       len: "length loc = 1+length (snd sig)+maxl"
   339       by (unfold correct_frame_def) auto
   340     
   341     from wt obtain
   342       eff: "\<forall>(pc', s')\<in>set (xcpt_eff (ins!pc) G pc (phi C sig!pc) et).
   343              pc' < length ins \<and> G \<turnstile> s' <=' phi C sig!pc'"
   344       by (simp add: wt_instr_def eff_def)
   345     
   346     from some_handler xp'
   347     have state': 
   348       "state' = (None, hp, ([xcp], loc, C, sig, handler)#frs)"
   349       by (cases "ins!pc", auto simp add: raise_system_xcpt_def split_beta 
   350                                split: split_if_asm) (* takes long! *)
   351 
   352     let ?f' = "([xcp], loc, C, sig, handler)"
   353     from eff
   354     obtain ST' LT' where
   355       phi_pc': "phi C sig ! handler = Some (ST', LT')" and
   356       frame': "correct_frame G hp (ST',LT') maxl ins ?f'" 
   357     proof (cases "ins!pc")
   358       case Return -- "can't generate exceptions:"
   359       with xp' have False by (simp add: split_beta split: split_if_asm)
   360       thus ?thesis ..
   361     next
   362       case New
   363       with some_handler xp'
   364       have xcp: "xcp = Addr (XcptRef OutOfMemory)"
   365         by (simp add: raise_system_xcpt_def split_beta new_Addr_OutOfMemory)
   366       with prehp have "cname_of hp xcp = Xcpt OutOfMemory" ..
   367       with New some_handler phi_pc eff 
   368       obtain ST' LT' where
   369         phi': "phi C sig ! handler = Some (ST', LT')" and
   370         less: "G \<turnstile> ([Class (Xcpt OutOfMemory)], LT) <=s (ST', LT')" and
   371         pc':  "handler < length ins"
   372         by (simp add: xcpt_eff_def match_et_imp_match) blast
   373       note phi'
   374       moreover
   375       { from xcp prehp
   376         have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt OutOfMemory)"
   377           by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
   378         moreover
   379         from wf less loc
   380         have "approx_loc G hp loc LT'"
   381           by (simp add: sup_state_conv) blast        
   382         moreover
   383         note wf less pc' len 
   384         ultimately
   385         have "correct_frame G hp (ST',LT') maxl ins ?f'"
   386           by (unfold correct_frame_def) (auto simp add: sup_state_conv 
   387               approx_stk_def approx_val_def split: err.split elim: conf_widen)
   388       }
   389       ultimately
   390       show ?thesis by (rule that)
   391     next 
   392       case Getfield
   393       with some_handler xp'
   394       have xcp: "xcp = Addr (XcptRef NullPointer)"
   395         by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
   396       with prehp have "cname_of hp xcp = Xcpt NullPointer" ..
   397       with Getfield some_handler phi_pc eff 
   398       obtain ST' LT' where
   399         phi': "phi C sig ! handler = Some (ST', LT')" and
   400         less: "G \<turnstile> ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and
   401         pc':  "handler < length ins"
   402         by (simp add: xcpt_eff_def match_et_imp_match) blast
   403       note phi'
   404       moreover
   405       { from xcp prehp
   406         have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt NullPointer)"
   407           by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
   408         moreover
   409         from wf less loc
   410         have "approx_loc G hp loc LT'"
   411           by (simp add: sup_state_conv) blast        
   412         moreover
   413         note wf less pc' len 
   414         ultimately
   415         have "correct_frame G hp (ST',LT') maxl ins ?f'"
   416           by (unfold correct_frame_def) (auto simp add: sup_state_conv 
   417               approx_stk_def approx_val_def split: err.split elim: conf_widen)
   418       }
   419       ultimately
   420       show ?thesis by (rule that)
   421     next
   422       case Putfield
   423       with some_handler xp'
   424       have xcp: "xcp = Addr (XcptRef NullPointer)"
   425         by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
   426       with prehp have "cname_of hp xcp = Xcpt NullPointer" ..
   427       with Putfield some_handler phi_pc eff 
   428       obtain ST' LT' where
   429         phi': "phi C sig ! handler = Some (ST', LT')" and
   430         less: "G \<turnstile> ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and
   431         pc':  "handler < length ins"
   432         by (simp add: xcpt_eff_def match_et_imp_match) blast
   433       note phi'
   434       moreover
   435       { from xcp prehp
   436         have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt NullPointer)"
   437           by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
   438         moreover
   439         from wf less loc
   440         have "approx_loc G hp loc LT'"
   441           by (simp add: sup_state_conv) blast        
   442         moreover
   443         note wf less pc' len 
   444         ultimately
   445         have "correct_frame G hp (ST',LT') maxl ins ?f'"
   446           by (unfold correct_frame_def) (auto simp add: sup_state_conv 
   447               approx_stk_def approx_val_def split: err.split elim: conf_widen)
   448       }
   449       ultimately
   450       show ?thesis by (rule that)
   451     next
   452       case Checkcast
   453       with some_handler xp'
   454       have xcp: "xcp = Addr (XcptRef ClassCast)"
   455         by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
   456       with prehp have "cname_of hp xcp = Xcpt ClassCast" ..
   457       with Checkcast some_handler phi_pc eff 
   458       obtain ST' LT' where
   459         phi': "phi C sig ! handler = Some (ST', LT')" and
   460         less: "G \<turnstile> ([Class (Xcpt ClassCast)], LT) <=s (ST', LT')" and
   461         pc':  "handler < length ins"
   462         by (simp add: xcpt_eff_def match_et_imp_match) blast
   463       note phi'
   464       moreover
   465       { from xcp prehp
   466         have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt ClassCast)"
   467           by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
   468         moreover
   469         from wf less loc
   470         have "approx_loc G hp loc LT'"
   471           by (simp add: sup_state_conv) blast        
   472         moreover
   473         note wf less pc' len 
   474         ultimately
   475         have "correct_frame G hp (ST',LT') maxl ins ?f'"
   476           by (unfold correct_frame_def) (auto simp add: sup_state_conv 
   477               approx_stk_def approx_val_def split: err.split elim: conf_widen)
   478       }
   479       ultimately
   480       show ?thesis by (rule that)
   481     next
   482       case Invoke
   483       with phi_pc eff 
   484       have 
   485         "\<forall>D\<in>set (match_any G pc et). 
   486         the (?m D) < length ins \<and> G \<turnstile> Some ([Class D], LT) <=' phi C sig!the (?m D)"
   487         by (simp add: xcpt_eff_def)
   488       moreover
   489       from some_handler
   490       obtain D where
   491         "D \<in> set (match_any G pc et)" and
   492         D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and
   493         "?m D = Some handler"
   494         by (blast dest: in_match_any)
   495       ultimately
   496       obtain 
   497         pc': "handler < length ins" and
   498         "G \<turnstile> Some ([Class D], LT) <=' phi C sig ! handler"
   499         by auto
   500       then
   501       obtain ST' LT' where
   502         phi': "phi C sig ! handler = Some (ST', LT')" and
   503         less: "G \<turnstile> ([Class D], LT) <=s (ST', LT')" 
   504         by auto
   505       from xp wt correct
   506       obtain addr T where
   507         xcp: "xcp = Addr addr" "hp addr = Some T"
   508         by (blast dest: exec_instr_xcpt_hp)
   509       note phi'
   510       moreover
   511       { from xcp D
   512         have "G,hp \<turnstile> xcp ::\<preceq> Class D"
   513           by (simp add: conf_def obj_ty_def)
   514         moreover
   515         from wf less loc
   516         have "approx_loc G hp loc LT'"
   517           by (simp add: sup_state_conv) blast        
   518         moreover
   519         note wf less pc' len 
   520         ultimately
   521         have "correct_frame G hp (ST',LT') maxl ins ?f'"
   522           by (unfold correct_frame_def) (auto simp add: sup_state_conv 
   523               approx_stk_def approx_val_def split: err.split elim: conf_widen)
   524       }
   525       ultimately
   526       show ?thesis by (rule that)
   527     next
   528       case Throw
   529       with phi_pc eff 
   530       have 
   531         "\<forall>D\<in>set (match_any G pc et). 
   532         the (?m D) < length ins \<and> G \<turnstile> Some ([Class D], LT) <=' phi C sig!the (?m D)"
   533         by (simp add: xcpt_eff_def)
   534       moreover
   535       from some_handler
   536       obtain D where
   537         "D \<in> set (match_any G pc et)" and
   538         D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and
   539         "?m D = Some handler"
   540         by (blast dest: in_match_any)
   541       ultimately
   542       obtain 
   543         pc': "handler < length ins" and
   544         "G \<turnstile> Some ([Class D], LT) <=' phi C sig ! handler"
   545         by auto
   546       then
   547       obtain ST' LT' where
   548         phi': "phi C sig ! handler = Some (ST', LT')" and
   549         less: "G \<turnstile> ([Class D], LT) <=s (ST', LT')" 
   550         by auto
   551       from xp wt correct
   552       obtain addr T where
   553         xcp: "xcp = Addr addr" "hp addr = Some T"
   554         by (blast dest: exec_instr_xcpt_hp)
   555       note phi'
   556       moreover
   557       { from xcp D
   558         have "G,hp \<turnstile> xcp ::\<preceq> Class D"
   559           by (simp add: conf_def obj_ty_def)
   560         moreover
   561         from wf less loc
   562         have "approx_loc G hp loc LT'"
   563           by (simp add: sup_state_conv) blast        
   564         moreover
   565         note wf less pc' len 
   566         ultimately
   567         have "correct_frame G hp (ST',LT') maxl ins ?f'"
   568           by (unfold correct_frame_def) (auto simp add: sup_state_conv 
   569               approx_stk_def approx_val_def split: err.split elim: conf_widen)
   570       }
   571       ultimately
   572       show ?thesis by (rule that)
   573     qed (insert xp', auto) -- "the other instructions don't generate exceptions"
   574 
   575     from state' meth hp_ok "class" frames phi_pc' frame' prehp
   576     have ?thesis by (unfold correct_state_def) simp
   577   }
   578   ultimately
   579   show ?thesis by (cases "?match") blast+ 
   580 qed
   581 
   582 
   583 
   584 section {* Single Instructions *}
   585 
   586 text {*
   587   In this section we look at each single (welltyped) instruction, and
   588   prove that the state after execution of the instruction still conforms.
   589   Since we have already handled exceptions above, we can now assume, that
   590   on exception occurs for this (single step) execution.
   591 *}
   592 
   593 lemmas [iff] = not_Err_eq
   594 
   595 lemma Load_correct:
   596 "\<lbrakk> wf_prog wt G;
   597     method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   598     ins!pc = Load idx; 
   599     wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   600     Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
   601     G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
   602 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   603 apply (clarsimp simp add: defs1)
   604 apply (blast intro: approx_loc_imp_approx_val_sup)
   605 done
   606 
   607 lemma Store_correct:
   608 "\<lbrakk> wf_prog wt G;
   609   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
   610   ins!pc = Store idx;
   611   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
   612   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
   613   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
   614 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   615 apply (clarsimp simp add: defs1)
   616 apply (blast intro: approx_loc_subst)
   617 done
   618 
   619 
   620 lemma LitPush_correct:
   621 "\<lbrakk> wf_prog wt G;
   622     method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   623     ins!pc = LitPush v;
   624     wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   625     Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
   626     G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
   627 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
   628 apply (clarsimp simp add: defs1 sup_PTS_eq)
   629 apply (blast dest: conf_litval intro: conf_widen)
   630 done
   631 
   632 
   633 lemma Cast_conf2:
   634   "\<lbrakk> wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; 
   635       G\<turnstile>Class C\<preceq>T; is_class G C\<rbrakk> 
   636   \<Longrightarrow> G,h\<turnstile>v::\<preceq>T"
   637 apply (unfold cast_ok_def)
   638 apply (frule widen_Class)
   639 apply (elim exE disjE) 
   640  apply (simp add: null)
   641 apply (clarsimp simp add: conf_def obj_ty_def)
   642 apply (cases v)
   643 apply auto
   644 done
   645 
   646 lemmas defs2 = defs1 raise_system_xcpt_def
   647 
   648 lemma Checkcast_correct:
   649 "\<lbrakk> wt_jvm_prog G phi;
   650     method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   651     ins!pc = Checkcast D; 
   652     wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   653     Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   654     G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   655     fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   656 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   657 apply (clarsimp simp add: defs2 wt_jvm_prog_def split: split_if_asm)
   658 apply (blast intro: Cast_conf2)
   659 done
   660 
   661 
   662 lemma Getfield_correct:
   663 "\<lbrakk> wt_jvm_prog G phi;
   664   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   665   ins!pc = Getfield F D; 
   666   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   667   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   668   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   669   fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   670 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   671 apply (clarsimp simp add: defs2 wt_jvm_prog_def split_beta
   672                 split: option.split split_if_asm)
   673 apply (frule conf_widen)
   674 apply assumption+
   675 apply (drule conf_RefTD)
   676 apply (clarsimp simp add: defs2)
   677 apply (rule conjI)
   678  apply (drule widen_cfs_fields)
   679  apply assumption+
   680  apply (erule wf_prog_ws_prog)
   681  apply (erule conf_widen)
   682  prefer 2
   683   apply assumption
   684  apply (simp add: hconf_def oconf_def lconf_def)
   685  apply (elim allE)
   686  apply (erule impE, assumption)
   687  apply simp
   688  apply (elim allE)
   689  apply (erule impE, assumption)
   690  apply clarsimp
   691 apply blast
   692 done
   693 
   694 
   695 lemma Putfield_correct:
   696 "\<lbrakk> wf_prog wt G;
   697   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   698   ins!pc = Putfield F D; 
   699   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   700   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   701   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   702   fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   703 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   704 apply (clarsimp simp add: defs2 split_beta split: option.split List.split split_if_asm)
   705 apply (frule conf_widen)
   706 prefer 2
   707   apply assumption
   708  apply assumption
   709 apply (drule conf_RefTD)
   710 apply clarsimp
   711 apply (blast 
   712        intro: 
   713          hext_upd_obj approx_stk_sup_heap
   714          approx_loc_sup_heap 
   715          hconf_field_update
   716          preallocated_field_update
   717          correct_frames_field_update conf_widen 
   718        dest: 
   719          widen_cfs_fields)
   720 done
   721     
   722 
   723 lemma New_correct:
   724 "\<lbrakk> wf_prog wt G;
   725   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   726   ins!pc = New X; 
   727   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   728   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   729   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   730   fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   731 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   732 proof -
   733   assume wf:   "wf_prog wt G"
   734   assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
   735   assume ins:  "ins!pc = New X"
   736   assume wt:   "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
   737   assume exec: "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
   738   assume conf: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
   739   assume no_x: "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None"
   740 
   741   from ins conf meth
   742   obtain ST LT where
   743     heap_ok:    "G\<turnstile>h hp\<surd>" and
   744     prealloc:   "preallocated hp" and
   745     phi_pc:     "phi C sig!pc = Some (ST,LT)" and
   746     is_class_C: "is_class G C" and
   747     frame:      "correct_frame G hp (ST,LT) maxl ins (stk, loc, C, sig, pc)" and
   748     frames:     "correct_frames G hp phi rT sig frs"
   749     by (auto simp add: correct_state_def iff del: not_None_eq)
   750 
   751   from phi_pc ins wt
   752   obtain ST' LT' where
   753     is_class_X: "is_class G X" and
   754     maxs:       "length ST < maxs" and
   755     suc_pc:     "Suc pc < length ins" and
   756     phi_suc:    "phi C sig ! Suc pc = Some (ST', LT')" and
   757     less:       "G \<turnstile> (Class X # ST, LT) <=s (ST', LT')"
   758     by (unfold wt_instr_def eff_def norm_eff_def) auto
   759  
   760   obtain oref xp' where
   761     new_Addr: "new_Addr hp = (oref,xp')"
   762     by (cases "new_Addr hp") 
   763   with ins no_x
   764   obtain hp: "hp oref = None" and "xp' = None"
   765     by (auto dest: new_AddrD simp add: raise_system_xcpt_def)
   766   
   767   with exec ins meth new_Addr 
   768   have state':
   769     "state' = Norm (hp(oref\<mapsto>(X, init_vars (fields (G, X)))), 
   770               (Addr oref # stk, loc, C, sig, Suc pc) # frs)" 
   771     (is "state' = Norm (?hp', ?f # frs)")
   772     by simp    
   773   moreover
   774   from wf hp heap_ok is_class_X
   775   have hp': "G \<turnstile>h ?hp' \<surd>"
   776     by - (rule hconf_newref, 
   777           auto simp add: oconf_def dest: fields_is_type)
   778   moreover
   779   from hp
   780   have sup: "hp \<le>| ?hp'" by (rule hext_new)
   781   from hp frame less suc_pc wf
   782   have "correct_frame G ?hp' (ST', LT') maxl ins ?f"
   783     apply (unfold correct_frame_def sup_state_conv)
   784     apply (clarsimp simp add: conf_def fun_upd_apply approx_val_def)
   785     apply (blast intro: approx_stk_sup_heap approx_loc_sup_heap sup)
   786     done      
   787   moreover
   788   from hp frames wf heap_ok is_class_X
   789   have "correct_frames G ?hp' phi rT sig frs"
   790     by - (rule correct_frames_newref, 
   791           auto simp add: oconf_def dest: fields_is_type)
   792   moreover
   793   from hp prealloc have "preallocated ?hp'" by (rule preallocated_newref)
   794   ultimately
   795   show ?thesis
   796     by (simp add: is_class_C meth phi_suc correct_state_def del: not_None_eq)
   797 qed
   798 
   799 lemmas [simp del] = split_paired_Ex
   800 
   801 
   802 lemma Invoke_correct: 
   803 "\<lbrakk> wt_jvm_prog G phi; 
   804   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   805   ins ! pc = Invoke C' mn pTs; 
   806   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   807   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   808   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   809   fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   810 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
   811 proof -
   812   assume wtprog: "wt_jvm_prog G phi"
   813   assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
   814   assume ins:    "ins ! pc = Invoke C' mn pTs"
   815   assume wti:    "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
   816   assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
   817   assume approx: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
   818   assume no_xcp: "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None"
   819   
   820   from wtprog 
   821   obtain wfmb where
   822     wfprog: "wf_prog wfmb G" 
   823     by (simp add: wt_jvm_prog_def)
   824       
   825   from ins method approx
   826   obtain s where
   827     heap_ok: "G\<turnstile>h hp\<surd>" and
   828     prealloc:"preallocated hp" and
   829     phi_pc:  "phi C sig!pc = Some s" and
   830     is_class_C: "is_class G C" and
   831     frame:   "correct_frame G hp s maxl ins (stk, loc, C, sig, pc)" and
   832     frames:  "correct_frames G hp phi rT sig frs"
   833     by (auto iff del: not_None_eq simp add: correct_state_def)
   834 
   835   from ins wti phi_pc
   836   obtain apTs X ST LT D' rT body where 
   837     is_class: "is_class G C'" and
   838     s:  "s = (rev apTs @ X # ST, LT)" and
   839     l:  "length apTs = length pTs" and
   840     X:  "G\<turnstile> X \<preceq> Class C'" and
   841     w:  "\<forall>(x, y)\<in>set (zip apTs pTs). G \<turnstile> x \<preceq> y" and
   842     mC':"method (G, C') (mn, pTs) = Some (D', rT, body)" and
   843     pc: "Suc pc < length ins" and
   844     eff: "G \<turnstile> norm_eff (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc"
   845     by (simp add: wt_instr_def eff_def del: not_None_eq) 
   846        (elim exE conjE, rule that)
   847 
   848   from eff
   849   obtain ST' LT' where
   850     s': "phi C sig ! Suc pc = Some (ST', LT')"
   851     by (simp add: norm_eff_def split_paired_Ex) blast
   852 
   853   from X 
   854   obtain T where
   855     X_Ref: "X = RefT T"
   856     by - (drule widen_RefT2, erule exE, rule that)
   857   
   858   from s ins frame 
   859   obtain 
   860     a_stk: "approx_stk G hp stk (rev apTs @ X # ST)" and
   861     a_loc: "approx_loc G hp loc LT" and
   862     suc_l: "length loc = Suc (length (snd sig) + maxl)"
   863     by (simp add: correct_frame_def)
   864 
   865   from a_stk
   866   obtain opTs stk' oX where
   867     opTs:   "approx_stk G hp opTs (rev apTs)" and
   868     oX:     "approx_val G hp oX (OK X)" and
   869     a_stk': "approx_stk G hp stk' ST" and
   870     stk':   "stk = opTs @ oX # stk'" and
   871     l_o:    "length opTs = length apTs" 
   872             "length stk' = length ST"  
   873     by - (drule approx_stk_append, auto)
   874 
   875   from oX X_Ref
   876   have oX_conf: "G,hp \<turnstile> oX ::\<preceq> RefT T"
   877     by (simp add: approx_val_def)
   878 
   879   from stk' l_o l
   880   have oX_pos: "last (take (Suc (length pTs)) stk) = oX" by simp
   881 
   882   with state' method ins no_xcp oX_conf
   883   obtain ref where oX_Addr: "oX = Addr ref"
   884     by (auto simp add: raise_system_xcpt_def dest: conf_RefTD)
   885 
   886   with oX_conf X_Ref
   887   obtain obj D where
   888     loc:    "hp ref = Some obj" and
   889     obj_ty: "obj_ty obj = Class D" and
   890     D:      "G \<turnstile> Class D \<preceq> X"
   891     by (auto simp add: conf_def) blast
   892   
   893   with X_Ref obtain X' where X': "X = Class X'"
   894     by (blast dest: widen_Class)
   895       
   896   with X have X'_subcls: "G \<turnstile> X' \<preceq>C C'"  by simp
   897 
   898   with mC' wfprog
   899   obtain D0 rT0 maxs0 maxl0 ins0 et0 where
   900     mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxs0, maxl0, ins0, et0)" "G\<turnstile>rT0\<preceq>rT"
   901     by (auto dest: subtype_widen_methd intro: that)
   902     
   903   from X' D have D_subcls: "G \<turnstile> D \<preceq>C X'" by simp
   904   
   905   with wfprog mX
   906   obtain D'' rT' mxs' mxl' ins' et' where
   907     mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')" 
   908         "G \<turnstile> rT' \<preceq> rT0"
   909     by (auto dest: subtype_widen_methd intro: that)
   910   
   911   from mX mD have rT': "G \<turnstile> rT' \<preceq> rT" by - (rule widen_trans)
   912   
   913   from is_class X'_subcls D_subcls
   914   have is_class_D: "is_class G D" by (auto dest: subcls_is_class2)
   915   
   916   with mD wfprog
   917   obtain mD'': 
   918     "method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')"
   919     "is_class G D''"
   920     by (auto dest: wf_prog_ws_prog [THEN method_in_md])
   921       
   922   from loc obj_ty have "fst (the (hp ref)) = D" by (simp add: obj_ty_def)
   923 
   924   with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD no_xcp
   925   have state'_val:
   926     "state' =
   927      Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' arbitrary, 
   928                 D'', (mn, pTs), 0) # (opTs @ Addr ref # stk', loc, C, sig, pc) # frs)"
   929     (is "state' = Norm (hp, ?f # ?f' # frs)")
   930     by (simp add: raise_system_xcpt_def)
   931     
   932   from wtprog mD''
   933   have start: "wt_start G D'' pTs mxl' (phi D'' (mn, pTs)) \<and> ins' \<noteq> []"
   934     by (auto dest: wt_jvm_prog_impl_wt_start)
   935     
   936   then obtain LT0 where
   937     LT0: "phi D'' (mn, pTs) ! 0 = Some ([], LT0)"
   938     by (clarsimp simp add: wt_start_def sup_state_conv)
   939 
   940   have c_f: "correct_frame G hp ([], LT0) mxl' ins' ?f"
   941   proof -
   942     from start LT0
   943     have sup_loc: 
   944       "G \<turnstile> (OK (Class D'') # map OK pTs @ replicate mxl' Err) <=l LT0"
   945       (is "G \<turnstile> ?LT <=l LT0")
   946       by (simp add: wt_start_def sup_state_conv)
   947 
   948     have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)"
   949       by (simp add: approx_loc_def list_all2_def set_replicate_conv_if)
   950     
   951     from wfprog mD is_class_D
   952     have "G \<turnstile> Class D \<preceq> Class D''"
   953       by (auto dest: method_wf_mdecl)
   954     with obj_ty loc
   955     have a: "approx_val G hp (Addr ref) (OK (Class D''))"
   956       by (simp add: approx_val_def conf_def)
   957 
   958     from opTs w l l_o wfprog 
   959     have "approx_stk G hp opTs (rev pTs)" 
   960       by (auto elim!: approx_stk_all_widen simp add: zip_rev)
   961     hence "approx_stk G hp (rev opTs) pTs" by (subst approx_stk_rev)
   962 
   963     with r a l_o l
   964     have "approx_loc G hp (Addr ref # rev opTs @ replicate mxl' arbitrary) ?LT"
   965       (is "approx_loc G hp ?lt ?LT")
   966       by (auto simp add: approx_loc_append approx_stk_def)
   967 
   968     from this sup_loc wfprog
   969     have "approx_loc G hp ?lt LT0" by (rule approx_loc_widen)
   970     with start l_o l
   971     show ?thesis by (simp add: correct_frame_def)
   972   qed
   973 
   974   from state'_val heap_ok mD'' ins method phi_pc s X' l mX
   975        frames s' LT0 c_f is_class_C stk' oX_Addr frame prealloc and l
   976   show ?thesis
   977     apply (simp add: correct_state_def)
   978     apply (intro exI conjI)
   979        apply blast
   980       apply (rule l)
   981      apply (rule mX)
   982     apply (rule mD)
   983     done
   984 qed
   985 
   986 lemmas [simp del] = map_append
   987 
   988 lemma Return_correct:
   989 "\<lbrakk> wt_jvm_prog G phi; 
   990   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   991   ins ! pc = Return; 
   992   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   993   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   994   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
   995 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   996 proof -
   997   assume wt_prog: "wt_jvm_prog G phi"
   998   assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
   999   assume ins: "ins ! pc = Return"
  1000   assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
  1001   assume s': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
  1002   assume correct: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
  1003 
  1004   from wt_prog 
  1005   obtain wfmb where wf: "wf_prog wfmb G" by (simp add: wt_jvm_prog_def)
  1006 
  1007   from meth ins s'
  1008   have "frs = [] \<Longrightarrow> ?thesis" by (simp add: correct_state_def)
  1009   moreover
  1010   { fix f frs' 
  1011     assume frs': "frs = f#frs'"
  1012     moreover
  1013     obtain stk' loc' C' sig' pc' where
  1014       f: "f = (stk',loc',C',sig',pc')" by (cases f)
  1015     moreover
  1016     obtain mn pt where
  1017       sig: "sig = (mn,pt)" by (cases sig)
  1018     moreover
  1019     note meth ins s'
  1020     ultimately
  1021     have state':
  1022       "state' = (None,hp,(hd stk#(drop (1+length pt) stk'),loc',C',sig',pc'+1)#frs')"
  1023       (is "state' = (None,hp,?f'#frs')")
  1024       by simp
  1025     
  1026     from correct meth
  1027     obtain ST LT where
  1028       hp_ok:  "G \<turnstile>h hp \<surd>" and
  1029       alloc:  "preallocated hp" and
  1030       phi_pc: "phi C sig ! pc = Some (ST, LT)" and
  1031       frame:  "correct_frame G hp (ST, LT) maxl ins (stk,loc,C,sig,pc)" and
  1032       frames: "correct_frames G hp phi rT sig frs"
  1033       by (simp add: correct_state_def, clarify, blast)    
  1034 
  1035     from phi_pc ins wt
  1036     obtain T ST' where "ST = T # ST'" "G \<turnstile> T \<preceq> rT"
  1037       by (simp add: wt_instr_def) blast    
  1038     with wf frame 
  1039     have hd_stk: "G,hp \<turnstile> (hd stk) ::\<preceq> rT"
  1040       by (auto simp add: correct_frame_def elim: conf_widen)
  1041 
  1042     from f frs' frames sig
  1043     obtain apTs ST0' ST' LT' D D' D'' rT' rT'' maxs' maxl' ins' et' body where
  1044       phi':   "phi C' sig' ! pc' = Some (ST',LT')" and
  1045       class': "is_class G C'" and
  1046       meth':  "method (G,C') sig' = Some (C',rT',maxs',maxl',ins',et')" and
  1047       ins':   "ins' ! pc' = Invoke D' mn pt" and
  1048       frame': "correct_frame G hp (ST', LT') maxl' ins' f" and
  1049       frames':"correct_frames G hp phi rT' sig' frs'" and
  1050       rT'':   "G \<turnstile> rT \<preceq> rT''" and
  1051       meth'': "method (G, D) sig = Some (D'', rT'', body)" and
  1052       ST0':   "ST' = rev apTs @ Class D # ST0'" and
  1053       len':   "length apTs = length pt" 
  1054       by clarsimp blast    
  1055 
  1056     from f frame'
  1057     obtain
  1058       stk': "approx_stk G hp stk' ST'" and
  1059       loc': "approx_loc G hp loc' LT'" and
  1060       pc':  "pc' < length ins'" and
  1061       lloc':"length loc' = Suc (length (snd sig') + maxl')"
  1062       by (simp add: correct_frame_def)
  1063 
  1064     from wt_prog class' meth' pc'  
  1065     have "wt_instr (ins'!pc') G rT' (phi C' sig') maxs' (length ins') et' pc'"
  1066       by (rule wt_jvm_prog_impl_wt_instr)
  1067     with ins' phi' sig
  1068     obtain apTs ST0 X ST'' LT'' body' rT0 mD where
  1069       phi_suc: "phi C' sig' ! Suc pc' = Some (ST'', LT'')" and
  1070       ST0:     "ST' = rev apTs @ X # ST0" and
  1071       len:     "length apTs = length pt" and
  1072       less:    "G \<turnstile> (rT0 # ST0, LT') <=s (ST'', LT'')" and
  1073       methD':  "method (G, D') sig = Some (mD, rT0, body')" and
  1074       lessD':  "G \<turnstile> X \<preceq> Class D'" and
  1075       suc_pc': "Suc pc' < length ins'"
  1076       by (clarsimp simp add: wt_instr_def eff_def norm_eff_def) blast
  1077 
  1078     from len len' ST0 ST0'
  1079     have "X = Class D" by simp
  1080     with lessD'
  1081     have "G \<turnstile> D \<preceq>C D'" by simp
  1082     moreover
  1083     note wf meth'' methD'
  1084     ultimately
  1085     have "G \<turnstile> rT'' \<preceq> rT0" by (auto dest: subcls_widen_methd)
  1086     with wf hd_stk rT''
  1087     have hd_stk': "G,hp \<turnstile> (hd stk) ::\<preceq> rT0" by (auto elim: conf_widen widen_trans)
  1088         
  1089     have frame'':
  1090       "correct_frame G hp (ST'',LT'') maxl' ins' ?f'"
  1091     proof -
  1092       from wf hd_stk' len stk' less ST0
  1093       have "approx_stk G hp (hd stk # drop (1+length pt) stk') ST''" 
  1094         by (auto simp add: sup_state_conv
  1095                  dest!: approx_stk_append elim: conf_widen)
  1096       moreover
  1097       from wf loc' less
  1098       have "approx_loc G hp loc' LT''" by (simp add: sup_state_conv) blast
  1099       moreover
  1100       note suc_pc' lloc'
  1101       ultimately
  1102       show ?thesis by (simp add: correct_frame_def)
  1103     qed
  1104 
  1105     with state' frs' f meth hp_ok hd_stk phi_suc frames' meth' phi' class' alloc
  1106     have ?thesis by (simp add: correct_state_def)
  1107   }
  1108   ultimately
  1109   show ?thesis by (cases frs) blast+
  1110 qed
  1111   
  1112 lemmas [simp] = map_append
  1113 
  1114 lemma Goto_correct:
  1115 "\<lbrakk> wf_prog wt G; 
  1116   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  1117   ins ! pc = Goto branch; 
  1118   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
  1119   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
  1120   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
  1121 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  1122 apply (clarsimp simp add: defs2)
  1123 apply fast
  1124 done
  1125 
  1126 
  1127 lemma Ifcmpeq_correct:
  1128 "\<lbrakk> wf_prog wt G; 
  1129   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  1130   ins ! pc = Ifcmpeq branch; 
  1131   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
  1132   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
  1133   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
  1134 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  1135 apply (clarsimp simp add: defs2)
  1136 apply fast
  1137 done
  1138 
  1139 lemma Pop_correct:
  1140 "\<lbrakk> wf_prog wt G; 
  1141   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  1142   ins ! pc = Pop;
  1143   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
  1144   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
  1145   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
  1146 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  1147 apply (clarsimp simp add: defs2)
  1148 apply fast
  1149 done
  1150 
  1151 lemma Dup_correct:
  1152 "\<lbrakk> wf_prog wt G; 
  1153   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  1154   ins ! pc = Dup;
  1155   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
  1156   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
  1157   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
  1158 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  1159 apply (clarsimp simp add: defs2)
  1160 apply (blast intro: conf_widen)
  1161 done
  1162 
  1163 lemma Dup_x1_correct:
  1164 "\<lbrakk> wf_prog wt G; 
  1165   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  1166   ins ! pc = Dup_x1;
  1167   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
  1168   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
  1169   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
  1170 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  1171 apply (clarsimp simp add: defs2)
  1172 apply (blast intro: conf_widen)
  1173 done
  1174 
  1175 lemma Dup_x2_correct:
  1176 "\<lbrakk> wf_prog wt G; 
  1177   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  1178   ins ! pc = Dup_x2;
  1179   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
  1180   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
  1181   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
  1182 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  1183 apply (clarsimp simp add: defs2)
  1184 apply (blast intro: conf_widen)
  1185 done
  1186 
  1187 lemma Swap_correct:
  1188 "\<lbrakk> wf_prog wt G; 
  1189   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  1190   ins ! pc = Swap;
  1191   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
  1192   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
  1193   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
  1194 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  1195 apply (clarsimp simp add: defs2)
  1196 apply (blast intro: conf_widen)
  1197 done
  1198 
  1199 lemma IAdd_correct:
  1200 "\<lbrakk> wf_prog wt G; 
  1201   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  1202   ins ! pc = IAdd; 
  1203   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
  1204   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
  1205   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
  1206 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  1207 apply (clarsimp simp add: defs2 approx_val_def conf_def)
  1208 apply blast
  1209 done
  1210 
  1211 lemma Throw_correct:
  1212 "\<lbrakk> wf_prog wt G; 
  1213   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
  1214   ins ! pc = Throw; 
  1215   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
  1216   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
  1217   fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
  1218 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  1219   by simp
  1220 
  1221 
  1222 text {*
  1223   The next theorem collects the results of the sections above,
  1224   i.e.~exception handling and the execution step for each 
  1225   instruction. It states type safety for single step execution:
  1226   in welltyped programs, a conforming state is transformed
  1227   into another conforming state when one instruction is executed.
  1228 *}
  1229 theorem instr_correct:
  1230 "\<lbrakk> wt_jvm_prog G phi;
  1231   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
  1232   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
  1233   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
  1234 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  1235 apply (frule wt_jvm_prog_impl_wt_instr_cor)
  1236 apply assumption+
  1237 apply (cases "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs)")
  1238 defer
  1239 apply (erule xcpt_correct, assumption+) 
  1240 apply (cases "ins!pc")
  1241 prefer 8
  1242 apply (rule Invoke_correct, assumption+)
  1243 prefer 8
  1244 apply (rule Return_correct, assumption+)
  1245 prefer 5
  1246 apply (rule Getfield_correct, assumption+)
  1247 prefer 6
  1248 apply (rule Checkcast_correct, assumption+)
  1249 
  1250 apply (unfold wt_jvm_prog_def)
  1251 apply (rule Load_correct, assumption+)
  1252 apply (rule Store_correct, assumption+)
  1253 apply (rule LitPush_correct, assumption+)
  1254 apply (rule New_correct, assumption+)
  1255 apply (rule Putfield_correct, assumption+)
  1256 apply (rule Pop_correct, assumption+)
  1257 apply (rule Dup_correct, assumption+)
  1258 apply (rule Dup_x1_correct, assumption+)
  1259 apply (rule Dup_x2_correct, assumption+)
  1260 apply (rule Swap_correct, assumption+)
  1261 apply (rule IAdd_correct, assumption+)
  1262 apply (rule Goto_correct, assumption+)
  1263 apply (rule Ifcmpeq_correct, assumption+)
  1264 apply (rule Throw_correct, assumption+)
  1265 done
  1266 
  1267 section {* Main *}
  1268 
  1269 lemma correct_state_impl_Some_method:
  1270   "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> 
  1271   \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
  1272 by (auto simp add: correct_state_def Let_def)
  1273 
  1274 
  1275 lemma BV_correct_1 [rule_format]:
  1276 "\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk> 
  1277  \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  1278 apply (simp only: split_tupled_all)
  1279 apply (rename_tac xp hp frs)
  1280 apply (case_tac xp)
  1281  apply (case_tac frs)
  1282   apply simp
  1283  apply (simp only: split_tupled_all)
  1284  apply hypsubst
  1285  apply (frule correct_state_impl_Some_method)
  1286  apply (force intro: instr_correct)
  1287 apply (case_tac frs)
  1288 apply simp_all
  1289 done
  1290 
  1291 
  1292 
  1293 lemma L0:
  1294   "\<lbrakk> xp=None; frs\<noteq>[] \<rbrakk> \<Longrightarrow> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
  1295 by (clarsimp simp add: neq_Nil_conv split_beta)
  1296 
  1297 lemma L1:
  1298   "\<lbrakk>wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]\<rbrakk> 
  1299   \<Longrightarrow> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
  1300 apply (drule L0)
  1301 apply assumption
  1302 apply (fast intro: BV_correct_1)
  1303 done
  1304 
  1305 theorem BV_correct [rule_format]:
  1306 "\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s -jvm\<rightarrow> t \<rbrakk> \<Longrightarrow> G,phi \<turnstile>JVM s\<surd> \<longrightarrow> G,phi \<turnstile>JVM t\<surd>"
  1307 apply (unfold exec_all_def)
  1308 apply (erule rtrancl_induct)
  1309  apply simp
  1310 apply (auto intro: BV_correct_1)
  1311 done
  1312 
  1313 
  1314 theorem BV_correct_implies_approx:
  1315 "\<lbrakk> wt_jvm_prog G phi; 
  1316     G \<turnstile> s0 -jvm\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk> 
  1317 \<Longrightarrow> approx_stk G hp stk (fst (the (phi C sig ! pc))) \<and> 
  1318     approx_loc G hp loc (snd (the (phi C sig ! pc)))"
  1319 apply (drule BV_correct)
  1320 apply assumption+
  1321 apply (simp add: correct_state_def correct_frame_def split_def 
  1322             split: option.splits)
  1323 done
  1324 
  1325 lemma 
  1326   fixes G :: jvm_prog ("\<Gamma>")
  1327   assumes wf: "wf_prog wf_mb \<Gamma>"
  1328   shows hconf_start: "\<Gamma> \<turnstile>h (start_heap \<Gamma>) \<surd>"
  1329   apply (unfold hconf_def start_heap_def)
  1330   apply (auto simp add: fun_upd_apply blank_def oconf_def split: split_if_asm)
  1331   apply (simp add: fields_is_type 
  1332           [OF _ wf [THEN wf_prog_ws_prog] 
  1333 	        is_class_xcpt [OF wf [THEN wf_prog_ws_prog]]])+
  1334   done
  1335     
  1336 lemma 
  1337   fixes G :: jvm_prog ("\<Gamma>") and Phi :: prog_type ("\<Phi>")
  1338   shows BV_correct_initial: 
  1339   "wt_jvm_prog \<Gamma> \<Phi> \<Longrightarrow> is_class \<Gamma> C \<Longrightarrow> method (\<Gamma>,C) (m,[]) = Some (C, b)
  1340   \<Longrightarrow> \<Gamma>,\<Phi> \<turnstile>JVM start_state G C m \<surd>"
  1341   apply (cases b)
  1342   apply (unfold  start_state_def)
  1343   apply (unfold correct_state_def)
  1344   apply (auto simp add: preallocated_start)
  1345    apply (simp add: wt_jvm_prog_def hconf_start)
  1346   apply (drule wt_jvm_prog_impl_wt_start, assumption+)
  1347   apply (clarsimp simp add: wt_start_def)
  1348   apply (auto simp add: correct_frame_def)
  1349    apply (simp add: approx_stk_def sup_state_conv)
  1350   apply (auto simp add: sup_state_conv approx_val_def dest!: widen_RefT split: err.splits)
  1351   done  
  1352 
  1353 theorem
  1354   fixes G :: jvm_prog ("\<Gamma>") and Phi :: prog_type ("\<Phi>")
  1355   assumes welltyped:   "wt_jvm_prog \<Gamma> \<Phi>" and
  1356           main_method: "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)"  
  1357   shows typesafe:
  1358   "G \<turnstile> start_state \<Gamma> C m -jvm\<rightarrow> s  \<Longrightarrow>  \<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
  1359 proof -
  1360   from welltyped main_method
  1361   have "\<Gamma>,\<Phi> \<turnstile>JVM start_state \<Gamma> C m \<surd>" by (rule BV_correct_initial)
  1362   moreover
  1363   assume "G \<turnstile> start_state \<Gamma> C m -jvm\<rightarrow> s"
  1364   ultimately  
  1365   show "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" using welltyped by - (rule BV_correct)
  1366 qed
  1367   
  1368 end