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

Last change on this file since 502 was 500, checked in by campbell, 10 years ago

Use dependent pointer type to ensure that the representation is always
compatible with the memory region used.
Add a couple of missing checks as a result...

File size: 22.7 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 #pc #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| #r #b #pc #of whd in ⊢ (??%? → ?) #e
90    elim (bind_inversion ????? e) #s * #es #e'
91    elim (bind_inversion ????? e') #u * #eu #e'' -e';
92    elim (bind_inversion ????? e'') #s' * #es' #e'''; -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 = r). elim (eq_region_dec r s) in eu; //; normalize; #_ #e destruct.
102            #e >e in Hty #Hty
103            cases (pointer_compat_dec b s') in e'''
104            #Hcompat #e''' whd in e''':(??%?); destruct (e'''); /2/
105        ]
106    ]
107] qed.
108
109let rec expr_lvalue_ind
110  (P:expr → Prop)
111  (Q:expr_descr → type → Prop)
112  (ci:∀ty,i.P (Expr (Econst_int i) ty))
113  (cf:∀ty,f.P (Expr (Econst_float f) ty))
114  (lv:∀e,ty. Q e ty → Plvalue P e ty)
115  (vr:∀v,ty.Q (Evar v) ty)
116  (dr:∀e,ty.P e → Q (Ederef e) ty)
117  (ao:∀ty,e,ty'.Q e ty' → P (Expr (Eaddrof (Expr e ty')) ty))
118  (uo:∀ty,op,e.P e → P (Expr (Eunop op e) ty))
119  (bo:∀ty,op,e1,e2.P e1 → P e2 → P (Expr (Ebinop op e1 e2) ty))
120  (ca:∀ty,ty',e.P e → P (Expr (Ecast ty' e) ty))
121  (cd:∀ty,e1,e2,e3.P e1 → P e2 → P e3 → P (Expr (Econdition e1 e2 e3) ty))
122  (ab:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eandbool e1 e2) ty))
123  (ob:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eorbool e1 e2) ty))
124  (sz:∀ty,ty'. P (Expr (Esizeof ty') ty))
125  (fl:∀ty,e,ty',i. Q e ty' → Q (Efield (Expr e ty') i) ty)
126  (co:∀ty,l,e. P e → P (Expr (Ecost l e) ty))
127  (xx:∀e,ty. is_not_lvalue e → Q e ty)
128  (e:expr) on e : P e ≝
129match e with
130[ Expr e' ty ⇒
131  match e' with
132  [ Econst_int i ⇒ ci ty i
133  | Econst_float f ⇒ cf ty f
134  | Evar v ⇒ lv (Evar v) ty (vr v ty)
135  | 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''))
136  | 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) ]
137  | 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'')
138  | 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)
139  | 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'')
140  | 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)
141  | 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)
142  | 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)
143  | Esizeof ty' ⇒ sz ty ty'
144  | 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)) ]
145  | 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'')
146  ]
147]
148and lvalue_expr_ind
149  (P:expr → Prop)
150  (Q:expr_descr → type → Prop)
151  (ci:∀ty,i.P (Expr (Econst_int i) ty))
152  (cf:∀ty,f.P (Expr (Econst_float f) ty))
153  (lv:∀e,ty. Q e ty → Plvalue P e ty)
154  (vr:∀v,ty.Q (Evar v) ty)
155  (dr:∀e,ty.P e → Q (Ederef e) ty)
156  (ao:∀ty,e,ty'.Q e ty' → P (Expr (Eaddrof (Expr e ty')) ty))
157  (uo:∀ty,op,e.P e → P (Expr (Eunop op e) ty))
158  (bo:∀ty,op,e1,e2.P e1 → P e2 → P (Expr (Ebinop op e1 e2) ty))
159  (ca:∀ty,ty',e.P e → P (Expr (Ecast ty' e) ty))
160  (cd:∀ty,e1,e2,e3.P e1 → P e2 → P e3 → P (Expr (Econdition e1 e2 e3) ty))
161  (ab:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eandbool e1 e2) ty))
162  (ob:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eorbool e1 e2) ty))
163  (sz:∀ty,ty'. P (Expr (Esizeof ty') ty))
164  (fl:∀ty,e,ty',i. Q e ty' → Q (Efield (Expr e ty') i) ty)
165  (co:∀ty,l,e. P e → P (Expr (Ecost l e) ty))
166  (xx:∀e,ty. is_not_lvalue e → Q e ty)
167  (e:expr_descr) (ty:type) on e : Q e ty ≝
168  match e return λe0. Q e0 ty with
169  [ Evar v ⇒ vr v ty
170  | 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'')
171  | 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'') ]
172  | _ ⇒ xx ? ty ?
173  ]. whd; @I qed.
174
175
176theorem exec_expr_sound: ∀ge:genv. ∀en:env. ∀m:mem. ∀e:expr.
177(P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)).
178#ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e)
179(* XXX // fails [ 1,2: #ty #c whd //  *)
180[ #ty #c whd %
181| #ty #c whd %2
182(* expressions that are lvalues *)
183| #e' #ty cases e'; //; [ #i #He' | #e #He' | #e #i #He' ] whd in He' ⊢ %;
184    @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H
185    @opt_bind_OK #vl #evl whd in evl:(??%?); @(eval_Elvalue … evl)
186    >H in He' #He' @He'
187| #v #ty
188    whd in ⊢ (???%);
189    lapply (refl ? (get ident PTree block v en));
190    cases (get ident PTree block v en) in ⊢ (???% → %);
191    [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind
192        whd; @(eval_Evar_global … eget efind)
193    | #loc #eget @(eval_Evar_local … eget)
194    ]
195| #ty #e #He whd in ⊢ (???%)
196    @bind2_OK #v cases v // #r #l #pc #ofs #tr #Hv whd
197    @eval_Ederef [ 3: >Hv in He #He @He | *: skip ]
198| #ty #e'' #ty'' #He'' @bind2_OK #x cases x #loc #ofs #tr #H
199  cases ty // *#pty
200  cases loc in H ⊢ % * #loc' #H
201  whd try @I
202  @eval_Eaddrof >H in He'' #He'' @He''
203| #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1
204    @opt_bind_OK #v #ev
205    @(eval_Eunop … ev)
206    >Hv1 in He1 #He1 @He1
207| #ty #op #e1 #e2 #He1 #He2
208    @bind2_OK #v1 #tr1 #ev1 >ev1 in He1 #He1
209    @bind2_OK #v2 #tr2 #ev2 >ev2 in He2 #He2
210    @opt_bind_OK #v #ev whd in He1 He2; whd;
211    @(eval_Ebinop … He1 He2 ev)
212| #ty #ty' #e' #He'
213    @bind2_OK #v #tr #Hv >Hv in He' #He'
214    @bind_OK #v' #ev'
215    @(eval_Ecast … He' ?)
216    (* XXX /2/; *)
217    @(exec_cast_sound … ev')
218| #ty #e1 #e2 #e3 #He1 #He2 #He3
219    @bind2_OK #vb #tr1 #Hvb >Hvb in He1 #He1
220    @bind_OK #b
221    cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
222    @bind2_OK #v #tr #Hv
223    [ >Hv in He2 #He2 whd in He2 Hv:(??%?) ⊢%;
224        @(eval_Econdition_true … He1 ? He2) @(bool_of ??? Hb)
225    | >Hv in He3 #He3 whd in He3 Hv:(??%?) ⊢%;
226        @(eval_Econdition_false … He1 ? He3) @(bool_of ??? Hb)
227    ]
228| #ty #e1 #e2 #He1 #He2
229    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1
230    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
231    [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2
232        @bind_OK #b2 #eb2
233        @(eval_Eandbool_2 … He1 … He2)
234        [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ]
235    | @(eval_Eandbool_1 … He1) @(bool_of … Hb1)
236    ]
237| #ty #e1 #e2 #He1 #He2
238    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1
239    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
240    [ @(eval_Eorbool_1 … He1) @(bool_of … Hb1)
241    | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2
242        @bind_OK #b2 #eb2
243        @(eval_Eorbool_2 … He1 … He2)
244        [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ]
245    ]
246| #ty #ty' whd; (* XXX //*) @eval_Esizeof
247| #ty #e' #ty' #i cases ty'; //;
248    [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
249        @bind_OK #delta #Hdelta >H in He' #He'
250        @(eval_Efield_struct …  He' (refl ??) Hdelta)
251    | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
252        >H in He' #He'
253        @(eval_Efield_union … He' (refl ??))
254    ]
255| #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He' #He'
256    @(eval_Ecost … He')
257(* exec_lvalue fails on non-lvalues. *)
258| #e' #ty cases e';
259    [ 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 ]
260    @I
261] qed.
262
263lemma addrof_eval_lvalue: ∀ge,en,m,e,r,loc,pc,off,tr,ty.
264eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr r loc pc off) tr →
265eval_lvalue ge en m e loc off tr.
266#ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H;
267[ 1,2,5: #a #b #H @False_ind destruct (H);
268| #a #b #c #d #e #f #H1 #g #H2 <H2 in H1 #H1 @False_ind
269    @(eval_lvalue_inv_ind … H1)
270    [ #a #b #c #d #bad destruct (bad);
271    | #a #b #c #d #e #bad destruct (bad);
272    | #a #b #c #d #e #f #g #h #bad destruct (bad);
273    | #a #b #c #d #e #f #g #h #i #j #k #l #m #bad @False_ind destruct (bad);
274    | #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
275    ]
276| #e' #ty' #r' #loc' #ofs' #tr' #H' #pc' #e1 #e2 #e3 destruct (e1 e2 e3); @H'
277| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
278| #a #b #c #d #e #f #g #h #i #j #k #l #k #l #bad destruct (bad);
279| #a #b #c #d #e #f #g #h #i #j #k #l #m #bad destruct (bad);
280| #a #b #c #d #e #f #g #h #i #j #k #l #m #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 #bad destruct (bad);
284| #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad  destruct (bad);
285| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
286| #a #b #c #d #e #f #g #bad destruct (bad);
287] qed.
288
289lemma addrof_exec_lvalue: ∀ge,en,m,e,r,loc,off,tr.
290exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 →
291exec_expr ge en m (Expr (Eaddrof e) (Tpointer r Tvoid)) = OK ? 〈Vptr r (mk_block r loc) (same_compat ??) off, tr〉.
292#ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?)
293>H whd in ⊢ (??%?) cases r @refl
294qed.
295
296theorem exec_lvalue_sound: ∀ge,en,m,e.
297P_res ? (λr.eval_lvalue ge en m e (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue ge en m e).
298#ge #en #m #e lapply (refl ? (exec_lvalue ge en m e));
299cases (exec_lvalue ge en m e) in ⊢ (???% → %);
300[ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ % #locr #loci #H
301    @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ /2/ ]
302    lapply (addrof_exec_lvalue … H) #H'
303    lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer locr Tvoid)))
304    >H' #H'' @H''
305| #_ whd @I
306] qed.
307
308(* Plain equality versions of the above *)
309
310definition exec_expr_sound' ≝ λge,en,m,e,v.
311  λH:exec_expr ge en m e = OK ? v.
312  P_res_to_P ???? (exec_expr_sound ge en m e) H.
313
314definition exec_lvalue_sound' ≝ λge,en,m,e,loc,off,tr.
315  λH:exec_lvalue ge en m e = OK ? 〈〈loc,off〉,tr〉.
316  P_res_to_P ???? (exec_lvalue_sound ge en m e) H.
317
318lemma 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).
319#ge #e #m #l elim l;
320 whd; (* XXX //; *)
321[ %
322| #e1 #es #IH
323  @bind2_OK #v #tr1 #Hv
324  @bind2_OK #vs #tr2 #Hvs
325  whd; @eval_Econs
326  [ @(P_res_to_P … (exec_expr_sound ge e m e1) Hv)
327  | @(P_res_to_P … IH Hvs)
328  ]
329] qed.
330
331lemma exec_alloc_variables_sound : ∀l,en,m,en',m'.
332  exec_alloc_variables en m l = 〈en',m'〉 →
333  alloc_variables en m l en' m'.
334#l elim l
335[ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct %
336| * #id #ty #t #IH #en #m #en' #m'
337  lapply (refl ? (alloc m O (sizeof ty) Any)) #ALLOC #EXEC
338  whd in EXEC:(??%?) ALLOC:(???%)
339 @(alloc_variables_cons … ALLOC)
340 @IH @EXEC
341qed.
342
343lemma exec_bind_parameters_sound : ∀ps,vs,en,m.
344  P_res ? (λm'. bind_parameters en m ps vs m') (exec_bind_parameters en m ps vs).
345#ps elim ps
346[ * //
347| * #id #ty #ps' #IH *
348    [ //
349    | #v #vs #en #m
350      @opt_bind_OK #b #GET
351      @opt_bind_OK #m' #STORE
352      lapply (refl ? (exec_bind_parameters en m' ps' vs))
353      cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %) [2: #_ %]
354      #m'' #BIND
355      @(bind_parameters_cons … GET STORE)
356      lapply (IH vs en m') whd in ⊢ (% → ?) >BIND //
357    ]
358] qed.
359
360lemma check_eventval_list_sound : ∀vs,tys.
361  P_res ? (λevs. eventval_list_match evs tys vs) (check_eventval_list vs tys).
362#vs0 elim vs0
363[ * //
364| #v #vs #IH *
365  [ //
366  | #ty #tys whd in ⊢ (???%)
367    cases ty cases v // #v'
368    @bind_OK #evs #CHECK
369    @(evl_match_cons ??????? (P_res_to_P … CHECK)) //
370  ]
371] qed.
372
373theorem exec_step_sound: ∀ge,st.
374  P_io ??? (λr. step ge st (\fst r) (\snd r)) (exec_step ge st).
375#ge #st cases st;
376[ #f #s #k #e #m cases s;
377  [ cases k;
378    [ whd in ⊢ (?????%);
379        lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %);
380        //; #H whd;
381        @step_skip_call //;
382    | #s' #k' whd; (* XXX //; *) @step_skip_seq
383    | #ex #s' #k' @step_skip_or_continue_while % //;
384    | #ex #s' #k'
385        @res_bindIO2_OK #v #tr #Hv
386        letin bexpr ≝ (exec_bool_of_val v (typeof ex));
387        lapply (refl ? bexpr);
388        cases bexpr in ⊢ (???% → %);
389        [ #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
390            whd in ⊢ (?????%);
391            [ @(step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv))
392              [ % // | @(bool_of … Hb) ]
393            | @(step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv))
394              [ % // | @(bool_of … Hb) ]
395            ]
396        | #_ //;
397        ]
398    | #ex #s1 #s2 #k' @step_skip_or_continue_for2 % //;
399    | #ex #s1 #s2 #k' @step_skip_for3
400    | #k' @step_skip_break_switch % //;
401    | #r #f' #e' #k' whd in ⊢ (?????%);
402        lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %);
403        //; #H whd;
404        @step_skip_call //;
405    ]
406  | #ex1 #ex2
407    @res_bindIO2_OK #x cases x; #y cases y; #pcl #loc #ofs #tr1 #Hlval
408    @res_bindIO2_OK #v2 #tr2 #Hv2
409    @opt_bindIO_OK #m' #em'
410    whd; @(step_assign … (exec_lvalue_sound' … Hlval) (exec_expr_sound' … Hv2) em')
411  | #lex #fex #args
412    @res_bindIO2_OK #vf #tr1 #Hvf0 lapply (exec_expr_sound' … Hvf0); #Hvf
413    @res_bindIO2_OK #vargs #tr2 #Hvargs0 lapply (P_res_to_P ???? (exec_exprlist_sound …) Hvargs0); #Hvargs
414    @opt_bindIO_OK #fd #efd
415    @bindIO_OK #ety
416    cases lex; whd;
417    [ @(step_call_none … Hvf Hvargs efd ety)
418    | #lhs'
419        @res_bindIO2_OK #x cases x; #y cases y; #pcl #loc #ofs #tr3 #Hlocofs
420        whd; @(step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety)
421    ]
422  | #s1 #s2 whd; (* XXX //; *) @step_seq
423  | #ex #s1 #s2
424    @res_bindIO2_OK #v #tr #Hv
425    letin bexpr ≝ (exec_bool_of_val v (typeof ex));
426    lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
427    #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
428    [ @(step_ifthenelse_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
429    | @(step_ifthenelse_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
430    ]
431  | #ex #s'
432    @res_bindIO2_OK #v #tr #Hv
433    letin bexpr ≝ (exec_bool_of_val v (typeof ex));
434    lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
435    #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
436    [ @(step_while_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
437    | @(step_while_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
438    ]
439  | #ex #s' whd; (* XXX //; *) @step_dowhile
440  | #s1 #ex #s2 #s3 whd in ⊢ (?????%); elim (is_Sskip s1); #Hs1 whd in ⊢ (?????%);
441    [ >Hs1
442      @res_bindIO2_OK #v #tr #Hv
443      letin bexpr ≝ (exec_bool_of_val v (typeof ex));
444      lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
445      #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
446      [ @(step_for_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
447      | @(step_for_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
448      ]
449    | @step_for_start //;
450    ]
451  | whd in ⊢ (?????%); cases k; //;
452    [ #s' #k' whd (* XXX // *) @step_break_seq
453    | #ex #s' #k' whd (* //; *) @step_break_while
454    | #ex #s' #k' whd (* //; *) @step_break_dowhile
455    | #ex #s1 #s2 #k' whd (* //; *) @step_break_for2
456    | #k' @step_skip_break_switch %2  //
457    ]
458  | whd in ⊢ (?????%); cases k; //;
459    [ #s' #k' whd; (* XXX //;*) @step_continue_seq
460    | #ex #s' #k' whd; @step_skip_or_continue_while %2 ; //;
461    | #ex #s' #k' whd;
462      @res_bindIO2_OK #v #tr #Hv
463      letin bexpr ≝ (exec_bool_of_val v (typeof ex));
464      lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
465      #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
466      [ @(step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv))
467        [ %2 ; // | @(bool_of … Hb) ]
468      | @(step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv))
469        [ %2 ; // | @(bool_of … Hb) ]
470      ]
471    | #ex #s1 #s2 #k' whd; @step_skip_or_continue_for2 %2 ; //
472    | #k' whd; (* XXX //;*) @step_continue_switch
473    ]
474  | #r whd in ⊢ (?????%); cases r;
475    [ whd; lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %); //; #H
476        @step_return_0 @H
477    | #ex cases (type_eq_dec (fn_return f) Tvoid); //; whd in ⊢ (% → ?????%); #Hnotvoid
478        @res_bindIO2_OK #v #tr #Hv
479        whd; @(step_return_1 … Hnotvoid (exec_expr_sound' … Hv))
480    ]
481  | #ex #ls @res_bindIO2_OK #v cases v; //; #n #tr #Hv
482    @step_switch @(exec_expr_sound' … Hv)
483  | #l #s' whd; @step_label (* XXX //; *)
484  | #l whd in ⊢ (?????%); lapply (refl ? (find_label l (fn_body f) (call_cont k)));
485      cases (find_label l (fn_body f) (call_cont k)) in ⊢ (???% → %); //;
486      #sk cases sk; #s' #k' #H
487      @(step_goto … H)
488  | #l #s' whd; (* XXX //; *) @step_cost
489  ]
490| #f0 #vargs #k #m whd in ⊢ (?????%); cases f0;
491  [ #fn whd in ⊢ (?????%)
492    lapply (refl ? (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)))
493    cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %)
494    #en' #m' #ALLOC whd in ⊢ (?????%)
495    @res_bindIO_OK #m2 #BIND
496    whd; @(step_internal_function … (exec_alloc_variables_sound … ALLOC))
497    @(P_res_to_P … (exec_bind_parameters_sound …) BIND)
498  | #id #argtys #rty @res_bindIO_OK #evs #Hevs
499    @bindIO_OK #eres whd;
500    @step_external_function % [ @(P_res_to_P … (check_eventval_list_sound …) Hevs)
501                              | @mk_val_correct ]
502  ] 
503| #v #k' #m' whd in ⊢ (?????%); cases k'; //;
504    #r #f #e #k whd in ⊢ (?????%); cases r;
505  [ whd; @step_returnstate_0
506  | #x cases x; #y cases y; #z cases z; #pcl #b #ofs #ty
507    @opt_bindIO_OK #m' #em' @step_returnstate_1 whd in em':(??%?); //;
508  ]
509]
510qed.
511
512lemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
513#p cases p; #fns #main #vars
514whd in ⊢ (???%);
515@bind_OK #ge #Ege
516@bind_OK #m #Em
517@opt_bind_OK #x cases x; #sp #b #esb
518@opt_bind_OK #f #ef
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.