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

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

Port Clight semantics to the new-new matita syntax.

File size: 22.8 KB
Line 
1include "Cexec.ma".
2
3(*include "Plogic/connectives.ma".*)
4
5lemma 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
8cases v; [ | #i | #f | #r1 | #r #b #of ]
9cases 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 whd in H:(??%?); destruct;
11[ lapply (eq_spec i zero); elim (eq i zero);
12  [ #e >e @bool_of_val_false //;
13  | #ne @bool_of_val_true /2/;
14  ]
15| elim (eq_dec f Fzero);
16  [ #e >e >(Feq_zero_true …) @bool_of_val_false //;
17  | #ne >(Feq_zero_false …) //; @bool_of_val_true /2/;
18  ]
19| @bool_of_val_false //
20| @bool_of_val_true //
21] qed.
22
23lemma bool_val_distinct: Vtrue ≠ Vfalse.
24% #H whd in H:(??%%); destruct; @(absurd ? e0 one_not_zero)
25qed.
26
27lemma 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 cases b; #H inversion H; #v' #ty' #H' #ev #et #ev //;
30@False_ind @(absurd ? ev ?)
31[ 2: @sym_neq ] @bool_val_distinct
32qed.
33
34lemma 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'
36whd in ⊢ (??%? → ?);
37lapply (eq_spec i zero); cases (eq i zero);
38[ #e >e
39    cases ty; [ | #sz #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
40    whd in ⊢ (??%? → ?); #H destruct;
41    cases ty' in H ⊢ %; [ | #sz #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
42    whd in ⊢ (??%? → ?); #H destruct (H); @cast_ip_z //;
43| #_ whd in ⊢ (??%? → ?); #H destruct
44]
45qed.
46
47definition 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'
49cases v;
50[ #H whd in H:(??%?); destruct;
51| #i cases ty;
52  [ #H whd in H:(??%?); destruct;
53  | 3: #a #H whd in H:(??%?); destruct;
54  | 7,8,9: #a #b #H whd in H:(??%?); destruct;
55  | #sz1 #si1 cases ty';
56    [ #H whd in H:(??%?); destruct;
57    | 3: #a #H whd in H:(??%?); destruct; //
58    | 2,7,8,9: #a #b #H whd in H:(??%?); destruct; //
59    | 4,5,6: [ #sp #ty'' letin t ≝ (Tpointer sp ty'')
60                 | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n)
61                 | #args #rty letin t ≝ (Tfunction args rty) ]
62        whd in ⊢ (??%? → ?);
63        lapply (try_cast_null_sound m i (Tint sz1 si1) t v');
64        cases (try_cast_null m i (Tint sz1 si1) t);
65        [ 1,3,5: #v'' #H' #e @H' @e
66        | *: #_ whd in ⊢ (??%? → ?); #H destruct (H);
67        ]
68    ]
69  | *: [ #sp #ty'' letin t ≝ (Tpointer sp ty'')
70           | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n)
71           | #args #rty letin t ≝ (Tfunction args rty) ]
72        whd in ⊢ (??%? → ?);
73        lapply (try_cast_null_sound m i t ty' v');
74        cases (try_cast_null m i t ty');
75        [ 1,3,5: #v'' #H' #e @H' @e
76        | *: #_ whd in ⊢ (??%? → ?); #H destruct (H);
77        ]
78  ]
79| #f cases ty;  [ 3: #x | 2,4,6,7,8,9: #x #y | 5: #x #y #z ]
80                    [ cases ty'; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ]
81                        whd in e:(??%?); destruct; //;
82                    | *: #e whd in e:(??%?); destruct
83                    ]
84| #r cases ty; [ 3: #x | 2,4,6,7,8,9: #x #y | 5: #x #y #z ]
85    whd in ⊢ (??%? → ?); #H destruct; cases (eq_region_dec r ?) in H;
86    whd in ⊢ (? → ??%? → ?); #H1 #H2 destruct;
87    cases ty' in H2; normalize; try #a try #b try #c try #d destruct;
88    @cast_pp_z //;
89| #sp #b #of whd in ⊢ (??%? → ?); #e
90    elim (bind_inversion ????? e); #s *; #es #e'
91    elim (bind_inversion ????? e'); #u *; #eu #e''
92    elim (bind_inversion ????? e''); #s' *; #es' #e'''
93    cut (type_region ty s);
94    [ cases ty in es:(??%?) ⊢ %; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ]
95        whd in e:(??%?); destruct; //;
96    | #Hty
97        cut (type_region ty' s');
98        [ cases ty' in es' ⊢ %; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ]
99            whd in e:(??%?); destruct; //;
100        | #Hty'
101            cut (s = sp). elim (eq_region_dec sp s) in eu; //; normalize; #_ #e destruct.
102            #e <e
103            whd in match (is_pointer_compat ??) in e''';
104            cases (pointer_compat_dec (block_space m b) s') in e'''; #Hcompat #e'''
105            whd in e''':(??%?); destruct (e'''); /2/
106        ]
107    ]
108] qed.
109
110let 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  ]. whd; @I qed.
175
176
177theorem 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 @(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(* XXX // fails [ 1,2: #ty #c whd //  *)
181[ #ty #c whd %
182| #ty #c whd %2
183(* expressions that are lvalues *)
184| #e' #ty cases e'; //; [ #i #He' | #e #He' | #e #i #He' ] whd in He' ⊢ %;
185    @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H
186    @opt_bind_OK #vl #evl whd in evl:(??%?); @(eval_Elvalue … evl)
187    >H in He' #He' @He'
188| #v #ty
189    whd in ⊢ (???%);
190    lapply (refl ? (get ident PTree block v en));
191    cases (get ident PTree block v en) in ⊢ (???% → %);
192    [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind
193        whd; @(eval_Evar_global … eget efind)
194    | #loc #eget @(eval_Evar_local … eget)
195    ]
196| #ty #e #He whd in ⊢ (???%);
197    @bind2_OK #v cases v; //; #sp #l #ofs #tr #Hv whd;
198    @eval_Ederef >Hv in He #He @He
199| #ty #e'' #ty'' #He'' @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H
200    whd; @eval_Eaddrof >H in He'' #He'' @He''
201| #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1
202    @opt_bind_OK #v #ev
203    @(eval_Eunop … ev)
204    >Hv1 in He1 #He1 @He1
205| #ty #op #e1 #e2 #He1 #He2
206    @bind2_OK #v1 #tr1 #ev1 >ev1 in He1 #He1
207    @bind2_OK #v2 #tr2 #ev2 >ev2 in He2 #He2
208    @opt_bind_OK #v #ev whd in He1 He2; whd;
209    @(eval_Ebinop … He1 He2 ev)
210| #ty #ty' #e' #He'
211    @bind2_OK #v #tr #Hv >Hv in He' #He'
212    @bind_OK #v' #ev'
213    @(eval_Ecast … He' ?)
214    (* XXX /2/; *)
215    @(exec_cast_sound … ev')
216| #ty #e1 #e2 #e3 #He1 #He2 #He3
217    @bind2_OK #vb #tr1 #Hvb >Hvb in He1 #He1
218    @bind_OK #b
219    cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
220    @bind2_OK #v #tr #Hv
221    [ >Hv in He2 #He2 whd in He2 Hv:(??%?) ⊢%;
222        @(eval_Econdition_true … He1 ? He2) @(bool_of ??? Hb)
223    | >Hv in He3 #He3 whd in He3 Hv:(??%?) ⊢%;
224        @(eval_Econdition_false … He1 ? He3) @(bool_of ??? Hb)
225    ]
226| #ty #e1 #e2 #He1 #He2
227    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1
228    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
229    [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2
230        @bind_OK #b2 #eb2
231        @(eval_Eandbool_2 … He1 … He2)
232        [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ]
233    | @(eval_Eandbool_1 … He1) @(bool_of … Hb1)
234    ]
235| #ty #e1 #e2 #He1 #He2
236    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1
237    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
238    [ @(eval_Eorbool_1 … He1) @(bool_of … Hb1)
239    | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2
240        @bind_OK #b2 #eb2
241        @(eval_Eorbool_2 … He1 … He2)
242        [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ]
243    ]
244| #ty #ty' whd; (* XXX //*) @eval_Esizeof
245| #ty #e' #ty' #i cases ty'; //;
246    [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
247        @bind_OK #delta #Hdelta >H in He' #He'
248        @(eval_Efield_struct …  He' (refl ??) Hdelta)
249    | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
250        >H in He' #He'
251        @(eval_Efield_union … He' (refl ??))
252    ]
253| #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He' #He'
254    @(eval_Ecost … He')
255(* exec_lvalue fails on non-lvalues. *)
256| #e' #ty cases e';
257    [ 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 ]
258    @I
259] qed.
260
261lemma addrof_eval_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
262eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr sp loc off) tr →
263eval_lvalue ge en m e sp loc off tr.
264#ge #en #m #e #sp #loc #off #tr #ty #H inversion H;
265[ 1,2,5: #a #b #H @False_ind destruct (H);
266| #a #b #c #d #e #f #g #H1 #i #H2 <H2 in H1 #H1 @False_ind
267    @(eval_lvalue_inv_ind … H1)
268    [ #a #b #c #d #bad destruct (bad);
269    | #a #b #c #d #e #f #bad destruct (bad);
270    | #a #b #c #d #e #f #g #bad destruct (bad);
271    | #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad @False_ind destruct (bad);
272    | #a #b #c #d #e #f #g #h #i #j #k #l #bad destruct (bad);
273    ]
274| #e' #ty' #sp' #loc' #ofs' #tr' #H #e1 #e2 #e3 destruct (e1 e2 e3); @H
275| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
276| #a #b #c #d #e #f #g #h #i #j #k #l #k #l #bad destruct (bad);
277| #a #b #c #d #e #f #g #h #i #j #k #l #m #bad destruct (bad);
278| #a #b #c #d #e #f #g #h #i #j #k #l #m #bad destruct (bad);
279| #a #b #c #d #e #f #g #h #bad destruct (bad);
280| #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad destruct (bad);
281| #a #b #c #d #e #f #g #h #bad destruct (bad);
282| #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad  destruct (bad);
283| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
284| #a #b #c #d #e #f #g #bad destruct (bad);
285] qed.
286
287lemma addrof_exec_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
288exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉 →
289exec_expr ge en m (Expr (Eaddrof e) ty) = OK ? 〈Vptr sp loc off, tr〉.
290#ge #en #m #e #sp #loc #off #tr #ty #H whd in ⊢ (??%?);
291>H //;
292qed.
293
294theorem exec_lvalue_sound: ∀ge,en,m,e.
295P_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).
296#ge #en #m #e lapply (refl ? (exec_lvalue ge en m e));
297cases (exec_lvalue ge en m e) in ⊢ (???% → %);
298[ #x cases x; #y cases y; #z cases z; #sp #loc #off #tr #H whd;
299    @(addrof_eval_lvalue … Tvoid)
300    lapply (addrof_exec_lvalue … Tvoid H); #H'
301    lapply (exec_expr_sound ge en m (Expr (Eaddrof e) Tvoid));
302    >H' #H'' @H''
303| #_ whd; @I
304] qed.
305
306(* Plain equality versions of the above *)
307
308definition exec_expr_sound' ≝ λge,en,m,e,v.
309  λH:exec_expr ge en m e = OK ? v.
310  P_res_to_P ???? (exec_expr_sound ge en m e) H.
311
312definition exec_lvalue_sound' ≝ λge,en,m,e,sp,loc,off,tr.
313  λH:exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉.
314  P_res_to_P ???? (exec_lvalue_sound ge en m e) H.
315
316lemma 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).
317#ge #e #m #l elim l;
318 whd; (* XXX //; *)
319[ %
320| #e1 #es #IH
321  @bind2_OK #v #tr1 #Hv
322  @bind2_OK #vs #tr2 #Hvs
323  whd; @eval_Econs
324  [ @(P_res_to_P … (exec_expr_sound ge e m e1) Hv)
325  | @(P_res_to_P … IH Hvs)
326  ]
327] qed.
328
329lemma exec_alloc_variables_sound : ∀l,en,m,en',m'.
330  exec_alloc_variables en m l = 〈en',m'〉 →
331  alloc_variables en m l en' m'.
332#l elim l
333[ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct %
334| * #id #ty #t #IH #en #m #en' #m'
335  lapply (refl ? (alloc m O (sizeof ty) Any)) #ALLOC #EXEC
336  whd in EXEC:(??%?) ALLOC:(???%)
337 @(alloc_variables_cons … ALLOC)
338 @IH @EXEC
339qed.
340
341lemma exec_bind_parameters_sound : ∀ps,vs,en,m.
342  P_res ? (λm'. bind_parameters en m ps vs m') (exec_bind_parameters en m ps vs).
343#ps elim ps
344[ * //
345| * #id #ty #ps' #IH *
346    [ //
347    | #v #vs #en #m
348      @opt_bind_OK #b #GET
349      @opt_bind_OK #m' #STORE
350      lapply (refl ? (exec_bind_parameters en m' ps' vs))
351      cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %) [2: #_ %]
352      #m'' #BIND
353      @(bind_parameters_cons … GET STORE)
354      lapply (IH vs en m') whd in ⊢ (% → ?) >BIND //
355    ]
356] qed.
357
358lemma check_eventval_list_sound : ∀vs,tys.
359  P_res ? (λevs. eventval_list_match evs tys vs) (check_eventval_list vs tys).
360#vs0 elim vs0
361[ * //
362| #v #vs #IH *
363  [ //
364  | #ty #tys whd in ⊢ (???%)
365    cases ty cases v // #v'
366    @bind_OK #evs #CHECK
367    @(evl_match_cons ??????? (P_res_to_P … CHECK)) //
368  ]
369] qed.
370
371theorem exec_step_sound: ∀ge,st.
372  P_io ??? (λr. step ge st (\fst r) (\snd r)) (exec_step ge st).
373#ge #st cases st;
374[ #f #s #k #e #m cases s;
375  [ cases k;
376    [ whd in ⊢ (?????%);
377        lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %);
378        //; #H whd;
379        @step_skip_call //;
380    | #s' #k' whd; (* XXX //; *) @step_skip_seq
381    | #ex #s' #k' @step_skip_or_continue_while % //;
382    | #ex #s' #k'
383        @res_bindIO2_OK #v #tr #Hv
384        letin bexpr ≝ (exec_bool_of_val v (typeof ex));
385        lapply (refl ? bexpr);
386        cases bexpr in ⊢ (???% → %);
387        [ #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
388            whd in ⊢ (?????%);
389            [ @(step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv))
390              [ % // | @(bool_of … Hb) ]
391            | @(step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv))
392              [ % // | @(bool_of … Hb) ]
393            ]
394        | #_ //;
395        ]
396    | #ex #s1 #s2 #k' @step_skip_or_continue_for2 % //;
397    | #ex #s1 #s2 #k' @step_skip_for3
398    | #k' @step_skip_break_switch % //;
399    | #r #f' #e' #k' whd in ⊢ (?????%);
400        lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %);
401        //; #H whd;
402        @step_skip_call //;
403    ]
404  | #ex1 #ex2
405    @res_bindIO2_OK #x cases x; #y cases y; #pcl #loc #ofs #tr1 #Hlval
406    @res_bindIO2_OK #v2 #tr2 #Hv2
407    @opt_bindIO_OK #m' #em'
408    whd; @(step_assign … (exec_lvalue_sound' … Hlval) (exec_expr_sound' … Hv2) em')
409  | #lex #fex #args
410    @res_bindIO2_OK #vf #tr1 #Hvf0 lapply (exec_expr_sound' … Hvf0); #Hvf
411    @res_bindIO2_OK #vargs #tr2 #Hvargs0 lapply (P_res_to_P ???? (exec_exprlist_sound …) Hvargs0); #Hvargs
412    @opt_bindIO_OK #fd #efd
413    @bindIO_OK #ety
414    cases lex; whd;
415    [ @(step_call_none … Hvf Hvargs efd ety)
416    | #lhs'
417        @res_bindIO2_OK #x cases x; #y cases y; #pcl #loc #ofs #tr3 #Hlocofs
418        whd; @(step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety)
419    ]
420  | #s1 #s2 whd; (* XXX //; *) @step_seq
421  | #ex #s1 #s2
422    @res_bindIO2_OK #v #tr #Hv
423    letin bexpr ≝ (exec_bool_of_val v (typeof ex));
424    lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
425    #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
426    [ @(step_ifthenelse_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
427    | @(step_ifthenelse_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
428    ]
429  | #ex #s'
430    @res_bindIO2_OK #v #tr #Hv
431    letin bexpr ≝ (exec_bool_of_val v (typeof ex));
432    lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
433    #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
434    [ @(step_while_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
435    | @(step_while_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
436    ]
437  | #ex #s' whd; (* XXX //; *) @step_dowhile
438  | #s1 #ex #s2 #s3 whd in ⊢ (?????%); elim (is_Sskip s1); #Hs1 whd in ⊢ (?????%);
439    [ >Hs1
440      @res_bindIO2_OK #v #tr #Hv
441      letin bexpr ≝ (exec_bool_of_val v (typeof ex));
442      lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
443      #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
444      [ @(step_for_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
445      | @(step_for_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
446      ]
447    | @step_for_start //;
448    ]
449  | whd in ⊢ (?????%); cases k; //;
450    [ #s' #k' whd (* XXX // *) @step_break_seq
451    | #ex #s' #k' whd (* //; *) @step_break_while
452    | #ex #s' #k' whd (* //; *) @step_break_dowhile
453    | #ex #s1 #s2 #k' whd (* //; *) @step_break_for2
454    | #k' @step_skip_break_switch %2  //
455    ]
456  | whd in ⊢ (?????%); cases k; //;
457    [ #s' #k' whd; (* XXX //;*) @step_continue_seq
458    | #ex #s' #k' whd; @step_skip_or_continue_while %2 ; //;
459    | #ex #s' #k' whd;
460      @res_bindIO2_OK #v #tr #Hv
461      letin bexpr ≝ (exec_bool_of_val v (typeof ex));
462      lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
463      #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
464      [ @(step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv))
465        [ %2 ; // | @(bool_of … Hb) ]
466      | @(step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv))
467        [ %2 ; // | @(bool_of … Hb) ]
468      ]
469    | #ex #s1 #s2 #k' whd; @step_skip_or_continue_for2 %2 ; //
470    | #k' whd; (* XXX //;*) @step_continue_switch
471    ]
472  | #r whd in ⊢ (?????%); cases r;
473    [ whd; lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %); //; #H
474        @step_return_0 @H
475    | #ex cases (type_eq_dec (fn_return f) Tvoid); //; whd in ⊢ (% → ?????%); #Hnotvoid
476        @res_bindIO2_OK #v #tr #Hv
477        whd; @(step_return_1 … Hnotvoid (exec_expr_sound' … Hv))
478    ]
479  | #ex #ls @res_bindIO2_OK #v cases v; //; #n #tr #Hv
480    @step_switch @(exec_expr_sound' … Hv)
481  | #l #s' whd; @step_label (* XXX //; *)
482  | #l whd in ⊢ (?????%); lapply (refl ? (find_label l (fn_body f) (call_cont k)));
483      cases (find_label l (fn_body f) (call_cont k)) in ⊢ (???% → %); //;
484      #sk cases sk; #s' #k' #H
485      @(step_goto … H)
486  | #l #s' whd; (* XXX //; *) @step_cost
487  ]
488| #f0 #vargs #k #m whd in ⊢ (?????%); cases f0;
489  [ #fn whd in ⊢ (?????%)
490    lapply (refl ? (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)))
491    cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %)
492    #en' #m' #ALLOC whd in ⊢ (?????%)
493    @res_bindIO_OK #m2 #BIND
494    whd; @(step_internal_function … (exec_alloc_variables_sound … ALLOC))
495    @(P_res_to_P … (exec_bind_parameters_sound …) BIND)
496  | #id #argtys #rty @res_bindIO_OK #evs #Hevs
497    @bindIO_OK #eres whd;
498    @step_external_function % [ @(P_res_to_P … (check_eventval_list_sound …) Hevs)
499                              | @mk_val_correct ]
500  ] 
501| #v #k' #m' whd in ⊢ (?????%); cases k'; //;
502    #r #f #e #k whd in ⊢ (?????%); cases r;
503  [ whd; @step_returnstate_0
504  | #x cases x; #y cases y; #z cases z; #pcl #b #ofs #ty
505    @opt_bindIO_OK #m' #em' @step_returnstate_1 whd in em':(??%?); //;
506  ]
507]
508qed.
509
510lemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
511#p cases p; #fns #main #vars
512whd in ⊢ (???%);
513@bind_OK #ge #Ege
514@bind_OK #m #Em
515@opt_bind_OK #x cases x; #sp #b #esb
516@opt_bind_OK #u #ecode
517@opt_bind_OK #f #ef
518cases sp in esb ecode; #esb #ecode whd in ecode:(??%%); [ 1,2,3,4,5: destruct (ecode); ]
519whd; % [ whd in ⊢ (???(??%)) // | @(initial_state_intro … Ege Em esb ef) ]
520qed.
521
522theorem exec_steps_sound: ∀ge,n,st.
523 P_io ??? (λts:trace×state. star (mk_transrel ?? step) ge st (\fst ts) (\snd ts))
524 (exec_steps n ge st).
525#ge #n elim n;
526[ #st whd in ⊢ (?????%); elim (is_final_state st); #H whd; %
527| #n' #IH #st whd in ⊢ (?????%); elim (is_final_state st); #H
528  [ whd; %
529  | @(P_bindIO2_OK ????????? (exec_step_sound …)) #t #s' cases s';
530      [ #f #s #k #e #m | #fd #args #k #m | #r #k #m ]
531      whd in ⊢ (? → ?????(??????%?));
532      cases m; #mc #mn #mp #Hstep
533      whd in ⊢ (?????(??????%?));
534      @(P_bindIO2_OK ????????? (IH …)) #t' #s'' #Hsteps
535      whd; @(star_step ????????? Hsteps) [ 2,5,8: @Hstep | 3,6,9: // ]
536  ]
537qed.
Note: See TracBrowser for help on using the repository browser.