source: src/Clight/CexecSound.ma @ 1139

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

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

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