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

Last change on this file since 484 was 484, checked in by campbell, 8 years ago

Separate out null values from integer zeros.

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