source: src/Clight/CexecSound.ma @ 2106

Last change on this file since 2106 was 2106, checked in by campbell, 6 years ago

Fix up a couple of proofs broken by recent changes.

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