4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 |
5 |
6 The invariant for the type safety proof. |
6 The invariant for the type safety proof. |
7 *) |
7 *) |
8 |
8 |
9 header "Type Safety Invariant" |
9 header "BV Type Safety Invariant" |
10 |
10 |
11 theory Correct = BVSpec: |
11 theory Correct = BVSpec: |
12 |
12 |
13 constdefs |
13 constdefs |
14 approx_val :: "[jvm_prog,aheap,val,ty err] => bool" |
14 approx_val :: "[jvm_prog,aheap,val,ty err] => bool" |
15 "approx_val G h v any == case any of Err => True | Ok T => G,h\<turnstile>v::\<preceq>T" |
15 "approx_val G h v any == case any of Err => True | Ok T => G,h\<turnstile>v::\<preceq>T" |
16 |
16 |
17 approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool" |
17 approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool" |
18 "approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT" |
18 "approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT" |
19 |
19 |
20 approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool" |
20 approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool" |
21 "approx_stk G hp stk ST == approx_loc G hp stk (map Ok ST)" |
21 "approx_stk G hp stk ST == approx_loc G hp stk (map Ok ST)" |
22 |
22 |
23 correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool" |
23 correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool" |
24 "correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc). |
24 "correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc). |
25 approx_stk G hp stk ST \<and> approx_loc G hp loc LT \<and> |
25 approx_stk G hp stk ST \<and> approx_loc G hp loc LT \<and> |
26 pc < length ins \<and> length loc=length(snd sig)+maxl+1" |
26 pc < length ins \<and> length loc=length(snd sig)+maxl+1" |
27 |
27 |
28 correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] => frame => bool" |
28 correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] |
29 "correct_frame_opt G hp s == case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t" |
29 => frame => bool" |
|
30 "correct_frame_opt G hp s == |
|
31 case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t" |
30 |
32 |
31 |
33 |
32 consts |
34 consts |
33 correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] => bool" |
35 correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] => bool" |
34 primrec |
36 primrec |
91 lemma approx_val_Null: |
93 lemma approx_val_Null: |
92 "approx_val G hp Null (Ok (RefT x))" |
94 "approx_val G hp Null (Ok (RefT x))" |
93 by (auto intro: null simp add: approx_val_def) |
95 by (auto intro: null simp add: approx_val_def) |
94 |
96 |
95 lemma approx_val_imp_approx_val_assConvertible [rule_format]: |
97 lemma approx_val_imp_approx_val_assConvertible [rule_format]: |
96 "wf_prog wt G ==> approx_val G hp v (Ok T) --> G\<turnstile> T\<preceq>T' --> approx_val G hp v (Ok T')" |
98 "wf_prog wt G ==> approx_val G hp v (Ok T) --> G\<turnstile> T\<preceq>T' |
|
99 --> approx_val G hp v (Ok T')" |
97 by (cases T) (auto intro: conf_widen simp add: approx_val_def) |
100 by (cases T) (auto intro: conf_widen simp add: approx_val_def) |
98 |
101 |
99 lemma approx_val_imp_approx_val_sup_heap [rule_format]: |
102 lemma approx_val_imp_approx_val_sup_heap [rule_format]: |
100 "approx_val G hp v at --> hp \<le>| hp' --> approx_val G hp' v at" |
103 "approx_val G hp v at --> hp \<le>| hp' --> approx_val G hp' v at" |
101 apply (simp add: approx_val_def split: err.split) |
104 apply (simp add: approx_val_def split: err.split) |
102 apply (blast intro: conf_hext) |
105 apply (blast intro: conf_hext) |
103 . |
106 done |
104 |
107 |
105 lemma approx_val_imp_approx_val_heap_update: |
108 lemma approx_val_imp_approx_val_heap_update: |
106 "[|hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'|] |
109 "[|hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'|] |
107 ==> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T" |
110 ==> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T" |
108 by (cases v, auto simp add: obj_ty_def conf_def) |
111 by (cases v, auto simp add: obj_ty_def conf_def) |
109 |
112 |
110 lemma approx_val_imp_approx_val_sup [rule_format]: |
113 lemma approx_val_imp_approx_val_sup [rule_format]: |
111 "wf_prog wt G ==> (approx_val G h v us) --> (G \<turnstile> us <=o us') --> (approx_val G h v us')" |
114 "wf_prog wt G ==> (approx_val G h v us) --> (G \<turnstile> us <=o us') |
|
115 --> (approx_val G h v us')" |
112 apply (simp add: sup_PTS_eq approx_val_def split: err.split) |
116 apply (simp add: sup_PTS_eq approx_val_def split: err.split) |
113 apply (blast intro: conf_widen) |
117 apply (blast intro: conf_widen) |
114 . |
118 done |
115 |
119 |
116 lemma approx_loc_imp_approx_val_sup: |
120 lemma approx_loc_imp_approx_val_sup: |
117 "[|wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \<turnstile> LT!idx <=o at|] |
121 "[| wf_prog wt G; approx_loc G hp loc LT; idx < length LT; |
|
122 v = loc!idx; G \<turnstile> LT!idx <=o at |] |
118 ==> approx_val G hp v at" |
123 ==> approx_val G hp v at" |
119 apply (unfold approx_loc_def) |
124 apply (unfold approx_loc_def) |
120 apply (unfold list_all2_def) |
125 apply (unfold list_all2_def) |
121 apply (auto intro: approx_val_imp_approx_val_sup simp add: split_def all_set_conv_all_nth) |
126 apply (auto intro: approx_val_imp_approx_val_sup |
122 . |
127 simp add: split_def all_set_conv_all_nth) |
|
128 done |
123 |
129 |
124 |
130 |
125 (** approx_loc **) |
131 (** approx_loc **) |
126 |
132 |
127 lemma approx_loc_Cons [iff]: |
133 lemma approx_loc_Cons [iff]: |
128 "approx_loc G hp (s#xs) (l#ls) = (approx_val G hp s l \<and> approx_loc G hp xs ls)" |
134 "approx_loc G hp (s#xs) (l#ls) = |
|
135 (approx_val G hp s l \<and> approx_loc G hp xs ls)" |
129 by (simp add: approx_loc_def) |
136 by (simp add: approx_loc_def) |
130 |
137 |
131 lemma assConv_approx_stk_imp_approx_loc [rule_format]: |
138 lemma assConv_approx_stk_imp_approx_loc [rule_format]: |
132 "wf_prog wt G ==> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) |
139 "wf_prog wt G ==> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) |
133 --> length tys_n = length ts --> approx_stk G hp s tys_n --> |
140 --> length tys_n = length ts --> approx_stk G hp s tys_n --> |
134 approx_loc G hp s (map Ok ts)" |
141 approx_loc G hp s (map Ok ts)" |
135 apply (unfold approx_stk_def approx_loc_def list_all2_def) |
142 apply (unfold approx_stk_def approx_loc_def list_all2_def) |
136 apply (clarsimp simp add: all_set_conv_all_nth) |
143 apply (clarsimp simp add: all_set_conv_all_nth) |
137 apply (rule approx_val_imp_approx_val_assConvertible) |
144 apply (rule approx_val_imp_approx_val_assConvertible) |
138 apply auto |
145 apply auto |
139 . |
146 done |
140 |
147 |
141 |
148 |
142 lemma approx_loc_imp_approx_loc_sup_heap [rule_format]: |
149 lemma approx_loc_imp_approx_loc_sup_heap [rule_format]: |
143 "\<forall>lvars. approx_loc G hp lvars lt --> hp \<le>| hp' --> approx_loc G hp' lvars lt" |
150 "\<forall>lvars. approx_loc G hp lvars lt --> hp \<le>| hp' |
|
151 --> approx_loc G hp' lvars lt" |
144 apply (unfold approx_loc_def list_all2_def) |
152 apply (unfold approx_loc_def list_all2_def) |
145 apply (cases lt) |
153 apply (cases lt) |
146 apply simp |
154 apply simp |
147 apply clarsimp |
155 apply clarsimp |
148 apply (rule approx_val_imp_approx_val_sup_heap) |
156 apply (rule approx_val_imp_approx_val_sup_heap) |
149 apply auto |
157 apply auto |
150 . |
158 done |
151 |
159 |
152 lemma approx_loc_imp_approx_loc_sup [rule_format]: |
160 lemma approx_loc_imp_approx_loc_sup [rule_format]: |
153 "wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt' --> approx_loc G hp lvars lt'" |
161 "wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt' |
|
162 --> approx_loc G hp lvars lt'" |
154 apply (unfold sup_loc_def approx_loc_def list_all2_def) |
163 apply (unfold sup_loc_def approx_loc_def list_all2_def) |
155 apply (auto simp add: all_set_conv_all_nth) |
164 apply (auto simp add: all_set_conv_all_nth) |
156 apply (auto elim: approx_val_imp_approx_val_sup) |
165 apply (auto elim: approx_val_imp_approx_val_sup) |
157 . |
166 done |
158 |
167 |
159 |
168 |
160 lemma approx_loc_imp_approx_loc_subst [rule_format]: |
169 lemma approx_loc_imp_approx_loc_subst [rule_format]: |
161 "\<forall>loc idx x X. (approx_loc G hp loc LT) --> (approx_val G hp x X) |
170 "\<forall>loc idx x X. (approx_loc G hp loc LT) --> (approx_val G hp x X) |
162 --> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))" |
171 --> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))" |
163 apply (unfold approx_loc_def list_all2_def) |
172 apply (unfold approx_loc_def list_all2_def) |
164 apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update) |
173 apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update) |
165 . |
174 done |
166 |
175 |
167 |
176 |
168 lemmas [cong] = conj_cong |
177 lemmas [cong] = conj_cong |
169 |
178 |
170 lemma approx_loc_append [rule_format]: |
179 lemma approx_loc_append [rule_format]: |
171 "\<forall>L1 l2 L2. length l1=length L1 --> |
180 "\<forall>L1 l2 L2. length l1=length L1 --> |
172 approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)" |
181 approx_loc G hp (l1@l2) (L1@L2) = |
|
182 (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)" |
173 apply (unfold approx_loc_def list_all2_def) |
183 apply (unfold approx_loc_def list_all2_def) |
174 apply simp |
184 apply simp |
175 apply blast |
185 apply blast |
176 . |
186 done |
177 |
187 |
178 lemmas [cong del] = conj_cong |
188 lemmas [cong del] = conj_cong |
179 |
189 |
180 |
190 |
181 (** approx_stk **) |
191 (** approx_stk **) |
182 |
192 |
183 lemma approx_stk_rev_lem: |
193 lemma approx_stk_rev_lem: |
184 "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t" |
194 "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t" |
185 apply (unfold approx_stk_def approx_loc_def list_all2_def) |
195 apply (unfold approx_stk_def approx_loc_def list_all2_def) |
186 apply (auto simp add: zip_rev sym [OF rev_map]) |
196 apply (auto simp add: zip_rev sym [OF rev_map]) |
187 . |
197 done |
188 |
198 |
189 lemma approx_stk_rev: |
199 lemma approx_stk_rev: |
190 "approx_stk G hp (rev s) t = approx_stk G hp s (rev t)" |
200 "approx_stk G hp (rev s) t = approx_stk G hp s (rev t)" |
191 by (auto intro: subst [OF approx_stk_rev_lem]) |
201 by (auto intro: subst [OF approx_stk_rev_lem]) |
192 |
202 |
193 |
203 |
194 lemma approx_stk_imp_approx_stk_sup_heap [rule_format]: |
204 lemma approx_stk_imp_approx_stk_sup_heap [rule_format]: |
195 "\<forall>lvars. approx_stk G hp lvars lt --> hp \<le>| hp' --> approx_stk G hp' lvars lt" |
205 "\<forall>lvars. approx_stk G hp lvars lt --> hp \<le>| hp' |
|
206 --> approx_stk G hp' lvars lt" |
196 by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def) |
207 by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def) |
197 |
208 |
198 lemma approx_stk_imp_approx_stk_sup [rule_format]: |
209 lemma approx_stk_imp_approx_stk_sup [rule_format]: |
199 "wf_prog wt G ==> approx_stk G hp lvars st --> (G \<turnstile> map Ok st <=l (map Ok st')) |
210 "wf_prog wt G ==> approx_stk G hp lvars st --> (G \<turnstile> map Ok st <=l (map Ok st')) |
200 --> approx_stk G hp lvars st'" |
211 --> approx_stk G hp lvars st'" |
241 lemma oconf_imp_oconf_heap_newref [rule_format]: |
252 lemma oconf_imp_oconf_heap_newref [rule_format]: |
242 "hp x = None --> G,hp\<turnstile>obj\<surd> --> G,hp\<turnstile>obj'\<surd> --> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>" |
253 "hp x = None --> G,hp\<turnstile>obj\<surd> --> G,hp\<turnstile>obj'\<surd> --> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>" |
243 apply (unfold oconf_def lconf_def) |
254 apply (unfold oconf_def lconf_def) |
244 apply simp |
255 apply simp |
245 apply (fast intro: conf_hext sup_heap_newref) |
256 apply (fast intro: conf_hext sup_heap_newref) |
246 . |
257 done |
247 |
258 |
248 |
259 |
249 lemma oconf_imp_oconf_heap_update [rule_format]: |
260 lemma oconf_imp_oconf_heap_update [rule_format]: |
250 "hp a = Some obj' --> obj_ty obj' = obj_ty obj'' --> G,hp\<turnstile>obj\<surd> |
261 "hp a = Some obj' --> obj_ty obj' = obj_ty obj'' --> G,hp\<turnstile>obj\<surd> |
251 --> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>" |
262 --> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>" |
252 apply (unfold oconf_def lconf_def) |
263 apply (unfold oconf_def lconf_def) |
253 apply simp |
264 apply simp |
254 apply (force intro: approx_val_imp_approx_val_heap_update) |
265 apply (force intro: approx_val_imp_approx_val_heap_update) |
255 . |
266 done |
256 |
267 |
257 |
268 |
258 (** hconf **) |
269 (** hconf **) |
259 |
270 |
260 |
271 |
261 lemma hconf_imp_hconf_newref [rule_format]: |
272 lemma hconf_imp_hconf_newref [rule_format]: |
262 "hp x = None --> G\<turnstile>h hp\<surd> --> G,hp\<turnstile>obj\<surd> --> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>" |
273 "hp x = None --> G\<turnstile>h hp\<surd> --> G,hp\<turnstile>obj\<surd> --> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>" |
263 apply (simp add: hconf_def) |
274 apply (simp add: hconf_def) |
264 apply (fast intro: oconf_imp_oconf_heap_newref) |
275 apply (fast intro: oconf_imp_oconf_heap_newref) |
265 . |
276 done |
266 |
277 |
267 lemma hconf_imp_hconf_field_update [rule_format]: |
278 lemma hconf_imp_hconf_field_update [rule_format]: |
268 "map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and> |
279 "map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and> |
269 G,hp\<turnstile>v::\<preceq>T \<and> G\<turnstile>h hp\<surd> --> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>" |
280 G,hp\<turnstile>v::\<preceq>T \<and> G\<turnstile>h hp\<surd> --> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>" |
270 apply (simp add: hconf_def) |
281 apply (simp add: hconf_def) |
271 apply (force intro: oconf_imp_oconf_heap_update oconf_imp_oconf_field_update |
282 apply (force intro: oconf_imp_oconf_heap_update oconf_imp_oconf_field_update |
272 simp add: obj_ty_def) |
283 simp add: obj_ty_def) |
273 . |
284 done |
274 |
285 |
275 (** correct_frames **) |
286 (** correct_frames **) |
276 |
287 |
277 lemmas [simp del] = fun_upd_apply |
288 lemmas [simp del] = fun_upd_apply |
278 |
289 |