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

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

Tcomp_ptr should take the memory region and use that to calculate its size.

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