source: Deliverables/D3.1/C-semantics/CexecSound.ma @ 485

Last change on this file since 485 was 485, checked in by campbell, 9 years ago

Fix treatment of pointers in initialisation data, a little like later versions
of CompCert?. Remove obsolete Init_pointer.

File size: 23.0 KB
Line 
1include "Cexec.ma".
2
3include "Plogic/connectives.ma".
4
5nlemma exec_bool_of_val_sound: ∀v,ty,r.
6 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
7#v ty r;
8ncases v; ##[ ##| #i ##| #f ##| #r1 ##| #r b of ##]
9ncases ty; ##[ ##2,11,20,29,38: #sz sg ##| ##3,12,21,30,39: #sz ##| ##4,13,22,31,40: #r ty ##| ##5,14,23,32,41: #r ty n ##| ##6,15,24,33,42: #args rty ##| ##7,8,16,17,25,26,34,35,43,44: #id fs ##| ##9,18,27,36,45: #r id ##]
10#H; nwhd in H:(??%?); ndestruct;
11##[ nlapply (eq_spec i zero); nelim (eq i zero);
12  ##[ #e; nrewrite > e; napply bool_of_val_false; //;
13  ##| #ne; napply bool_of_val_true; /2/;
14  ##]
15##| nelim (eq_dec f Fzero);
16  ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); napply bool_of_val_false; //;
17  ##| #ne; nrewrite > (Feq_zero_false …); //; napply bool_of_val_true; /2/;
18  ##]
19##| napply bool_of_val_false; //
20##| napply bool_of_val_true; //
21##] nqed.
22
23nlemma bool_val_distinct: Vtrue ≠ Vfalse.
24@; #H; nwhd in H:(??%%); ndestruct; napply (absurd ? e0 one_not_zero);
25nqed.
26
27nlemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) →
28  if b then is_true v ty else is_false v ty.
29#v ty b; ncases b; #H; ninversion H; #v' ty' H' ev et ev; //;
30napply False_ind; napply (absurd ? ev ?);
31##[ ##2: napply sym_neq ##] napply bool_val_distinct;
32nqed.
33
34nlemma try_cast_null_sound: ∀m,i,ty,ty',v'. try_cast_null m i ty ty' = OK ? v' → cast m (Vint i) ty ty' v'.
35#m i ty ty' v';
36nwhd in ⊢ (??%? → ?);
37nlapply (eq_spec i zero); ncases (eq i zero);
38##[ #e; nrewrite > e;
39    ncases ty; ##[ ##| #sz sg ##| #fs ##| #sp ty ##| #sp ty n ##| #args rty ##| #id fs ##| #id fs ##| #r id ##]
40    nwhd in ⊢ (??%? → ?); #H; ndestruct;
41    ncases ty' in H ⊢ %; ##[ ##| #sz sg ##| #fs ##| #sp ty ##| #sp ty n ##| #args rty ##| #id fs ##| #id fs ##| #r id ##]
42    nwhd in ⊢ (??%? → ?); #H; ndestruct (H); napply cast_ip_z; //;
43##| #_; nwhd in ⊢ (??%? → ?); #H; ndestruct
44##]
45nqed.
46
47ndefinition exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'.
48#m v ty ty' v';
49ncases v;
50##[ #H; nwhd in H:(??%?); ndestruct;
51##| #i; ncases ty;
52  ##[ #H; nwhd in H:(??%?); ndestruct;
53  ##| ##3: #a; #H; nwhd in H:(??%?); ndestruct;
54  ##| ##7,8,9: #a b; #H; nwhd in H:(??%?); ndestruct;
55  ##| #sz1 si1; ncases ty';
56    ##[ #H; nwhd in H:(??%?); ndestruct;
57    ##| ##3: #a; #H; nwhd in H:(??%?); ndestruct; //
58    ##| ##2,7,8,9: #a b; #H; nwhd in H:(??%?); ndestruct; //
59    ##| ##4,5,6: ##[ #sp ty''; nletin t ≝ (Tpointer sp ty'')
60                 ##| #sp ty'' n; nletin t ≝ (Tarray sp ty'' n)
61                 ##| #args rty; nletin t ≝ (Tfunction args rty) ##]
62        nwhd in ⊢ (??%? → ?);
63        nlapply (try_cast_null_sound m i (Tint sz1 si1) t v');
64        ncases (try_cast_null m i (Tint sz1 si1) t);
65        ##[ ##1,3,5: #v''; #H' e; napply H'; napply e;
66        ##| ##*: #_; nwhd in ⊢ (??%? → ?); #H; ndestruct (H);
67        ##]
68    ##]
69  ##| ##*: ##[ #sp ty''; nletin t ≝ (Tpointer sp ty'')
70           ##| #sp ty'' n; nletin t ≝ (Tarray sp ty'' n)
71           ##| #args rty; nletin t ≝ (Tfunction args rty) ##]
72        nwhd in ⊢ (??%? → ?);
73        nlapply (try_cast_null_sound m i t ty' v');
74        ncases (try_cast_null m i t ty');
75        ##[ ##1,3,5: #v''; #H' e; napply H'; napply e;
76        ##| ##*: #_; nwhd in ⊢ (??%? → ?); #H; ndestruct (H);
77        ##]
78  ##]
79##| #f; ncases ty;  ##[ ##3: #x; ##| ##2,4,6,7,8,9: #x y; ##| ##5: #x y z; ##]
80                    ##[ ncases ty'; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
81                        nwhd in e:(??%?); ndestruct; //;
82                    ##| ##*: #e; nwhd in e:(??%?); ndestruct
83                    ##]
84##| #r; ncases ty; ##[ ##3: #x; ##| ##2,4,6,7,8,9: #x y; ##| ##5: #x y z; ##]
85    nwhd in ⊢ (??%? → ?); #H; ndestruct; ncases (eq_region_dec r ?) in H;
86    nwhd in ⊢ (? → ??%? → ?); #H1 H2; ndestruct;
87    ncases ty' in H2; nnormalize; ntry #a; ntry #b; ntry #c; ntry #d; ndestruct;
88    napply cast_pp_z; //;
89##| #sp b of; nwhd in ⊢ (??%? → ?); #e;
90    nelim (bind_inversion ????? e); #s; *; #es e';
91    nelim (bind_inversion ????? e'); #u; *; #eu e'';
92    nelim (bind_inversion ????? e''); #s'; *; #es' e''';
93    ncut (type_region ty s);
94    ##[ ncases ty in es:(??%?) ⊢ %; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
95        nwhd in e:(??%?); ndestruct; //;
96    ##| #Hty;
97        ncut (type_region ty' s');
98        ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
99            nwhd in e:(??%?); ndestruct; //;
100        ##| #Hty';
101            ncut (s = sp). nelim (eq_region_dec sp s) in eu; //; nnormalize; #_; #e; ndestruct.
102            #e; nrewrite < e;
103            nwhd in match (is_pointer_compat ??) in e''';
104            ncases (pointer_compat_dec (block_space m b) s') in e'''; #Hcompat e''';
105            nwhd in e''':(??%?); ndestruct (e'''); /2/
106        ##]
107    ##]
108##] nqed.
109
110nlet rec expr_lvalue_ind
111  (P:expr → Prop)
112  (Q:expr_descr → type → Prop)
113  (ci:∀ty,i.P (Expr (Econst_int i) ty))
114  (cf:∀ty,f.P (Expr (Econst_float f) ty))
115  (lv:∀e,ty. Q e ty → Plvalue P e ty)
116  (vr:∀v,ty.Q (Evar v) ty)
117  (dr:∀e,ty.P e → Q (Ederef e) ty)
118  (ao:∀ty,e,ty'.Q e ty' → P (Expr (Eaddrof (Expr e ty')) ty))
119  (uo:∀ty,op,e.P e → P (Expr (Eunop op e) ty))
120  (bo:∀ty,op,e1,e2.P e1 → P e2 → P (Expr (Ebinop op e1 e2) ty))
121  (ca:∀ty,ty',e.P e → P (Expr (Ecast ty' e) ty))
122  (cd:∀ty,e1,e2,e3.P e1 → P e2 → P e3 → P (Expr (Econdition e1 e2 e3) ty))
123  (ab:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eandbool e1 e2) ty))
124  (ob:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eorbool e1 e2) ty))
125  (sz:∀ty,ty'. P (Expr (Esizeof ty') ty))
126  (fl:∀ty,e,ty',i. Q e ty' → Q (Efield (Expr e ty') i) ty)
127  (co:∀ty,l,e. P e → P (Expr (Ecost l e) ty))
128  (xx:∀e,ty. is_not_lvalue e → Q e ty)
129  (e:expr) on e : P e ≝
130match e with
131[ Expr e' ty ⇒
132  match e' with
133  [ Econst_int i ⇒ ci ty i
134  | Econst_float f ⇒ cf ty f
135  | Evar v ⇒ lv (Evar v) ty (vr v ty)
136  | Ederef e'' ⇒ lv (Ederef e'') ty (dr e'' ty (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e''))
137  | Eaddrof e'' ⇒ match e'' with [ Expr e0 ty0 ⇒ ao ty e0 ty0 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e0 ty0) ]
138  | Eunop op e'' ⇒ uo ty op e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
139  | Ebinop op e1 e2 ⇒ bo ty op e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
140  | Ecast ty' e'' ⇒ ca ty ty' e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
141  | Econdition e1 e2 e3 ⇒ cd ty e1 e2 e3 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e3)
142  | Eandbool e1 e2 ⇒ ab ty e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
143  | Eorbool e1 e2 ⇒ ob ty e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
144  | Esizeof ty' ⇒ sz ty ty'
145  | Efield e'' i ⇒ match e'' with [ Expr ef tyf ⇒ lv (Efield (Expr ef tyf) i) ty (fl ty ef tyf i (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx ef tyf)) ]
146  | Ecost l e'' ⇒ co ty l e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
147  ]
148]
149and lvalue_expr_ind
150  (P:expr → Prop)
151  (Q:expr_descr → type → Prop)
152  (ci:∀ty,i.P (Expr (Econst_int i) ty))
153  (cf:∀ty,f.P (Expr (Econst_float f) ty))
154  (lv:∀e,ty. Q e ty → Plvalue P e ty)
155  (vr:∀v,ty.Q (Evar v) ty)
156  (dr:∀e,ty.P e → Q (Ederef e) ty)
157  (ao:∀ty,e,ty'.Q e ty' → P (Expr (Eaddrof (Expr e ty')) ty))
158  (uo:∀ty,op,e.P e → P (Expr (Eunop op e) ty))
159  (bo:∀ty,op,e1,e2.P e1 → P e2 → P (Expr (Ebinop op e1 e2) ty))
160  (ca:∀ty,ty',e.P e → P (Expr (Ecast ty' e) ty))
161  (cd:∀ty,e1,e2,e3.P e1 → P e2 → P e3 → P (Expr (Econdition e1 e2 e3) ty))
162  (ab:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eandbool e1 e2) ty))
163  (ob:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eorbool e1 e2) ty))
164  (sz:∀ty,ty'. P (Expr (Esizeof ty') ty))
165  (fl:∀ty,e,ty',i. Q e ty' → Q (Efield (Expr e ty') i) ty)
166  (co:∀ty,l,e. P e → P (Expr (Ecost l e) ty))
167  (xx:∀e,ty. is_not_lvalue e → Q e ty)
168  (e:expr_descr) (ty:type) on e : Q e ty ≝
169  match e return λe0. Q e0 ty with
170  [ Evar v ⇒ vr v ty
171  | Ederef e'' ⇒ dr e'' ty (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
172  | Efield e' i ⇒ match e' return λe1.Q (Efield e1 i) ty with [ Expr e'' ty'' ⇒ fl ty e'' ty'' i (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'' ty'') ]
173  | _ ⇒ xx ? ty ?
174  ]. nwhd; napply I; nqed.
175
176
177ntheorem exec_expr_sound: ∀ge:genv. ∀en:env. ∀m:mem. ∀e:expr.
178(P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)).
179#ge en m e; napply (expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e);
180##[ ##1,2: #ty c; nwhd; //;
181(* expressions that are lvalues *)
182##| #e' ty; ncases e'; //; ##[ #i He' ##| #e He' ##| #e i He' ##] nwhd in He' ⊢ %;
183    napply bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
184    napply opt_bind_OK;  #vl evl; nwhd in evl:(??%?); napply (eval_Elvalue … evl);
185    nrewrite > H in He'; #He'; napply He';
186##| #v ty;
187    nwhd in ⊢ (???%);
188    nlapply (refl ? (get ident PTree block v en));
189    ncases (get ident PTree block v en) in ⊢ (???% → %);
190    ##[ #eget; napply opt_bind_OK; #sploc; ncases sploc; #sp loc efind;
191        nwhd; napply (eval_Evar_global … eget efind);
192    ##| #loc eget; napply (eval_Evar_local … eget);
193    ##]
194##| #ty e He; nwhd in ⊢ (???%);
195    napply bind2_OK; #v; ncases v; //; #sp l ofs tr Hv; nwhd;
196    napply eval_Ederef; nrewrite > Hv in He; #He; napply He;
197##| #ty e'' ty'' He''; napply bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
198    nwhd; napply eval_Eaddrof; nrewrite > H in He''; #He''; napply He'';
199##| #ty op e1 He1; napply bind2_OK; #v1 tr Hv1;
200    napply opt_bind_OK; #v ev;
201    napply (eval_Eunop … ev);
202    nrewrite > Hv1 in He1; #He1; napply He1;
203##| #ty op e1 e2 He1 He2;
204    napply bind2_OK; #v1 tr1 ev1; nrewrite > ev1 in He1; #He1;
205    napply bind2_OK; #v2 tr2 ev2; nrewrite > ev2 in He2; #He2;
206    napply opt_bind_OK; #v ev; nwhd in He1 He2; nwhd;
207    napply (eval_Ebinop … He1 He2 ev);
208##| #ty ty' e' He';
209    napply bind2_OK; #v tr Hv; nrewrite > Hv in He'; #He';
210    napply bind_OK; #v' ev';
211    napply (eval_Ecast … He' ?);
212    /2/;
213##| #ty e1 e2 e3 He1 He2 He3;
214    napply bind2_OK; #vb tr1 Hvb; nrewrite > Hvb in He1; #He1;
215    napply bind_OK; #b;
216    ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
217    napply bind2_OK; #v tr Hv;
218    ##[ nrewrite > Hv in He2; #He2; nwhd in He2 Hv:(??%?) ⊢%;
219        napply (eval_Econdition_true … He1 ? He2);  napply (bool_of ??? Hb);
220    ##| nrewrite > Hv in He3; #He3; nwhd in He3 Hv:(??%?) ⊢%;
221        napply (eval_Econdition_false … He1 ? He3);  napply (bool_of ??? Hb);
222    ##]
223##| #ty e1 e2 He1 He2;
224    napply bind2_OK; #v1 tr1 Hv1; nrewrite > Hv1 in He1; #He1;
225    napply bind_OK; #b1; ncases b1; #eb1; nlapply (exec_bool_of_val_sound … eb1); #Hb1;
226    ##[ napply bind2_OK; #v2 tr2 Hv2; nrewrite > Hv2 in He2; #He2;
227        napply bind_OK; #b2 eb2;
228        napply (eval_Eandbool_2 … He1 … He2);
229        ##[ napply (bool_of … Hb1); ##| napply (exec_bool_of_val_sound … eb2); ##]
230    ##| napply (eval_Eandbool_1 … He1); napply (bool_of … Hb1);
231    ##]
232##| #ty e1 e2 He1 He2;
233    napply bind2_OK; #v1 tr1 Hv1; nrewrite > Hv1 in He1; #He1;
234    napply bind_OK; #b1; ncases b1; #eb1; nlapply (exec_bool_of_val_sound … eb1); #Hb1;
235    ##[ napply (eval_Eorbool_1 … He1); napply (bool_of … Hb1);
236    ##| napply bind2_OK; #v2 tr2 Hv2; nrewrite > Hv2 in He2; #He2;
237        napply bind_OK; #b2 eb2;
238        napply (eval_Eorbool_2 … He1 … He2);
239        ##[ napply (bool_of … Hb1); ##| napply (exec_bool_of_val_sound … eb2); ##]
240    ##]
241##| #ty ty'; nwhd; //
242##| #ty e' ty' i; ncases ty'; //;
243    ##[ #id fs He'; napply bind2_OK;  #x; ncases x; #sp l ofs H;
244        napply bind_OK; #delta Hdelta; nrewrite > H in He'; #He';
245        napply (eval_Efield_struct …  He' (refl ??) Hdelta);
246    ##| #id fs He'; napply bind2_OK;  #x; ncases x; #sp l ofs H;
247        nrewrite > H in He'; #He';
248        napply (eval_Efield_union … He' (refl ??));
249    ##]
250##| #ty l e' He'; napply bind2_OK; #v tr1 H; nrewrite > H in He'; #He';
251    napply (eval_Ecost … He');
252(* exec_lvalue fails on non-lvalues. *)
253##| #e' ty; ncases e';
254    ##[ ##1,2,5,12: #a H ##| ##3,4: #a; * ##| ##13,14: #a b; * ##| ##6,8,10,11: #a b H ##| ##7,9: #a b c H ##]
255    napply I;
256##] nqed.
257
258nlemma addrof_eval_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
259eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr sp loc off) tr →
260eval_lvalue ge en m e sp loc off tr.
261#ge en m e sp loc off tr ty H; ninversion H;
262##[ ##1,2,5: #a b H; napply False_ind; ndestruct (H);
263##| #a b c d e f g H1 i H2; nrewrite < H2 in H1; #H1; napply False_ind;
264    napply (eval_lvalue_inv_ind … H1);
265    ##[ #a b c d bad; ndestruct (bad);
266    ##| #a b c d e f bad; ndestruct (bad);
267    ##| #a b c d e f g bad; ndestruct (bad);
268    ##| #a b c d e f g  h i j k l m n bad; napply False_ind; ndestruct (bad);
269    ##| #a b c d e f g h i j k l bad; ndestruct (bad);
270    ##]
271##| #e' ty' sp' loc' ofs' tr' H e1 e2 e3; ndestruct (e1 e2 e3); napply H;
272##| #a b c d e f g h i bad; ndestruct (bad);
273##| #a b c d e f g h i j k l k l bad; ndestruct (bad);
274##| #a b c d e f g h i j k l m bad; ndestruct (bad);
275##| #a b c d e f g h i j k l m bad; ndestruct (bad);
276##| #a b c d e f g h bad; ndestruct (bad);
277##| #a b c d e f g h i j k l m n bad; ndestruct (bad);
278##| #a b c d e f g h bad; ndestruct (bad);
279##| #a b c d e f g h i j k l m n bad;  ndestruct (bad);
280##| #a b c d e f g h i bad; ndestruct (bad);
281##| #a b c d e f g bad; ndestruct (bad);
282##] nqed.
283
284nlemma addrof_exec_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
285exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉 →
286exec_expr ge en m (Expr (Eaddrof e) ty) = OK ? 〈Vptr sp loc off, tr〉.
287#ge en m e sp loc off tr ty H; nwhd in ⊢ (??%?);
288nrewrite > H; //;
289nqed.
290
291ntheorem exec_lvalue_sound: ∀ge,en,m,e.
292P_res ? (λr.eval_lvalue ge en m e (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) (exec_lvalue ge en m e).
293#ge en m e; nlapply (refl ? (exec_lvalue ge en m e));
294ncases (exec_lvalue ge en m e) in ⊢ (???% → %);
295##[ #x; ncases x; #y; ncases y; #z; ncases z; #sp loc off tr H; nwhd;
296    napply (addrof_eval_lvalue … Tvoid);
297    nlapply (addrof_exec_lvalue … Tvoid H); #H';
298    nlapply (exec_expr_sound ge en m (Expr (Eaddrof e) Tvoid));
299    nrewrite > H'; #H''; napply H'';
300##| #_; nwhd; napply I;
301##] nqed.
302
303(* Plain equality versions of the above *)
304
305ndefinition exec_expr_sound' ≝ λge,en,m,e,v.
306  λH:exec_expr ge en m e = OK ? v.
307  P_res_to_P ???? (exec_expr_sound ge en m e) H.
308
309ndefinition exec_lvalue_sound' ≝ λge,en,m,e,sp,loc,off,tr.
310  λH:exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉.
311  P_res_to_P ???? (exec_lvalue_sound ge en m e) H.
312
313nlemma exec_exprlist_sound: ∀ge,e,m,l. P_res ? (λvltr:list val×trace. eval_exprlist ge e m l (\fst vltr) (\snd vltr)) (exec_exprlist ge e m l).
314#ge e m l; nelim l;
315 nwhd; //;
316 #e1 es; #IH;
317napply bind2_OK; #v tr1 Hv;
318napply bind2_OK; #vs tr2 Hvs;
319nwhd; napply eval_Econs;
320##[ napply (P_res_to_P … (exec_expr_sound ge e m e1) Hv);
321##| napply (P_res_to_P … IH Hvs);
322##] nqed.
323
324ntheorem exec_step_sound: ∀ge,st.
325  P_io ??? (λr. step ge st (\fst r) (\snd r)) (exec_step ge st).
326#ge st; ncases st;
327##[ #f s k e m; ncases s;
328  ##[ ncases k;
329    ##[ nwhd in ⊢ (?????%);
330        nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %);
331        //; #H; nwhd;
332        napply step_skip_call; //;
333    ##| #s' k'; nwhd; //;
334    ##| #ex s' k'; napply step_skip_or_continue_while; @; //;
335    ##| #ex s' k';
336        napply res_bindIO2_OK; #v tr Hv;
337        nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
338        nlapply (refl ? bexpr);
339        ncases bexpr in ⊢ (???% → %);
340        ##[ #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
341            nwhd in ⊢ (?????%);
342            ##[ napply (step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv));
343              ##[ @; // ##| napply (bool_of … Hb); ##]
344            ##| napply (step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv));
345              ##[ @; // ##| napply (bool_of … Hb); ##]
346            ##]
347        ##| #_; //;
348        ##]
349    ##| #ex s1 s2 k'; napply step_skip_or_continue_for2; @; //;
350    ##| #ex s1 s2 k'; napply step_skip_for3;
351    ##| #k'; napply step_skip_break_switch; @; //;
352    ##| #r f' e' k'; nwhd in ⊢ (?????%);
353        nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %);
354        //; #H; nwhd;
355        napply step_skip_call; //;
356    ##]
357  ##| #ex1 ex2;
358    napply res_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr1 Hlval;
359    napply res_bindIO2_OK; #v2 tr2 Hv2;
360    napply opt_bindIO_OK; #m' em';
361    nwhd; napply (step_assign … (exec_lvalue_sound' … Hlval) (exec_expr_sound' … Hv2) em');
362  ##| #lex fex args;
363    napply res_bindIO2_OK; #vf tr1 Hvf0; nlapply (exec_expr_sound' … Hvf0); #Hvf;
364    napply res_bindIO2_OK; #vargs tr2 Hvargs0; nlapply (P_res_to_P ???? (exec_exprlist_sound …) Hvargs0); #Hvargs;
365    napply opt_bindIO_OK; #fd efd;
366    napply bindIO_OK; #ety;
367    ncases lex; nwhd;
368    ##[ napply (step_call_none … Hvf Hvargs efd ety);
369    ##| #lhs';
370        napply res_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr3 Hlocofs;
371        nwhd; napply (step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety);
372    ##]
373  ##| #s1 s2; nwhd; //;
374  ##| #ex s1 s2;
375    napply res_bindIO2_OK; #v tr Hv;
376    nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
377    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
378    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
379    ##[ napply (step_ifthenelse_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
380    ##| napply (step_ifthenelse_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb)
381    ##]
382  ##| #ex s';
383    napply res_bindIO2_OK; #v tr Hv;
384    nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
385    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
386    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
387    ##[ napply (step_while_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
388    ##| napply (step_while_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
389    ##]
390  ##| #ex s'; nwhd; //;
391  ##| #s1 ex s2 s3; nwhd in ⊢ (?????%); nelim (is_Sskip s1); #Hs1; nwhd in ⊢ (?????%);
392    ##[ nrewrite > Hs1;
393      napply res_bindIO2_OK; #v tr Hv;
394      nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
395      nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
396      #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
397      ##[ napply (step_for_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
398      ##| napply (step_for_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
399      ##]
400    ##| napply step_for_start; //;
401    ##]
402  ##| nwhd in ⊢ (?????%); ncases k; //;
403    ##[ #s' k'; nwhd; //;
404    ##| #ex s' k'; nwhd; //;
405    ##| #ex s' k'; nwhd; //;
406    ##| #ex s1 s2 k'; nwhd; //;
407    ##| #k'; napply step_skip_break_switch; @2; //;
408    ##]
409  ##| nwhd in ⊢ (?????%); ncases k; //;
410    ##[ #s' k'; nwhd; //;
411    ##| #ex s' k'; nwhd; napply step_skip_or_continue_while; @2; //;
412    ##| #ex s' k'; nwhd;
413      napply res_bindIO2_OK; #v tr Hv;
414      nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
415      nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
416      #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
417      ##[ napply (step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv));
418        ##[ @2; // ##| napply (bool_of … Hb); ##]
419      ##| napply (step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv));
420        ##[ @2; // ##| napply (bool_of … Hb); ##]
421      ##]
422    ##| #ex s1 s2 k'; nwhd; napply step_skip_or_continue_for2; @2; //
423    ##| #k'; nwhd; //;
424    ##]
425  ##| #r; nwhd in ⊢ (?????%); ncases r;
426    ##[ nwhd; nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %); //; #H;
427        napply step_return_0; napply H;
428    ##| #ex; ncases (type_eq_dec (fn_return f) Tvoid); //; nwhd in ⊢ (% → ?????%); #Hnotvoid;
429        napply res_bindIO2_OK; #v tr Hv;
430        nwhd; napply (step_return_1 … Hnotvoid (exec_expr_sound' … Hv));
431    ##]
432  ##| #ex ls; napply res_bindIO2_OK; #v; ncases v; //; #n tr Hv;
433    napply step_switch; napply (exec_expr_sound' … Hv);
434  ##| #l s'; nwhd; //;
435  ##| #l; nwhd in ⊢ (?????%); nlapply (refl ? (find_label l (fn_body f) (call_cont k)));
436      ncases (find_label l (fn_body f) (call_cont k)) in ⊢ (???% → %); //;
437      #sk; ncases sk; #s' k' H;
438      napply (step_goto … H);
439  ##| #l s'; nwhd; //;
440  ##]
441##| #f0 vargs k m; nwhd in ⊢ (?????%); ncases f0;
442  ##[ #fn;
443    napply extract_subset_pair_io; #e m1 ealloc Halloc;
444    napply sig_bindIO_OK; #m2 Hbind;
445    nwhd; napply (step_internal_function … Halloc Hbind);
446  ##| #id argtys rty; napply sig_bindIO_OK; #evs Hevs;
447    napply bindIO_OK; #eres; nwhd;
448    napply step_external_function; @; ##[ napply Hevs; ##| napply mk_val_correct; ##]
449  ##] 
450##| #v k' m'; nwhd in ⊢ (?????%); ncases k'; //;
451    #r f e k; nwhd in ⊢ (?????%); ncases r;
452  ##[ nwhd; //;
453  ##| #x; ncases x; #y; ncases y; #z; ncases z; #pcl b ofs ty;
454    napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; nwhd in em':(??%?); //;
455  ##]
456##]
457nqed.
458
459nlemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
460#p; ncases p; #fns main vars;
461nwhd in ⊢ (???%);
462napply bind_OK; #ge Ege;
463napply bind_OK; #m Em;
464napply opt_bind_OK; #x; ncases x; #sp b esb;
465napply opt_bind_OK; #u ecode;
466napply opt_bind_OK; #f ef;
467ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4,5: ndestruct (ecode); ##]
468nwhd; @; //; napply (initial_state_intro … Ege Em esb ef);
469nqed.
470
471ntheorem exec_steps_sound: ∀ge,n,st.
472 P_io ??? (λts:trace×state. star (mk_transrel ?? step) ge st (\fst ts) (\snd ts))
473 (exec_steps n ge st).
474#ge n; nelim n;
475##[ #st; nwhd in ⊢ (?????%); nelim (is_final_state st); #H; nwhd; //;
476##| #n' IH st; nwhd in ⊢ (?????%); nelim (is_final_state st); #H;
477  ##[ nwhd; //;
478  ##| napply (P_bindIO2_OK ????????? (exec_step_sound …)); #t s'; ncases s';
479      ##[ #f s k e m; ##| #fd args k m; ##| #r k m; ##]
480      nwhd in ⊢ (? → ?????(??????%?));
481      ncases m; #mc mn mp; #Hstep;
482      nwhd in ⊢ (?????(??????%?));
483      napply (P_bindIO2_OK ????????? (IH …)); #t' s'' Hsteps;
484      nwhd; napply (star_step ????????? Hsteps); ##[ ##2,5,8: napply Hstep; ##| ##3,6,9: // ##]
485  ##]
486nqed.
Note: See TracBrowser for help on using the repository browser.