src/HOL/MicroJava/DFA/LBVCorrect.thy
author haftmann
Tue Nov 24 14:37:23 2009 +0100 (2009-11-24)
changeset 33954 1bc3b688548c
child 58886 8a6cac7c7247
permissions -rwxr-xr-x
backported parts of abstract byte code verifier from AFP/Jinja
haftmann@33954
     1
(*  Author:     Gerwin Klein
haftmann@33954
     2
    Copyright   1999 Technische Universitaet Muenchen
haftmann@33954
     3
*)
haftmann@33954
     4
haftmann@33954
     5
header {* \isaheader{Correctness of the LBV} *}
haftmann@33954
     6
haftmann@33954
     7
theory LBVCorrect
haftmann@33954
     8
imports LBVSpec Typing_Framework
haftmann@33954
     9
begin
haftmann@33954
    10
haftmann@33954
    11
locale lbvs = lbv +
haftmann@33954
    12
  fixes s0  :: 'a ("s\<^sub>0")
haftmann@33954
    13
  fixes c   :: "'a list"
haftmann@33954
    14
  fixes ins :: "'b list"
haftmann@33954
    15
  fixes phi :: "'a list" ("\<phi>")
haftmann@33954
    16
  defines phi_def:
haftmann@33954
    17
  "\<phi> \<equiv> map (\<lambda>pc. if c!pc = \<bottom> then wtl (take pc ins) c 0 s0 else c!pc) 
haftmann@33954
    18
       [0..<length ins]"
haftmann@33954
    19
haftmann@33954
    20
  assumes bounded: "bounded step (length ins)"
haftmann@33954
    21
  assumes cert: "cert_ok c (length ins) \<top> \<bottom> A"
haftmann@33954
    22
  assumes pres: "pres_type step (length ins) A"
haftmann@33954
    23
haftmann@33954
    24
haftmann@33954
    25
lemma (in lbvs) phi_None [intro?]:
haftmann@33954
    26
  "\<lbrakk> pc < length ins; c!pc = \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = wtl (take pc ins) c 0 s0"
haftmann@33954
    27
  by (simp add: phi_def)
haftmann@33954
    28
haftmann@33954
    29
lemma (in lbvs) phi_Some [intro?]:
haftmann@33954
    30
  "\<lbrakk> pc < length ins; c!pc \<noteq> \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = c ! pc"
haftmann@33954
    31
  by (simp add: phi_def)
haftmann@33954
    32
haftmann@33954
    33
lemma (in lbvs) phi_len [simp]:
haftmann@33954
    34
  "length \<phi> = length ins"
haftmann@33954
    35
  by (simp add: phi_def)
haftmann@33954
    36
haftmann@33954
    37
haftmann@33954
    38
lemma (in lbvs) wtl_suc_pc:
haftmann@33954
    39
  assumes all: "wtl ins c 0 s\<^sub>0 \<noteq> \<top>" 
haftmann@33954
    40
  assumes pc:  "pc+1 < length ins"
haftmann@33954
    41
  shows "wtl (take (pc+1) ins) c 0 s0 \<sqsubseteq>\<^sub>r \<phi>!(pc+1)"
haftmann@33954
    42
proof -
haftmann@33954
    43
  from all pc
haftmann@33954
    44
  have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s0) \<noteq> T" by (rule wtl_all)
haftmann@33954
    45
  with pc show ?thesis by (simp add: phi_def wtc split: split_if_asm)
haftmann@33954
    46
qed
haftmann@33954
    47
haftmann@33954
    48
haftmann@33954
    49
lemma (in lbvs) wtl_stable:
haftmann@33954
    50
  assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>" 
haftmann@33954
    51
  assumes s0:  "s0 \<in> A" 
haftmann@33954
    52
  assumes pc:  "pc < length ins" 
haftmann@33954
    53
  shows "stable r step \<phi> pc"
haftmann@33954
    54
proof (unfold stable_def, clarify)
haftmann@33954
    55
  fix pc' s' assume step: "(pc',s') \<in> set (step pc (\<phi> ! pc))" 
haftmann@33954
    56
                      (is "(pc',s') \<in> set (?step pc)")
haftmann@33954
    57
  
haftmann@33954
    58
  from bounded pc step have pc': "pc' < length ins" by (rule boundedD)
haftmann@33954
    59
haftmann@33954
    60
  from wtl have tkpc: "wtl (take pc ins) c 0 s0 \<noteq> \<top>" (is "?s1 \<noteq> _") by (rule wtl_take)
haftmann@33954
    61
  from wtl have s2: "wtl (take (pc+1) ins) c 0 s0 \<noteq> \<top>" (is "?s2 \<noteq> _") by (rule wtl_take)
haftmann@33954
    62
  
haftmann@33954
    63
  from wtl pc have wt_s1: "wtc c pc ?s1 \<noteq> \<top>" by (rule wtl_all)
haftmann@33954
    64
haftmann@33954
    65
  have c_Some: "\<forall>pc t. pc < length ins \<longrightarrow> c!pc \<noteq> \<bottom> \<longrightarrow> \<phi>!pc = c!pc" 
haftmann@33954
    66
    by (simp add: phi_def)
haftmann@33954
    67
  from pc have c_None: "c!pc = \<bottom> \<Longrightarrow> \<phi>!pc = ?s1" ..
haftmann@33954
    68
haftmann@33954
    69
  from wt_s1 pc c_None c_Some
haftmann@33954
    70
  have inst: "wtc c pc ?s1  = wti c pc (\<phi>!pc)"
haftmann@33954
    71
    by (simp add: wtc split: split_if_asm)
haftmann@33954
    72
haftmann@33954
    73
  from pres cert s0 wtl pc have "?s1 \<in> A" by (rule wtl_pres)
haftmann@33954
    74
  with pc c_Some cert c_None
haftmann@33954
    75
  have "\<phi>!pc \<in> A" by (cases "c!pc = \<bottom>") (auto dest: cert_okD1)
haftmann@33954
    76
  with pc pres
haftmann@33954
    77
  have step_in_A: "snd`set (?step pc) \<subseteq> A" by (auto dest: pres_typeD2)
haftmann@33954
    78
haftmann@33954
    79
  show "s' <=_r \<phi>!pc'" 
haftmann@33954
    80
  proof (cases "pc' = pc+1")
haftmann@33954
    81
    case True
haftmann@33954
    82
    with pc' cert
haftmann@33954
    83
    have cert_in_A: "c!(pc+1) \<in> A" by (auto dest: cert_okD1)
haftmann@33954
    84
    from True pc' have pc1: "pc+1 < length ins" by simp
haftmann@33954
    85
    with tkpc have "?s2 = wtc c pc ?s1" by - (rule wtl_Suc)
haftmann@33954
    86
    with inst 
haftmann@33954
    87
    have merge: "?s2 = merge c pc (?step pc) (c!(pc+1))" by (simp add: wti)
haftmann@33954
    88
    also    
haftmann@33954
    89
    from s2 merge have "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp
haftmann@33954
    90
    with cert_in_A step_in_A
haftmann@33954
    91
    have "?merge = (map snd [(p',t') \<leftarrow> ?step pc. p'=pc+1] ++_f (c!(pc+1)))"
haftmann@33954
    92
      by (rule merge_not_top_s) 
haftmann@33954
    93
    finally
haftmann@33954
    94
    have "s' <=_r ?s2" using step_in_A cert_in_A True step 
haftmann@33954
    95
      by (auto intro: pp_ub1')
haftmann@33954
    96
    also 
haftmann@33954
    97
    from wtl pc1 have "?s2 <=_r \<phi>!(pc+1)" by (rule wtl_suc_pc)
haftmann@33954
    98
    also note True [symmetric]
haftmann@33954
    99
    finally show ?thesis by simp    
haftmann@33954
   100
  next
haftmann@33954
   101
    case False
haftmann@33954
   102
    from wt_s1 inst
haftmann@33954
   103
    have "merge c pc (?step pc) (c!(pc+1)) \<noteq> \<top>" by (simp add: wti)
haftmann@33954
   104
    with step_in_A
haftmann@33954
   105
    have "\<forall>(pc', s')\<in>set (?step pc). pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" 
haftmann@33954
   106
      by - (rule merge_not_top)
haftmann@33954
   107
    with step False 
haftmann@33954
   108
    have ok: "s' <=_r c!pc'" by blast
haftmann@33954
   109
    moreover
haftmann@33954
   110
    from ok
haftmann@33954
   111
    have "c!pc' = \<bottom> \<Longrightarrow> s' = \<bottom>" by simp
haftmann@33954
   112
    moreover
haftmann@33954
   113
    from c_Some pc'
haftmann@33954
   114
    have "c!pc' \<noteq> \<bottom> \<Longrightarrow> \<phi>!pc' = c!pc'" by auto
haftmann@33954
   115
    ultimately
haftmann@33954
   116
    show ?thesis by (cases "c!pc' = \<bottom>") auto 
haftmann@33954
   117
  qed
haftmann@33954
   118
qed
haftmann@33954
   119
haftmann@33954
   120
  
haftmann@33954
   121
lemma (in lbvs) phi_not_top:
haftmann@33954
   122
  assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
haftmann@33954
   123
  assumes pc:  "pc < length ins"
haftmann@33954
   124
  shows "\<phi>!pc \<noteq> \<top>"
haftmann@33954
   125
proof (cases "c!pc = \<bottom>")
haftmann@33954
   126
  case False with pc
haftmann@33954
   127
  have "\<phi>!pc = c!pc" ..
haftmann@33954
   128
  also from cert pc have "\<dots> \<noteq> \<top>" by (rule cert_okD4)
haftmann@33954
   129
  finally show ?thesis .
haftmann@33954
   130
next
haftmann@33954
   131
  case True with pc
haftmann@33954
   132
  have "\<phi>!pc = wtl (take pc ins) c 0 s0" ..
haftmann@33954
   133
  also from wtl have "\<dots> \<noteq> \<top>" by (rule wtl_take)
haftmann@33954
   134
  finally show ?thesis .
haftmann@33954
   135
qed
haftmann@33954
   136
haftmann@33954
   137
lemma (in lbvs) phi_in_A:
haftmann@33954
   138
  assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
haftmann@33954
   139
  assumes s0:  "s0 \<in> A"
haftmann@33954
   140
  shows "\<phi> \<in> list (length ins) A"
haftmann@33954
   141
proof -
haftmann@33954
   142
  { fix x assume "x \<in> set \<phi>"
haftmann@33954
   143
    then obtain xs ys where "\<phi> = xs @ x # ys" 
haftmann@33954
   144
      by (auto simp add: in_set_conv_decomp)
haftmann@33954
   145
    then obtain pc where pc: "pc < length \<phi>" and x: "\<phi>!pc = x"
haftmann@33954
   146
      by (simp add: that [of "length xs"] nth_append)
haftmann@33954
   147
    
haftmann@33954
   148
    from pres cert wtl s0 pc
haftmann@33954
   149
    have "wtl (take pc ins) c 0 s0 \<in> A" by (auto intro!: wtl_pres)
haftmann@33954
   150
    moreover
haftmann@33954
   151
    from pc have "pc < length ins" by simp
haftmann@33954
   152
    with cert have "c!pc \<in> A" ..
haftmann@33954
   153
    ultimately
haftmann@33954
   154
    have "\<phi>!pc \<in> A" using pc by (simp add: phi_def)
haftmann@33954
   155
    hence "x \<in> A" using x by simp
haftmann@33954
   156
  } 
haftmann@33954
   157
  hence "set \<phi> \<subseteq> A" ..
haftmann@33954
   158
  thus ?thesis by (unfold list_def) simp
haftmann@33954
   159
qed
haftmann@33954
   160
haftmann@33954
   161
haftmann@33954
   162
lemma (in lbvs) phi0:
haftmann@33954
   163
  assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
haftmann@33954
   164
  assumes 0:   "0 < length ins"
haftmann@33954
   165
  shows "s0 <=_r \<phi>!0"
haftmann@33954
   166
proof (cases "c!0 = \<bottom>")
haftmann@33954
   167
  case True
haftmann@33954
   168
  with 0 have "\<phi>!0 = wtl (take 0 ins) c 0 s0" ..
haftmann@33954
   169
  moreover have "wtl (take 0 ins) c 0 s0 = s0" by simp
haftmann@33954
   170
  ultimately have "\<phi>!0 = s0" by simp
haftmann@33954
   171
  thus ?thesis by simp
haftmann@33954
   172
next
haftmann@33954
   173
  case False
haftmann@33954
   174
  with 0 have "phi!0 = c!0" ..
haftmann@33954
   175
  moreover 
haftmann@33954
   176
  from wtl have "wtl (take 1 ins) c 0 s0 \<noteq> \<top>"  by (rule wtl_take)
haftmann@33954
   177
  with 0 False 
haftmann@33954
   178
  have "s0 <=_r c!0" by (auto simp add: neq_Nil_conv wtc split: split_if_asm)
haftmann@33954
   179
  ultimately
haftmann@33954
   180
  show ?thesis by simp
haftmann@33954
   181
qed
haftmann@33954
   182
haftmann@33954
   183
haftmann@33954
   184
theorem (in lbvs) wtl_sound:
haftmann@33954
   185
  assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>" 
haftmann@33954
   186
  assumes s0: "s0 \<in> A" 
haftmann@33954
   187
  shows "\<exists>ts. wt_step r \<top> step ts"
haftmann@33954
   188
proof -
haftmann@33954
   189
  have "wt_step r \<top> step \<phi>"
haftmann@33954
   190
  proof (unfold wt_step_def, intro strip conjI)
haftmann@33954
   191
    fix pc assume "pc < length \<phi>"
haftmann@33954
   192
    then have pc: "pc < length ins" by simp
haftmann@33954
   193
    with wtl show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
haftmann@33954
   194
    from wtl s0 pc show "stable r step \<phi> pc" by (rule wtl_stable)
haftmann@33954
   195
  qed
haftmann@33954
   196
  thus ?thesis ..
haftmann@33954
   197
qed
haftmann@33954
   198
haftmann@33954
   199
haftmann@33954
   200
theorem (in lbvs) wtl_sound_strong:
haftmann@33954
   201
  assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>" 
haftmann@33954
   202
  assumes s0: "s0 \<in> A" 
haftmann@33954
   203
  assumes nz: "0 < length ins"
haftmann@33954
   204
  shows "\<exists>ts \<in> list (length ins) A. wt_step r \<top> step ts \<and> s0 <=_r ts!0"
haftmann@33954
   205
proof -
haftmann@33954
   206
  from wtl s0 have "\<phi> \<in> list (length ins) A" by (rule phi_in_A)
haftmann@33954
   207
  moreover
haftmann@33954
   208
  have "wt_step r \<top> step \<phi>"
haftmann@33954
   209
  proof (unfold wt_step_def, intro strip conjI)
haftmann@33954
   210
    fix pc assume "pc < length \<phi>"
haftmann@33954
   211
    then have pc: "pc < length ins" by simp
haftmann@33954
   212
    with wtl show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
haftmann@33954
   213
    from wtl s0 pc show "stable r step \<phi> pc" by (rule wtl_stable)
haftmann@33954
   214
  qed
haftmann@33954
   215
  moreover
haftmann@33954
   216
  from wtl nz have "s0 <=_r \<phi>!0" by (rule phi0)
haftmann@33954
   217
  ultimately
haftmann@33954
   218
  show ?thesis by fast
haftmann@33954
   219
qed
haftmann@33954
   220
haftmann@33954
   221
end