Changeset 487 for Deliverables/D3.1/Csemantics/CexecSound.ma
 Timestamp:
 Feb 9, 2011, 11:49:17 AM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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