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