source: src/Clight/CexecSound.ma @ 1350

Last change on this file since 1350 was 1350, checked in by sacerdot, 10 years ago

Porting to latest destruct tactic.

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