src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10042 7164dc0d24d8
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
nipkow@8011
     1
(*  Title:      HOL/MicroJava/BV/BVSpecTypeSafe.thy
nipkow@8011
     2
    ID:         $Id$
nipkow@8011
     3
    Author:     Cornelia Pusch
nipkow@8011
     4
    Copyright   1999 Technische Universitaet Muenchen
nipkow@8011
     5
nipkow@8011
     6
Proof that the specification of the bytecode verifier only admits type safe
nipkow@8011
     7
programs.
nipkow@8011
     8
*)
nipkow@8011
     9
kleing@9757
    10
header "Type Safety Proof"
kleing@9757
    11
kleing@9757
    12
theory BVSpecTypeSafe = Correct:
kleing@9757
    13
kleing@9757
    14
lemmas defs1 = sup_state_def correct_state_def correct_frame_def wt_instr_def step_def
kleing@9757
    15
lemmas [simp del] = split_paired_All
kleing@9757
    16
kleing@9757
    17
lemma wt_jvm_prog_impl_wt_instr_cor:
kleing@9757
    18
  "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
    19
      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
kleing@9757
    20
  ==> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"
kleing@9757
    21
apply (unfold correct_state_def Let_def correct_frame_def)
kleing@9757
    22
apply simp
kleing@9757
    23
apply (blast intro: wt_jvm_prog_impl_wt_instr)
wenzelm@9819
    24
done
kleing@9757
    25
kleing@9757
    26
lemma Load_correct:
kleing@9757
    27
"\<lbrakk> wf_prog wt G;
kleing@9757
    28
   method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
    29
   ins!pc = Load idx; 
kleing@9757
    30
   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
    31
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
kleing@9757
    32
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
kleing@9757
    33
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
    34
apply (clarsimp simp add: defs1 map_eq_Cons)
kleing@9757
    35
apply (rule conjI)
kleing@9757
    36
 apply (rule approx_loc_imp_approx_val_sup)
kleing@9757
    37
 apply simp+
kleing@9757
    38
apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
wenzelm@9819
    39
done
kleing@9757
    40
kleing@9757
    41
lemma Store_correct:
kleing@9757
    42
"\<lbrakk> wf_prog wt G;
kleing@9757
    43
  method (G,C) sig = Some (C,rT,maxl,ins);
kleing@9757
    44
  ins!pc = Store idx;
kleing@9757
    45
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
kleing@9757
    46
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
kleing@9757
    47
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
kleing@9757
    48
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
    49
apply (clarsimp simp add: defs1 map_eq_Cons)
kleing@9757
    50
apply (rule conjI)
kleing@9757
    51
 apply (blast intro: approx_stk_imp_approx_stk_sup)
kleing@9757
    52
apply (blast intro: approx_loc_imp_approx_loc_subst approx_loc_imp_approx_loc_sup)
wenzelm@9819
    53
done
kleing@9757
    54
kleing@9757
    55
kleing@9757
    56
lemma conf_Intg_Integer [iff]:
kleing@9757
    57
  "G,h \<turnstile> Intg i \<Colon>\<preceq> PrimT Integer"
kleing@9757
    58
by (simp add: conf_def)
kleing@9757
    59
kleing@9757
    60
kleing@9757
    61
lemma Bipush_correct:
kleing@9757
    62
"\<lbrakk> wf_prog wt G;
kleing@9757
    63
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
    64
  ins!pc = Bipush i; 
kleing@9757
    65
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
    66
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
kleing@9757
    67
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
wenzelm@9819
    68
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
    69
apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons)
kleing@9757
    70
apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
wenzelm@9819
    71
done
kleing@9757
    72
kleing@9757
    73
lemma NT_subtype_conv:
kleing@9757
    74
  "G \<turnstile> NT \<preceq> T = (T=NT \<or> (\<exists>C. T = Class C))"
kleing@9757
    75
proof -
kleing@9757
    76
  have "\<And>T T'. G \<turnstile> T' \<preceq> T \<Longrightarrow> T' = NT \<longrightarrow> (T=NT | (\<exists>C. T = Class C))"
kleing@9757
    77
    apply (erule widen.induct)
kleing@9757
    78
    apply auto
kleing@9757
    79
    apply (case_tac R)
kleing@9757
    80
    apply auto
wenzelm@9819
    81
    done
kleing@9757
    82
  note l = this
kleing@9757
    83
kleing@9757
    84
  show ?thesis 
kleing@9757
    85
    by (force intro: null dest: l)
kleing@9757
    86
qed
kleing@9757
    87
kleing@9757
    88
lemma Aconst_null_correct:
kleing@9757
    89
"\<lbrakk> wf_prog wt G;
kleing@9757
    90
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
    91
  ins!pc =  Aconst_null; 
kleing@9757
    92
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
    93
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
kleing@9757
    94
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
wenzelm@9819
    95
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
    96
apply (clarsimp simp add: defs1 map_eq_Cons)
kleing@9757
    97
apply (rule conjI)
kleing@9757
    98
 apply (force simp add: approx_val_Null NT_subtype_conv)
kleing@9757
    99
apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
wenzelm@9819
   100
done
kleing@9757
   101
kleing@9757
   102
kleing@9757
   103
lemma Cast_conf2:
kleing@9757
   104
  "\<lbrakk>wf_prog ok G; G,h\<turnstile>v\<Colon>\<preceq>RefT rt; cast_ok G C h v; G\<turnstile>Class C\<preceq>T; is_class G C\<rbrakk> 
kleing@9757
   105
  \<Longrightarrow> G,h\<turnstile>v\<Colon>\<preceq>T"
kleing@9757
   106
apply (unfold cast_ok_def)
kleing@9757
   107
apply (frule widen_Class)
kleing@9757
   108
apply (elim exE disjE)
kleing@9757
   109
 apply (simp add: null)
kleing@9757
   110
apply (clarsimp simp add: conf_def obj_ty_def)
kleing@9757
   111
apply (cases v)
kleing@9757
   112
apply (auto intro: null rtrancl_trans)
wenzelm@9819
   113
done
kleing@9757
   114
kleing@9757
   115
kleing@9757
   116
lemma Checkcast_correct:
kleing@9757
   117
"\<lbrakk> wf_prog wt G;
kleing@9757
   118
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
   119
  ins!pc = Checkcast D; 
kleing@9757
   120
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
   121
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
kleing@9757
   122
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
kleing@9757
   123
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   124
apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def)
kleing@9757
   125
apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup Cast_conf2)
wenzelm@9819
   126
done
kleing@9757
   127
kleing@9757
   128
kleing@9757
   129
lemma Getfield_correct:
kleing@9757
   130
"\<lbrakk> wf_prog wt G;
kleing@9757
   131
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
   132
  ins!pc = Getfield F D; 
kleing@9757
   133
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
   134
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
kleing@9757
   135
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
wenzelm@9819
   136
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   137
apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def split: option.split)
kleing@9757
   138
apply (frule conf_widen)
kleing@9757
   139
apply assumption+
kleing@9757
   140
apply (drule conf_RefTD)
kleing@9757
   141
apply (clarsimp simp add: defs1 approx_val_def)
kleing@9757
   142
apply (rule conjI)
kleing@9757
   143
 apply (drule widen_cfs_fields)
kleing@9757
   144
 apply assumption+
kleing@9757
   145
 apply (force intro: conf_widen simp add: hconf_def oconf_def lconf_def)
kleing@9757
   146
apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
wenzelm@9819
   147
done
kleing@9757
   148
kleing@9757
   149
lemma Putfield_correct:
kleing@9757
   150
"\<lbrakk> wf_prog wt G;
kleing@9757
   151
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
   152
  ins!pc = Putfield F D; 
kleing@9757
   153
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
   154
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
kleing@9757
   155
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
wenzelm@9819
   156
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   157
apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split)
kleing@9757
   158
apply (clarsimp simp add: approx_val_def)
kleing@9757
   159
apply (frule conf_widen)
kleing@9757
   160
prefer 2
kleing@9757
   161
apply assumption
kleing@9757
   162
apply assumption
kleing@9757
   163
apply (drule conf_RefTD)
kleing@9757
   164
apply clarsimp
wenzelm@9819
   165
apply (blast intro: sup_heap_update_value approx_stk_imp_approx_stk_sup_heap
wenzelm@9819
   166
  approx_stk_imp_approx_stk_sup
wenzelm@9819
   167
  approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
wenzelm@9819
   168
  hconf_imp_hconf_field_update
wenzelm@9819
   169
  correct_frames_imp_correct_frames_field_update conf_widen dest: widen_cfs_fields)
wenzelm@9819
   170
done
kleing@9757
   171
kleing@9757
   172
lemma collapse_paired_All:
kleing@9757
   173
  "(\<forall>x y. P(x,y)) = (\<forall>z. P z)"
kleing@9757
   174
  by fast
kleing@9757
   175
kleing@9757
   176
lemma New_correct:
kleing@9757
   177
"\<lbrakk> wf_prog wt G;
kleing@9757
   178
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
   179
  ins!pc = New cl_idx; 
kleing@9757
   180
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
   181
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
kleing@9757
   182
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
kleing@9757
   183
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   184
apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def
kleing@9757
   185
		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 
kleing@9757
   186
       split: option.split)
kleing@9757
   187
apply (force dest!: iffD1 [OF collapse_paired_All]
kleing@9757
   188
            intro: sup_heap_newref approx_stk_imp_approx_stk_sup_heap approx_stk_imp_approx_stk_sup
kleing@9757
   189
                   approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
kleing@9757
   190
                   hconf_imp_hconf_newref correct_frames_imp_correct_frames_newref
kleing@9757
   191
                   correct_init_obj simp add:  NT_subtype_conv approx_val_def conf_def
kleing@9757
   192
		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 
kleing@9757
   193
       split: option.split)
wenzelm@9819
   194
done
kleing@9757
   195
kleing@9757
   196
kleing@9757
   197
(****** Method Invocation ******)
kleing@9757
   198
kleing@9757
   199
lemmas [simp del] = split_paired_Ex
kleing@9757
   200
kleing@9757
   201
lemma Invoke_correct:
kleing@9757
   202
"\<lbrakk> wt_jvm_prog G phi; 
kleing@9757
   203
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
   204
  ins ! pc = Invoke C' mn pTs; 
kleing@9757
   205
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
   206
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
kleing@9757
   207
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
kleing@9757
   208
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
kleing@9757
   209
proof -
kleing@9757
   210
  assume wtprog: "wt_jvm_prog G phi"
kleing@9757
   211
  assume method: "method (G,C) sig = Some (C,rT,maxl,ins)"
kleing@9757
   212
  assume ins:    "ins ! pc = Invoke C' mn pTs"
kleing@9757
   213
  assume wti:    "wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"
kleing@9757
   214
  assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
kleing@9757
   215
  assume approx: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
kleing@9757
   216
  
kleing@9757
   217
  from wtprog 
kleing@9757
   218
  obtain wfmb where
kleing@9757
   219
    wfprog: "wf_prog wfmb G" 
kleing@9757
   220
    by (simp add: wt_jvm_prog_def)
kleing@9757
   221
kleing@9757
   222
  from ins method approx
kleing@9757
   223
  obtain s where
kleing@9757
   224
    heap_ok: "G\<turnstile>h hp\<surd>" and
kleing@9757
   225
    phi_pc:  "phi C sig!pc = Some s" and
kleing@9757
   226
    frame:   "correct_frame G hp s maxl ins (stk, loc, C, sig, pc)" and
kleing@9757
   227
    frames:  "correct_frames G hp phi rT sig frs"
kleing@9757
   228
    by (clarsimp simp add: correct_state_def)
kleing@9757
   229
kleing@9757
   230
  from ins wti phi_pc
kleing@9757
   231
  obtain apTs X ST LT D' rT body where 
kleing@9757
   232
    s: "s = (rev apTs @ X # ST, LT)" and
kleing@9757
   233
    l: "length apTs = length pTs" and
kleing@9757
   234
    X: "G\<turnstile> X \<preceq> Class C'" and
kleing@9757
   235
    w: "\<forall>x\<in>set (zip apTs pTs). x \<in> widen G" and
kleing@9757
   236
    mC': "method (G, C') (mn, pTs) = Some (D', rT, body)" and
kleing@9757
   237
    pc:  "Suc pc < length ins" and
kleing@9757
   238
    step: "G \<turnstile> step (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc"
kleing@9757
   239
    by (simp add: wt_instr_def) (elim exE conjE, rule that)
kleing@9757
   240
kleing@9757
   241
  from step
kleing@9757
   242
  obtain ST' LT' where
kleing@9757
   243
    s': "phi C sig ! Suc pc = Some (ST', LT')"
kleing@9757
   244
    by (simp add: step_def split_paired_Ex) (elim, rule that)
kleing@9757
   245
kleing@9757
   246
  from X 
kleing@9757
   247
  obtain T where
kleing@9757
   248
    X_Ref: "X = RefT T"
kleing@9757
   249
    by - (drule widen_RefT2, erule exE, rule that)
kleing@9757
   250
  
kleing@9757
   251
  from s ins frame 
kleing@9757
   252
  obtain 
kleing@9757
   253
    a_stk: "approx_stk G hp stk (rev apTs @ X # ST)" and
kleing@9757
   254
    a_loc: "approx_loc G hp loc LT" and
kleing@9757
   255
    suc_l: "length loc = Suc (length (snd sig) + maxl)"
kleing@9757
   256
    by (simp add: correct_frame_def)
kleing@9757
   257
kleing@9757
   258
  from a_stk
kleing@9757
   259
  obtain opTs stk' oX where
kleing@9757
   260
    opTs:   "approx_stk G hp opTs (rev apTs)" and
kleing@9757
   261
    oX:     "approx_val G hp oX (Ok X)" and
kleing@9757
   262
    a_stk': "approx_stk G hp stk' ST" and
kleing@9757
   263
    stk':   "stk = opTs @ oX # stk'" and
kleing@9757
   264
    l_o:    "length opTs = length apTs" 
kleing@9757
   265
            "length stk' = length ST" 
kleing@9757
   266
    by - (drule approx_stk_append_lemma, simp, elim, simp)
kleing@9757
   267
kleing@9757
   268
  from oX 
kleing@9757
   269
  have "\<exists>T'. typeof (option_map obj_ty \<circ> hp) oX = Some T' \<and> G \<turnstile> T' \<preceq> X"
kleing@9757
   270
    by (clarsimp simp add: approx_val_def conf_def)
kleing@9757
   271
kleing@9757
   272
  with X_Ref
kleing@9757
   273
  obtain T' where
kleing@9757
   274
    oX_Ref: "typeof (option_map obj_ty \<circ> hp) oX = Some (RefT T')"
kleing@9757
   275
            "G \<turnstile> RefT T' \<preceq> X" 
kleing@9757
   276
    apply (elim, simp)
kleing@9757
   277
    apply (frule widen_RefT2)
kleing@9757
   278
    by (elim, simp)
kleing@9757
   279
kleing@9757
   280
  from stk' l_o l
kleing@9757
   281
  have oX_pos: "last (take (Suc (length pTs)) stk) = oX" 
kleing@9757
   282
    by simp
kleing@9757
   283
kleing@9757
   284
  with state' method ins 
kleing@9757
   285
  have Null_ok: "oX = Null \<Longrightarrow> ?thesis"
kleing@9757
   286
    by (simp add: correct_state_def raise_xcpt_def)
kleing@9757
   287
  
kleing@9757
   288
  { fix ref
kleing@9757
   289
    assume oX_Addr: "oX = Addr ref"
kleing@9757
   290
    
kleing@9757
   291
    with oX_Ref
kleing@9757
   292
    obtain obj where
kleing@9757
   293
      loc: "hp ref = Some obj" "obj_ty obj = RefT T'"
kleing@9757
   294
      by clarsimp
kleing@9757
   295
kleing@9757
   296
    then 
kleing@9757
   297
    obtain D where
kleing@9757
   298
      obj_ty: "obj_ty obj = Class D"
kleing@9757
   299
      by (auto simp add: obj_ty_def)
kleing@9757
   300
kleing@9757
   301
    with X_Ref oX_Ref loc
kleing@9757
   302
    obtain D: "G \<turnstile> Class D \<preceq> X"
kleing@9757
   303
      by simp
kleing@9757
   304
kleing@9757
   305
    with X_Ref
kleing@9757
   306
    obtain X' where 
kleing@9757
   307
      X': "X = Class X'"
kleing@9757
   308
      by - (drule widen_Class, elim, rule that)
kleing@9757
   309
      
kleing@9757
   310
    with X
kleing@9757
   311
    have "G \<turnstile> X' \<preceq>C C'" 
kleing@9757
   312
      by simp
kleing@9757
   313
kleing@9757
   314
    with mC' wfprog
kleing@9757
   315
    obtain D0 rT0 maxl0 ins0 where
kleing@9757
   316
      mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxl0, ins0)" "G\<turnstile>rT0\<preceq>rT"
kleing@9757
   317
      by (auto dest: subtype_widen_methd)
kleing@9757
   318
kleing@9757
   319
    from X' D
kleing@9757
   320
    have "G \<turnstile> D \<preceq>C X'" 
kleing@9757
   321
      by simp
kleing@9757
   322
kleing@9757
   323
    with wfprog mX
kleing@9757
   324
    obtain D'' rT' mxl' ins' where
kleing@9757
   325
      mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxl', ins')" 
kleing@9757
   326
          "G \<turnstile> rT' \<preceq> rT0"
kleing@9757
   327
      by (auto dest: subtype_widen_methd)
kleing@9757
   328
kleing@9757
   329
    from mX mD
kleing@9757
   330
    have rT': "G \<turnstile> rT' \<preceq> rT"
kleing@9757
   331
      by - (rule widen_trans)
kleing@9757
   332
    
kleing@9757
   333
    from mD wfprog
kleing@9757
   334
    obtain mD'': 
kleing@9757
   335
      "method (G, D'') (mn, pTs) = Some (D'', rT', mxl', ins')"
kleing@9757
   336
      "is_class G D''" 
kleing@9757
   337
      by (auto dest: method_in_md)
kleing@9757
   338
      
kleing@9757
   339
    from loc obj_ty
kleing@9757
   340
    have "fst (the (hp ref)) = D"
kleing@9757
   341
      by (simp add: obj_ty_def)
kleing@9757
   342
kleing@9757
   343
    with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD 
kleing@9757
   344
    have state'_val:
kleing@9757
   345
      "state' =
kleing@9757
   346
       Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' arbitrary, 
kleing@9757
   347
                  D'', (mn, pTs), 0) # (stk', loc, C, sig, Suc pc) # frs)"
kleing@9757
   348
      (is "state' = Norm (hp, ?f # ?f' # frs)")
kleing@9757
   349
      by (simp add: raise_xcpt_def)
kleing@9757
   350
    
kleing@9757
   351
    from wtprog mD''
kleing@9757
   352
    have start: "wt_start G D'' pTs mxl' (phi D'' (mn, pTs)) \<and> ins' \<noteq> []"
kleing@9757
   353
      by (auto dest: wt_jvm_prog_impl_wt_start)
kleing@9757
   354
    
kleing@9757
   355
    then
kleing@9757
   356
    obtain LT0 where
kleing@9757
   357
      LT0: "phi D'' (mn, pTs) ! 0 = Some ([], LT0)"
kleing@9757
   358
      by (clarsimp simp add: wt_start_def sup_state_def)
kleing@9757
   359
kleing@9757
   360
    have c_f: "correct_frame G hp ([], LT0) mxl' ins' ?f"
kleing@9757
   361
    proof -
kleing@9757
   362
      from start LT0
kleing@9757
   363
      have sup_loc: 
kleing@9757
   364
        "G \<turnstile> (Ok (Class D'') # map Ok pTs @ replicate mxl' Err) <=l LT0"
kleing@9757
   365
        (is "G \<turnstile> ?LT <=l LT0")
kleing@9757
   366
        by (simp add: wt_start_def sup_state_def)
kleing@9757
   367
kleing@9757
   368
      have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)"
kleing@9757
   369
        by (simp add: approx_loc_def approx_val_Err list_all2_def set_replicate_conv_if)
kleing@9757
   370
kleing@9757
   371
      from wfprog mD
kleing@9757
   372
      have "G \<turnstile> Class D \<preceq> Class D''"
kleing@9757
   373
        by (auto dest: method_wf_mdecl)
kleing@9757
   374
      with obj_ty loc
kleing@9757
   375
      have a: "approx_val G hp (Addr ref) (Ok (Class D''))"
kleing@9757
   376
        by (simp add: approx_val_def conf_def)
kleing@9757
   377
kleing@9757
   378
      from w l
kleing@9757
   379
      have "\<forall>x\<in>set (zip (rev apTs) (rev pTs)). x \<in> widen G"
kleing@9757
   380
        by (auto simp add: zip_rev)
kleing@9757
   381
      with wfprog l l_o opTs
kleing@9757
   382
      have "approx_loc G hp opTs (map Ok (rev pTs))"
kleing@9757
   383
        by (auto intro: assConv_approx_stk_imp_approx_loc)
kleing@9757
   384
      hence "approx_stk G hp opTs (rev pTs)"
kleing@9757
   385
        by (simp add: approx_stk_def)
kleing@9757
   386
      hence "approx_stk G hp (rev opTs) pTs"
kleing@9757
   387
        by (simp add: approx_stk_rev)
kleing@9757
   388
kleing@9757
   389
      with r a l_o l
kleing@9757
   390
      have "approx_loc G hp (Addr ref # rev opTs @ replicate mxl' arbitrary) ?LT"
kleing@9757
   391
        (is "approx_loc G hp ?lt ?LT")
kleing@9757
   392
        by (auto simp add: approx_loc_append approx_stk_def)
kleing@9757
   393
kleing@9757
   394
      from wfprog this sup_loc
kleing@9757
   395
      have "approx_loc G hp ?lt LT0"
kleing@9757
   396
        by (rule approx_loc_imp_approx_loc_sup)
kleing@9757
   397
kleing@9757
   398
      with start l_o l
kleing@9757
   399
      show ?thesis
kleing@9757
   400
        by (simp add: correct_frame_def)
kleing@9757
   401
    qed
kleing@9757
   402
kleing@9757
   403
    have c_f': "correct_frame G hp (tl ST', LT') maxl ins ?f'"
kleing@9757
   404
    proof -    
kleing@9757
   405
      from s s' mC' step l
kleing@9757
   406
      have "G \<turnstile> LT <=l LT'"
kleing@9757
   407
        by (simp add: step_def sup_state_def)
kleing@9757
   408
      with wfprog a_loc
kleing@9757
   409
      have a: "approx_loc G hp loc LT'"
kleing@9757
   410
        by (rule approx_loc_imp_approx_loc_sup)
kleing@9757
   411
      moreover
kleing@9757
   412
      from s s' mC' step l
kleing@9757
   413
      have  "G \<turnstile> map Ok ST <=l map Ok (tl ST')"
kleing@9757
   414
        by (auto simp add: step_def sup_state_def map_eq_Cons)
kleing@9757
   415
      with wfprog a_stk'
kleing@9757
   416
      have "approx_stk G hp stk' (tl ST')"
kleing@9757
   417
        by (rule approx_stk_imp_approx_stk_sup)
kleing@9757
   418
      ultimately
kleing@9757
   419
      show ?thesis
kleing@9757
   420
        by (simp add: correct_frame_def suc_l pc)
kleing@9757
   421
    qed
kleing@9757
   422
kleing@9757
   423
    with state'_val heap_ok mD'' ins method phi_pc s X' l 
kleing@9757
   424
         frames s' LT0 c_f c_f'
kleing@9757
   425
    have ?thesis
kleing@9757
   426
      by (simp add: correct_state_def) (intro exI conjI, force+)
kleing@9757
   427
  }
kleing@9757
   428
  
kleing@9757
   429
  with Null_ok oX_Ref
kleing@9757
   430
  show "G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   431
    by - (cases oX, auto)
kleing@9757
   432
qed
kleing@9757
   433
kleing@9757
   434
lemmas [simp del] = map_append
kleing@9757
   435
kleing@9757
   436
lemma Return_correct:
kleing@9757
   437
"\<lbrakk> wt_jvm_prog G phi;  
kleing@9757
   438
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
   439
  ins ! pc = Return; 
kleing@9757
   440
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
   441
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
kleing@9757
   442
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
kleing@9757
   443
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   444
apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm)
kleing@9757
   445
apply (frule wt_jvm_prog_impl_wt_instr)
wenzelm@9819
   446
apply (assumption, erule Suc_lessD)
kleing@9757
   447
apply (unfold wt_jvm_prog_def)
wenzelm@9819
   448
apply (fastsimp
wenzelm@9819
   449
  dest: subcls_widen_methd
wenzelm@9819
   450
  elim: widen_trans [COMP swap_prems_rl]
wenzelm@9819
   451
  intro: conf_widen
wenzelm@9819
   452
  simp: approx_val_def append_eq_conv_conj map_eq_Cons defs1)
wenzelm@9819
   453
done
kleing@9757
   454
kleing@9757
   455
lemmas [simp] = map_append
kleing@9757
   456
kleing@9757
   457
lemma Goto_correct:
kleing@9757
   458
"\<lbrakk> wf_prog wt G; 
kleing@9757
   459
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
   460
  ins ! pc = Goto branch; 
kleing@9757
   461
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
   462
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
kleing@9757
   463
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
kleing@9757
   464
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   465
apply (clarsimp simp add: defs1)
kleing@9757
   466
apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
wenzelm@9819
   467
done
kleing@9757
   468
kleing@9757
   469
kleing@9757
   470
lemma Ifcmpeq_correct:
kleing@9757
   471
"\<lbrakk> wf_prog wt G; 
kleing@9757
   472
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
   473
  ins ! pc = Ifcmpeq branch; 
kleing@9757
   474
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
   475
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
kleing@9757
   476
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
kleing@9757
   477
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   478
apply (clarsimp simp add: defs1)
kleing@9757
   479
apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
wenzelm@9819
   480
done
kleing@9757
   481
kleing@9757
   482
lemma Pop_correct:
kleing@9757
   483
"\<lbrakk> wf_prog wt G; 
kleing@9757
   484
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
   485
  ins ! pc = Pop;
kleing@9757
   486
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
   487
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
kleing@9757
   488
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
kleing@9757
   489
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   490
apply (clarsimp simp add: defs1)
kleing@9757
   491
apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
wenzelm@9819
   492
done
kleing@9757
   493
kleing@9757
   494
lemma Dup_correct:
kleing@9757
   495
"\<lbrakk> wf_prog wt G; 
kleing@9757
   496
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
   497
  ins ! pc = Dup;
kleing@9757
   498
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
   499
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
kleing@9757
   500
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
kleing@9757
   501
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   502
apply (clarsimp simp add: defs1 map_eq_Cons)
kleing@9757
   503
apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
kleing@9757
   504
             simp add: defs1 map_eq_Cons)
wenzelm@9819
   505
done
kleing@9757
   506
kleing@9757
   507
lemma Dup_x1_correct:
kleing@9757
   508
"\<lbrakk> wf_prog wt G; 
kleing@9757
   509
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
   510
  ins ! pc = Dup_x1;
kleing@9757
   511
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
   512
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
kleing@9757
   513
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
kleing@9757
   514
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   515
apply (clarsimp simp add: defs1 map_eq_Cons)
kleing@9757
   516
apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
kleing@9757
   517
             simp add: defs1 map_eq_Cons)
wenzelm@9819
   518
done
kleing@9757
   519
kleing@9757
   520
lemma Dup_x2_correct:
kleing@9757
   521
"\<lbrakk> wf_prog wt G; 
kleing@9757
   522
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
   523
  ins ! pc = Dup_x2;
kleing@9757
   524
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
   525
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
kleing@9757
   526
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
kleing@9757
   527
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   528
apply (clarsimp simp add: defs1 map_eq_Cons)
kleing@9757
   529
apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
kleing@9757
   530
             simp add: defs1 map_eq_Cons)
wenzelm@9819
   531
done
kleing@9757
   532
kleing@9757
   533
lemma Swap_correct:
kleing@9757
   534
"\<lbrakk> wf_prog wt G; 
kleing@9757
   535
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
   536
  ins ! pc = Swap;
kleing@9757
   537
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
   538
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
kleing@9757
   539
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
kleing@9757
   540
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   541
apply (clarsimp simp add: defs1 map_eq_Cons)
kleing@9757
   542
apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
kleing@9757
   543
             simp add: defs1 map_eq_Cons)
wenzelm@9819
   544
done
kleing@9757
   545
kleing@9757
   546
lemma IAdd_correct:
kleing@9757
   547
"\<lbrakk> wf_prog wt G; 
kleing@9757
   548
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
   549
  ins ! pc = IAdd; 
kleing@9757
   550
  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
kleing@9757
   551
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
kleing@9757
   552
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
kleing@9757
   553
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   554
apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
kleing@9757
   555
apply (blast intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup)
wenzelm@9819
   556
done
kleing@9757
   557
kleing@9757
   558
kleing@9757
   559
(** instr correct **)
kleing@9757
   560
kleing@9757
   561
lemma instr_correct:
kleing@9757
   562
"\<lbrakk> wt_jvm_prog G phi; 
kleing@9757
   563
  method (G,C) sig = Some (C,rT,maxl,ins); 
kleing@9757
   564
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
kleing@9757
   565
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
kleing@9757
   566
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   567
apply (frule wt_jvm_prog_impl_wt_instr_cor)
kleing@9757
   568
apply assumption+
kleing@9757
   569
apply (cases "ins!pc")
kleing@9757
   570
prefer 9
kleing@9757
   571
apply (blast intro: Invoke_correct)
kleing@9757
   572
prefer 9
kleing@9757
   573
apply (blast intro: Return_correct)
kleing@9757
   574
apply (unfold wt_jvm_prog_def)
kleing@9757
   575
apply (fast intro: Load_correct Store_correct Bipush_correct Aconst_null_correct 
kleing@9757
   576
       Checkcast_correct Getfield_correct Putfield_correct New_correct 
kleing@9757
   577
       Goto_correct Ifcmpeq_correct Pop_correct Dup_correct 
kleing@9757
   578
       Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+
wenzelm@9819
   579
done
kleing@9757
   580
kleing@9757
   581
kleing@9757
   582
(** Main **)
kleing@9757
   583
kleing@9757
   584
lemma correct_state_impl_Some_method:
kleing@9757
   585
  "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> 
kleing@9757
   586
  \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
kleing@9757
   587
by (auto simp add: correct_state_def Let_def)
kleing@9757
   588
kleing@9757
   589
wenzelm@9941
   590
lemma BV_correct_1 [rule_format]:
kleing@9757
   591
"\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk> 
wenzelm@9819
   592
 \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
wenzelm@9819
   593
apply (simp only: split_tupled_all)
kleing@9757
   594
apply (rename_tac xp hp frs)
kleing@9757
   595
apply (case_tac xp)
kleing@9757
   596
 apply (case_tac frs)
kleing@9757
   597
  apply simp
wenzelm@9819
   598
 apply (simp only: split_tupled_all)
wenzelm@9819
   599
 apply hypsubst
kleing@9757
   600
 apply (frule correct_state_impl_Some_method)
kleing@9757
   601
 apply (force intro: instr_correct)
kleing@9757
   602
apply (case_tac frs)
wenzelm@9819
   603
apply simp_all
wenzelm@9819
   604
done
kleing@9757
   605
kleing@9757
   606
kleing@9757
   607
lemma L0:
kleing@9757
   608
  "\<lbrakk> xp=None; frs\<noteq>[] \<rbrakk> \<Longrightarrow> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
kleing@9757
   609
by (clarsimp simp add: neq_Nil_conv simp del: split_paired_Ex)
kleing@9757
   610
kleing@9757
   611
lemma L1:
kleing@9757
   612
  "\<lbrakk>wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]\<rbrakk> 
kleing@9757
   613
  \<Longrightarrow> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
kleing@9757
   614
apply (drule L0)
kleing@9757
   615
apply assumption
kleing@9757
   616
apply (fast intro: BV_correct_1)
wenzelm@9819
   617
done
kleing@9757
   618
kleing@9757
   619
wenzelm@9941
   620
theorem BV_correct [rule_format]:
kleing@9757
   621
"\<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
   622
apply (unfold exec_all_def)
kleing@9757
   623
apply (erule rtrancl_induct)
kleing@9757
   624
 apply simp
kleing@9757
   625
apply (auto intro: BV_correct_1)
wenzelm@9819
   626
done
kleing@9757
   627
kleing@9757
   628
kleing@9757
   629
theorem BV_correct_initial:
kleing@9757
   630
"\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s0 -jvm\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk> 
kleing@9757
   631
 \<Longrightarrow>  approx_stk G hp stk (fst (the (((phi  C)  sig) ! pc))) \<and> approx_loc G hp loc (snd (the (((phi  C)  sig) ! pc)))"
kleing@9757
   632
apply (drule BV_correct)
kleing@9757
   633
apply assumption+
kleing@9757
   634
apply (simp add: correct_state_def correct_frame_def split_def split: option.splits)
wenzelm@9819
   635
done
kleing@9757
   636
kleing@9757
   637
end